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