src/Subcategories_ch7_1.v

   1 (****************************************************************************)
   2 (* Chapter 7.1: Subcategories                                               *)
   3 (****************************************************************************)
   4
   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.
  13
  14 (* Any morphism-predicate which is closed under composition and
  15  * passing to identity morphisms (of either the domain or codomain)
  16  *
  17  * We could recycle the "predicate on morphisms" to determine the
  18  * "predicate on objects", but this causes technical difficulties with
  19  * Coq *)
  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))
  24 }.
  25
  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.
  29   intros; auto.
  30   intros; auto.
  31   Defined.
  32
  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.
  36   Defined.
  37
  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))
  46   }.
  47   intros; apply Build_Equivalence. unfold Reflexive.
  48      intros; reflexivity.
  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.
  55   Defined.
  56 End SubCategoriesAreCategories.
  57 Coercion SubCategoriesAreCategories : SubCategory >-> Category.
  58
  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.
  66   Defined.
  67
  68 Definition FullImage `(F:Functor(c1:=C)(c2:=D)(fobj:=Fobj)) := FullSubcategory D (fun d => { c:C & (Fobj c)=d }).
  69
  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.
  74     intros.
  75     exists (F X).
  76     exists X.
  77     reflexivity.
  78     Defined.
  79   Definition RestrictToImage_fmor a b (f:a~>b) : (RestrictToImage_fobj a)~~{FullImage F}~~>(RestrictToImage_fobj b).
  80     exists (F \ f); auto.
  81     Defined.
  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.
  87     Defined.
  88   Lemma RestrictToImage_splits : F ≃ (RestrictToImage >>>> InclusionFunctor _ _).
  89     exists (fun A => iso_id (F A)).
  90     intros; simpl.
  91     setoid_rewrite left_identity.
  92     setoid_rewrite right_identity.
  93     reflexivity.
  94     Qed.
  95 End RestrictToImage.
  96
  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).
 103   Defined.
 104
 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).
 113   Section Forward.
 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)).
 121       intros.
 122       exists (F \ X).
 123       apply (pmor dom ran X).
 124       Defined.
 125     Definition FunctorWithRangeInSubCategory : Functor Cat1 SP FunctorWithRangeInSubCategory_fobj.
 126       apply Build_Functor with (fmor:=FunctorWithRangeInSubCategory_fmor);
 127         intros;
 128         unfold FunctorWithRangeInSubCategory_fmor;
 129         simpl.
 130       setoid_rewrite H; auto.
 131       apply (fmor_preserves_id F).
 132       apply (fmor_preserves_comp F).
 133       Defined.
 134   End Forward.
 135   Section Opposite.
 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).
 143       intros.
 144       exists (F \ X).
 145       apply (pmor dom ran X).
 146       Defined.
 147     (*
 148     Definition FunctorWithRangeInSubCategoryOp : Functor Cat1 SP⁽ºᑭ⁾ FunctorWithRangeInSubCategoryOp_fobj.
 149       apply Build_Functor with (fmor:=FunctorWithRangeInSubCategoryOp_fmor);
 150         intros;
 151         unfold FunctorWithRangeInSubCategoryOp_fmor;
 152         simpl.
 153       apply (fmor_respects(Functor:=F)); auto.
 154       apply (fmor_preserves_id(Functor:=F)).
 155       unfold eqv; simpl.
 156       set (@fmor_preserves_comp _ _ _ _ _ _ _ F _ _ f _ g) as qq.
 157       setoid_rewrite <- qq.
 158       apply reflexivity.
 159       Defined.
 160       *)
 161   End Opposite.
 162 End FunctorWithRangeInSubCategory.
 163
 164
 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'.
 168
 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))
 173   }.
 174   Coercion ff_invert : FullFunctor >-> Funclass.
 175
 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 }.
 179
 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
 183   ; cf_reflect_iso1 : forall a b (i:(F a) ≅ (F b)), F \ #(cf_reflect_iso a b i) ~~ #i
 184   ; cf_reflect_iso2 : forall a b (i:(F a) ≅ (F b)), F \ #(cf_reflect_iso a b i)⁻¹ ~~ #i⁻¹
 185   }.
 186
 187 (* "monic up to natural iso" *)
 188 Definition WeaklyMonic
 189     `{C:Category}
 190     `{D:Category}
 191      {Fobj}
 192      (F:@Functor _ _ C _ _ D Fobj) := forall
 193     `{E:Category}
 194     `{G :@Functor _ _ E _ _ C Gobj'}
 195     `{H :@Functor _ _ E _ _ C Hobj'},
 196     G >>>> F ≃ H >>>> F
 197     -> G ≃ H.
 198
 199 Section FullFaithfulFunctor_section.
 200   Context `(F:Functor(c1:=C1)(c2:=C2)(fobj:=Fobj)).
 201   Context  (F_full:FullFunctor F).
 202   Context  (F_faithful:FaithfulFunctor F).
 203
 204   Lemma ff_functor_section_id_preserved : forall a:C1, projT1 (F_full _ _ (id (F a))) ~~ id a.
 205     intros.
 206     set (F_full a a (id (F a))) as qq.
 207     destruct qq.
 208     simpl.
 209     apply F_faithful.
 210     setoid_rewrite fmor_preserves_id.
 211     auto.
 212     Qed.
 213
 214   Definition ff_functor_section_fobj (a:FullImage F) : C1 := projT1 (projT2 a).
 215
 216   Definition ff_functor_section_fmor {a b:FullImage F} (f:a~~{FullImage F}~~>b)
 217     : (ff_functor_section_fobj a)~~{C1}~~>(ff_functor_section_fobj b).
 218     destruct a as [ a1 [ a2 a3 ] ].
 219     subst.
 220     unfold ff_functor_section_fobj.
 221     simpl.
 222     destruct b as [ b1 [ b2 b3 ] ].
 223     subst.
 224     unfold ff_functor_section_fobj.
 225     simpl.
 226     apply (@ff_invert _ _ _ _ _ _ _ _ F_full).
 227     apply f.
 228     Defined.
 229
 230   Lemma ff_functor_section_respectful {a2 b2 c2 : C1}
 231     (x0 : Fobj b2 ~~{ C2 }~~> Fobj c2)
 232     (x  : Fobj a2 ~~{ C2 }~~> Fobj b2) :
 233     (let (x1, _) := F_full a2 b2 x in x1) >>>
 234     (let (x1, _) := F_full b2 c2 x0 in x1) ~~
 235     (let (x1, _) := F_full a2 c2 (x >>> x0) in x1).
 236     set (F_full _ _ x) as x_full.
 237     set (F_full _ _ x0) as x0_full.
 238     set (F_full _ _ (x >>> x0)) as x_x0_full.
 239     destruct x_full.
 240     destruct x0_full.
 241     destruct x_x0_full.
 242     apply F_faithful.
 243     setoid_rewrite e1.
 244     setoid_rewrite <- (fmor_preserves_comp F).
 245     setoid_rewrite e.
 246     setoid_rewrite e0.
 247     reflexivity.
 248     Qed.
 249
 250   Instance ff_functor_section_functor : Functor (FullImage F) C1 ff_functor_section_fobj :=
 251     { fmor := fun a b f => ff_functor_section_fmor f }.
 252     abstract (intros;
 253       destruct a; destruct b; destruct s; destruct s0; destruct f; destruct f'; simpl in *;
 254       subst; simpl; set (F_full x1 x2 x3) as ff1; set (F_full x1 x2 x4) as ff2; destruct ff1; destruct ff2;
 255       apply F_faithful;
 256       etransitivity; [ apply e | idtac ];
 257       symmetry;
 258       etransitivity; [ apply e0 | idtac ];
 259       symmetry; auto).
 260     abstract (intros;
 261       simpl;
 262       destruct a as [ a1 [ a2 a3 ] ];
 263       subst;
 264       simpl;
 265       apply ff_functor_section_id_preserved).
 266     abstract (intros;
 267       destruct a as [ a1 [ a2 a3 ] ];
 268       destruct b as [ b1 [ b2 b3 ] ];
 269       destruct c as [ c1 [ c2 c3 ] ];
 270       subst;
 271       simpl in *;
 272       destruct f;
 273       destruct g;
 274       simpl in *;
 275       apply ff_functor_section_respectful).
 276       Defined.
 277
 278   Lemma ff_functor_section_splits_helper (a2 b2:C1)(f:existT (fun d : C2, {c : C1 & Fobj c = d}) (Fobj a2)
 279         (existT (fun c : C1, Fobj c = Fobj a2) a2 (eq_refl _)) ~~{
 280       FullImage F
 281       }~~> existT (fun d : C2, {c : C1 & Fobj c = d})
 282              (Fobj b2) (existT (fun c : C1, Fobj c = Fobj b2) b2 (eq_refl _)))
 283      : F \ (let (x1, _) := F_full a2 b2 (let (x1, _) := f in x1) in x1) ~~ projT1 f.
 284     destruct f.
 285     simpl.
 286     set (F_full a2 b2 x) as qq.
 287     destruct qq.
 288     apply e.
 289     Qed.
 290
 291   Lemma ff_functor_section_splits : (ff_functor_section_functor >>>> RestrictToImage F) ~~~~ functor_id _.
 292     unfold EqualFunctors.
 293     intros.
 294     simpl.
 295     destruct a as [ a1 [ a2 a3 ] ].
 296     destruct b as [ b1 [ b2 b3 ] ].
 297     subst.
 298     simpl in *.
 299     inversion f; subst.
 300     inversion f'; subst.
 301     simpl in *.
 302     apply heq_morphisms_intro.
 303     simpl.
 304     etransitivity; [ idtac | apply H ].
 305     clear H.
 306     clear f'.
 307     apply ff_functor_section_splits_helper.
 308     Qed.
 309
 310   Definition ff_functor_section_splits_niso_helper a : ((ff_functor_section_functor >>>> RestrictToImage F) a ≅ (functor_id (FullImage F)) a).
 311     intros; simpl.
 312     unfold functor_fobj.
 313     unfold ff_functor_section_fobj.
 314     unfold RestrictToImage_fobj.
 315     destruct a as [ a1 [ a2 a3 ] ].
 316     simpl.
 317     subst.
 318     unfold functor_fobj.
 319     apply iso_id.
 320     Defined.
 321
 322   Lemma ff_functor_section_splits_niso : (ff_functor_section_functor >>>> RestrictToImage F) ≃ functor_id _.
 323     intros; simpl.
 324     exists ff_functor_section_splits_niso_helper.
 325     intros.
 326     simpl in *.
 327     destruct A as [ a1 [ a2 a3 ] ].
 328     destruct B as [ b1 [ b2 b3 ] ].
 329     simpl.
 330     destruct f; subst.
 331     simpl.
 332     setoid_rewrite left_identity.
 333     setoid_rewrite right_identity.
 334     set (F_full a2 b2 x) as qr.
 335     destruct qr.
 336     symmetry; auto.
 337     Qed.
 338
 339   Definition ff_functor_section_splits_niso_helper' a
 340     : ((RestrictToImage F >>>> ff_functor_section_functor) a ≅ (functor_id _) a).
 341     intros; simpl.
 342     unfold functor_fobj.
 343     unfold ff_functor_section_fobj.
 344     unfold RestrictToImage_fobj.
 345     simpl.
 346     apply iso_id.
 347     Defined.
 348
 349   Lemma ff_functor_section_splits_niso' : (RestrictToImage F >>>> ff_functor_section_functor) ≃ functor_id _.
 350     intros; simpl.
 351     exists ff_functor_section_splits_niso_helper'.
 352     intros.
 353     simpl in *.
 354     setoid_rewrite left_identity.
 355     setoid_rewrite right_identity.
 356     set (F_full _ _ (F \ f)) as qr.
 357     destruct qr.
 358     apply F_faithful in e.
 359     symmetry.
 360     auto.
 361     Qed.
 362
 363   Context (CF:ConservativeFunctor F).
 364
 365   Lemma if_fullimage `{C0:Category}{Aobj}{Bobj}{A:Functor C0 C1 Aobj}{B:Functor C0 C1 Bobj} :
 366     A >>>> F ≃ B >>>> F ->
 367     A >>>> RestrictToImage F ≃ B >>>> RestrictToImage F.
 368     intro H.
 369     destruct H.
 370     unfold IsomorphicFunctors.
 371     set (fun A  => functors_preserve_isos (RestrictToImage F) (cf_reflect_iso _ _ (x A))).
 372     exists i.
 373     intros.
 374     unfold RestrictToImage.
 375     unfold functor_comp.
 376     simpl.
 377     unfold functor_comp in H.
 378     simpl in H.
 379     rewrite (cf_reflect_iso1(ConservativeFunctor:=CF) _ _ (x A0)).
 380     rewrite (cf_reflect_iso1(ConservativeFunctor:=CF) _ _ (x B0)).
 381     apply H.
 382     Qed.
 383
 384   Lemma ffc_functor_weakly_monic : ConservativeFunctor F -> WeaklyMonic F.
 385     intro H.
 386     unfold WeaklyMonic; intros.
 387     apply (if_comp(F2:=G>>>>functor_id _)).
 388     apply if_inv.
 389     apply if_right_identity.
 390     apply if_inv.
 391     apply (if_comp(F2:=H0>>>>functor_id _)).
 392     apply if_inv.
 393     apply if_right_identity.
 394     eapply if_inv.
 395     apply (if_comp(F2:=G>>>>(RestrictToImage F >>>> ff_functor_section_functor))).
 396     apply (@if_respects _ _ _ _ _ _ _ _ _ _ G _ G _ (functor_id C1) _ (RestrictToImage F >>>> ff_functor_section_functor)).
 397     apply if_id.
 398     apply if_inv.
 399     apply ff_functor_section_splits_niso'.
 400     apply if_inv.
 401     apply (if_comp(F2:=H0>>>>(RestrictToImage F >>>> ff_functor_section_functor))).
 402     apply (@if_respects _ _ _ _ _ _ _ _ _ _ H0 _ H0 _ (functor_id C1) _ (RestrictToImage F >>>> ff_functor_section_functor)).
 403     apply if_id.
 404     apply if_inv.
 405     apply ff_functor_section_splits_niso'.
 406     assert
 407       ((H0 >>>> (RestrictToImage F >>>> ff_functor_section_functor))
 408         ≃ ((H0 >>>> RestrictToImage F) >>>> ff_functor_section_functor)).
 409     apply if_inv.
 410     apply if_associativity.
 411     apply (if_comp H2).
 412     clear H2.
 413     apply if_inv.
 414     assert
 415       ((G >>>> (RestrictToImage F >>>> ff_functor_section_functor))
 416         ≃ ((G >>>> RestrictToImage F) >>>> ff_functor_section_functor)).
 417     apply if_inv.
 418     apply if_associativity.
 419     apply (if_comp H2).
 420     clear H2.
 421     apply if_respects.
 422     apply if_fullimage.
 423     apply H1.
 424     apply if_id.
 425     Qed.
 426
 427   Opaque ff_functor_section_splits_niso_helper.
 428
 429 End FullFaithfulFunctor_section.