add FullSubcategoryInclusionFunctor

[coq-categories.git] / src / Subcategories_ch7_1.v

diff --git a/src/Subcategories_ch7_1.v b/src/Subcategories_ch7_1.v
index 2a88a7a..25391a1 100644 (file)
--- a/src/Subcategories_ch7_1.v
+++ b/src/Subcategories_ch7_1.v
@@ -3,7 +3,7 @@
 (****************************************************************************)
 
 Generalizable All Variables.
 (****************************************************************************)
 
 Generalizable All Variables.

-Require Import Preamble.
+Require Import Notations.

 Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.
 Require Import Isomorphisms_ch1_5.
 Require Import Categories_ch1_3.
 Require Import Functors_ch1_4.
 Require Import Isomorphisms_ch1_5.

@@ -37,23 +37,22 @@ Instance FullSubCategoriesAreCategories `(fsc:@FullSubcategory Ob Hom C Pobj)
   Defined.
 Coercion FullSubCategoriesAreCategories : FullSubcategory >-> Category.
 
   Defined.
 Coercion FullSubCategoriesAreCategories : FullSubcategory >-> Category.
 

-(* every category is a subcategory of itself! *)
+(* 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.
 (*
 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 *)
 (* the inclusion operation from a subcategory to its host is a functor *)

-Instance InclusionFunctor `(C:Category Ob Hom)`(SP:@SubCategory _ _ C Pobj Pmor)
+Instance FullSubcategoryInclusionFunctor `(SP:@FullSubcategory Ob Hom C Pobj)

   : Functor SP C (fun x => projT1 x) :=
   : Functor SP C (fun x => projT1 x) :=

-  { fmor := fun dom ran f => projT1 f }.
+  { fmor := fun dom ran f => f }.

   intros. unfold eqv in H. simpl in H. auto.
   intros. simpl. reflexivity.
   intros. simpl. reflexivity.
   Defined.
   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 :=
 
 (* 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 :=

@@ -68,7 +67,6 @@ Instance WideSubCategoriesAreCategories `{C:Category(Ob:=Ob)}{Pmor}(wsc:WideSubc
   ; 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))
   ; 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.
   }.
   intros; apply Build_Equivalence. unfold Reflexive.
      intros; reflexivity.

@@ -121,8 +119,37 @@ Section FullImage.
     auto.
     Defined.
 
     auto.
     Defined.
 

+  Lemma RestrictToImage_splits_niso : F ≃ (RestrictToImage >>>> FullImage_InclusionFunctor).
+    unfold IsomorphicFunctors.
+    exists (fun A => iso_id (fobj A)).
+    intros.
+    simpl.
+    setoid_rewrite left_identity.
+    setoid_rewrite right_identity.
+    reflexivity.
+    Qed.
+

 End FullImage.
 
 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 :=
 (*
 Instance func_opSubcat `(c1:Category)`(c2:Category)`(SP:@SubCategory _ _ c2 Pobj Pmor)
   {fobj}(F:Functor c1⁽ºᑭ⁾ SP fobj) : Functor c1 SP⁽ºᑭ⁾ fobj :=

@@ -211,6 +238,8 @@ 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 *)
   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
 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

@@ -229,7 +258,6 @@ Definition WeaklyMonic
     G >>>> F ≃ H >>>> F
     -> G ≃ H.
 
     G >>>> F ≃ H >>>> F
     -> G ≃ H.
 

-(*

 Section FullFaithfulFunctor_section.
   Context `(F:Functor(c1:=C1)(c2:=C2)(fobj:=Fobj)).
   Context  (F_full:FullFunctor F).
 Section FullFaithfulFunctor_section.
   Context `(F:Functor(c1:=C1)(c2:=C2)(fobj:=Fobj)).
   Context  (F_full:FullFunctor F).

@@ -245,23 +273,10 @@ Section FullFaithfulFunctor_section.
     auto.
     Qed.
 
     auto.
     Qed.
 

-  Definition ff_functor_section_fobj (a:FullImage F) : C1 := projT1 (projT2 a).
-
-  Definition ff_functor_section_fmor {a b:FullImage F} (f:a~~{FullImage F}~~>b)
-    : (ff_functor_section_fobj a)~~{C1}~~>(ff_functor_section_fobj b).
-    destruct a as [ a1 [ a2 a3 ] ].
-    destruct b as [ b1 [ b2 b3 ] ].
+  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'.
     set (@ff_invert _ _ _ _ _ _ _ _ F_full _ _ f) as f'.

-    destruct a as [ a1 [ a2 a3 ] ].
-    subst.
-    unfold ff_functor_section_fobj.
-    simpl.
-    destruct b as [ b1 [ b2 b3 ] ].
-    subst.
-    unfold ff_functor_section_fobj.
-    simpl.
-    apply (@ff_invert _ _ _ _ _ _ _ _ F_full).
-    apply f.
+    destruct f'.
+    apply x.

     Defined.
 
   Lemma ff_functor_section_respectful {a2 b2 c2 : C1}
     Defined.
 
   Lemma ff_functor_section_respectful {a2 b2 c2 : C1}

@@ -284,32 +299,22 @@ Section FullFaithfulFunctor_section.
     reflexivity.
     Qed.
 
     reflexivity.
     Qed.
 

-  Instance ff_functor_section_functor : Functor (FullImage F) C1 ff_functor_section_fobj :=
+  Instance ff_functor_section_functor : Functor (FullImage F) C1 (fun x => x) :=

     { fmor := fun a b f => ff_functor_section_fmor f }.
     { fmor := fun a b f => ff_functor_section_fmor f }.

-    abstract (intros;
-      destruct a; destruct b; destruct s; destruct s0; simpl in *;
-      subst; simpl; set (F_full x1 x2 f) as ff1; set (F_full x1 x2 f') as ff2; destruct ff1; destruct ff2;
-      apply F_faithful;
-      etransitivity; [ apply e | idtac ];
-      symmetry;
-      etransitivity; [ apply e0 | idtac ];
-      symmetry; auto).
-    abstract (intros;
-      simpl;
-      destruct a as [ a1 [ a2 a3 ] ];
-      subst;
-      simpl;
-      apply ff_functor_section_id_preserved).
-    abstract (intros;
-      destruct a as [ a1 [ a2 a3 ] ];
-      destruct b as [ b1 [ b2 b3 ] ];
-      destruct c as [ c1 [ c2 c3 ] ];
-      subst;
-      simpl in *;
-      simpl in *;
-      apply ff_functor_section_respectful).
+    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.
       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
   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

@@ -321,74 +326,40 @@ Section FullFaithfulFunctor_section.
     destruct qq.
     apply e.
     Qed.
     destruct qq.
     apply e.
     Qed.

-
+*)

   Lemma ff_functor_section_splits : (ff_functor_section_functor >>>> RestrictToImage F) ~~~~ functor_id _.
   Lemma ff_functor_section_splits : (ff_functor_section_functor >>>> RestrictToImage F) ~~~~ functor_id _.

-    unfold EqualFunctors.
-    intros.
-    simpl.
-    destruct a as [ a1 [ a2 a3 ] ].
-    destruct b as [ b1 [ b2 b3 ] ].
-    subst.
-    simpl in *.
-    simpl in *.
-    apply heq_morphisms_intro.
-    simpl.
-    unfold RestrictToImage_fmor; simpl.
-    etransitivity; [ idtac | apply H ].
-    clear H.
-    clear f'.
-    apply ff_functor_section_splits_helper.
+    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.
 
     Qed.
 

-  Definition ff_functor_section_splits_niso_helper a : ((ff_functor_section_functor >>>> RestrictToImage F) a ≅ (functor_id (FullImage F)) a).
-    intros; simpl.
-    unfold functor_fobj.
-    unfold ff_functor_section_fobj.
-    unfold RestrictToImage_fobj.
-    destruct a as [ a1 [ a2 a3 ] ].
-    simpl.
-    subst.
-    unfold functor_fobj.
-    apply iso_id.
-    Defined.
-

   Lemma ff_functor_section_splits_niso : (ff_functor_section_functor >>>> RestrictToImage F) ≃ functor_id _.
     intros; simpl.
   Lemma ff_functor_section_splits_niso : (ff_functor_section_functor >>>> RestrictToImage F) ≃ functor_id _.
     intros; simpl.

-    exists ff_functor_section_splits_niso_helper.
-    intros.
-    simpl in *.
-    destruct A as [ a1 [ a2 a3 ] ].
-    destruct B as [ b1 [ b2 b3 ] ].
-    simpl.
-    unfold RestrictToImage_fmor; simpl.
+    exists iso_id; intros.
+    symmetry.
+    unfold functor_comp; simpl.

     setoid_rewrite left_identity.
     setoid_rewrite right_identity.
     setoid_rewrite left_identity.
     setoid_rewrite right_identity.

-    set (F_full a2 b2 x) as qr.
-    destruct qr.
-    symmetry; auto.
+    unfold ff_functor_section_fmor.
+    destruct (F_full A B f).
+    auto.

     Qed.
 
     Qed.
 

-  Definition ff_functor_section_splits_niso_helper' a
-    : ((RestrictToImage F >>>> ff_functor_section_functor) a ≅ (functor_id _) a).
-    intros; simpl.
-    unfold functor_fobj.
-    unfold ff_functor_section_fobj.
-    unfold RestrictToImage_fobj.
-    simpl.
-    apply iso_id.
-    Defined.
-

   Lemma ff_functor_section_splits_niso' : (RestrictToImage F >>>> ff_functor_section_functor) ≃ functor_id _.
     intros; simpl.
   Lemma ff_functor_section_splits_niso' : (RestrictToImage F >>>> ff_functor_section_functor) ≃ functor_id _.
     intros; simpl.

-    exists ff_functor_section_splits_niso_helper'.
-    intros.
-    simpl in *.
+    exists iso_id; intros.
+    symmetry.
+    unfold functor_comp; simpl.

     setoid_rewrite left_identity.
     setoid_rewrite right_identity.
     setoid_rewrite left_identity.
     setoid_rewrite right_identity.

-    set (F_full _ _ (F \ f)) as qr.
-    destruct qr.
-    apply F_faithful in e.
-    symmetry.
+    unfold ff_functor_section_fmor.
+    destruct (F_full A B (F \ f)).
+    apply F_faithful.

     auto.
     Qed.
 
     auto.
     Qed.
 

@@ -425,13 +396,13 @@ Section FullFaithfulFunctor_section.
     apply if_right_identity.
     eapply if_inv.
     apply (if_comp(F2:=G>>>>(RestrictToImage F >>>> ff_functor_section_functor))).
     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_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_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_respects H0 H0 (functor_id C1) (RestrictToImage F >>>> ff_functor_section_functor)).

     apply if_id.
     apply if_inv.
     apply ff_functor_section_splits_niso'.
     apply if_id.
     apply if_inv.
     apply ff_functor_section_splits_niso'.

@@ -439,7 +410,7 @@ Section FullFaithfulFunctor_section.
       ((H0 >>>> (RestrictToImage F >>>> ff_functor_section_functor))
         ≃ ((H0 >>>> RestrictToImage F) >>>> ff_functor_section_functor)).
     apply if_inv.
       ((H0 >>>> (RestrictToImage F >>>> ff_functor_section_functor))
         ≃ ((H0 >>>> RestrictToImage F) >>>> ff_functor_section_functor)).
     apply if_inv.

-    apply if_associativity.
+    apply (if_associativity H0 (RestrictToImage F) ff_functor_section_functor).

     apply (if_comp H2).
     clear H2.
     apply if_inv.
     apply (if_comp H2).
     clear H2.
     apply if_inv.

@@ -447,16 +418,20 @@ Section FullFaithfulFunctor_section.
       ((G >>>> (RestrictToImage F >>>> ff_functor_section_functor))
         ≃ ((G >>>> RestrictToImage F) >>>> ff_functor_section_functor)).
     apply if_inv.
       ((G >>>> (RestrictToImage F >>>> ff_functor_section_functor))
         ≃ ((G >>>> RestrictToImage F) >>>> ff_functor_section_functor)).
     apply if_inv.

-    apply if_associativity.
+    apply (if_associativity G (RestrictToImage F) ff_functor_section_functor).

     apply (if_comp H2).
     clear H2.
     apply (if_comp H2).
     clear H2.

-    apply if_respects.
+    apply (if_respects (G >>>> RestrictToImage F) (H0 >>>> RestrictToImage F)
+      ff_functor_section_functor ff_functor_section_functor).

     apply if_fullimage.
     apply H1.
     apply if_fullimage.
     apply H1.

-    apply if_id.
+    simpl.
+    exists (ni_id _).
+    intros.
+    simpl.
+    setoid_rewrite left_identity.
+    setoid_rewrite right_identity.
+    reflexivity.

     Qed.
 
     Qed.
 

-  Opaque ff_functor_section_splits_niso_helper.
-

 End FullFaithfulFunctor_section.
 End FullFaithfulFunctor_section.

-*)
\ No newline at end of file