1 (****************************************************************************)
2 (* Chapter 7.1: Subcategories *)
3 (****************************************************************************)
5 Generalizable All Variables.
6 Require Import Preamble.
7 Require Import Categories_ch1_3.
8 Require Import Functors_ch1_4.
9 Require Import Isomorphisms_ch1_5.
10 Require Import OppositeCategories_ch1_6_2.
11 Require Import NaturalTransformations_ch7_4.
12 Require Import NaturalIsomorphisms_ch7_5.
14 (* Any morphism-predicate which is closed under composition and
15 * passing to identity morphisms (of either the domain or codomain)
17 * We could recycle the "predicate on morphisms" to determine the
18 * "predicate on objects", but this causes technical difficulties with
20 Class SubCategory `(C:Category Ob Hom)(Pobj:Ob->Type)(Pmor:forall a b:Ob, Pobj a -> Pobj b -> (a~>b) ->Type) : Type :=
21 { sc_id_included : forall (a:Ob)(pa:Pobj a), Pmor _ _ pa pa (id a)
22 ; sc_comp_included : forall (a b c:Ob)(pa:Pobj a)(pb:Pobj b)(pc:Pobj c) f g,
23 (Pmor _ _ pa pb f) -> (Pmor _ _ pb pc g) -> (Pmor _ _ pa pc (f>>>g))
26 (* every category is a subcategory of itself! *)
27 Instance IdentitySubCategory `(C:Category Ob Hom) : SubCategory C (fun _ => True) (fun _ _ _ _ _ => True).
28 intros; apply Build_SubCategory.
33 (* a full subcategory requires nothing more than a predicate on objects *)
34 Definition FullSubcategory `(C:Category)(Pobj:C->Type) : SubCategory C Pobj (fun _ _ _ _ _ => True).
35 apply Build_SubCategory; intros; auto.
38 Section SubCategoriesAreCategories.
39 (* Any such predicate determines a category *)
40 Instance SubCategoriesAreCategories `(C:Category Ob Hom)`(SP:@SubCategory _ _ C Pobj Pmor)
41 : Category (sigT Pobj) (fun dom ran => sigT (fun f => Pmor (projT1 dom) (projT1 ran) (projT2 dom) (projT2 ran) f)) :=
42 { id := fun t => existT (fun f => Pmor _ _ _ _ f) (id (projT1 t)) (sc_id_included _ (projT2 t))
43 ; eqv := fun a b f g => eqv _ _ (projT1 f) (projT1 g)
44 ; comp := fun a b c f g => existT (fun f => Pmor _ _ _ _ f) (projT1 f >>> projT1 g)
45 (sc_comp_included _ _ _ (projT2 a) (projT2 b) (projT2 c) _ _ (projT2 f) (projT2 g))
47 intros; apply Build_Equivalence. unfold Reflexive.
49 unfold Symmetric; intros; simpl; symmetry; auto.
50 unfold Transitive; intros; simpl. transitivity (projT1 y); auto.
51 intros; unfold Proper. unfold respectful. intros. simpl. apply comp_respects. auto. auto.
52 intros; simpl. apply left_identity.
53 intros; simpl. apply right_identity.
54 intros; simpl. apply associativity.
56 End SubCategoriesAreCategories.
57 Coercion SubCategoriesAreCategories : SubCategory >-> Category.
59 (* the inclusion operation from a subcategory to its host is a functor *)
60 Instance InclusionFunctor `(C:Category Ob Hom)`(SP:@SubCategory _ _ C Pobj Pmor)
61 : Functor SP C (fun x => projT1 x) :=
62 { fmor := fun dom ran f => projT1 f }.
63 intros. unfold eqv in H. simpl in H. auto.
64 intros. simpl. reflexivity.
65 intros. simpl. reflexivity.
68 Definition FullImage `(F:Functor(c1:=C)(c2:=D)(fobj:=Fobj)) := FullSubcategory D (fun d => { c:C & (Fobj c)=d }).
70 (* any functor may be restricted to its image *)
71 Section RestrictToImage.
72 Context `(F:Functor(c1:=C)(c2:=D)(fobj:=Fobj)).
73 Definition RestrictToImage_fobj : C -> FullImage F.
79 Definition RestrictToImage_fmor a b (f:a~>b) : (RestrictToImage_fobj a)~~{FullImage F}~~>(RestrictToImage_fobj b).
82 Instance RestrictToImage : Functor C (FullImage F) RestrictToImage_fobj :=
83 { fmor := fun a b f => RestrictToImage_fmor a b f }.
84 intros; simpl; apply fmor_respects; auto.
85 intros; simpl; apply fmor_preserves_id; auto.
86 intros; simpl; apply fmor_preserves_comp; auto.
88 Lemma RestrictToImage_splits : F ≃ (RestrictToImage >>>> InclusionFunctor _ _).
89 exists (fun A => iso_id (F A)).
91 setoid_rewrite left_identity.
92 setoid_rewrite right_identity.
97 Instance func_opSubcat `(c1:Category Ob1 Hom1)`(c2:Category Ob Hom)`(SP:@SubCategory _ _ c2 Pobj Pmor)
98 {fobj}(F:Functor c1⁽ºᑭ⁾ SP fobj) : Functor c1 SP⁽ºᑭ⁾ fobj :=
99 { fmor := fun a b f => fmor F f }.
100 intros. apply (@fmor_respects _ _ _ _ _ _ _ F _ _ f f' H).
101 intros. apply (@fmor_preserves_id _ _ _ _ _ _ _ F a).
102 intros. apply (@fmor_preserves_comp _ _ _ _ _ _ _ F _ _ g _ f).
105 (* if a functor's range falls within a subcategory, then it is already a functor into that subcategory *)
106 Section FunctorWithRangeInSubCategory.
107 Context `(Cat1:Category O1 Hom1).
108 Context `(Cat2:Category O2 Hom2).
109 Context (Pobj:Cat2 -> Type).
110 Context (Pmor:forall a b:Cat2, (Pobj a) -> (Pobj b) -> (a~~{Cat2}~~>b) -> Type).
111 Context (SP:SubCategory Cat2 Pobj Pmor).
112 Context (Fobj:Cat1->Cat2).
114 Context (F:Functor Cat1 Cat2 Fobj).
115 Context (pobj:forall a, Pobj (F a)).
116 Context (pmor:forall a b f, Pmor (F a) (F b) (pobj a) (pobj b) (F \ f)).
117 Definition FunctorWithRangeInSubCategory_fobj (X:Cat1) : SP :=
118 existT Pobj (Fobj X) (pobj X).
119 Definition FunctorWithRangeInSubCategory_fmor (dom ran:Cat1)(X:dom~>ran) : (@hom _ _ SP
120 (FunctorWithRangeInSubCategory_fobj dom) (FunctorWithRangeInSubCategory_fobj ran)).
123 apply (pmor dom ran X).
125 Definition FunctorWithRangeInSubCategory : Functor Cat1 SP FunctorWithRangeInSubCategory_fobj.
126 apply Build_Functor with (fmor:=FunctorWithRangeInSubCategory_fmor);
128 unfold FunctorWithRangeInSubCategory_fmor;
130 setoid_rewrite H; auto.
131 apply (fmor_preserves_id F).
132 apply (fmor_preserves_comp F).
136 Context (F:Functor Cat1 Cat2⁽ºᑭ⁾ Fobj).
137 Context (pobj:forall a, Pobj (F a)).
138 Context (pmor:forall a b f, Pmor (F b) (F a) (pobj b) (pobj a) (F \ f)).
139 Definition FunctorWithRangeInSubCategoryOp_fobj (X:Cat1) : SP :=
140 existT Pobj (Fobj X) (pobj X).
141 Definition FunctorWithRangeInSubCategoryOp_fmor (dom ran:Cat1)(X:dom~>ran) :
142 (FunctorWithRangeInSubCategoryOp_fobj dom)~~{SP⁽ºᑭ⁾}~~>(FunctorWithRangeInSubCategoryOp_fobj ran).
145 apply (pmor dom ran X).
148 Definition FunctorWithRangeInSubCategoryOp : Functor Cat1 SP⁽ºᑭ⁾ FunctorWithRangeInSubCategoryOp_fobj.
149 apply Build_Functor with (fmor:=FunctorWithRangeInSubCategoryOp_fmor);
151 unfold FunctorWithRangeInSubCategoryOp_fmor;
153 apply (fmor_respects(Functor:=F)); auto.
154 apply (fmor_preserves_id(Functor:=F)).
156 set (@fmor_preserves_comp _ _ _ _ _ _ _ F _ _ f _ g) as qq.
157 setoid_rewrite <- qq.
162 End FunctorWithRangeInSubCategory.
165 (* Definition 7.1: faithful functors *)
166 Definition FaithfulFunctor `(F:Functor(c1:=C1)(c2:=C2)(fobj:=Fobj)) :=
167 forall (a b:C1), forall (f f':a~>b), (fmor _ f)~~(fmor _ f') -> f~~f'.
169 (* Definition 7.1: full functors *)
170 Class FullFunctor `(F:Functor(c1:=C1)(c2:=C2)(fobj:=Fobj)) :=
171 { ff_invert : forall {a b}(f:(Fobj a)~~{C2}~~>(Fobj b)) , { f' : a~~{C1}~~>b & (F \ f') ~~ f }
172 ; ff_respects : forall {a b}, Proper (eqv (Fobj a) (Fobj b) ==> eqv a b) (fun x => projT1 (@ff_invert a b x))
174 Coercion ff_invert : FullFunctor >-> Funclass.
176 (* Definition 7.1: (essentially) surjective on objects *)
177 Definition EssentiallySurjectiveOnObjects `(F:Functor(c1:=C1)(c2:=C2)(fobj:=Fobj)) :=
178 forall o2:C2, { o1:C1 & (F o1) ≅ o2 }.
180 (* Definition 7.1: (essentially) injective on objects *)
181 Class ConservativeFunctor `(F:Functor(c1:=C1)(c2:=C2)(fobj:=Fobj)) :=
182 { cf_reflect_iso : forall (a b:C1), (F a) ≅ (F b) -> a ≅ b }.
184 (* "monic up to natural iso" *)
185 Definition WeaklyMonic
189 (F:@Functor _ _ C _ _ D Fobj) := forall
191 `{G :@Functor _ _ E _ _ C Gobj'}
192 `{H :@Functor _ _ E _ _ C Hobj'},
196 Section FullFaithfulFunctor_section.
197 Context `(F:Functor(c1:=C1)(c2:=C2)(fobj:=Fobj)).
198 Context (F_full:FullFunctor F).
199 Context (F_faithful:FaithfulFunctor F).
201 Lemma ff_functor_section_id_preserved : forall a:C1, projT1 (F_full _ _ (id (F a))) ~~ id a.
203 set (F_full a a (id (F a))) as qq.
207 setoid_rewrite fmor_preserves_id.
211 Definition ff_functor_section_fobj (a:FullImage F) : C1 := projT1 (projT2 a).
213 Definition ff_functor_section_fmor {a b:FullImage F} (f:a~~{FullImage F}~~>b)
214 : (ff_functor_section_fobj a)~~{C1}~~>(ff_functor_section_fobj b).
215 destruct a as [ a1 [ a2 a3 ] ].
217 unfold ff_functor_section_fobj.
219 destruct b as [ b1 [ b2 b3 ] ].
221 unfold ff_functor_section_fobj.
223 apply (@ff_invert _ _ _ _ _ _ _ _ F_full).
227 Lemma ff_functor_section_respectful {a2 b2 c2 : C1}
228 (x0 : Fobj b2 ~~{ C2 }~~> Fobj c2)
229 (x : Fobj a2 ~~{ C2 }~~> Fobj b2) :
230 (let (x1, _) := F_full a2 b2 x in x1) >>>
231 (let (x1, _) := F_full b2 c2 x0 in x1) ~~
232 (let (x1, _) := F_full a2 c2 (x >>> x0) in x1).
233 set (F_full _ _ x) as x_full.
234 set (F_full _ _ x0) as x0_full.
235 set (F_full _ _ (x >>> x0)) as x_x0_full.
241 setoid_rewrite <- (fmor_preserves_comp F).
247 Instance ff_functor_section_functor : Functor (FullImage F) C1 ff_functor_section_fobj :=
248 { fmor := fun a b f => ff_functor_section_fmor f }.
250 destruct a; destruct b; destruct s; destruct s0; destruct f; destruct f'; simpl in *;
251 subst; simpl; set (F_full x1 x2 x3) as ff1; set (F_full x1 x2 x4) as ff2; destruct ff1; destruct ff2;
253 etransitivity; [ apply e | idtac ];
255 etransitivity; [ apply e0 | idtac ];
259 destruct a as [ a1 [ a2 a3 ] ];
262 apply ff_functor_section_id_preserved).
264 destruct a as [ a1 [ a2 a3 ] ];
265 destruct b as [ b1 [ b2 b3 ] ];
266 destruct c as [ c1 [ c2 c3 ] ];
272 apply ff_functor_section_respectful).
275 Lemma ff_functor_section_splits_helper (a2 b2:C1)(f:existT (fun d : C2, {c : C1 & Fobj c = d}) (Fobj a2)
276 (existT (fun c : C1, Fobj c = Fobj a2) a2 (eq_refl _)) ~~{
278 }~~> existT (fun d : C2, {c : C1 & Fobj c = d})
279 (Fobj b2) (existT (fun c : C1, Fobj c = Fobj b2) b2 (eq_refl _)))
280 : F \ (let (x1, _) := F_full a2 b2 (let (x1, _) := f in x1) in x1) ~~ projT1 f.
283 set (F_full a2 b2 x) as qq.
288 Lemma ff_functor_section_splits : (ff_functor_section_functor >>>> RestrictToImage F) ~~~~ functor_id _.
289 unfold EqualFunctors.
292 destruct a as [ a1 [ a2 a3 ] ].
293 destruct b as [ b1 [ b2 b3 ] ].
299 apply heq_morphisms_intro.
301 etransitivity; [ idtac | apply H ].
304 apply ff_functor_section_splits_helper.
307 Definition ff_functor_section_splits_niso_helper a : ((ff_functor_section_functor >>>> RestrictToImage F) a ≅ (functor_id (FullImage F)) a).
310 unfold ff_functor_section_fobj.
311 unfold RestrictToImage_fobj.
312 destruct a as [ a1 [ a2 a3 ] ].
319 Lemma ff_functor_section_splits_niso : (ff_functor_section_functor >>>> RestrictToImage F) ≃ functor_id _.
321 exists ff_functor_section_splits_niso_helper.
324 destruct A as [ a1 [ a2 a3 ] ].
325 destruct B as [ b1 [ b2 b3 ] ].
329 setoid_rewrite left_identity.
330 setoid_rewrite right_identity.
331 set (F_full a2 b2 x) as qr.
336 Lemma ffc_functor_weakly_monic : ConservativeFunctor F -> WeaklyMonic F.
340 Opaque ff_functor_section_splits_niso_helper.
342 End FullFaithfulFunctor_section.