X-Git-Url: http://git.megacz.com/?p=coq-categories.git;a=blobdiff_plain;f=src%2FSubcategories_ch7_1.v;h=25391a12eda6a431ed4bac1e99f4d432314bc903;hp=2a88a7a452921e458ee6ba76ed4bf5d485ac0836;hb=20641452e40570b4bfc9429ca57b0cffca6eccfb;hpb=e928451c4c45cdbdd975bbfb229e8cc2616b8194

diff --git a/src/Subcategories_ch7_1.v b/src/Subcategories_ch7_1.v
index 2a88a7a..25391a1 100644
--- a/src/Subcategories_ch7_1.v
+++ b/src/Subcategories_ch7_1.v
@@ -3,7 +3,7 @@
 (****************************************************************************)
 
 Generalizable All Variables.
-Require Import Preamble.
+Require Import Notations.
 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.
 
-(* 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.
+*)
 (* 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) :=
-  { 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.
-*)
-
 
 (* 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))
-
   }.
   intros; apply Build_Equivalence. unfold Reflexive.
      intros; reflexivity.
@@ -121,8 +119,37 @@ Section FullImage.
     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.
 
+(* 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 :=
@@ -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 *)
+(* 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
@@ -229,7 +258,6 @@ Definition WeaklyMonic
     G >>>> F ≃ H >>>> F
     -> G ≃ H.
 
-(*
 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.
 
-  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'.
-    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}
@@ -284,32 +299,22 @@ Section FullFaithfulFunctor_section.
     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 }.
-    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.
-
+(*
   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.
-
+*)
   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.
 
-  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.
-    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.
-    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.
 
-  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.
-    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.
-    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.
 
@@ -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_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_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'.
@@ -439,7 +410,7 @@ Section FullFaithfulFunctor_section.
       ((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.
@@ -447,16 +418,20 @@ Section FullFaithfulFunctor_section.
       ((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_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_id.
+    simpl.
+    exists (ni_id _).
+    intros.
+    simpl.
+    setoid_rewrite left_identity.
+    setoid_rewrite right_identity.
+    reflexivity.
     Qed.
 
-  Opaque ff_functor_section_splits_niso_helper.
-
 End FullFaithfulFunctor_section.
-*)
\ No newline at end of file