; 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)
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.
(* 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
; 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.
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.
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.
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.
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 *.
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.
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.
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.
}.
Defined.
End PreMonoidalFullSubcategory.
-*)
\ No newline at end of file
+*)
projects / coq-categories.git / blobdiff