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.
15 * See the README for an explanation of why there is "WideSubcategory"
16 * and "FullSubcategory" but no "Subcategory"
19 (* a full subcategory requires nothing more than a predicate on objects *)
20 Class FullSubcategory `(C:Category)(Pobj:C->Type) := { }.
22 (* the category construction for full subcategories is simpler: *)
23 Instance FullSubCategoriesAreCategories `(fsc:@FullSubcategory Ob Hom C Pobj)
24 : Category (sigT Pobj) (fun dom ran => (projT1 dom)~~{C}~~>(projT1 ran)) :=
25 { id := fun t => id (projT1 t)
26 ; eqv := fun a b f g => eqv _ _ f g
27 ; comp := fun a b c f g => f >>> g
29 intros; apply Build_Equivalence. unfold Reflexive.
31 unfold Symmetric; intros; simpl; symmetry; auto.
32 unfold Transitive; intros; simpl. transitivity y; auto.
33 intros; unfold Proper. unfold respectful. intros. simpl. apply comp_respects. auto. auto.
34 intros; simpl. apply left_identity.
35 intros; simpl. apply right_identity.
36 intros; simpl. apply associativity.
38 Coercion FullSubCategoriesAreCategories : FullSubcategory >-> Category.
40 (* every category is a subcategory of itself! *)
42 Instance IdentitySubCategory `(C:Category Ob Hom) : SubCategory C (fun _ => True) (fun _ _ _ _ _ => True).
43 intros; apply Build_SubCategory.
47 (* the inclusion operation from a subcategory to its host is a functor *)
48 Instance InclusionFunctor `(C:Category Ob Hom)`(SP:@SubCategory _ _ C Pobj Pmor)
49 : Functor SP C (fun x => projT1 x) :=
50 { fmor := fun dom ran f => projT1 f }.
51 intros. unfold eqv in H. simpl in H. auto.
52 intros. simpl. reflexivity.
53 intros. simpl. reflexivity.
58 (* a wide subcategory includes all objects, so it requires nothing more than a predicate on each hom-set *)
59 Class WideSubcategory `(C:Category Ob Hom)(Pmor:forall a b:Ob, (a~>b) ->Type) : Type :=
60 { wsc_id_included : forall (a:Ob), Pmor a a (id a)
61 ; wsc_comp_included : forall (a b c:Ob) f g, (Pmor a b f) -> (Pmor b c g) -> (Pmor a c (f>>>g))
64 (* the category construction for full subcategories is simpler: *)
65 Instance WideSubCategoriesAreCategories `{C:Category(Ob:=Ob)}{Pmor}(wsc:WideSubcategory C Pmor)
66 : Category Ob (fun x y => sigT (Pmor x y)) :=
67 { id := fun t => existT _ (id t) (@wsc_id_included _ _ _ _ wsc t)
68 ; eqv := fun a b f g => eqv _ _ (projT1 f) (projT1 g)
69 ; comp := fun a b c f g => existT (Pmor a c) (projT1 f >>> projT1 g)
70 (@wsc_comp_included _ _ _ _ wsc _ _ _ _ _ (projT2 f) (projT2 g))
73 intros; apply Build_Equivalence. unfold Reflexive.
75 unfold Symmetric; intros; simpl; symmetry; auto.
76 unfold Transitive; intros; simpl. transitivity (projT1 y); auto.
77 intros; unfold Proper. unfold respectful. intros. simpl. apply comp_respects. auto. auto.
78 intros; simpl. apply left_identity.
79 intros; simpl. apply right_identity.
80 intros; simpl. apply associativity.
82 Coercion WideSubCategoriesAreCategories : WideSubcategory >-> Category.
84 (* the full image of a functor is a full subcategory *)
87 Context `(F:Functor(c1:=C)(c2:=D)).
89 Instance FullImage : Category C (fun x y => (F x)~~{D}~~>(F y)) :=
90 { id := fun t => id (F t)
91 ; eqv := fun x y f g => eqv(Category:=D) _ _ f g
92 ; comp := fun x y z f g => comp(Category:=D) _ _ _ f g
94 intros; apply Build_Equivalence. unfold Reflexive.
96 unfold Symmetric; intros; simpl; symmetry; auto.
97 unfold Transitive; intros; simpl. transitivity y; auto.
98 intros; unfold Proper. unfold respectful. intros. simpl. apply comp_respects. auto. auto.
99 intros; simpl. apply left_identity.
100 intros; simpl. apply right_identity.
101 intros; simpl. apply associativity.
104 Instance FullImage_InclusionFunctor : Functor FullImage D (fun x => F x) :=
105 { fmor := fun x y f => f }.
107 intros; simpl; reflexivity.
108 intros; simpl; reflexivity.
111 Instance RestrictToImage : Functor C FullImage (fun x => x) :=
112 { fmor := fun a b f => F \ f }.
113 intros; simpl; apply fmor_respects; auto.
114 intros; simpl; apply fmor_preserves_id; auto.
115 intros; simpl; apply fmor_preserves_comp; auto.
118 Lemma RestrictToImage_splits : F ~~~~ (RestrictToImage >>>> FullImage_InclusionFunctor).
119 unfold EqualFunctors; simpl; intros; apply heq_morphisms_intro.
127 Instance func_opSubcat `(c1:Category)`(c2:Category)`(SP:@SubCategory _ _ c2 Pobj Pmor)
128 {fobj}(F:Functor c1⁽ºᑭ⁾ SP fobj) : Functor c1 SP⁽ºᑭ⁾ fobj :=
129 { fmor := fun a b f => fmor F f }.
130 intros. apply (@fmor_respects _ _ _ _ _ _ _ F _ _ f f' H).
131 intros. apply (@fmor_preserves_id _ _ _ _ _ _ _ F a).
132 intros. apply (@fmor_preserves_comp _ _ _ _ _ _ _ F _ _ g _ f).
137 (* if a functor's range falls within a subcategory, then it is already a functor into that subcategory *)
138 Section FunctorWithRangeInSubCategory.
139 Context `(Cat1:Category O1 Hom1).
140 Context `(Cat2:Category O2 Hom2).
141 Context (Pobj:Cat2 -> Type).
142 Context (Pmor:forall a b:Cat2, (Pobj a) -> (Pobj b) -> (a~~{Cat2}~~>b) -> Type).
143 Context (SP:SubCategory Cat2 Pobj Pmor).
144 Context (Fobj:Cat1->Cat2).
146 Context (F:Functor Cat1 Cat2 Fobj).
147 Context (pobj:forall a, Pobj (F a)).
148 Context (pmor:forall a b f, Pmor (F a) (F b) (pobj a) (pobj b) (F \ f)).
149 Definition FunctorWithRangeInSubCategory_fobj (X:Cat1) : SP :=
150 existT Pobj (Fobj X) (pobj X).
151 Definition FunctorWithRangeInSubCategory_fmor (dom ran:Cat1)(X:dom~>ran) : (@hom _ _ SP
152 (FunctorWithRangeInSubCategory_fobj dom) (FunctorWithRangeInSubCategory_fobj ran)).
155 apply (pmor dom ran X).
157 Definition FunctorWithRangeInSubCategory : Functor Cat1 SP FunctorWithRangeInSubCategory_fobj.
158 apply Build_Functor with (fmor:=FunctorWithRangeInSubCategory_fmor);
160 unfold FunctorWithRangeInSubCategory_fmor;
162 setoid_rewrite H; auto.
163 apply (fmor_preserves_id F).
164 apply (fmor_preserves_comp F).
168 Context (F:Functor Cat1 Cat2⁽ºᑭ⁾ Fobj).
169 Context (pobj:forall a, Pobj (F a)).
170 Context (pmor:forall a b f, Pmor (F b) (F a) (pobj b) (pobj a) (F \ f)).
171 Definition FunctorWithRangeInSubCategoryOp_fobj (X:Cat1) : SP :=
172 existT Pobj (Fobj X) (pobj X).
173 Definition FunctorWithRangeInSubCategoryOp_fmor (dom ran:Cat1)(X:dom~>ran) :
174 (FunctorWithRangeInSubCategoryOp_fobj dom)~~{SP⁽ºᑭ⁾}~~>(FunctorWithRangeInSubCategoryOp_fobj ran).
177 apply (pmor dom ran X).
180 Definition FunctorWithRangeInSubCategoryOp : Functor Cat1 SP⁽ºᑭ⁾ FunctorWithRangeInSubCategoryOp_fobj.
181 apply Build_Functor with (fmor:=FunctorWithRangeInSubCategoryOp_fmor);
183 unfold FunctorWithRangeInSubCategoryOp_fmor;
185 apply (fmor_respects(Functor:=F)); auto.
186 apply (fmor_preserves_id(Functor:=F)).
188 set (@fmor_preserves_comp _ _ _ _ _ _ _ F _ _ f _ g) as qq.
189 setoid_rewrite <- qq.
194 End FunctorWithRangeInSubCategory.
198 (* Definition 7.1: faithful functors *)
199 Definition FaithfulFunctor `(F:Functor(c1:=C1)(c2:=C2)(fobj:=Fobj)) :=
200 forall (a b:C1), forall (f f':a~>b), (fmor _ f)~~(fmor _ f') -> f~~f'.
202 (* Definition 7.1: full functors *)
203 Class FullFunctor `(F:Functor(c1:=C1)(c2:=C2)(fobj:=Fobj)) :=
204 { ff_invert : forall {a b}(f:(Fobj a)~~{C2}~~>(Fobj b)) , { f' : a~~{C1}~~>b & (F \ f') ~~ f }
205 ; ff_respects : forall {a b}, Proper (eqv (Fobj a) (Fobj b) ==> eqv a b) (fun x => projT1 (@ff_invert a b x))
207 Coercion ff_invert : FullFunctor >-> Funclass.
209 (* Definition 7.1: (essentially) surjective on objects *)
210 Definition EssentiallySurjectiveOnObjects `(F:Functor(c1:=C1)(c2:=C2)(fobj:=Fobj)) :=
211 forall o2:C2, { o1:C1 & (F o1) ≅ o2 }.
213 (* Definition 7.1: (essentially) injective on objects *)
214 Class ConservativeFunctor `(F:Functor(c1:=C1)(c2:=C2)(fobj:=Fobj)) :=
215 { cf_reflect_iso : forall (a b:C1), (F a) ≅ (F b) -> a ≅ b
216 ; cf_reflect_iso1 : forall a b (i:(F a) ≅ (F b)), F \ #(cf_reflect_iso a b i) ~~ #i
217 ; cf_reflect_iso2 : forall a b (i:(F a) ≅ (F b)), F \ #(cf_reflect_iso a b i)⁻¹ ~~ #i⁻¹
220 (* "monic up to natural iso" *)
221 Definition WeaklyMonic
225 (F:@Functor _ _ C _ _ D Fobj) := forall
226 Eob EHom (E:@Category Eob EHom)
227 `{G :@Functor _ _ E _ _ C Gobj'}
228 `{H :@Functor _ _ E _ _ C Hobj'},
233 Section FullFaithfulFunctor_section.
234 Context `(F:Functor(c1:=C1)(c2:=C2)(fobj:=Fobj)).
235 Context (F_full:FullFunctor F).
236 Context (F_faithful:FaithfulFunctor F).
238 Lemma ff_functor_section_id_preserved : forall a:C1, projT1 (F_full _ _ (id (F a))) ~~ id a.
240 set (F_full a a (id (F a))) as qq.
244 setoid_rewrite fmor_preserves_id.
248 Definition ff_functor_section_fobj (a:FullImage F) : C1 := projT1 (projT2 a).
250 Definition ff_functor_section_fmor {a b:FullImage F} (f:a~~{FullImage F}~~>b)
251 : (ff_functor_section_fobj a)~~{C1}~~>(ff_functor_section_fobj b).
252 destruct a as [ a1 [ a2 a3 ] ].
253 destruct b as [ b1 [ b2 b3 ] ].
254 set (@ff_invert _ _ _ _ _ _ _ _ F_full _ _ f) as f'.
255 destruct a as [ a1 [ a2 a3 ] ].
257 unfold ff_functor_section_fobj.
259 destruct b as [ b1 [ b2 b3 ] ].
261 unfold ff_functor_section_fobj.
263 apply (@ff_invert _ _ _ _ _ _ _ _ F_full).
267 Lemma ff_functor_section_respectful {a2 b2 c2 : C1}
268 (x0 : Fobj b2 ~~{ C2 }~~> Fobj c2)
269 (x : Fobj a2 ~~{ C2 }~~> Fobj b2) :
270 (let (x1, _) := F_full a2 b2 x in x1) >>>
271 (let (x1, _) := F_full b2 c2 x0 in x1) ~~
272 (let (x1, _) := F_full a2 c2 (x >>> x0) in x1).
273 set (F_full _ _ x) as x_full.
274 set (F_full _ _ x0) as x0_full.
275 set (F_full _ _ (x >>> x0)) as x_x0_full.
281 setoid_rewrite <- (fmor_preserves_comp F).
287 Instance ff_functor_section_functor : Functor (FullImage F) C1 ff_functor_section_fobj :=
288 { fmor := fun a b f => ff_functor_section_fmor f }.
290 destruct a; destruct b; destruct s; destruct s0; simpl in *;
291 subst; simpl; set (F_full x1 x2 f) as ff1; set (F_full x1 x2 f') as ff2; destruct ff1; destruct ff2;
293 etransitivity; [ apply e | idtac ];
295 etransitivity; [ apply e0 | idtac ];
299 destruct a as [ a1 [ a2 a3 ] ];
302 apply ff_functor_section_id_preserved).
304 destruct a as [ a1 [ a2 a3 ] ];
305 destruct b as [ b1 [ b2 b3 ] ];
306 destruct c as [ c1 [ c2 c3 ] ];
310 apply ff_functor_section_respectful).
313 Lemma ff_functor_section_splits_helper (a2 b2:C1)(f:existT (fun d : C2, {c : C1 & Fobj c = d}) (Fobj a2)
314 (existT (fun c : C1, Fobj c = Fobj a2) a2 (eq_refl _)) ~~{
316 }~~> existT (fun d : C2, {c : C1 & Fobj c = d})
317 (Fobj b2) (existT (fun c : C1, Fobj c = Fobj b2) b2 (eq_refl _)))
318 : F \ (let (x1, _) := F_full a2 b2 f in x1) ~~ f.
320 set (F_full a2 b2 f) as qq.
325 Lemma ff_functor_section_splits : (ff_functor_section_functor >>>> RestrictToImage F) ~~~~ functor_id _.
326 unfold EqualFunctors.
329 destruct a as [ a1 [ a2 a3 ] ].
330 destruct b as [ b1 [ b2 b3 ] ].
334 apply heq_morphisms_intro.
336 unfold RestrictToImage_fmor; simpl.
337 etransitivity; [ idtac | apply H ].
340 apply ff_functor_section_splits_helper.
343 Definition ff_functor_section_splits_niso_helper a : ((ff_functor_section_functor >>>> RestrictToImage F) a ≅ (functor_id (FullImage F)) a).
346 unfold ff_functor_section_fobj.
347 unfold RestrictToImage_fobj.
348 destruct a as [ a1 [ a2 a3 ] ].
355 Lemma ff_functor_section_splits_niso : (ff_functor_section_functor >>>> RestrictToImage F) ≃ functor_id _.
357 exists ff_functor_section_splits_niso_helper.
360 destruct A as [ a1 [ a2 a3 ] ].
361 destruct B as [ b1 [ b2 b3 ] ].
363 unfold RestrictToImage_fmor; simpl.
364 setoid_rewrite left_identity.
365 setoid_rewrite right_identity.
366 set (F_full a2 b2 x) as qr.
371 Definition ff_functor_section_splits_niso_helper' a
372 : ((RestrictToImage F >>>> ff_functor_section_functor) a ≅ (functor_id _) a).
375 unfold ff_functor_section_fobj.
376 unfold RestrictToImage_fobj.
381 Lemma ff_functor_section_splits_niso' : (RestrictToImage F >>>> ff_functor_section_functor) ≃ functor_id _.
383 exists ff_functor_section_splits_niso_helper'.
386 setoid_rewrite left_identity.
387 setoid_rewrite right_identity.
388 set (F_full _ _ (F \ f)) as qr.
390 apply F_faithful in e.
395 Context (CF:ConservativeFunctor F).
397 Lemma if_fullimage `{C0:Category}{Aobj}{Bobj}{A:Functor C0 C1 Aobj}{B:Functor C0 C1 Bobj} :
398 A >>>> F ≃ B >>>> F ->
399 A >>>> RestrictToImage F ≃ B >>>> RestrictToImage F.
402 unfold IsomorphicFunctors.
403 set (fun A => functors_preserve_isos (RestrictToImage F) (cf_reflect_iso _ _ (x A))).
406 unfold RestrictToImage.
409 unfold functor_comp in H.
411 rewrite (cf_reflect_iso1(ConservativeFunctor:=CF) _ _ (x A0)).
412 rewrite (cf_reflect_iso1(ConservativeFunctor:=CF) _ _ (x B0)).
416 Lemma ffc_functor_weakly_monic : ConservativeFunctor F -> WeaklyMonic F.
418 unfold WeaklyMonic; intros.
419 apply (if_comp(F2:=G>>>>functor_id _)).
421 apply if_right_identity.
423 apply (if_comp(F2:=H0>>>>functor_id _)).
425 apply if_right_identity.
427 apply (if_comp(F2:=G>>>>(RestrictToImage F >>>> ff_functor_section_functor))).
428 apply (@if_respects _ _ _ _ _ _ _ _ _ _ G _ G _ (functor_id C1) _ (RestrictToImage F >>>> ff_functor_section_functor)).
431 apply ff_functor_section_splits_niso'.
433 apply (if_comp(F2:=H0>>>>(RestrictToImage F >>>> ff_functor_section_functor))).
434 apply (@if_respects _ _ _ _ _ _ _ _ _ _ H0 _ H0 _ (functor_id C1) _ (RestrictToImage F >>>> ff_functor_section_functor)).
437 apply ff_functor_section_splits_niso'.
439 ((H0 >>>> (RestrictToImage F >>>> ff_functor_section_functor))
440 ≃ ((H0 >>>> RestrictToImage F) >>>> ff_functor_section_functor)).
442 apply if_associativity.
447 ((G >>>> (RestrictToImage F >>>> ff_functor_section_functor))
448 ≃ ((G >>>> RestrictToImage F) >>>> ff_functor_section_functor)).
450 apply if_associativity.
459 Opaque ff_functor_section_splits_niso_helper.
461 End FullFaithfulFunctor_section.