Library UniMath.CategoryTheory.Subobjects
*************************************************************************
Definition and theory about subobjects of an object c
Contents:
Written by: Tomi Pannila and Anders Mörtberg, 2016-2017
- Category of subobjects (monos) of c (Subobjectscategory)
- Set of subobjects as equivalence classes of monos (SubObj)
- Proof that the set of subobjects of an object is a poset (SubObjPoset)
Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.MoreFoundations.Tactics.
Require Import UniMath.CategoryTheory.Core.Categories.
Require Import UniMath.CategoryTheory.Core.Isos.
Require Import UniMath.CategoryTheory.Core.Functors.
Require Import UniMath.CategoryTheory.slicecat.
Require Import UniMath.CategoryTheory.Monics.
Require Import UniMath.CategoryTheory.Subcategory.Core.
Require Import UniMath.CategoryTheory.categories.HSET.Core.
Require Import UniMath.CategoryTheory.limits.pullbacks.
Local Open Scope cat.
Section def_subobjects.
Context {C : precategory} (hsC : has_homsets C).
Definition Subobjectscategory (c : C) : precategory :=
slice_precat (subprecategory_of_monics C hsC)
(subprecategory_of_monics_ob C hsC c)
(has_homsets_subprecategory_of_monics C hsC).
Lemma has_homsets_Subobjectscategory (c : C) :
has_homsets (Subobjectscategory c).
Proof.
apply has_homsets_slice_precat.
Qed.
Context {C : precategory} (hsC : has_homsets C).
Definition Subobjectscategory (c : C) : precategory :=
slice_precat (subprecategory_of_monics C hsC)
(subprecategory_of_monics_ob C hsC c)
(has_homsets_subprecategory_of_monics C hsC).
Lemma has_homsets_Subobjectscategory (c : C) :
has_homsets (Subobjectscategory c).
Proof.
apply has_homsets_slice_precat.
Qed.
Construction of a subobject from a monic
Definition Subobjectscategory_ob {c c' : C} (h : C⟦c', c⟧) (isM : isMonic h) :
Subobjectscategory c := (subprecategory_of_monics_ob C hsC c',,(h,,isM)).
Subobjectscategory c := (subprecategory_of_monics_ob C hsC c',,(h,,isM)).
Given any subobject S of c and a morphism h : c' -> c, by taking then pullback of S by h we
obtain a subobject of c'.
Definition PullbackSubobject (PB : Pullbacks C) {c : C} (S : Subobjectscategory c) {c' : C} (h : C⟦c', c⟧) :
Subobjectscategory c'.
Proof.
set (pb := PB _ _ _ h (pr1 (pr2 S))).
use Subobjectscategory_ob.
- exact pb.
- exact (PullbackPr1 pb).
- use MonicPullbackisMonic'.
Defined.
End def_subobjects.
Subobjectscategory c'.
Proof.
set (pb := PB _ _ _ h (pr1 (pr2 S))).
use Subobjectscategory_ob.
- exact pb.
- exact (PullbackPr1 pb).
- use MonicPullbackisMonic'.
Defined.
End def_subobjects.
Equivalence classes of subobjects defined by identifying monos into c
with isomorphic source
Definition SubObj (c : C) : HSET :=
make_hSet (setquot (iso_eqrel (Subobjectscategory hsC c))) (isasetsetquot _).
Definition monorel c : hrel (Subobjectscategory hsC c) :=
λ f g, ∃ h, pr1 (pr2 f) = h · pr1 (pr2 g).
Lemma isrefl_monorel (c : C) : isrefl (monorel c).
Proof.
intros x; apply hinhpr.
∃ (pr1 (pr1 (identity x))).
now rewrite id_left.
Qed.
Lemma istrans_monorel (c : C) : istrans (monorel c).
Proof.
intros x y z h1.
apply hinhuniv; intros h2; generalize h1; clear h1.
apply hinhuniv; intros h1; apply hinhpr.
∃ (pr1 h1 · pr1 h2).
now rewrite <- assoc, <- (pr2 h2), <- (pr2 h1).
Qed.
Lemma ispreorder_monorel c : ispreorder (monorel c).
Proof.
exact (istrans_monorel c,,isrefl_monorel c).
Qed.
Lemma are_isomorphic_monorel {c : C} {x1 y1 x2 y2 : Subobjectscategory hsC c}
(h1 : are_isomorphic _ x1 y1) (h2 : are_isomorphic _ x2 y2) :
monorel c x1 x2 → monorel c y1 y2.
Proof.
apply hinhuniv; intros f.
change (ishinh_UU (iso x1 y1)) in h1.
change (ishinh_UU (iso x2 y2)) in h2.
apply h1; clear h1; intro h1.
apply h2; clear h2; intro h2.
intros P H; apply H; clear P H.
set (h1_inv := inv_from_iso h1).
set (Hh1 := iso_after_iso_inv h1).
∃ (pr1 (pr1 h1_inv) · pr1 f · pr1 (pr1 (pr1 h2))).
set (Htemp := maponpaths pr1 (pr2 (pr1 h2))).
apply pathsinv0; simpl in ×.
rewrite <-!assoc, <- Htemp.
intermediate_path (pr1 (pr1 h1_inv) · pr1 (pr2 x1)).
{ apply maponpaths, pathsinv0, (pr2 f). }
etrans; [ apply maponpaths, (maponpaths pr1 (pr2 (pr1 h1))) |]; simpl.
rewrite assoc.
etrans; [ eapply cancel_postcomposition, (maponpaths pr1 (maponpaths pr1 Hh1)) |].
apply id_left.
Qed.
make_hSet (setquot (iso_eqrel (Subobjectscategory hsC c))) (isasetsetquot _).
Definition monorel c : hrel (Subobjectscategory hsC c) :=
λ f g, ∃ h, pr1 (pr2 f) = h · pr1 (pr2 g).
Lemma isrefl_monorel (c : C) : isrefl (monorel c).
Proof.
intros x; apply hinhpr.
∃ (pr1 (pr1 (identity x))).
now rewrite id_left.
Qed.
Lemma istrans_monorel (c : C) : istrans (monorel c).
Proof.
intros x y z h1.
apply hinhuniv; intros h2; generalize h1; clear h1.
apply hinhuniv; intros h1; apply hinhpr.
∃ (pr1 h1 · pr1 h2).
now rewrite <- assoc, <- (pr2 h2), <- (pr2 h1).
Qed.
Lemma ispreorder_monorel c : ispreorder (monorel c).
Proof.
exact (istrans_monorel c,,isrefl_monorel c).
Qed.
Lemma are_isomorphic_monorel {c : C} {x1 y1 x2 y2 : Subobjectscategory hsC c}
(h1 : are_isomorphic _ x1 y1) (h2 : are_isomorphic _ x2 y2) :
monorel c x1 x2 → monorel c y1 y2.
Proof.
apply hinhuniv; intros f.
change (ishinh_UU (iso x1 y1)) in h1.
change (ishinh_UU (iso x2 y2)) in h2.
apply h1; clear h1; intro h1.
apply h2; clear h2; intro h2.
intros P H; apply H; clear P H.
set (h1_inv := inv_from_iso h1).
set (Hh1 := iso_after_iso_inv h1).
∃ (pr1 (pr1 h1_inv) · pr1 f · pr1 (pr1 (pr1 h2))).
set (Htemp := maponpaths pr1 (pr2 (pr1 h2))).
apply pathsinv0; simpl in ×.
rewrite <-!assoc, <- Htemp.
intermediate_path (pr1 (pr1 h1_inv) · pr1 (pr2 x1)).
{ apply maponpaths, pathsinv0, (pr2 f). }
etrans; [ apply maponpaths, (maponpaths pr1 (pr2 (pr1 h1))) |]; simpl.
rewrite assoc.
etrans; [ eapply cancel_postcomposition, (maponpaths pr1 (maponpaths pr1 Hh1)) |].
apply id_left.
Qed.
Construct a quotient relation on the Subobjects from the relation on monos
Definition SubObj_rel (c : C) : hrel (pr1 (SubObj c)).
Proof.
use quotrel.
- apply monorel.
- intros x1 y1 x2 y2 h1 h2.
apply hPropUnivalence.
+ apply (are_isomorphic_monorel h1 h2).
+ apply (are_isomorphic_monorel (eqrelsymm (iso_eqrel _) _ _ h1)
(eqrelsymm (iso_eqrel _) _ _ h2)).
Defined.
Lemma istrans_SubObj_rel (c : C) : istrans (SubObj_rel c).
Proof.
apply istransquotrel, istrans_monorel.
Qed.
Lemma isrefl_SubObj_rel (c : C) : isrefl (SubObj_rel c).
Proof.
apply isreflquotrel, isrefl_monorel.
Qed.
Lemma ispreorder_SubObj_rel (c : C) : ispreorder (SubObj_rel c).
Proof.
exact (istrans_SubObj_rel c,,isrefl_SubObj_rel c).
Qed.
Lemma isantisymm_SubObj_rel (c : C) : isantisymm (SubObj_rel c).
Proof.
unfold isantisymm; simpl.
assert (int : ∏ x1 x2, isaprop (SubObj_rel c x1 x2 → SubObj_rel c x2 x1 → x1 = x2)).
{ intros x1 x2.
repeat (apply impred; intro).
apply (isasetsetquot _ x1 x2).
}
apply (setquotuniv2prop _ (λ x1 x2, make_hProp _ (int x1 x2))).
intros x y h1 h2.
simpl in ×. apply (iscompsetquotpr (iso_eqrel (Subobjectscategory hsC c))).
generalize h1; clear h1; apply hinhuniv; intros [h1 Hh1].
generalize h2; clear h2; apply hinhuniv; intros [h2 Hh2].
apply hinhpr, (invmap (weq_iso _ (subprecategory_of_monics_ob C hsC c) _ _)).
induction x as [[x []] [fx Hfx]].
induction y as [[y []] [fy Hfy]].
simpl in ×.
assert (mon_h1 : isMonic h1).
{ apply (isMonic_postcomp _ h1 fy); rewrite <- Hh1; apply Hfx. }
assert (mon_h2 : isMonic h2).
{ apply (isMonic_postcomp _ h2 fx); rewrite <- Hh2; apply Hfy. }
use tpair.
- ∃ (h1,,mon_h1).
apply (@is_iso_from_is_z_iso (subprecategory_of_monics C hsC)).
∃ (h2,,mon_h2).
split; apply subtypePath; try (intros xx; apply isapropisMonic, hsC).
+ simpl; apply Hfx.
now rewrite <- assoc, <- Hh2, <- Hh1, id_left.
+ simpl; apply Hfy.
now rewrite <- assoc, <- Hh1, <- Hh2, id_left.
- apply subtypePath; simpl; try apply Hh1.
now intros xx; apply isapropisMonic, hsC.
Qed.
Definition SubObjPoset (c : C) : Poset :=
(SubObj c,,SubObj_rel c,,ispreorder_SubObj_rel c,,isantisymm_SubObj_rel c).
End subobj.
Proof.
use quotrel.
- apply monorel.
- intros x1 y1 x2 y2 h1 h2.
apply hPropUnivalence.
+ apply (are_isomorphic_monorel h1 h2).
+ apply (are_isomorphic_monorel (eqrelsymm (iso_eqrel _) _ _ h1)
(eqrelsymm (iso_eqrel _) _ _ h2)).
Defined.
Lemma istrans_SubObj_rel (c : C) : istrans (SubObj_rel c).
Proof.
apply istransquotrel, istrans_monorel.
Qed.
Lemma isrefl_SubObj_rel (c : C) : isrefl (SubObj_rel c).
Proof.
apply isreflquotrel, isrefl_monorel.
Qed.
Lemma ispreorder_SubObj_rel (c : C) : ispreorder (SubObj_rel c).
Proof.
exact (istrans_SubObj_rel c,,isrefl_SubObj_rel c).
Qed.
Lemma isantisymm_SubObj_rel (c : C) : isantisymm (SubObj_rel c).
Proof.
unfold isantisymm; simpl.
assert (int : ∏ x1 x2, isaprop (SubObj_rel c x1 x2 → SubObj_rel c x2 x1 → x1 = x2)).
{ intros x1 x2.
repeat (apply impred; intro).
apply (isasetsetquot _ x1 x2).
}
apply (setquotuniv2prop _ (λ x1 x2, make_hProp _ (int x1 x2))).
intros x y h1 h2.
simpl in ×. apply (iscompsetquotpr (iso_eqrel (Subobjectscategory hsC c))).
generalize h1; clear h1; apply hinhuniv; intros [h1 Hh1].
generalize h2; clear h2; apply hinhuniv; intros [h2 Hh2].
apply hinhpr, (invmap (weq_iso _ (subprecategory_of_monics_ob C hsC c) _ _)).
induction x as [[x []] [fx Hfx]].
induction y as [[y []] [fy Hfy]].
simpl in ×.
assert (mon_h1 : isMonic h1).
{ apply (isMonic_postcomp _ h1 fy); rewrite <- Hh1; apply Hfx. }
assert (mon_h2 : isMonic h2).
{ apply (isMonic_postcomp _ h2 fx); rewrite <- Hh2; apply Hfy. }
use tpair.
- ∃ (h1,,mon_h1).
apply (@is_iso_from_is_z_iso (subprecategory_of_monics C hsC)).
∃ (h2,,mon_h2).
split; apply subtypePath; try (intros xx; apply isapropisMonic, hsC).
+ simpl; apply Hfx.
now rewrite <- assoc, <- Hh2, <- Hh1, id_left.
+ simpl; apply Hfy.
now rewrite <- assoc, <- Hh1, <- Hh2, id_left.
- apply subtypePath; simpl; try apply Hh1.
now intros xx; apply isapropisMonic, hsC.
Qed.
Definition SubObjPoset (c : C) : Poset :=
(SubObj c,,SubObj_rel c,,ispreorder_SubObj_rel c,,isantisymm_SubObj_rel c).
End subobj.