Section Categoricity.
Context { M : ZFStruct }.
Context { MZF : ZF M }.
Context { N : ZFStruct }.
Context { NZF : ZF N }.
(* Suppose M and N are equipotent models *)
Variable F : M -> N.
Variable G : N -> M.
Variable FG : forall a, F (G a) = a.
Variable GF : forall x, G (F x) = x.
(* Then Iso must be both total and surjective, hence M N are isomorphic *)
Theorem cat_card :
iso M N.
Proof.
destruct (@Iso_tricho M MZF N NZF) as [H|[[IS[X HX]]|[IT[A HA]]]]; trivial.
- exfalso. pose (Y := sep (fun x => x nel G (i x)) X). pose (y := @j M N (F Y)).
specialize (sep_el (fun x => x nel G (i x)) X y). intros H. fold Y in H.
unfold y in H at 3. rewrite ij, GF in H; try apply IS.
assert (I : y el X) by now apply HX, j_dom. tauto.
- exfalso. pose (B := sep (fun a => a nel F (j a)) A). pose (b := i (G B)).
specialize (sep_el (fun a => a nel F (j a)) A b). intros H. fold B in H.
unfold b in H at 3. rewrite ji, FG in H; try apply IT.
assert (I : b el A) by now apply HA, i_ran. tauto.
Qed.
End Categoricity.
Lemma cat_ZFn (M N : ZFStruct) n :
ZFn n M -> ZFn n N -> iso M N.
Proof.
intros [[MZF M1] M2] [[NZF N1] N2].
destruct (@Iso_tricho M MZF N NZF) as [H|[[IS[X HX]]|[IT[A HA]]]]; trivial.
- exfalso. apply M2. exists (power X); simpl.
assert (XU : universe X) by now apply domain_universe.
exists X. split; try apply power_eager. split; trivial.
apply trans_strength; try now apply universe_trans.
destruct N1 as [a N1]. exists (j a).
split; try now apply HX, j_dom.
apply (Iso_strength N1), Iso_sym, j_Iso, IS; trivial.
- exfalso. apply N2. exists (power A); simpl.
apply range_domain_small in HA. apply tot_sur in IT.
assert (XU : universe A) by now apply (domain_universe (N:=M)).
exists A. split; try apply power_eager. split; trivial.
apply trans_strength; try now apply universe_trans.
destruct M1 as [x M1]. exists (j x).
split; try now apply HA, j_dom.
apply (Iso_strength M1), Iso_sym, j_Iso, IT; trivial.
Qed.
(* Type-level choice *)
Definition choice_type (X : Type) :=
forall (P : X -> Prop), ex P -> sig P.
Lemma choice_el (X : Type) P HP (c : choice_type X) :
P (proj1_sig (c P HP)).
Proof.
apply proj2_sig.
Qed.
Fact choice_ZFn (M N : ZFStruct) n :
ZFn n M -> ZFn n N -> choice_type M -> choice_type N.
Proof.
intros H1 H2 H P' HP'.
destruct (cat_ZFn H1 H2) as [I1 I2].
destruct H1 as [[H1 _] _], H2 as [[H2 _] _].
pose (P x := P' (@i M N x)). assert (HP : exists x, P x).
- destruct HP' as [y HP']. exists (@j M N y).
unfold P. rewrite (@ij M); trivial. apply I2.
- destruct (H P HP) as [x HX].
exists (@i M N x). apply HX.
Qed.
(* Set-level choice *)
Section AC.
Variable M : ZFStruct.
Hypothesis MZF : ZF M.
Definition parti X :=
(forall x, x el X -> (exists z, z el x)) /\
(forall x y z, x el X -> y el X -> z el x -> z el y -> x = y).
Definition trace X Y :=
forall x, x el X -> exists! y, y el Y /\ y el x.
Definition AC :=
forall X, parti X -> exists Y, trace X Y.
Fact choice_AC :
choice_type M -> AC.
Proof.
intros c X [H1 H2].
pose (cx x (HX : x el X) := proj1_sig (c _ (H1 _ HX))).
pose (Y := sep (fun z => exists x (HX : x el X), z = cx x HX) (union X)).
exists Y. intros x HX. exists (cx x HX).
assert (HCX : cx x HX el x) by apply proj2_sig.
repeat split; trivial.
- apply sep_el. split; eauto.
apply Union. now exists x.
- intros y [Y1 Y2]. apply sep_el in Y1 as [Y1 [x'[HX' ->]]].
assert (XX : x = x'). apply (H2 x x' (cx x' HX')); trivial. apply proj2_sig.
subst x'. now rewrite (proof_irrelevance _ HX HX').
Qed.
End AC.
Hint Resolve j_Iso i_Iso Iso_sym.
Hint Unfold total surjective.
Lemma Iso_parti (M N : ZFStruct) (MZF : ZF M) (NZF : ZF N) X X' :
@Iso M N X X' -> parti X' -> parti X.
Proof.
intros H [X1 X2]. split.
- intros x HX. destruct (Iso_btot H HX) as [x'[X3 X4]].
destruct (X1 x' X3) as [y' Y'].
destruct (Iso_bsur X4 Y') as [y[Y1 Y2]].
exists y. now apply (Iso_mem X4 Y2).
- intros x y z H1 H2 H3 H4.
destruct (Iso_btot H H1) as [x'[X3 X4]].
destruct (Iso_btot H H2) as [y'[X5 X6]].
destruct (Iso_btot X4 H3) as [z'[Z1 Z2]].
destruct (Iso_btot X6 H4) as [z''[Z3 Z4]].
destruct (Iso_fun Z2 Z4). destruct (X2 x' y' z' X3 X5 Z1 Z3).
apply (Iso_inj X4 X6).
Qed.
Fact AC_ZFn (M N : ZFStruct) n :
ZFn n M -> ZFn n N -> AC M -> AC N.
Proof.
intros H1 H2 H X' HX'. pose (X := @j M N X').
destruct (cat_ZFn H1 H2) as [I1 I2].
destruct H1 as [[H1 _] _], H2 as [[H2 _] _].
assert (HX : parti X) by now apply (Iso_parti H1 H2 (j_Iso (I2 X'))).
destruct (H X HX) as [Y HY]. exists (@i M N Y).
intros x' XX'. pose (x := @j M N x').
assert (XX : x el X) by now rewrite <- (Iso_mem (j_Iso (I2 X')) (j_Iso (I2 x'))) in XX'.
destruct (HY x XX) as [y [Y1 Y2]]. exists (@i M N y). split.
- rewrite <- (Iso_mem (i_Iso (I1 Y)) (i_Iso (I1 y))).
now rewrite <- (Iso_mem (j_Iso (I2 x')) (i_Iso (I1 y))).
- intros z' HZ. rewrite <- (@ij M _ N _); try apply I2. f_equal. apply Y2.
rewrite <- (Iso_mem (j_Iso (I2 x')) (j_Iso (I2 z'))) in HZ.
now rewrite <- (Iso_mem (i_Iso (I1 Y)) (j_Iso (I2 z'))) in HZ.
Qed.