(****************************************************************************) (* Chapter 7.1: Subcategories *) (****************************************************************************) Generalizable All Variables. Require Import Notations. Require Import Categories_ch1_3. Require Import Functors_ch1_4. Require Import Isomorphisms_ch1_5. Require Import OppositeCategories_ch1_6_2. Require Import NaturalTransformations_ch7_4. Require Import NaturalIsomorphisms_ch7_5. (* * See the README for an explanation of why there is "WideSubcategory" * and "FullSubcategory" but no "Subcategory" *) (* a full subcategory requires nothing more than a predicate on objects *) Class FullSubcategory `(C:Category)(Pobj:C->Type) := { }. (* the category construction for full subcategories is simpler: *) Instance FullSubCategoriesAreCategories `(fsc:@FullSubcategory Ob Hom C Pobj) : Category (sigT Pobj) (fun dom ran => (projT1 dom)~~{C}~~>(projT1 ran)) := { id := fun t => id (projT1 t) ; eqv := fun a b f g => eqv _ _ f g ; comp := fun a b c f g => f >>> g }. intros; apply Build_Equivalence. unfold Reflexive. intros; reflexivity. unfold Symmetric; intros; simpl; symmetry; auto. unfold Transitive; intros; simpl. transitivity y; auto. intros; unfold Proper. unfold respectful. intros. simpl. apply comp_respects. auto. auto. intros; simpl. apply left_identity. intros; simpl. apply right_identity. intros; simpl. apply associativity. Defined. Coercion FullSubCategoriesAreCategories : FullSubcategory >-> Category. (* every category is a subcategory of itself *) (* Instance IdentitySubCategory `(C:Category Ob Hom) : SubCategory C (fun _ => True) (fun _ _ _ _ _ => True). intros; apply Build_SubCategory. intros; auto. intros; auto. Defined. (* the inclusion operation from a subcategory to its host is a functor *) Instance InclusionFunctor `(C:Category Ob Hom)`(SP:@SubCategory _ _ C Pobj Pmor) : Functor SP C (fun x => projT1 x) := { fmor := fun dom ran f => projT1 f }. intros. unfold eqv in H. simpl in H. auto. intros. simpl. reflexivity. intros. simpl. reflexivity. Defined. *) (* a wide subcategory includes all objects, so it requires nothing more than a predicate on each hom-set *) Class WideSubcategory `(C:Category Ob Hom)(Pmor:forall a b:Ob, (a~>b) ->Type) : Type := { wsc_id_included : forall (a:Ob), Pmor a a (id a) ; wsc_comp_included : forall (a b c:Ob) f g, (Pmor a b f) -> (Pmor b c g) -> (Pmor a c (f>>>g)) }. (* the category construction for full subcategories is simpler: *) Instance WideSubCategoriesAreCategories `{C:Category(Ob:=Ob)}{Pmor}(wsc:WideSubcategory C Pmor) : Category Ob (fun x y => sigT (Pmor x y)) := { id := fun t => existT _ (id t) (@wsc_id_included _ _ _ _ wsc t) ; eqv := fun a b f g => eqv _ _ (projT1 f) (projT1 g) ; comp := fun a b c f g => existT (Pmor a c) (projT1 f >>> projT1 g) (@wsc_comp_included _ _ _ _ wsc _ _ _ _ _ (projT2 f) (projT2 g)) }. intros; apply Build_Equivalence. unfold Reflexive. intros; reflexivity. unfold Symmetric; intros; simpl; symmetry; auto. unfold Transitive; intros; simpl. transitivity (projT1 y); auto. intros; unfold Proper. unfold respectful. intros. simpl. apply comp_respects. auto. auto. intros; simpl. apply left_identity. intros; simpl. apply right_identity. intros; simpl. apply associativity. Defined. Coercion WideSubCategoriesAreCategories : WideSubcategory >-> Category. (* the full image of a functor is a full subcategory *) Section FullImage. Context `(F:Functor(c1:=C)(c2:=D)). Instance FullImage : Category C (fun x y => (F x)~~{D}~~>(F y)) := { id := fun t => id (F t) ; eqv := fun x y f g => eqv(Category:=D) _ _ f g ; comp := fun x y z f g => comp(Category:=D) _ _ _ f g }. intros; apply Build_Equivalence. unfold Reflexive. intros; reflexivity. unfold Symmetric; intros; simpl; symmetry; auto. unfold Transitive; intros; simpl. transitivity y; auto. intros; unfold Proper. unfold respectful. intros. simpl. apply comp_respects. auto. auto. intros; simpl. apply left_identity. intros; simpl. apply right_identity. intros; simpl. apply associativity. Defined. Instance FullImage_InclusionFunctor : Functor FullImage D (fun x => F x) := { fmor := fun x y f => f }. intros; auto. intros; simpl; reflexivity. intros; simpl; reflexivity. Defined. Instance RestrictToImage : Functor C FullImage (fun x => x) := { fmor := fun a b f => F \ f }. intros; simpl; apply fmor_respects; auto. intros; simpl; apply fmor_preserves_id; auto. intros; simpl; apply fmor_preserves_comp; auto. Defined. Lemma RestrictToImage_splits : F ~~~~ (RestrictToImage >>>> FullImage_InclusionFunctor). unfold EqualFunctors; simpl; intros; apply heq_morphisms_intro. apply fmor_respects. auto. Defined. End FullImage. (* any functor may be restricted to a subcategory of its domain *) Section RestrictDomain. Context `{C:Category}. Context `{D:Category}. Context `(F:!Functor C D fobj). Context {Pmor}(S:WideSubcategory C Pmor). Instance RestrictDomain : Functor S D fobj := { fmor := fun a b f => F \ (projT1 f) }. intros; destruct f; destruct f'; simpl in *. apply fmor_respects; auto. intros. simpl. apply fmor_preserves_id. intros; simpl; destruct f; destruct g; simpl in *. apply fmor_preserves_comp. Defined. End RestrictDomain. (* Instance func_opSubcat `(c1:Category)`(c2:Category)`(SP:@SubCategory _ _ c2 Pobj Pmor) {fobj}(F:Functor c1⁽ºᑭ⁾ SP fobj) : Functor c1 SP⁽ºᑭ⁾ fobj := { fmor := fun a b f => fmor F f }. intros. apply (@fmor_respects _ _ _ _ _ _ _ F _ _ f f' H). intros. apply (@fmor_preserves_id _ _ _ _ _ _ _ F a). intros. apply (@fmor_preserves_comp _ _ _ _ _ _ _ F _ _ g _ f). Defined. *) (* (* if a functor's range falls within a subcategory, then it is already a functor into that subcategory *) Section FunctorWithRangeInSubCategory. Context `(Cat1:Category O1 Hom1). Context `(Cat2:Category O2 Hom2). Context (Pobj:Cat2 -> Type). Context (Pmor:forall a b:Cat2, (Pobj a) -> (Pobj b) -> (a~~{Cat2}~~>b) -> Type). Context (SP:SubCategory Cat2 Pobj Pmor). Context (Fobj:Cat1->Cat2). Section Forward. Context (F:Functor Cat1 Cat2 Fobj). Context (pobj:forall a, Pobj (F a)). Context (pmor:forall a b f, Pmor (F a) (F b) (pobj a) (pobj b) (F \ f)). Definition FunctorWithRangeInSubCategory_fobj (X:Cat1) : SP := existT Pobj (Fobj X) (pobj X). Definition FunctorWithRangeInSubCategory_fmor (dom ran:Cat1)(X:dom~>ran) : (@hom _ _ SP (FunctorWithRangeInSubCategory_fobj dom) (FunctorWithRangeInSubCategory_fobj ran)). intros. exists (F \ X). apply (pmor dom ran X). Defined. Definition FunctorWithRangeInSubCategory : Functor Cat1 SP FunctorWithRangeInSubCategory_fobj. apply Build_Functor with (fmor:=FunctorWithRangeInSubCategory_fmor); intros; unfold FunctorWithRangeInSubCategory_fmor; simpl. setoid_rewrite H; auto. apply (fmor_preserves_id F). apply (fmor_preserves_comp F). Defined. End Forward. Section Opposite. Context (F:Functor Cat1 Cat2⁽ºᑭ⁾ Fobj). Context (pobj:forall a, Pobj (F a)). Context (pmor:forall a b f, Pmor (F b) (F a) (pobj b) (pobj a) (F \ f)). Definition FunctorWithRangeInSubCategoryOp_fobj (X:Cat1) : SP := existT Pobj (Fobj X) (pobj X). Definition FunctorWithRangeInSubCategoryOp_fmor (dom ran:Cat1)(X:dom~>ran) : (FunctorWithRangeInSubCategoryOp_fobj dom)~~{SP⁽ºᑭ⁾}~~>(FunctorWithRangeInSubCategoryOp_fobj ran). intros. exists (F \ X). apply (pmor dom ran X). Defined. (* Definition FunctorWithRangeInSubCategoryOp : Functor Cat1 SP⁽ºᑭ⁾ FunctorWithRangeInSubCategoryOp_fobj. apply Build_Functor with (fmor:=FunctorWithRangeInSubCategoryOp_fmor); intros; unfold FunctorWithRangeInSubCategoryOp_fmor; simpl. apply (fmor_respects(Functor:=F)); auto. apply (fmor_preserves_id(Functor:=F)). unfold eqv; simpl. set (@fmor_preserves_comp _ _ _ _ _ _ _ F _ _ f _ g) as qq. setoid_rewrite <- qq. apply reflexivity. Defined. *) End Opposite. End FunctorWithRangeInSubCategory. *) (* Definition 7.1: faithful functors *) Definition FaithfulFunctor `(F:Functor(c1:=C1)(c2:=C2)(fobj:=Fobj)) := forall (a b:C1), forall (f f':a~>b), (fmor _ f)~~(fmor _ f') -> f~~f'. (* Definition 7.1: full functors *) Class FullFunctor `(F:Functor(c1:=C1)(c2:=C2)(fobj:=Fobj)) := { ff_invert : forall {a b}(f:(Fobj a)~~{C2}~~>(Fobj b)) , { f' : a~~{C1}~~>b & (F \ f') ~~ f } ; ff_respects : forall {a b}, Proper (eqv (Fobj a) (Fobj b) ==> eqv a b) (fun x => projT1 (@ff_invert a b x)) }. Coercion ff_invert : FullFunctor >-> Funclass. (* Definition 7.1: (essentially) surjective on objects *) Definition EssentiallySurjectiveOnObjects `(F:Functor(c1:=C1)(c2:=C2)(fobj:=Fobj)) := forall o2:C2, { o1:C1 & (F o1) ≅ o2 }. (* Definition 7.1: (essentially) injective on objects *) (* TODO *) Class ConservativeFunctor `(F:Functor(c1:=C1)(c2:=C2)(fobj:=Fobj)) := { cf_reflect_iso : forall (a b:C1), (F a) ≅ (F b) -> a ≅ b ; cf_reflect_iso1 : forall a b (i:(F a) ≅ (F b)), F \ #(cf_reflect_iso a b i) ~~ #i ; cf_reflect_iso2 : forall a b (i:(F a) ≅ (F b)), F \ #(cf_reflect_iso a b i)⁻¹ ~~ #i⁻¹ }. (* "monic up to natural iso" *) Definition WeaklyMonic `{C:Category} `{D:Category} {Fobj} (F:@Functor _ _ C _ _ D Fobj) := forall Eob EHom (E:@Category Eob EHom) `{G :@Functor _ _ E _ _ C Gobj'} `{H :@Functor _ _ E _ _ C Hobj'}, G >>>> F ≃ H >>>> F -> G ≃ H. Section FullFaithfulFunctor_section. Context `(F:Functor(c1:=C1)(c2:=C2)(fobj:=Fobj)). Context (F_full:FullFunctor F). Context (F_faithful:FaithfulFunctor F). Lemma ff_functor_section_id_preserved : forall a:C1, projT1 (F_full _ _ (id (F a))) ~~ id a. intros. set (F_full a a (id (F a))) as qq. destruct qq. simpl. apply F_faithful. setoid_rewrite fmor_preserves_id. auto. Qed. Definition ff_functor_section_fmor {a b:FullImage F} (f:a~~{FullImage F}~~>b) : a~~{C1}~~>b. set (@ff_invert _ _ _ _ _ _ _ _ F_full _ _ f) as f'. destruct f'. apply x. Defined. Lemma ff_functor_section_respectful {a2 b2 c2 : C1} (x0 : Fobj b2 ~~{ C2 }~~> Fobj c2) (x : Fobj a2 ~~{ C2 }~~> Fobj b2) : (let (x1, _) := F_full a2 b2 x in x1) >>> (let (x1, _) := F_full b2 c2 x0 in x1) ~~ (let (x1, _) := F_full a2 c2 (x >>> x0) in x1). set (F_full _ _ x) as x_full. set (F_full _ _ x0) as x0_full. set (F_full _ _ (x >>> x0)) as x_x0_full. destruct x_full. destruct x0_full. destruct x_x0_full. apply F_faithful. setoid_rewrite e1. setoid_rewrite <- (fmor_preserves_comp F). setoid_rewrite e. setoid_rewrite e0. reflexivity. Qed. Instance ff_functor_section_functor : Functor (FullImage F) C1 (fun x => x) := { fmor := fun a b f => ff_functor_section_fmor f }. intros. unfold ff_functor_section_fmor; simpl. destruct (F_full a b f). destruct (F_full a b f'). apply F_faithful. setoid_rewrite e0. setoid_rewrite e. auto. intros; simpl; subst. apply ff_functor_section_id_preserved. intros; simpl in *. apply ff_functor_section_respectful. Defined. (* Lemma ff_functor_section_splits_helper (a2 b2:C1)(f:existT (fun d : C2, {c : C1 & Fobj c = d}) (Fobj a2) (existT (fun c : C1, Fobj c = Fobj a2) a2 (eq_refl _)) ~~{ FullImage F }~~> existT (fun d : C2, {c : C1 & Fobj c = d}) (Fobj b2) (existT (fun c : C1, Fobj c = Fobj b2) b2 (eq_refl _))) : F \ (let (x1, _) := F_full a2 b2 f in x1) ~~ f. simpl. set (F_full a2 b2 f) as qq. destruct qq. apply e. Qed. *) Lemma ff_functor_section_splits : (ff_functor_section_functor >>>> RestrictToImage F) ~~~~ functor_id _. unfold EqualFunctors; intros; simpl. unfold ff_functor_section_fmor; simpl. destruct (F_full a b f). idtac. apply (@heq_morphisms_intro _ _ (FullImage F) a b). unfold eqv; simpl. setoid_rewrite e. apply H. Qed. Lemma ff_functor_section_splits_niso : (ff_functor_section_functor >>>> RestrictToImage F) ≃ functor_id _. intros; simpl. exists iso_id; intros. symmetry. unfold functor_comp; simpl. setoid_rewrite left_identity. setoid_rewrite right_identity. unfold ff_functor_section_fmor. destruct (F_full A B f). auto. Qed. Lemma ff_functor_section_splits_niso' : (RestrictToImage F >>>> ff_functor_section_functor) ≃ functor_id _. intros; simpl. exists iso_id; intros. symmetry. unfold functor_comp; simpl. setoid_rewrite left_identity. setoid_rewrite right_identity. unfold ff_functor_section_fmor. destruct (F_full A B (F \ f)). apply F_faithful. auto. Qed. Context (CF:ConservativeFunctor F). Lemma if_fullimage `{C0:Category}{Aobj}{Bobj}{A:Functor C0 C1 Aobj}{B:Functor C0 C1 Bobj} : A >>>> F ≃ B >>>> F -> A >>>> RestrictToImage F ≃ B >>>> RestrictToImage F. intro H. destruct H. unfold IsomorphicFunctors. set (fun A => functors_preserve_isos (RestrictToImage F) (cf_reflect_iso _ _ (x A))). exists i. intros. unfold RestrictToImage. unfold functor_comp. simpl. unfold functor_comp in H. simpl in H. rewrite (cf_reflect_iso1(ConservativeFunctor:=CF) _ _ (x A0)). rewrite (cf_reflect_iso1(ConservativeFunctor:=CF) _ _ (x B0)). apply H. Qed. Lemma ffc_functor_weakly_monic : ConservativeFunctor F -> WeaklyMonic F. intro H. unfold WeaklyMonic; intros. apply (if_comp(F2:=G>>>>functor_id _)). apply if_inv. apply if_right_identity. apply if_inv. apply (if_comp(F2:=H0>>>>functor_id _)). apply if_inv. apply if_right_identity. eapply if_inv. apply (if_comp(F2:=G>>>>(RestrictToImage F >>>> ff_functor_section_functor))). apply (if_respects G G (functor_id C1) (RestrictToImage F >>>> ff_functor_section_functor)). apply if_id. apply if_inv. apply ff_functor_section_splits_niso'. apply if_inv. apply (if_comp(F2:=H0>>>>(RestrictToImage F >>>> ff_functor_section_functor))). apply (if_respects H0 H0 (functor_id C1) (RestrictToImage F >>>> ff_functor_section_functor)). apply if_id. apply if_inv. apply ff_functor_section_splits_niso'. assert ((H0 >>>> (RestrictToImage F >>>> ff_functor_section_functor)) ≃ ((H0 >>>> RestrictToImage F) >>>> ff_functor_section_functor)). apply if_inv. apply (if_associativity H0 (RestrictToImage F) ff_functor_section_functor). apply (if_comp H2). clear H2. apply if_inv. assert ((G >>>> (RestrictToImage F >>>> ff_functor_section_functor)) ≃ ((G >>>> RestrictToImage F) >>>> ff_functor_section_functor)). apply if_inv. apply (if_associativity G (RestrictToImage F) ff_functor_section_functor). apply (if_comp H2). clear H2. apply (if_respects (G >>>> RestrictToImage F) (H0 >>>> RestrictToImage F) ff_functor_section_functor ff_functor_section_functor). apply if_fullimage. apply H1. simpl. exists (ni_id _). intros. simpl. setoid_rewrite left_identity. setoid_rewrite right_identity. reflexivity. Qed. End FullFaithfulFunctor_section.