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
 184 (* "monic up to natural iso" *)
 185 Definition WeaklyMonic
 186     `{C:Category}
 187     `{D:Category}
 188      {Fobj}
 189      (F:@Functor _ _ C _ _ D Fobj) := forall
 190     `{E:Category}
 191     `{G :@Functor _ _ E _ _ C Gobj'}
 192     `{H :@Functor _ _ E _ _ C Hobj'},
 193     G >>>> F ≃ H >>>> F
 194     -> G ≃ H.
 195
 196 Section FullFaithfulFunctor_section.
 197   Context `(F:Functor(c1:=C1)(c2:=C2)(fobj:=Fobj)).
 198   Context  (F_full:FullFunctor F).
 199   Context  (F_faithful:FaithfulFunctor F).
 200
 201   Lemma ff_functor_section_id_preserved : forall a:C1, projT1 (F_full _ _ (id (F a))) ~~ id a.
 202     intros.
 203     set (F_full a a (id (F a))) as qq.
 204     destruct qq.
 205     simpl.
 206     apply F_faithful.
 207     setoid_rewrite fmor_preserves_id.
 208     auto.
 209     Qed.
 210
 211   Definition ff_functor_section_fobj (a:FullImage F) : C1 := projT1 (projT2 a).
 212
 213   Definition ff_functor_section_fmor {a b:FullImage F} (f:a~~{FullImage F}~~>b)
 214     : (ff_functor_section_fobj a)~~{C1}~~>(ff_functor_section_fobj b).
 215     destruct a as [ a1 [ a2 a3 ] ].
 216     subst.
 217     unfold ff_functor_section_fobj.
 218     simpl.
 219     destruct b as [ b1 [ b2 b3 ] ].
 220     subst.
 221     unfold ff_functor_section_fobj.
 222     simpl.
 223     apply (@ff_invert _ _ _ _ _ _ _ _ F_full).
 224     apply f.
 225     Defined.
 226
 227   Lemma ff_functor_section_respectful {a2 b2 c2 : C1}
 228     (x0 : Fobj b2 ~~{ C2 }~~> Fobj c2)
 229     (x  : Fobj a2 ~~{ C2 }~~> Fobj b2) :
 230     (let (x1, _) := F_full a2 b2 x in x1) >>>
 231     (let (x1, _) := F_full b2 c2 x0 in x1) ~~
 232     (let (x1, _) := F_full a2 c2 (x >>> x0) in x1).
 233     set (F_full _ _ x) as x_full.
 234     set (F_full _ _ x0) as x0_full.
 235     set (F_full _ _ (x >>> x0)) as x_x0_full.
 236     destruct x_full.
 237     destruct x0_full.
 238     destruct x_x0_full.
 239     apply F_faithful.
 240     setoid_rewrite e1.
 241     setoid_rewrite <- (fmor_preserves_comp F).
 242     setoid_rewrite e.
 243     setoid_rewrite e0.
 244     reflexivity.
 245     Qed.
 246
 247   Instance ff_functor_section_functor : Functor (FullImage F) C1 ff_functor_section_fobj :=
 248     { fmor := fun a b f => ff_functor_section_fmor f }.
 249     abstract (intros;
 250       destruct a; destruct b; destruct s; destruct s0; destruct f; destruct f'; simpl in *;
 251       subst; simpl; set (F_full x1 x2 x3) as ff1; set (F_full x1 x2 x4) as ff2; destruct ff1; destruct ff2;
 252       apply F_faithful;
 253       etransitivity; [ apply e | idtac ];
 254       symmetry;
 255       etransitivity; [ apply e0 | idtac ];
 256       symmetry; auto).
 257     abstract (intros;
 258       simpl;
 259       destruct a as [ a1 [ a2 a3 ] ];
 260       subst;
 261       simpl;
 262       apply ff_functor_section_id_preserved).
 263     abstract (intros;
 264       destruct a as [ a1 [ a2 a3 ] ];
 265       destruct b as [ b1 [ b2 b3 ] ];
 266       destruct c as [ c1 [ c2 c3 ] ];
 267       subst;
 268       simpl in *;
 269       destruct f;
 270       destruct g;
 271       simpl in *;
 272       apply ff_functor_section_respectful).
 273       Defined.
 274
 275   Lemma ff_functor_section_splits_helper (a2 b2:C1)(f:existT (fun d : C2, {c : C1 & Fobj c = d}) (Fobj a2)
 276         (existT (fun c : C1, Fobj c = Fobj a2) a2 (eq_refl _)) ~~{
 277       FullImage F
 278       }~~> existT (fun d : C2, {c : C1 & Fobj c = d})
 279              (Fobj b2) (existT (fun c : C1, Fobj c = Fobj b2) b2 (eq_refl _)))
 280      : F \ (let (x1, _) := F_full a2 b2 (let (x1, _) := f in x1) in x1) ~~ projT1 f.
 281     destruct f.
 282     simpl.
 283     set (F_full a2 b2 x) as qq.
 284     destruct qq.
 285     apply e.
 286     Qed.
 287
 288   Lemma ff_functor_section_splits : (ff_functor_section_functor >>>> RestrictToImage F) ~~~~ functor_id _.
 289     unfold EqualFunctors.
 290     intros.
 291     simpl.
 292     destruct a as [ a1 [ a2 a3 ] ].
 293     destruct b as [ b1 [ b2 b3 ] ].
 294     subst.
 295     simpl in *.
 296     inversion f; subst.
 297     inversion f'; subst.
 298     simpl in *.
 299     apply heq_morphisms_intro.
 300     simpl.
 301     etransitivity; [ idtac | apply H ].
 302     clear H.
 303     clear f'.
 304     apply ff_functor_section_splits_helper.
 305     Qed.
 306
 307   Definition ff_functor_section_splits_niso_helper a : ((ff_functor_section_functor >>>> RestrictToImage F) a ≅ (functor_id (FullImage F)) a).
 308     intros; simpl.
 309     unfold functor_fobj.
 310     unfold ff_functor_section_fobj.
 311     unfold RestrictToImage_fobj.
 312     destruct a as [ a1 [ a2 a3 ] ].
 313     simpl.
 314     subst.
 315     unfold functor_fobj.
 316     apply iso_id.
 317     Defined.
 318
 319   Lemma ff_functor_section_splits_niso : (ff_functor_section_functor >>>> RestrictToImage F) ≃ functor_id _.
 320     intros; simpl.
 321     exists ff_functor_section_splits_niso_helper.
 322     intros.
 323     simpl in *.
 324     destruct A as [ a1 [ a2 a3 ] ].
 325     destruct B as [ b1 [ b2 b3 ] ].
 326     simpl.
 327     destruct f; subst.
 328     simpl.
 329     setoid_rewrite left_identity.
 330     setoid_rewrite right_identity.
 331     set (F_full a2 b2 x) as qr.
 332     destruct qr.
 333     symmetry; auto.
 334     Qed.
 335
 336   Lemma ffc_functor_weakly_monic : ConservativeFunctor F -> WeaklyMonic F.
 337     admit.
 338     Qed.
 339
 340   Opaque ff_functor_section_splits_niso_helper.
 341
 342 End FullFaithfulFunctor_section.