[B] Redefine eq_cardinal, invertible, FiniteT

Use `inverse_map` throughout, instead of `bijective`. This makes it
easier to re-use lemmas.

Use `invertible` instead of `bijective` because it is a slightly
stronger property. In particular `FiniteT` behaves a bit better with
`invertible` than with `bijective`.

Move the definition of `eq_cardinal` from Cardinals to
FiniteTypes, because to do it the the other way around, a some lemmas
need to be moved.

Author: Columbus240

theories/Topology/Compactness.v

@@ -685,7 +685,7 @@ Lemma compact_hausdorff_homeo {X Y : TopologicalSpace} (f : X -> Y) :
 Proof.
   intros.
   apply bijective_impl_invertible in H1.
-  destruct H1 as [g Hgf Hfg].
+  destruct H1 as [g [Hgf Hfg]].
   split; auto.
   exists g. repeat split; auto.
   apply continuous_closed.

theories/Topology/Homeomorphisms.v

@@ -18,9 +18,8 @@ Lemma homeomorphism_is_invertible: forall {X Y:TopologicalSpace}
   homeomorphism f -> invertible f.
 Proof.
 intros.
-destruct H as [_ [g]].
-unfold inverse_map in *.
-exists g; tauto.
+destruct H as [_ [g []]].
+exists g; assumption.
 Qed.
 
 Definition open_map {X Y:TopologicalSpace} (f:X -> Y) : Prop :=
@@ -37,16 +36,31 @@ erewrite inverse_map_image_inverse_image;
   eauto.
 Qed.
 
+Lemma inverse_open_map_continuous
+  {X Y : TopologicalSpace} (f : X -> Y) (g : Y -> X) :
+  inverse_map f g ->
+  open_map f <-> continuous g.
+Proof.
+  intros Hfg.
+  split.
+  - (* -> *)
+    intros Hf U HU.
+    erewrite <- inverse_map_image_inverse_image;
+      eauto.
+  - (* <- *)
+    intros Hg U HU.
+    erewrite inverse_map_image_inverse_image;
+      eauto.
+Qed.
+
 Lemma invertible_open_map_is_homeomorphism: forall {X Y:TopologicalSpace}
   (f:X -> Y),
   invertible f -> continuous f -> open_map f -> homeomorphism f.
 Proof.
-intros. split; auto.
-destruct H as [g].
-exists g; split; [|split]; try tauto.
-intros U HU.
-erewrite <- inverse_map_image_inverse_image;
-  eauto. split; auto.
+intros X Y f [g Hfg] Hfcont Hfopen.
+split; auto.
+exists g; split; auto.
+eapply inverse_open_map_continuous; eassumption.
 Qed.
 
 (** every continuous self-inverse map is a homeomorphism *)

theories/Topology/SeparatednessAxioms.v

@@ -60,7 +60,7 @@ Proof.
   rewrite <- (proj1 (injective_inverse_image_Singleton g)).
   2: {
     apply invertible_impl_bijective.
-    exists f; apply Hfg.
+    exists f. apply inverse_map_sym, Hfg.
   }
   apply continuous_closed.
   { apply Hcont_g. }

theories/ZornsLemma/CSB.v

@@ -203,11 +203,21 @@ unfold CSB_bijection2; case (classic_dec (Y_even y)).
   + trivial.
 Qed.
 
+Theorem CSB_inverse_map :
+  exists (h0 : X -> Y) (h1 : Y -> X),
+    inverse_map h0 h1.
+Proof.
+  exists CSB_bijection, CSB_bijection2.
+  split.
+  - exact CSB_comp1.
+  - exact CSB_comp2.
+Qed.
+
 Theorem CSB: exists h:X->Y, bijective h.
 Proof.
 exists CSB_bijection.
 apply invertible_impl_bijective.
-exists CSB_bijection2.
+exists CSB_bijection2. split.
 - exact CSB_comp1.
 - exact CSB_comp2.
 Qed.

theories/ZornsLemma/Cardinals.v

@@ -15,8 +15,6 @@ From ZornsLemma Require Import FiniteTypes.
 From ZornsLemma Require Import InfiniteTypes.
 From Coq Require Import RelationClasses.
 
-Definition eq_cardinal (A B : Type) : Prop :=
-  exists f : A -> B, bijective f.
 Definition le_cardinal (A B : Type) : Prop :=
   exists f : A -> B, injective f.
 
@@ -27,21 +25,6 @@ Definition ge_cardinal (kappa lambda:Type) : Prop :=
 Definition gt_cardinal (kappa lambda:Type) : Prop :=
   lt_cardinal lambda kappa.
 
-Global Instance eq_cardinal_equiv : Equivalence eq_cardinal.
-Proof.
-split.
-- red; intro. exists id. apply id_bijective.
-- red; intros ? ? [f Hf].
-  apply bijective_impl_invertible in Hf.
-  destruct Hf as [g Hfg Hgf].
-  exists g.
-  apply invertible_impl_bijective.
-  exists f; auto.
-- intros ? ? ? [f Hf] [g Hg].
-  exists (compose g f).
-  apply bijective_compose; auto.
-Qed.
-
 Instance le_cardinal_preorder : PreOrder le_cardinal.
 Proof.
 split.
@@ -56,20 +39,20 @@ Instance le_cardinal_PartialOrder :
 Proof.
 split.
 - intros [f Hf]; split.
-  + exists f; apply Hf.
-  + apply bijective_impl_invertible in Hf.
-    destruct Hf as [g Hgf Hfg].
+  + exists f. apply invertible_impl_bijective; assumption.
+  + destruct Hf as [g Hfg].
     exists g. apply invertible_impl_bijective.
-    exists f; auto.
+    exists f. apply inverse_map_sym.
+    assumption.
 - intros [[f Hf] [g Hg]].
-  apply CSB with (f := f) (g := g); auto.
+  apply CSB_inverse_map with (f := f) (g := g); auto.
 Qed.
 
 Lemma eq_cardinal_impl_le_cardinal: forall kappa lambda: Type,
   eq_cardinal kappa lambda -> le_cardinal kappa lambda.
 Proof.
 intros ? ? [f Hf].
-exists f. apply Hf.
+exists f. apply invertible_impl_bijective; auto.
 Qed.
 
 (** This lemma is helpful, if one wants
@@ -171,6 +154,7 @@ split.
   assumption.
 - intros [f Hf].
   apply (cantor_diag2 _ f).
+  apply invertible_impl_bijective.
   apply Hf.
 Qed.
 
@@ -561,18 +545,17 @@ Lemma FiniteT_cardinality {X : Type} :
   FiniteT X <-> lt_cardinal X nat.
 Proof.
 split; intros.
-- constructor.
+- split.
   + destruct (FiniteT_nat_embeds H) as [f].
     exists f. assumption.
-  + intros [f []].
+  + intros H0.
     apply nat_infinite.
-    apply surj_finite with (f := f); auto.
-    intros; apply classic.
+    apply bij_finite with X; assumption.
 - destruct H as [[f Hf] H].
   apply NNPP. intro.
   destruct (infinite_nat_inj _ H0) as [g].
   contradict H.
-  apply CSB with (f := f) (g := g);
+  apply CSB_inverse_map with (f := f) (g := g);
     auto.
 Qed.
 
@@ -591,15 +574,13 @@ split.
     contradiction.
   + (* |B| ≠ |A| *)
     intro.
-    destruct H0 as [f Hf].
-    apply bijective_impl_invertible in Hf.
-    destruct Hf as [g Hgf Hfg].
+    destruct H0 as [f [g [Hgf Hfg]]].
     pose proof (invertible_impl_bijective g).
     destruct H0 as [Hg0 Hg1].
-    { exists f; assumption. }
+    { exists f; split; assumption. }
     apply (H g Hg0).
 - intros [[f Hf]] g Hg.
   contradict H.
-  apply CSB with (f := f) (g := g);
+  apply CSB_inverse_map with (f := f) (g := g);
     assumption.
 Qed.

theories/ZornsLemma/CardinalsEns.v

@@ -791,9 +791,10 @@ Proof.
           exists n. subst. unfold f0.
           apply subset_eq. reflexivity.
       }
-      destruct H as [g Hg0 Hg1].
-      eapply bij_finite with (f := g); eauto.
-      eexists; eauto.
+      destruct H as [g Hg0].
+      eapply bij_finite with _.
+      2: exists g, f0; split; apply Hg0.
+      assumption.
   - (* <- *)
     intros [[[H0 H1]|[f [Hf0 Hf1]]] H2].
     { specialize (H0 0). contradiction. }

theories/ZornsLemma/CountableTypes.v

@@ -39,8 +39,9 @@ apply exclusive_dec.
 - intro.
   destruct H0 as [? [f ?]].
   contradiction nat_infinite.
-  apply bij_finite with _ f; trivial.
-  apply bijective_impl_invertible; trivial.
+  apply bijective_impl_invertible in H1.
+  apply bij_finite with X; auto.
+  exists f; auto.
 - destruct (classic (FiniteT X)).
   + left; trivial.
   + right.
@@ -140,15 +141,16 @@ induction H.
   intros.
   pose proof (equal_f H4).
   apply H5.
-- destruct H1 as [f1], IHFiniteT as [f0].
+- destruct H1 as [f [f1 Hf]].
+  destruct IHFiniteT as [f0 Hf0].
   exists (fun h => f0 (fun x => h (f x))).
   intros h1 h2 ?.
-  apply H3 in H4.
-  pose proof (equal_f H4).
-  simpl in H5.
+  apply Hf0 in H1.
+  pose proof (equal_f H1).
+  simpl in H2.
   extensionality y.
-  rewrite <- (H2 y).
-  apply H5.
+  rewrite <- (proj2 Hf y).
+  apply H2.
 Qed.
 
 Lemma inj_countable {X Y : Type} (f : X -> Y) :
@@ -186,10 +188,11 @@ induction H.
     injection H1 as H1 + discriminate H1 + trivial.
   now destruct (H0 _ _ H1).
 - destruct IHFiniteT as [g],
-           H0 as [finv].
+           H0 as [f [finv]].
   exists (fun y:Y => g (finv y)).
   intros y1 y2 ?.
-  apply H1 in H3.
+  apply H1 in H2.
+  destruct H0.
   congruence.
 Qed.
 

theories/ZornsLemma/Filters.v

@@ -40,10 +40,11 @@ induction H.
   apply filter_intersection.
   + apply IHFiniteT; auto.
   + apply H0.
-- rewrite IndexedIntersection_surj_fn with S f.
+- destruct H1 as [f Hf].
+  rewrite IndexedIntersection_surj_fn with S f.
   2: {
-    apply invertible_impl_bijective in H1.
-    apply H1.
+    apply invertible_impl_bijective.
+    assumption.
   }
   apply IHFiniteT; auto.
 Qed.

theories/ZornsLemma/FiniteIntersections.v

@@ -88,10 +88,10 @@ induction H.
 - rewrite IndexedIntersection_option_Intersection.
   constructor 3; auto.
   constructor 2; trivial.
-- rewrite IndexedIntersection_surj_fn with V f.
+- destruct H1 as [f Hf].
+  rewrite IndexedIntersection_surj_fn with V f.
   2: {
-    apply invertible_impl_bijective in H1.
-    destruct H1. assumption.
+    apply invertible_impl_bijective; auto.
   }
   apply IHFiniteT.
   auto.