From cef6be4de10acb4593acd67c0baa254f261971a1 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Thu, 31 Mar 2011 18:28:38 -0700 Subject: [PATCH] remove unproven step1_lemma (it has a proof now) --- src/BijectionLemma.v | 71 +++++++++++++ src/ReificationsIsomorphicToGeneralizedArrows.v | 129 +++++++++-------------- 2 files changed, 123 insertions(+), 77 deletions(-) create mode 100644 src/BijectionLemma.v diff --git a/src/BijectionLemma.v b/src/BijectionLemma.v new file mode 100644 index 0000000..f63cf17 --- /dev/null +++ b/src/BijectionLemma.v @@ -0,0 +1,71 @@ +(*********************************************************************************************************************************) +(* Bijection Lemma *) +(* *) +(* Used in the proof that the mapping between the category of reifications and category of generalized arrows is in fact *) +(* a functor *) +(* *) +(*********************************************************************************************************************************) + +Generalizable All Variables. +Require Import Preamble. +Require Import General. +Require Import Categories_ch1_3. +Require Import Functors_ch1_4. +Require Import Isomorphisms_ch1_5. +Require Import ProductCategories_ch1_6_1. +Require Import OppositeCategories_ch1_6_2. +Require Import Enrichment_ch2_8. +Require Import Subcategories_ch7_1. +Require Import NaturalTransformations_ch7_4. +Require Import NaturalIsomorphisms_ch7_5. +Require Import MonoidalCategories_ch7_8. +Require Import Coherence_ch7_8. +Require Import Enrichment_ch2_8. +Require Import RepresentableStructure_ch7_2. + +Section BijectionLemma. + + (* given two categories with (for simplicity) the same objects *) + Context {Obj:Type}. + Context {CHom}{C:Category Obj CHom}. + Context {DHom}{D:Category Obj DHom}. + + (* and a functor which is (for simplicity) identity on objects *) + Context {F:Functor C D (fun x => x)}. + + (* and a mapping in the opposite direction, which respects equivalence *) + Context {M:forall x y, (x~~{D}~~>y) -> (x~~{C}~~>y)}. + Implicit Arguments M [ [x] [y] ]. + Context {M_respects:forall x y, forall (f g:x~~{D}~~>y), f~~g -> M f ~~ M g}. + + Add Parametric Morphism (x y:Obj) : (@M x y) + with signature ((@eqv D _ D x y) ==> (@eqv C _ C x y)) as parametric_morphism_fmor''. + intros; apply M_respects; auto. + Defined. + + (* + * If the functor and the mapping form a bijection, then the fact + * that the functor preserves composition forces the mapping to do so + * as well + *) + + Lemma bijection_lemma : + (forall A B, forall f:(A~~{C}~~>B), M (F \ f) ~~ f) -> + (forall A B, forall f:(A~~{D}~~>B), F \ (M f) ~~ f) -> + forall A B C, forall f:(A~~{D}~~>B), forall g:(B~~{D}~~>C), M f >>> M g ~~ M (f >>> g). + + intro lem1. + intro lem2. + intros. + rewrite <- (lem2 _ _ f). + rewrite <- (lem2 _ _ g). + + set (@fmor_preserves_comp _ _ _ _ _ _ _ F) as q. + rewrite q. + rewrite lem1. + rewrite lem1. + rewrite lem1. + reflexivity. + Qed. + +End BijectionLemma. diff --git a/src/ReificationsIsomorphicToGeneralizedArrows.v b/src/ReificationsIsomorphicToGeneralizedArrows.v index 1542b46..8edd1e0 100644 --- a/src/ReificationsIsomorphicToGeneralizedArrows.v +++ b/src/ReificationsIsomorphicToGeneralizedArrows.v @@ -30,16 +30,10 @@ Require Import GeneralizedArrowCategory. Require Import ReificationCategory. Require Import ReificationsAndGeneralizedArrows. Require Import WeakFunctorCategory. +Require Import BijectionLemma. Section ReificationsIsomorphicToGeneralizedArrows. - Lemma step1_lemma (s0 s1 s2:SmallSMMEs.SMMEs)(r01:Reification s0 s1 (me_i s1))(r12:Reification s1 s2 (me_i s2)) : - (step1_functor s0 s1 r01 >>>> - InclusionFunctor (enr_v s1) (FullImage (HomFunctor s1 (me_i s1)))) >>>> step1_functor s1 s2 r12 - ≃ step1_functor s0 s2 (compose_reifications s0 s1 s2 r01 r12). - admit. - Defined. - Definition M1 {c1 c2 : SmallSMMEs.SMMEs} : (c1 ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> c2) -> (c1 ~~{ MorphismsOfCategoryOfReifications }~~> c2). @@ -157,6 +151,44 @@ Section ReificationsIsomorphicToGeneralizedArrows. apply (garrow_from_reification s1 s2 r). Defined. + Lemma eqv1 a b (f : a ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> b) + (f' : a ~~{ MorphismsOfCategoryOfGeneralizedArrows }~~> b) + (H : generalizedArrowOrIdentityFunc a b f ≃ generalizedArrowOrIdentityFunc a b f') : + generalizedArrowOrIdentityFunc a b (M2 a b (M1 f)) ≃ generalizedArrowOrIdentityFunc a b f'. + unfold hom in *. + set (@roundtrip_garrow_to_garrow _ a _ _ b) as q. + destruct f; simpl in *. + apply H. + apply if_inv. + apply (if_comp (if_inv H)). + clear H. + unfold mf_f in q. + apply (if_respects(F0:=ga_functor g)(F1:=garrow_functor s1 s2 (reification_from_garrow s1 s2 g)) + (G0:=HomFunctor s2 (mon_i s2))(G1:=HomFunctor s2 (mon_i s2))). + apply q. + apply if_id. + Qed. + + + Lemma eqv2 a b (f : a ~~{ MorphismsOfCategoryOfReifications }~~> b) + (f' : a ~~{ MorphismsOfCategoryOfReifications }~~> b) + (H : reificationOrIdentityFunc a b f ≃ reificationOrIdentityFunc a b f') : + reificationOrIdentityFunc _ _ (M1 (M2 _ _ f)) ≃ reificationOrIdentityFunc _ _ f'. + unfold hom in *. + set (@roundtrip_reification_to_reification _ a _ _ b) as q. + destruct f; simpl. + apply H. + apply if_inv. + apply (if_comp (if_inv H)). + clear H. + simpl. + unfold mf_f; simpl. + simpl in q. + unfold mf_f in q. + simpl in q. + apply q. + Qed. + Lemma M2_respects : forall a b (f f':a~~{MorphismsOfCategoryOfReifications}~~>b), f ~~ f' -> @@ -194,89 +226,32 @@ Section ReificationsIsomorphicToGeneralizedArrows. unfold garrow_functor. unfold step2_functor. apply if_inv in H. - set (if_comp H (@step1_niso _ s1 _ _ s2 r)) as yy. - set (if_comp (if_inv (@step1_niso _ s1 _ _ s2 r0)) yy) as yy'. apply (if_comp (@roundtrip_lemma _ s1 _ _ s2 r)). apply if_inv. apply (if_comp (@roundtrip_lemma _ s1 _ _ s2 r0)). - apply yy'. + apply (if_comp (if_inv (@step1_niso _ s1 _ _ s2 r0)) (if_comp H (@step1_niso _ s1 _ _ s2 r))). Qed. Definition M2_Functor : Functor MorphismsOfCategoryOfReifications MorphismsOfCategoryOfGeneralizedArrows (fun x => x). refine {| fmor := fun a b f => M2 _ _ f |}. apply M2_respects. intros; simpl; apply if_id. - intros. - simpl. - destruct f; simpl. - apply if_id. - destruct g; simpl. - apply if_id. - unfold mf_f; simpl. - apply (if_respects - (F0:=((garrow_functor s1 s0 r >>>> HomFunctor s0 (mon_i s0)) >>>> garrow_functor s0 s2 r0)) - (F1:=(garrow_functor s1 s2 (compose_reifications s1 s0 s2 r r0))) - (G0:=(HomFunctor s2 (mon_i s2))) - (G1:=(HomFunctor s2 (mon_i s2)))); - [ idtac | apply if_id ]. - eapply if_comp. - idtac. - apply (if_associativity (garrow_functor s1 s0 r) (HomFunctor s0 (mon_i s0)) (garrow_functor s0 s2 r0)). - idtac. - unfold garrow_functor at 1. - unfold step2_functor at 1. - set (roundtrip_lemma' - (HomFunctor (enr_c (smme_e s0)) (me_i (smme_mon s0))) - (ffme_mf_full (smme_mee s0)) (ffme_mf_faithful (smme_mee s0)) - (step1_functor (smme_see s1) (smme_mee s0) r) - ) as q. - set (if_respects - (G0:=garrow_functor (smme_see s0) (smme_mee s2) r0) - (G1:=garrow_functor (smme_see s0) (smme_mee s2) r0) - q (if_id _)) as q'. - apply (if_comp q'). - clear q' q. - unfold garrow_functor at 2. - unfold garrow_functor at 1. - eapply if_comp. - eapply if_inv. - apply (if_associativity _ (step1_functor s0 s2 r0) (step2_functor s2)). - apply (if_respects - (G0:=step2_functor s2) - (G1:=step2_functor s2)); [ idtac | apply if_id ]. - apply step1_lemma. - Defined. + intros; apply (@bijection_lemma _ _ _ _ _ M1_Functor M2); intros. + apply M2_respects; auto. + unfold fmor; simpl. + apply (@eqv1 _ _ f0 f0). + apply if_id. + unfold fmor; simpl. + apply (@eqv2 _ _ f0 f0). + apply if_id. + Defined. Theorem ReificationsAreGArrows : IsomorphicCategories CategoryOfGeneralizedArrows CategoryOfReifications. refine {| ic_f := M1_Functor ; ic_g := M2_Functor |}. unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *. - unfold hom in *. - set (@roundtrip_garrow_to_garrow _ a _ _ b) as q. - destruct f; simpl in *. - apply H. - apply if_inv. - apply (if_comp (if_inv H)). - clear H. - unfold mf_f in q. - apply (if_respects(F0:=ga_functor g)(F1:=garrow_functor s1 s2 (reification_from_garrow s1 s2 g)) - (G0:=HomFunctor s2 (mon_i s2))(G1:=HomFunctor s2 (mon_i s2))). - apply q. - apply if_id. - + apply (eqv1 _ _ f f'); auto. unfold EqualFunctors; intros; apply heq_morphisms_intro; unfold eqv in *; simpl in *. - unfold hom in *. - set (@roundtrip_reification_to_reification _ a _ _ b) as q. - destruct f; simpl. - apply H. - apply if_inv. - apply (if_comp (if_inv H)). - clear H. - simpl. - unfold mf_f; simpl. - simpl in q. - unfold mf_f in q. - simpl in q. - apply q. - Qed. + apply (eqv2 _ _ f f'); auto. + Qed. End ReificationsIsomorphicToGeneralizedArrows. -- 1.7.10.4