X-Git-Url: http://git.megacz.com/?p=coq-categories.git;a=blobdiff_plain;f=src%2FPreMonoidalCategories.v;h=07513d82c20a6bedb676fdc99b2ce82301164e77;hp=d0b7cd2926dd63ed188d8891713472ca62d39190;hb=5f3bdb7947de02d8d60f1af77c999a3c80f7dbba;hpb=1dd1bee2b13b43812ebbc078bdbf774886392886 diff --git a/src/PreMonoidalCategories.v b/src/PreMonoidalCategories.v index d0b7cd2..07513d8 100644 --- a/src/PreMonoidalCategories.v +++ b/src/PreMonoidalCategories.v @@ -19,8 +19,8 @@ Class PreMonoidalCat `(bc:BinoidalCat(C:=C))(I:C) := ; pmon_assoc : forall a b, (bin_second a >>>> bin_first b) <~~~> (bin_first b >>>> bin_second a) ; pmon_cancelr : (bin_first I) <~~~> functor_id C ; pmon_cancell : (bin_second I) <~~~> functor_id C -; pmon_pentagon : Pentagon (fun a b c f => f ⋉ c) (fun a b c f => c ⋊ f) (fun a b c => #((pmon_assoc a c) b)⁻¹) -; pmon_triangle : Triangle (fun a b c f => f ⋉ c) (fun a b c f => c ⋊ f) (fun a b c => #((pmon_assoc a c) b)⁻¹) +; pmon_pentagon : Pentagon (fun a b c f => f ⋉ c) (fun a b c f => c ⋊ f) (fun a b c => #((pmon_assoc a c) b)) +; pmon_triangle : Triangle (fun a b c f => f ⋉ c) (fun a b c f => c ⋊ f) (fun a b c => #((pmon_assoc a c) b)) (fun a => #(pmon_cancell a)) (fun a => #(pmon_cancelr a)) ; pmon_assoc_rr : forall a b, (bin_first (a⊗b)) <~~~> (bin_first a >>>> bin_first b) ; pmon_assoc_ll : forall a b, (bin_second (a⊗b)) <~~~> (bin_second b >>>> bin_second a) @@ -54,31 +54,31 @@ Implicit Arguments pmon_assoc [ Ob Hom C bin_obj' bc I PreMonoidalCat ]. Coercion pmon_bin : PreMonoidalCat >-> BinoidalCat. (* this turns out to be Exercise VII.1.1 from Mac Lane's CWM *) -Lemma MacLane_ex_VII_1_1 `{mn:PreMonoidalCat(I:=EI)} d c +Lemma MacLane_ex_VII_1_1 `{mn:PreMonoidalCat(I:=EI)} b a : - let α := fun a b c => #((pmon_assoc a c) b)⁻¹ - in α EI c d >>> #(pmon_cancell _) ⋉ _ ~~ #(pmon_cancell _). + let α := fun a b c => #((pmon_assoc a c) b) + in α a b EI >>> _ ⋊ #(pmon_cancelr _) ~~ #(pmon_cancelr _). intros. simpl in α. (* following Mac Lane's hint, we aim for (λ >>> α >>> λ×1)~~(λ >>> λ) *) - set (epic _ (iso_epic (pmon_cancell (EI⊗(c⊗d))))) as q. + set (epic _ (iso_epic (pmon_cancelr ((a⊗b)⊗EI)))) as q. apply q. clear q. (* next, we show that the hint goal above is implied by the bottom-left 1/5th of the big whiteboard diagram *) - set (ni_commutes pmon_cancell (α EI c d)) as q. + set (ni_commutes pmon_cancelr (α a b EI)) as q. setoid_rewrite <- associativity. setoid_rewrite q. clear q. setoid_rewrite associativity. - set (ni_commutes pmon_cancell (#(pmon_cancell c) ⋉ d)) as q. + set (ni_commutes pmon_cancelr (a ⋊ #(pmon_cancelr b))) as q. simpl in q. setoid_rewrite q. clear q. - set (ni_commutes pmon_cancell (#(pmon_cancell (c⊗d)))) as q. + set (ni_commutes pmon_cancelr (#(pmon_cancelr (a⊗b)))) as q. simpl in q. setoid_rewrite q. clear q. @@ -89,68 +89,59 @@ Lemma MacLane_ex_VII_1_1 `{mn:PreMonoidalCat(I:=EI)} d c (* now we carry out the proof in the whiteboard diagram, starting from the pentagon diagram *) (* top 2/5ths *) - assert (α EI EI (c⊗d) >>> α _ _ _ >>> (#(pmon_cancelr _) ⋉ _ ⋉ _) ~~ _ ⋊ #(pmon_cancell _) >>> α _ _ _). - set (pmon_triangle EI (c⊗d)) as tria. + assert (α (a⊗b) EI EI >>> α _ _ _ >>> (_ ⋊ (_ ⋊ #(pmon_cancell _))) ~~ #(pmon_cancelr _) ⋉ _ >>> α _ _ _). + set (pmon_triangle (a⊗b) EI) as tria. simpl in tria. - setoid_rewrite <- tria. - clear tria. unfold α; simpl. - set (ni_commutes (pmon_assoc_rr c d) #(pmon_cancelr EI)) as x. - simpl in x. - setoid_rewrite pmon_coherent_r in x. - simpl in x. + setoid_rewrite tria. + clear tria. setoid_rewrite associativity. - setoid_rewrite x. - clear x. - reflexivity. + apply comp_respects; try reflexivity. + set (ni_commutes (pmon_assoc_ll a b) #(pmon_cancell EI)) as x. + simpl in x. + setoid_rewrite pmon_coherent_l in x. + apply x. (* bottom 3/5ths *) - assert (_ ⋊ α _ _ _ >>> α EI (EI⊗c) d >>> α _ _ _ ⋉ _ >>> (#(pmon_cancelr _) ⋉ _ ⋉ _) ~~ - _ ⋊ α _ _ _ >>> _ ⋊ (#(pmon_cancell _) ⋉ _) >>> α _ _ _ ). + assert (((#((pmon_assoc a EI) b) ⋉ EI >>> #((pmon_assoc a EI) (b ⊗ EI))) >>> + a ⋊ #((pmon_assoc b EI) EI)) >>> a ⋊ (b ⋊ #(pmon_cancell EI)) + ~~ α _ _ _ ⋉ _ >>> (_ ⋊ #(pmon_cancelr _)) ⋉ _ >>> α _ _ _). + unfold α; simpl. repeat setoid_rewrite associativity. apply comp_respects; try reflexivity. - set (ni_commutes (pmon_assoc EI d) (#(pmon_cancell c) )) as x. + set (ni_commutes (pmon_assoc a EI) (#(pmon_cancelr b) )) as x. simpl in x. setoid_rewrite <- associativity. - apply iso_shift_right' in x. - symmetry in x. - setoid_rewrite <- associativity in x. - apply iso_shift_left' in x. simpl in x. setoid_rewrite <- x. clear x. setoid_rewrite associativity. apply comp_respects; try reflexivity. - setoid_rewrite (fmor_preserves_comp (-⋉d)). - apply (fmor_respects (-⋉d)). + setoid_rewrite (fmor_preserves_comp (a⋊-)). + apply (fmor_respects (a⋊-)). - set (pmon_triangle EI c) as tria. + set (pmon_triangle b EI) as tria. simpl in tria. + symmetry. apply tria. - set (pmon_pentagon EI EI c d) as penta. unfold pmon_pentagon in penta. simpl in penta. + set (pmon_pentagon a b EI EI) as penta. unfold pmon_pentagon in penta. simpl in penta. - set (@comp_respects _ _ _ _ _ _ _ _ penta (#(pmon_cancelr EI) ⋉ c ⋉ d) (#(pmon_cancelr EI) ⋉ c ⋉ d)) as qq. + set (@comp_respects _ _ _ _ _ _ _ _ penta (a ⋊ (b ⋊ #(pmon_cancell EI))) (a ⋊ (b ⋊ #(pmon_cancell EI)))) as qq. unfold α in H. setoid_rewrite H in qq. unfold α in H0. setoid_rewrite H0 in qq. clear H0 H. - assert (EI⋊(iso_backward ((pmon_assoc EI d) c) >>> #(pmon_cancell c) ⋉ d) ~~ EI⋊ #(pmon_cancell (c ⊗ d)) ). - apply (@monic _ _ _ _ _ _ (iso_monic (iso_inv _ _ ((pmon_assoc EI d) c)))). - - symmetry. - setoid_rewrite <- fmor_preserves_comp. - apply qq; try reflexivity. + unfold α. + apply (monic _ (iso_monic ((pmon_assoc a EI) b))). + apply qq. clear qq penta. - - setoid_rewrite fmor_preserves_comp. - apply H. - + reflexivity. Qed. Class PreMonoidalFunctor @@ -165,8 +156,8 @@ Class PreMonoidalFunctor ; mf_center : forall `(f:a~>b), CentralMorphism f -> CentralMorphism (mf_F \ f) ; mf_cancell : ∀ b, #(pmon_cancell _) ~~ #mf_i ⋉ _ >>> #(mf_first b I1) >>> mf_F \ #(pmon_cancell b) ; mf_cancelr : ∀ a, #(pmon_cancelr _) ~~ _ ⋊ #mf_i >>> #(mf_second a I1) >>> mf_F \ #(pmon_cancelr a) -; mf_assoc : ∀ a b c, #(pmon_assoc _ _ _) >>> _ ⋊ #(mf_second _ _) >>> #(mf_second _ _) ~~ - #(mf_second _ _) ⋉ _ >>> #(mf_second _ _) >>> mf_F \ #(pmon_assoc a c b) +; mf_assoc : ∀ a b c, #(pmon_assoc _ _ _) >>> _ ⋊ #(mf_first _ _) >>> #(mf_second _ _) ~~ + #(mf_second _ _) ⋉ _ >>> #(mf_first _ _) >>> mf_F \ #(pmon_assoc a c b) }. Coercion mf_F : PreMonoidalFunctor >-> Functor. @@ -197,8 +188,7 @@ Section PreMonoidalFunctorsCompose. eapply ni_comp. apply (ni_associativity PMF12 PMF23 (- ⋉fobj23 (fobj12 a))). eapply ni_comp. - apply (ni_respects PMF12 PMF12 (PMF23 >>>> - ⋉fobj23 (fobj12 a)) (- ⋉fobj12 a >>>> PMF23)). - apply ni_id. + apply (ni_respects1 PMF12 (PMF23 >>>> - ⋉fobj23 (fobj12 a)) (- ⋉fobj12 a >>>> PMF23)). apply mf_first23. clear mf_first23. @@ -211,7 +201,7 @@ Section PreMonoidalFunctorsCompose. eapply ni_inv. eapply (ni_associativity _ PMF12 PMF23). - apply ni_respects; [ idtac | apply ni_id ]. + apply ni_respects2. apply ni_inv. apply mf_first12. Defined. @@ -224,8 +214,7 @@ Section PreMonoidalFunctorsCompose. eapply ni_comp. apply (ni_associativity PMF12 PMF23 (fobj23 (fobj12 a) ⋊-)). eapply ni_comp. - apply (ni_respects PMF12 PMF12 (PMF23 >>>> fobj23 (fobj12 a) ⋊-) (fobj12 a ⋊- >>>> PMF23)). - apply ni_id. + apply (ni_respects1 PMF12 (PMF23 >>>> fobj23 (fobj12 a) ⋊-) (fobj12 a ⋊- >>>> PMF23)). apply mf_second23. clear mf_second23. @@ -238,124 +227,129 @@ Section PreMonoidalFunctorsCompose. eapply ni_inv. eapply (ni_associativity (a ⋊-) PMF12 PMF23). - apply ni_respects; [ idtac | apply ni_id ]. + apply ni_respects2. apply ni_inv. apply mf_second12. Defined. - Lemma compose_assoc_coherence a b c : - (#((pmon_assoc (compose_mf a) (fobj23 (fobj12 c))) (compose_mf b)) >>> - compose_mf a ⋊ #((compose_mf_second b) c)) >>> + (* this proof is really gross; I will write a better one some other day *) + Lemma mf_associativity_comp : + ∀a b c : C1, + (#((pmon_assoc (compose_mf a) (compose_mf c)) (fobj23 (fobj12 b))) >>> + compose_mf a ⋊ #((compose_mf_first c) b)) >>> #((compose_mf_second a) (b ⊗ c)) ~~ - (#((compose_mf_second a) b) ⋉ fobj23 (fobj12 c) >>> - #((compose_mf_second (a ⊗ b)) c)) >>> compose_mf \ #((pmon_assoc a c) b). -(* - set (mf_assoc a b c) as x. - set (mf_assoc (fobj12 a) (fobj12 b) (fobj12 c)) as x'. - unfold functor_fobj in *. - simpl in *. - etransitivity. - etransitivity. - etransitivity. - Focus 3. - apply x'. - - apply iso_shift_left' in x'. - + (#((compose_mf_second a) b) ⋉ compose_mf c >>> + #((compose_mf_first c) (a ⊗ b))) >>> compose_mf \ #((pmon_assoc a c) b). + intros; intros. unfold compose_mf_second; simpl. + unfold compose_mf_first; simpl. + unfold functor_comp; simpl. + unfold ni_respects1. unfold functor_fobj; simpl. - set (mf_second (fobj12 b)) as m. - assert (mf_second (fobj12 b)=m). reflexivity. - destruct m; simpl. - setoid_rewrite <- fmor_preserves_comp. - setoid_rewrite <- fmor_preserves_comp. - setoid_rewrite <- fmor_preserves_comp. - setoid_rewrite <- fmor_preserves_comp. - setoid_rewrite <- fmor_preserves_comp. - setoid_rewrite fmor_preserves_id. - setoid_rewrite fmor_preserves_id. - setoid_rewrite fmor_preserves_id. - setoid_rewrite right_identity. - setoid_rewrite left_identity. - setoid_rewrite left_identity. - setoid_rewrite left_identity. - - set (mf_second (fobj12 (a ⊗ b))) as m''. - assert (mf_second (fobj12 (a ⊗ b))=m''). reflexivity. - destruct m''; simpl. - unfold functor_fobj; simpl. - setoid_rewrite fmor_preserves_id. - setoid_rewrite fmor_preserves_id. - setoid_rewrite right_identity. - setoid_rewrite left_identity. - setoid_rewrite left_identity. - setoid_rewrite left_identity. - - set (mf_second (fobj12 a)) as m'. - assert (mf_second (fobj12 a)=m'). reflexivity. + + set (mf_first (fobj12 c)) as m'. + assert (mf_first (fobj12 c)=m'). reflexivity. destruct m'; simpl. - setoid_rewrite <- fmor_preserves_comp. - setoid_rewrite <- fmor_preserves_comp. - setoid_rewrite <- fmor_preserves_comp. - setoid_rewrite <- fmor_preserves_comp. - setoid_rewrite <- fmor_preserves_comp. - setoid_rewrite left_identity. - setoid_rewrite left_identity. - setoid_rewrite left_identity. - setoid_rewrite right_identity. - assert (fobj23 (fobj12 a) ⋊ PMF23 \ id (PMF12 (b ⊗ c)) ~~ id _). - (* *) - setoid_rewrite H2. - setoid_rewrite left_identity. - assert ((id (fobj23 (fobj12 a) ⊗ fobj23 (fobj12 b)) ⋉ fobj23 (fobj12 c)) ~~ id _). - (* *) - setoid_rewrite H3. - setoid_rewrite left_identity. - assert (id (fobj23 (fobj12 a ⊗ fobj12 b)) ⋉ fobj23 (fobj12 c) ~~ id _). - (* *) - setoid_rewrite H4. - setoid_rewrite left_identity. - clear H4. - setoid_rewrite left_identity. - assert (id (fobj23 (fobj12 (a ⊗ b))) ⋉ fobj23 (fobj12 c) ~~ id _). - (* *) - setoid_rewrite H4. - setoid_rewrite right_identity. - clear H4. - assert ((fobj23 (fobj12 a) ⋊ PMF23 \ id (PMF12 b)) ⋉ fobj23 (fobj12 c) ~~ id _). - (* *) - setoid_rewrite H4. - setoid_rewrite left_identity. - clear H4. - unfold functor_comp in ni_commutes0; simpl in ni_commutes0. - unfold functor_comp in ni_commutes; simpl in ni_commutes. - unfold functor_comp in ni_commutes1; simpl in ni_commutes1. + set (mf_second (fobj12 a)) as m. + assert (mf_second (fobj12 a)=m). reflexivity. + destruct m; simpl. - unfold functor_fobj in *. - simpl in *. - setoid_rewrite x in x'. - rewrite H1. - set (ni_commutes0 (a ) - setoid_rewrite fmor_preserves_id. + Implicit Arguments id [[Ob][Hom][Category][a]]. + idtac. + + symmetry. etransitivity. - eapply comp_respects. + repeat setoid_rewrite <- fmor_preserves_comp. + repeat setoid_rewrite fmor_preserves_id. + repeat setoid_rewrite left_identity. + repeat setoid_rewrite right_identity. + reflexivity. + symmetry. + etransitivity. + repeat setoid_rewrite <- fmor_preserves_comp. + repeat setoid_rewrite fmor_preserves_id. + repeat setoid_rewrite left_identity. + repeat setoid_rewrite right_identity. reflexivity. - eapply comp_respects. - eapply comp_respects. - apply - Focus 2. - eapply fmor_preserves_id. - setoid_rewrite (fmor_preserves_id PMF23). -*) - admit. - Qed. + assert ( (#((pmon_assoc (fobj23 (fobj12 a)) (fobj23 (fobj12 c))) + (fobj23 (fobj12 b))) >>> + fobj23 (fobj12 a) + ⋊ ( + (#(ni_iso (fobj12 b)) >>> ( (PMF23 \ #((mf_first c) b) ))))) >>> + ( + (#(ni_iso0 (fobj12 (b ⊗ c))) >>> + ((PMF23 \ #((mf_second a) (b ⊗ c)))))) ~~ + (( + (#(ni_iso0 (fobj12 b)) >>> ( (PMF23 \ #((mf_second a) b) )))) + ⋉ fobj23 (fobj12 c) >>> + ( + (#(ni_iso (fobj12 (a ⊗ b))) >>> + ( (PMF23 \ #((mf_first c) (a ⊗ b))))))) >>> + PMF23 \ (PMF12 \ #((pmon_assoc a c) b)) + ). + + repeat setoid_rewrite associativity. + setoid_rewrite (fmor_preserves_comp PMF23). + unfold functor_comp in *. + unfold functor_fobj in *. + simpl in *. + rename ni_commutes into ni_commutes7. + set (mf_assoc(PreMonoidalFunctor:=PMF12)) as q. + set (ni_commutes7 _ _ (#((mf_second a) b))) as q'. + simpl in q'. + repeat setoid_rewrite associativity. + symmetry. + setoid_rewrite <- (fmor_preserves_comp (-⋉ fobj23 (fobj12 c))). + repeat setoid_rewrite <- associativity. + setoid_rewrite juggle1. + setoid_rewrite <- q'. + repeat setoid_rewrite associativity. + setoid_rewrite fmor_preserves_comp. + idtac. + unfold functor_fobj in *. + simpl in *. + repeat setoid_rewrite <- associativity. + setoid_rewrite <- q. + clear q. + repeat setoid_rewrite <- fmor_preserves_comp. + repeat setoid_rewrite <- associativity. + apply comp_respects; try reflexivity. + + set (mf_assoc(PreMonoidalFunctor:=PMF23) (fobj12 a) (fobj12 b) (fobj12 c)) as q. + unfold functor_fobj in *. + simpl in *. + + rewrite H in q. + rewrite H0 in q. + simpl in q. + repeat setoid_rewrite <- associativity. + repeat setoid_rewrite <- associativity in q. + setoid_rewrite <- q. + clear q. + unfold functor_fobj; simpl. + + repeat setoid_rewrite associativity. + apply comp_respects; try reflexivity. + apply comp_respects; try reflexivity. + auto. + + repeat setoid_rewrite associativity. + repeat setoid_rewrite associativity in H1. + repeat setoid_rewrite <- fmor_preserves_comp in H1. + repeat setoid_rewrite associativity in H1. + apply H1. + Qed. + Implicit Arguments id [[Ob][Hom][Category]]. + + (* this proof is really gross; I will write a better one some other day *) Instance PreMonoidalFunctorsCompose : PreMonoidalFunctor PM1 PM3 (fobj23 ○ fobj12) := { mf_i := compose_mf_i ; mf_F := compose_mf ; mf_first := compose_mf_first ; mf_second := compose_mf_second }. + intros; unfold compose_mf_first; unfold compose_mf_second. set (mf_first (PMF12 a)) as x in *. set (mf_second (PMF12 b)) as y in *. @@ -368,31 +362,12 @@ Section PreMonoidalFunctorsCompose. repeat setoid_rewrite right_identity. set (mf_consistent (PMF12 a) (PMF12 b)) as later. apply comp_respects; try reflexivity. - unfold functor_comp. - unfold functor_fobj; simpl. - set (ni_commutes _ _ (id (fobj12 b))) as x. - unfold functor_comp in x. - simpl in x. - unfold functor_fobj in x. - symmetry in x. - etransitivity. - apply x. - clear x. - set (ni_commutes0 _ _ (id (fobj12 a))) as x'. - unfold functor_comp in x'. - simpl in x'. - unfold functor_fobj in x'. - etransitivity; [ idtac | apply x' ]. - clear x'. - setoid_rewrite fmor_preserves_id. - setoid_rewrite fmor_preserves_id. - setoid_rewrite right_identity. rewrite <- H in later. rewrite <- H0 in later. simpl in later. apply later. apply fmor_respects. - apply (mf_consistent a b). + apply mf_consistent. intros. simpl. @@ -428,22 +403,13 @@ Section PreMonoidalFunctorsCompose. repeat setoid_rewrite associativity. apply comp_respects; try reflexivity. - set (ni_commutes _ _ (id (fobj12 I1))) as x. + set (ni_commutes _ _ #mf_i) as x. unfold functor_comp in x. unfold functor_fobj in x. simpl in x. - setoid_rewrite <- x. - clear x. - setoid_rewrite fmor_preserves_id. - setoid_rewrite fmor_preserves_id. - setoid_rewrite right_identity. - rewrite H. simpl. - clear H. - unfold functor_comp in ni_commutes. - simpl in ni_commutes. - apply ni_commutes. + apply x. intros. unfold compose_mf_second; simpl. @@ -473,24 +439,16 @@ Section PreMonoidalFunctorsCompose. repeat setoid_rewrite associativity. apply comp_respects; try reflexivity. - set (ni_commutes _ _ (id (fobj12 I1))) as x. + set (ni_commutes _ _ #mf_i) as x. unfold functor_comp in x. unfold functor_fobj in x. simpl in x. - setoid_rewrite <- x. - clear x. - setoid_rewrite fmor_preserves_id. - setoid_rewrite fmor_preserves_id. - setoid_rewrite right_identity. - rewrite H. simpl. - clear H. - unfold functor_comp in ni_commutes. - simpl in ni_commutes. - apply ni_commutes. + apply x. + + apply mf_associativity_comp. - apply compose_assoc_coherence. Defined. End PreMonoidalFunctorsCompose. @@ -815,4 +773,4 @@ Section PreMonoidalFullSubcategory. }. Defined. End PreMonoidalFullSubcategory. -*) \ No newline at end of file +*)