Library UniMath.CategoryTheory.HomotopicalCategory
HomotopicalCategory
Contents
- Definitions:
- two_of_six
- two_of_three
- homotopical_category
- homotopical_functor
- is_minimal (minimal homotopical category)
- Properties:
- two_of_six_is_prop
- two_of_three_is_prop
- is_homotopical_is_prop
- is_homotopical_functor_is_prop
- is_minimal_is_prop
- Results:
- two_of_six_implies_two_of_three
- cats_minimal_homotopical (any category is a minimal homotopical category)
Require Import UniMath.Foundations.All.
Require Import UniMath.MoreFoundations.All.
Require Import UniMath.CategoryTheory.Monics.
Require Import UniMath.CategoryTheory.Epis.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.Core.Isos.
Open Scope cat.
Definition morph_class (C : category) := ∏ (x y : C), hsubtype (x --> y).
Definition category_with_weq := ∑ C : category, morph_class C.
Definition category_with_weq_pr1 (C : category_with_weq) : category := pr1 C.
Coercion category_with_weq_pr1 : category_with_weq >-> category.
Definition two_of_six {C : category} (W : morph_class C) :=
∏ (x y z t : C)
(f : x --> y)
(g : y --> z)
(h : z --> t)
(gf : W x z (f · g))
(hg : W y t (g · h)),
(W x y f)
× (W y z g)
× (W z t h)
× (W x t (f · g · h)).
Proposition two_of_six_is_prop {C : category} (W : morph_class C) : isaprop (two_of_six W).
Show proof.
unfold two_of_six.
repeat (apply impred ; intro).
apply isofhleveltotal2. apply (W _ _ _).
intro. apply isofhleveltotal2. apply (W _ _ _).
intro. apply isofhleveltotal2. apply (W _ _ _).
intro. apply (W _ _ _).
repeat (apply impred ; intro).
apply isofhleveltotal2. apply (W _ _ _).
intro. apply isofhleveltotal2. apply (W _ _ _).
intro. apply isofhleveltotal2. apply (W _ _ _).
intro. apply (W _ _ _).
Definition is_homotopical (C : category_with_weq) : UU := two_of_six (pr2 C).
Proposition is_homotopical_is_prop (C : category_with_weq) : isaprop (is_homotopical C).
Show proof.
Definition homotopical_category : UU := ∑ (C : category_with_weq), is_homotopical C.
Definition homotopical_category_pr1 (C : homotopical_category) : category_with_weq := pr1 C.
Coercion homotopical_category_pr1 : homotopical_category >-> category_with_weq.
Definition category_with_weq_pr2 (C : category_with_weq) : morph_class (pr1 C) := pr2 C.
Definition is_homotopical_functor {C C' : homotopical_category} (F : functor C C') : UU :=
∏ (x y : C) (f : category_with_weq_pr2 C x y), category_with_weq_pr2 C' _ _ (# F (pr1 f)).
Proposition is_homotopical_functor_is_prop {C C' : homotopical_category} (F : functor C C') : isaprop (is_homotopical_functor F).
Show proof.
Definition homotopical_functor (C C' : homotopical_category) : UU := ∑ f : functor C C', is_homotopical_functor f.
Definition two_of_three {C : category} (W : morph_class C) :=
∏ (x y z : C)
(f : x --> y)
(g : y --> z),
(W _ _ f × W _ _ g -> W _ _ (f · g)) ×
(W _ _ f × W _ _ (f · g) -> W _ _ g) ×
(W _ _ g × W _ _ (f · g) -> W _ _ f).
Proposition two_of_three_is_prop {C : category} (W : morph_class C) : isaprop (two_of_three W).
Show proof.
unfold two_of_three.
repeat (apply impred ; intro).
apply isofhleveltotal2.
- apply impred. intros. apply (W _ _ _).
- intros. apply isofhleveltotal2. apply impred. intros. apply (W _ _ _).
intros. apply impred. intros. apply (W _ _ _).
repeat (apply impred ; intro).
apply isofhleveltotal2.
- apply impred. intros. apply (W _ _ _).
- intros. apply isofhleveltotal2. apply impred. intros. apply (W _ _ _).
intros. apply impred. intros. apply (W _ _ _).
Lemma two_of_six_implies_two_of_three {C : category} {W : morph_class C} (p : two_of_six W) : two_of_three W.
Show proof.
unfold two_of_three.
intros.
split.
- intros.
rewrite <- (id_right f) in X.
rewrite <- (id_left g) in X.
pose (p _ _ _ _ _ _ _ (pr1 X) (pr2 X)).
rewrite id_right in d.
apply (pr222 d).
- split.
intros.
destruct X as [ X1 X2 ].
rewrite <- (id_left f) in X1.
pose (p _ _ _ _ _ _ _ X1 X2).
apply (pr122 d).
intros.
destruct X as [ X1 X2 ].
rewrite <- (id_right g) in X1.
pose (p _ _ _ _ _ _ _ X2 X1).
apply (pr1 d).
intros.
split.
- intros.
rewrite <- (id_right f) in X.
rewrite <- (id_left g) in X.
pose (p _ _ _ _ _ _ _ (pr1 X) (pr2 X)).
rewrite id_right in d.
apply (pr222 d).
- split.
intros.
destruct X as [ X1 X2 ].
rewrite <- (id_left f) in X1.
pose (p _ _ _ _ _ _ _ X1 X2).
apply (pr122 d).
intros.
destruct X as [ X1 X2 ].
rewrite <- (id_right g) in X1.
pose (p _ _ _ _ _ _ _ X2 X1).
apply (pr1 d).
Lemma left_inv_monic_is_right_inv {C : category} {x y : C} (f : x -->y) (f_is_monic : isMonic f) (g : y --> x) (is_left_inv : g · f = identity _) : f · g = identity _.
Show proof.
apply (maponpaths (fun k => f · k)) in is_left_inv.
rewrite assoc in is_left_inv.
rewrite id_right in is_left_inv.
rewrite <- id_left in is_left_inv.
apply f_is_monic in is_left_inv.
apply is_left_inv.
rewrite assoc in is_left_inv.
rewrite id_right in is_left_inv.
rewrite <- id_left in is_left_inv.
apply f_is_monic in is_left_inv.
apply is_left_inv.
Lemma right_inv_epi_is_left_inv {C : category} {x y : C} (f : x --> y) (f_is_epic : isEpi f) (g : y --> x) (is_right_inv : f · g = identity _) : g · f = identity _.
Show proof.
apply (maponpaths (fun k => k · f)) in is_right_inv.
rewrite id_left in is_right_inv.
rewrite <- id_right in is_right_inv.
rewrite <- assoc in is_right_inv.
apply f_is_epic in is_right_inv.
apply is_right_inv.
rewrite id_left in is_right_inv.
rewrite <- id_right in is_right_inv.
rewrite <- assoc in is_right_inv.
apply f_is_epic in is_right_inv.
apply is_right_inv.
Lemma iso_two_of_three_right {C : precategory} {x y z : C} {f : x --> y} {g : y --> z} (gf_is_iso : is_iso (f · g)) (f_is_iso : is_iso f) : is_iso g.
Show proof.
assert (g_right_inv : g · ((inv_from_iso (make_iso _ gf_is_iso)) · f) = identity _).
pose (iso_inv_after_iso (make_iso _ gf_is_iso)).
apply (maponpaths (fun k => (inv_from_iso (make_iso _ f_is_iso)) · k · f)) in p.
simpl in p.
rewrite assoc in p.
rewrite assoc in p.
rewrite iso_after_iso_inv in p.
rewrite id_left in p.
rewrite id_right in p.
rewrite iso_after_iso_inv in p.
rewrite <- assoc in p.
apply p.
assert (g_left_inv : ((inv_from_iso (make_iso _ gf_is_iso)) · f) · g = identity _).
rewrite <- assoc.
apply (iso_after_iso_inv (make_iso _ gf_is_iso)).
eapply (is_iso_qinv _ _).
exists g_right_inv. apply g_left_inv.
pose (iso_inv_after_iso (make_iso _ gf_is_iso)).
apply (maponpaths (fun k => (inv_from_iso (make_iso _ f_is_iso)) · k · f)) in p.
simpl in p.
rewrite assoc in p.
rewrite assoc in p.
rewrite iso_after_iso_inv in p.
rewrite id_left in p.
rewrite id_right in p.
rewrite iso_after_iso_inv in p.
rewrite <- assoc in p.
apply p.
assert (g_left_inv : ((inv_from_iso (make_iso _ gf_is_iso)) · f) · g = identity _).
rewrite <- assoc.
apply (iso_after_iso_inv (make_iso _ gf_is_iso)).
eapply (is_iso_qinv _ _).
exists g_right_inv. apply g_left_inv.
Lemma z_iso_two_of_three_right {C : category} {x y z : C} {f : x --> y} {g : y --> z} (gf_is_iso : is_z_isomorphism (f · g)) (f_is_iso : is_z_isomorphism f) : is_z_isomorphism g.
Show proof.
apply is_z_iso_from_is_iso.
eapply iso_two_of_three_right.
exact (is_iso_from_is_z_iso _ gf_is_iso).
exact (is_iso_from_is_z_iso _ f_is_iso).
eapply iso_two_of_three_right.
exact (is_iso_from_is_z_iso _ gf_is_iso).
exact (is_iso_from_is_z_iso _ f_is_iso).
Lemma iso_two_of_three_left {C : precategory} {x y z : C} {f : x --> y} {g : y --> z} (gf_is_iso : is_iso (f · g)) (g_is_iso : is_iso g) : is_iso f.
Show proof.
assert (f_right_inv : f · (g · (inv_from_iso (make_iso _ gf_is_iso))) = identity _).
rewrite assoc.
apply (iso_inv_after_iso (make_iso _ gf_is_iso)).
assert (f_left_inv : (g · (inv_from_iso (make_iso _ gf_is_iso))) · f = identity _).
pose (iso_after_iso_inv (make_iso _ gf_is_iso)).
apply (maponpaths (fun k => g · k · (inv_from_iso (make_iso _ g_is_iso)))) in p.
simpl in p.
rewrite <- assoc in p.
rewrite <- assoc in p.
rewrite <- assoc in p.
rewrite id_right in p.
pose (iso_inv_after_iso (make_iso _ g_is_iso)).
simpl in p0.
rewrite p0 in p.
clear p0.
rewrite id_right in p.
rewrite assoc in p.
apply p.
eapply (is_iso_qinv _ _).
exists f_right_inv. apply f_left_inv.
rewrite assoc.
apply (iso_inv_after_iso (make_iso _ gf_is_iso)).
assert (f_left_inv : (g · (inv_from_iso (make_iso _ gf_is_iso))) · f = identity _).
pose (iso_after_iso_inv (make_iso _ gf_is_iso)).
apply (maponpaths (fun k => g · k · (inv_from_iso (make_iso _ g_is_iso)))) in p.
simpl in p.
rewrite <- assoc in p.
rewrite <- assoc in p.
rewrite <- assoc in p.
rewrite id_right in p.
pose (iso_inv_after_iso (make_iso _ g_is_iso)).
simpl in p0.
rewrite p0 in p.
clear p0.
rewrite id_right in p.
rewrite assoc in p.
apply p.
eapply (is_iso_qinv _ _).
exists f_right_inv. apply f_left_inv.
Lemma z_iso_two_of_three_left {C : category} {x y z : C} {f : x --> y} {g : y --> z} (gf_is_iso : is_z_isomorphism (f · g)) (g_is_iso : is_z_isomorphism g) : is_z_isomorphism f.
Show proof.
apply is_z_iso_from_is_iso.
eapply iso_two_of_three_left.
exact (is_iso_from_is_z_iso _ gf_is_iso).
exact (is_iso_from_is_z_iso _ g_is_iso).
eapply iso_two_of_three_left.
exact (is_iso_from_is_z_iso _ gf_is_iso).
exact (is_iso_from_is_z_iso _ g_is_iso).
Definition is_minimal (C : homotopical_category) : UU := ∏ (x y : C) (f : pr21 C x y), is_iso (pr1 f).
Proposition is_minimal_is_prop (C : homotopical_category) : isaprop (is_minimal C).
Show proof.
unfold is_minimal.
apply impred ; intro.
apply impred ; intro.
apply impred ; intro.
apply isaprop_is_iso.
apply impred ; intro.
apply impred ; intro.
apply impred ; intro.
apply isaprop_is_iso.
Lemma cats_minimal_homotopical (C : category) : homotopical_category.
Show proof.
unfold homotopical_category.
pose (C_Weq := (C ,, (fun x y f => (is_z_isomorphism f ,, isaprop_is_z_isomorphism f))) : category_with_weq ).
exists C_Weq.
unfold is_homotopical.
unfold two_of_six.
intros.
assert (g_is_iso : is_z_isomorphism g).
{
assert (g_is_monic : isMonic g).
apply (isMonic_postcomp _ g h).
simpl in hg.
apply (is_iso_isMonic _ _ hg).
assert (g_left_inv : ((is_z_isomorphism_mor gf) · f · g) = identity _).
rewrite <- assoc.
apply (z_iso_after_z_iso_inv (f · g ,, gf)).
pose (g_right_inv := left_inv_monic_is_right_inv _ g_is_monic _ g_left_inv).
eapply make_is_z_isomorphism.
split.
apply g_right_inv.
apply g_left_inv.
}
pose (f_is_iso := z_iso_two_of_three_left gf g_is_iso).
split. apply f_is_iso.
split. apply g_is_iso.
split. apply (z_iso_two_of_three_right hg g_is_iso).
rewrite <- assoc.
apply is_z_isomorphism_comp.
apply f_is_iso.
apply hg.
pose (C_Weq := (C ,, (fun x y f => (is_z_isomorphism f ,, isaprop_is_z_isomorphism f))) : category_with_weq ).
exists C_Weq.
unfold is_homotopical.
unfold two_of_six.
intros.
assert (g_is_iso : is_z_isomorphism g).
{
assert (g_is_monic : isMonic g).
apply (isMonic_postcomp _ g h).
simpl in hg.
apply (is_iso_isMonic _ _ hg).
assert (g_left_inv : ((is_z_isomorphism_mor gf) · f · g) = identity _).
rewrite <- assoc.
apply (z_iso_after_z_iso_inv (f · g ,, gf)).
pose (g_right_inv := left_inv_monic_is_right_inv _ g_is_monic _ g_left_inv).
eapply make_is_z_isomorphism.
split.
apply g_right_inv.
apply g_left_inv.
}
pose (f_is_iso := z_iso_two_of_three_left gf g_is_iso).
split. apply f_is_iso.
split. apply g_is_iso.
split. apply (z_iso_two_of_three_right hg g_is_iso).
rewrite <- assoc.
apply is_z_isomorphism_comp.
apply f_is_iso.
apply hg.