src/Subcategories_ch7_1.v

   1 (****************************************************************************)
   2 (* Chapter 7.1: Subcategories                                               *)
   3 (****************************************************************************)
   4
   5 Generalizable All Variables.
   6 Require Import Notations.
   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.
  13
  14 (*
  15  * See the README for an explanation of why there is "WideSubcategory"
  16  * and "FullSubcategory" but no "Subcategory"
  17  *)
  18
  19 (* a full subcategory requires nothing more than a predicate on objects *)
  20 Class FullSubcategory `(C:Category)(Pobj:C->Type) := { }.
  21
  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
  28 }.
  29   intros; apply Build_Equivalence. unfold Reflexive.
  30      intros; reflexivity.
  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.
  37   Defined.
  38 Coercion FullSubCategoriesAreCategories : FullSubcategory >-> Category.
  39
  40 (* every category is a subcategory of itself *)
  41 (*
  42 Instance IdentitySubCategory `(C:Category Ob Hom) : SubCategory C (fun _ => True) (fun _ _ _ _ _ => True).
  43   intros; apply Build_SubCategory.
  44   intros; auto.
  45   intros; auto.
  46   Defined.
  47 *)
  48 (* the inclusion operation from a subcategory to its host is a functor *)
  49 Instance FullSubcategoryInclusionFunctor `(SP:@FullSubcategory Ob Hom C Pobj)
  50   : Functor SP C (fun x => projT1 x) :=
  51   { fmor := fun dom ran f => f }.
  52   intros. unfold eqv in H. simpl in H. auto.
  53   intros. simpl. reflexivity.
  54   intros. simpl. reflexivity.
  55   Defined.
  56
  57 (* a wide subcategory includes all objects, so it requires nothing more than a predicate on each hom-set *)
  58 Class WideSubcategory `(C:Category Ob Hom)(Pmor:forall a b:Ob, (a~>b) ->Type) : Type :=
  59 { wsc_id_included    : forall (a:Ob), Pmor a a (id a)
  60 ; wsc_comp_included  : forall (a b c:Ob) f g, (Pmor a b f) -> (Pmor b c g) -> (Pmor a c (f>>>g))
  61 }.
  62
  63 (* the category construction for full subcategories is simpler: *)
  64 Instance WideSubCategoriesAreCategories `{C:Category(Ob:=Ob)}{Pmor}(wsc:WideSubcategory C Pmor)
  65   : Category Ob (fun x y => sigT (Pmor x y)) :=
  66   { id   := fun t         => existT _ (id t) (@wsc_id_included _ _ _ _ wsc t)
  67   ; eqv  := fun a b f g   => eqv _ _ (projT1 f) (projT1 g)
  68   ; comp := fun a b c f g => existT (Pmor a c) (projT1 f >>> projT1 g)
  69                                     (@wsc_comp_included _ _ _ _ wsc _ _ _ _ _ (projT2 f) (projT2 g))
  70   }.
  71   intros; apply Build_Equivalence. unfold Reflexive.
  72      intros; reflexivity.
  73      unfold Symmetric; intros; simpl; symmetry; auto.
  74      unfold Transitive; intros; simpl. transitivity (projT1 y); auto.
  75   intros; unfold Proper. unfold respectful. intros. simpl. apply comp_respects. auto. auto.
  76   intros; simpl. apply left_identity.
  77   intros; simpl. apply right_identity.
  78   intros; simpl. apply associativity.
  79   Defined.
  80 Coercion WideSubCategoriesAreCategories : WideSubcategory >-> Category.
  81
  82 (* the full image of a functor is a full subcategory *)
  83 Section FullImage.
  84
  85   Context `(F:Functor(c1:=C)(c2:=D)).
  86
  87   Instance FullImage : Category C (fun x y => (F x)~~{D}~~>(F y)) :=
  88   { id    := fun t         => id (F t)
  89   ; eqv   := fun x y   f g => eqv(Category:=D)  _ _ f g
  90   ; comp  := fun x y z f g => comp(Category:=D) _ _ _ f g
  91   }.
  92   intros; apply Build_Equivalence. unfold Reflexive.
  93      intros; reflexivity.
  94      unfold Symmetric; intros; simpl; symmetry; auto.
  95      unfold Transitive; intros; simpl. transitivity y; auto.
  96   intros; unfold Proper. unfold respectful. intros. simpl. apply comp_respects. auto. auto.
  97   intros; simpl. apply left_identity.
  98   intros; simpl. apply right_identity.
  99   intros; simpl. apply associativity.
 100   Defined.
 101
 102   Instance FullImage_InclusionFunctor : Functor FullImage D (fun x => F x) :=
 103     { fmor := fun x y f => f }.
 104     intros; auto.
 105     intros; simpl; reflexivity.
 106     intros; simpl; reflexivity.
 107     Defined.
 108
 109   Instance RestrictToImage : Functor C FullImage (fun x => x) :=
 110     { fmor := fun a b f => F \ f }.
 111     intros; simpl; apply fmor_respects; auto.
 112     intros; simpl; apply fmor_preserves_id; auto.
 113     intros; simpl; apply fmor_preserves_comp; auto.
 114     Defined.
 115
 116   Lemma RestrictToImage_splits : F ~~~~ (RestrictToImage >>>> FullImage_InclusionFunctor).
 117     unfold EqualFunctors; simpl; intros; apply heq_morphisms_intro.
 118     apply fmor_respects.
 119     auto.
 120     Defined.
 121
 122   Lemma RestrictToImage_splits_niso : F ≃ (RestrictToImage >>>> FullImage_InclusionFunctor).
 123     unfold IsomorphicFunctors.
 124     exists (fun A => iso_id (fobj A)).
 125     intros.
 126     simpl.
 127     setoid_rewrite left_identity.
 128     setoid_rewrite right_identity.
 129     reflexivity.
 130     Qed.
 131
 132 End FullImage.
 133
 134 (* any functor may be restricted to a subcategory of its domain *)
 135 Section RestrictDomain.
 136
 137   Context `{C:Category}.
 138   Context `{D:Category}.
 139   Context `(F:!Functor C D fobj).
 140   Context  {Pmor}(S:WideSubcategory C Pmor).
 141
 142   Instance RestrictDomain : Functor S D fobj :=
 143     { fmor  := fun a b f => F \ (projT1 f) }.
 144     intros; destruct f; destruct f'; simpl in *.
 145       apply fmor_respects; auto.
 146     intros. simpl. apply fmor_preserves_id.
 147     intros; simpl; destruct f; destruct g; simpl in *.
 148       apply fmor_preserves_comp.
 149     Defined.
 150
 151 End RestrictDomain.
 152
 153 (*
 154 Instance func_opSubcat `(c1:Category)`(c2:Category)`(SP:@SubCategory _ _ c2 Pobj Pmor)
 155   {fobj}(F:Functor c1⁽ºᑭ⁾ SP fobj) : Functor c1 SP⁽ºᑭ⁾ fobj :=
 156   { fmor                := fun a b f => fmor F f }.
 157   intros. apply (@fmor_respects _ _ _ _ _ _ _ F _ _ f f' H).
 158   intros. apply (@fmor_preserves_id _ _ _ _ _ _ _ F a).
 159   intros. apply (@fmor_preserves_comp _ _ _ _ _ _ _ F _ _ g _ f).
 160   Defined.
 161 *)
 162
 163 (*
 164 (* if a functor's range falls within a subcategory, then it is already a functor into that subcategory *)
 165 Section FunctorWithRangeInSubCategory.
 166   Context `(Cat1:Category O1 Hom1).
 167   Context `(Cat2:Category O2 Hom2).
 168   Context (Pobj:Cat2 -> Type).
 169   Context (Pmor:forall a b:Cat2, (Pobj a) -> (Pobj b) -> (a~~{Cat2}~~>b) -> Type).
 170   Context (SP:SubCategory Cat2 Pobj Pmor).
 171   Context (Fobj:Cat1->Cat2).
 172   Section Forward.
 173     Context (F:Functor Cat1 Cat2 Fobj).
 174     Context (pobj:forall a, Pobj (F a)).
 175     Context (pmor:forall a b f, Pmor (F a) (F b) (pobj a) (pobj b) (F \ f)).
 176     Definition FunctorWithRangeInSubCategory_fobj (X:Cat1) : SP :=
 177       existT Pobj (Fobj X) (pobj X).
 178     Definition FunctorWithRangeInSubCategory_fmor (dom ran:Cat1)(X:dom~>ran) : (@hom _ _ SP
 179       (FunctorWithRangeInSubCategory_fobj dom) (FunctorWithRangeInSubCategory_fobj ran)).
 180       intros.
 181       exists (F \ X).
 182       apply (pmor dom ran X).
 183       Defined.
 184     Definition FunctorWithRangeInSubCategory : Functor Cat1 SP FunctorWithRangeInSubCategory_fobj.
 185       apply Build_Functor with (fmor:=FunctorWithRangeInSubCategory_fmor);
 186         intros;
 187         unfold FunctorWithRangeInSubCategory_fmor;
 188         simpl.
 189       setoid_rewrite H; auto.
 190       apply (fmor_preserves_id F).
 191       apply (fmor_preserves_comp F).
 192       Defined.
 193   End Forward.
 194   Section Opposite.
 195     Context (F:Functor Cat1 Cat2⁽ºᑭ⁾ Fobj).
 196     Context (pobj:forall a, Pobj (F a)).
 197     Context (pmor:forall a b f, Pmor (F b) (F a) (pobj b) (pobj a) (F \ f)).
 198     Definition FunctorWithRangeInSubCategoryOp_fobj (X:Cat1) : SP :=
 199       existT Pobj (Fobj X) (pobj X).
 200     Definition FunctorWithRangeInSubCategoryOp_fmor (dom ran:Cat1)(X:dom~>ran) :
 201       (FunctorWithRangeInSubCategoryOp_fobj dom)~~{SP⁽ºᑭ⁾}~~>(FunctorWithRangeInSubCategoryOp_fobj ran).
 202       intros.
 203       exists (F \ X).
 204       apply (pmor dom ran X).
 205       Defined.
 206     (*
 207     Definition FunctorWithRangeInSubCategoryOp : Functor Cat1 SP⁽ºᑭ⁾ FunctorWithRangeInSubCategoryOp_fobj.
 208       apply Build_Functor with (fmor:=FunctorWithRangeInSubCategoryOp_fmor);
 209         intros;
 210         unfold FunctorWithRangeInSubCategoryOp_fmor;
 211         simpl.
 212       apply (fmor_respects(Functor:=F)); auto.
 213       apply (fmor_preserves_id(Functor:=F)).
 214       unfold eqv; simpl.
 215       set (@fmor_preserves_comp _ _ _ _ _ _ _ F _ _ f _ g) as qq.
 216       setoid_rewrite <- qq.
 217       apply reflexivity.
 218       Defined.
 219       *)
 220   End Opposite.
 221 End FunctorWithRangeInSubCategory.
 222 *)
 223
 224
 225 (* Definition 7.1: faithful functors *)
 226 Definition FaithfulFunctor `(F:Functor(c1:=C1)(c2:=C2)(fobj:=Fobj)) :=
 227   forall (a b:C1), forall (f f':a~>b), (fmor _ f)~~(fmor _ f') -> f~~f'.
 228
 229 (* Definition 7.1: full functors *)
 230 Class FullFunctor `(F:Functor(c1:=C1)(c2:=C2)(fobj:=Fobj)) :=
 231   { ff_invert         : forall {a b}(f:(Fobj a)~~{C2}~~>(Fobj b)) , { f' : a~~{C1}~~>b & (F \ f') ~~ f }
 232   ; ff_respects       : forall {a b}, Proper (eqv (Fobj a) (Fobj b) ==> eqv a b) (fun x => projT1 (@ff_invert a b x))
 233   }.
 234   Coercion ff_invert : FullFunctor >-> Funclass.
 235
 236 (* Definition 7.1: (essentially) surjective on objects *)
 237 Definition EssentiallySurjectiveOnObjects `(F:Functor(c1:=C1)(c2:=C2)(fobj:=Fobj)) :=
 238   forall o2:C2, { o1:C1 & (F o1) ≅ o2 }.
 239
 240 (* Definition 7.1: (essentially) injective on objects *)
 241 (* TODO *)
 242
 243 Class ConservativeFunctor `(F:Functor(c1:=C1)(c2:=C2)(fobj:=Fobj)) :=
 244   { cf_reflect_iso  : forall (a b:C1),  (F a) ≅ (F b) -> a ≅ b
 245   ; cf_reflect_iso1 : forall a b (i:(F a) ≅ (F b)), F \ #(cf_reflect_iso a b i) ~~ #i
 246   ; cf_reflect_iso2 : forall a b (i:(F a) ≅ (F b)), F \ #(cf_reflect_iso a b i)⁻¹ ~~ #i⁻¹
 247   }.
 248
 249 (* "monic up to natural iso" *)
 250 Definition WeaklyMonic
 251     `{C:Category}
 252     `{D:Category}
 253      {Fobj}
 254      (F:@Functor _ _ C _ _ D Fobj) := forall
 255      Eob EHom (E:@Category Eob EHom)
 256     `{G :@Functor _ _ E _ _ C Gobj'}
 257     `{H :@Functor _ _ E _ _ C Hobj'},
 258     G >>>> F ≃ H >>>> F
 259     -> G ≃ H.
 260
 261 Section FullFaithfulFunctor_section.
 262   Context `(F:Functor(c1:=C1)(c2:=C2)(fobj:=Fobj)).
 263   Context  (F_full:FullFunctor F).
 264   Context  (F_faithful:FaithfulFunctor F).
 265
 266   Lemma ff_functor_section_id_preserved : forall a:C1, projT1 (F_full _ _ (id (F a))) ~~ id a.
 267     intros.
 268     set (F_full a a (id (F a))) as qq.
 269     destruct qq.
 270     simpl.
 271     apply F_faithful.
 272     setoid_rewrite fmor_preserves_id.
 273     auto.
 274     Qed.
 275
 276   Definition ff_functor_section_fmor {a b:FullImage F} (f:a~~{FullImage F}~~>b) : a~~{C1}~~>b.
 277     set (@ff_invert _ _ _ _ _ _ _ _ F_full _ _ f) as f'.
 278     destruct f'.
 279     apply x.
 280     Defined.
 281
 282   Lemma ff_functor_section_respectful {a2 b2 c2 : C1}
 283     (x0 : Fobj b2 ~~{ C2 }~~> Fobj c2)
 284     (x  : Fobj a2 ~~{ C2 }~~> Fobj b2) :
 285     (let (x1, _) := F_full a2 b2 x in x1) >>>
 286     (let (x1, _) := F_full b2 c2 x0 in x1) ~~
 287     (let (x1, _) := F_full a2 c2 (x >>> x0) in x1).
 288     set (F_full _ _ x) as x_full.
 289     set (F_full _ _ x0) as x0_full.
 290     set (F_full _ _ (x >>> x0)) as x_x0_full.
 291     destruct x_full.
 292     destruct x0_full.
 293     destruct x_x0_full.
 294     apply F_faithful.
 295     setoid_rewrite e1.
 296     setoid_rewrite <- (fmor_preserves_comp F).
 297     setoid_rewrite e.
 298     setoid_rewrite e0.
 299     reflexivity.
 300     Qed.
 301
 302   Instance ff_functor_section_functor : Functor (FullImage F) C1 (fun x => x) :=
 303     { fmor := fun a b f => ff_functor_section_fmor f }.
 304     intros.
 305       unfold ff_functor_section_fmor; simpl.
 306       destruct (F_full a b f).
 307       destruct (F_full a b f').
 308       apply F_faithful.
 309       setoid_rewrite e0.
 310       setoid_rewrite e.
 311       auto.
 312     intros; simpl; subst.
 313       apply ff_functor_section_id_preserved.
 314     intros; simpl in *.
 315       apply ff_functor_section_respectful.
 316       Defined.
 317 (*
 318   Lemma ff_functor_section_splits_helper (a2 b2:C1)(f:existT (fun d : C2, {c : C1 & Fobj c = d}) (Fobj a2)
 319         (existT (fun c : C1, Fobj c = Fobj a2) a2 (eq_refl _)) ~~{
 320       FullImage F
 321       }~~> existT (fun d : C2, {c : C1 & Fobj c = d})
 322              (Fobj b2) (existT (fun c : C1, Fobj c = Fobj b2) b2 (eq_refl _)))
 323      : F \ (let (x1, _) := F_full a2 b2 f in x1) ~~ f.
 324     simpl.
 325     set (F_full a2 b2 f) as qq.
 326     destruct qq.
 327     apply e.
 328     Qed.
 329 *)
 330   Lemma ff_functor_section_splits : (ff_functor_section_functor >>>> RestrictToImage F) ~~~~ functor_id _.
 331     unfold EqualFunctors; intros; simpl.
 332     unfold ff_functor_section_fmor; simpl.
 333     destruct (F_full a b f).
 334     idtac.
 335     apply (@heq_morphisms_intro _ _ (FullImage F) a b).
 336     unfold eqv; simpl.
 337     setoid_rewrite e.
 338     apply H.
 339     Qed.
 340
 341   Lemma ff_functor_section_splits_niso : (ff_functor_section_functor >>>> RestrictToImage F) ≃ functor_id _.
 342     intros; simpl.
 343     exists iso_id; intros.
 344     symmetry.
 345     unfold functor_comp; simpl.
 346     setoid_rewrite left_identity.
 347     setoid_rewrite right_identity.
 348     unfold ff_functor_section_fmor.
 349     destruct (F_full A B f).
 350     auto.
 351     Qed.
 352
 353   Lemma ff_functor_section_splits_niso' : (RestrictToImage F >>>> ff_functor_section_functor) ≃ functor_id _.
 354     intros; simpl.
 355     exists iso_id; intros.
 356     symmetry.
 357     unfold functor_comp; simpl.
 358     setoid_rewrite left_identity.
 359     setoid_rewrite right_identity.
 360     unfold ff_functor_section_fmor.
 361     destruct (F_full A B (F \ f)).
 362     apply F_faithful.
 363     auto.
 364     Qed.
 365
 366   Context (CF:ConservativeFunctor F).
 367
 368   Lemma if_fullimage `{C0:Category}{Aobj}{Bobj}{A:Functor C0 C1 Aobj}{B:Functor C0 C1 Bobj} :
 369     A >>>> F ≃ B >>>> F ->
 370     A >>>> RestrictToImage F ≃ B >>>> RestrictToImage F.
 371     intro H.
 372     destruct H.
 373     unfold IsomorphicFunctors.
 374     set (fun A  => functors_preserve_isos (RestrictToImage F) (cf_reflect_iso _ _ (x A))).
 375     exists i.
 376     intros.
 377     unfold RestrictToImage.
 378     unfold functor_comp.
 379     simpl.
 380     unfold functor_comp in H.
 381     simpl in H.
 382     rewrite (cf_reflect_iso1(ConservativeFunctor:=CF) _ _ (x A0)).
 383     rewrite (cf_reflect_iso1(ConservativeFunctor:=CF) _ _ (x B0)).
 384     apply H.
 385     Qed.
 386
 387   Lemma ffc_functor_weakly_monic : ConservativeFunctor F -> WeaklyMonic F.
 388     intro H.
 389     unfold WeaklyMonic; intros.
 390     apply (if_comp(F2:=G>>>>functor_id _)).
 391     apply if_inv.
 392     apply if_right_identity.
 393     apply if_inv.
 394     apply (if_comp(F2:=H0>>>>functor_id _)).
 395     apply if_inv.
 396     apply if_right_identity.
 397     eapply if_inv.
 398     apply (if_comp(F2:=G>>>>(RestrictToImage F >>>> ff_functor_section_functor))).
 399     apply (if_respects G G (functor_id C1) (RestrictToImage F >>>> ff_functor_section_functor)).
 400     apply if_id.
 401     apply if_inv.
 402     apply ff_functor_section_splits_niso'.
 403     apply if_inv.
 404     apply (if_comp(F2:=H0>>>>(RestrictToImage F >>>> ff_functor_section_functor))).
 405     apply (if_respects H0 H0 (functor_id C1) (RestrictToImage F >>>> ff_functor_section_functor)).
 406     apply if_id.
 407     apply if_inv.
 408     apply ff_functor_section_splits_niso'.
 409     assert
 410       ((H0 >>>> (RestrictToImage F >>>> ff_functor_section_functor))
 411         ≃ ((H0 >>>> RestrictToImage F) >>>> ff_functor_section_functor)).
 412     apply if_inv.
 413     apply (if_associativity H0 (RestrictToImage F) ff_functor_section_functor).
 414     apply (if_comp H2).
 415     clear H2.
 416     apply if_inv.
 417     assert
 418       ((G >>>> (RestrictToImage F >>>> ff_functor_section_functor))
 419         ≃ ((G >>>> RestrictToImage F) >>>> ff_functor_section_functor)).
 420     apply if_inv.
 421     apply (if_associativity G (RestrictToImage F) ff_functor_section_functor).
 422     apply (if_comp H2).
 423     clear H2.
 424     apply (if_respects (G >>>> RestrictToImage F) (H0 >>>> RestrictToImage F)
 425       ff_functor_section_functor ff_functor_section_functor).
 426     apply if_fullimage.
 427     apply H1.
 428     simpl.
 429     exists (ni_id _).
 430     intros.
 431     simpl.
 432     setoid_rewrite left_identity.
 433     setoid_rewrite right_identity.
 434     reflexivity.
 435     Qed.
 436
 437 End FullFaithfulFunctor_section.