From fd14c25703d15bd78088c67ff3d417d435b6b136 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Mon, 11 Apr 2011 03:15:40 +0000 Subject: [PATCH] FullSubcategoryInclusionFunctor for a monoidal subcategory is monoidal --- src/PreMonoidalCategories.v | 61 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 61 insertions(+) diff --git a/src/PreMonoidalCategories.v b/src/PreMonoidalCategories.v index b35a6a6..2764abd 100644 --- a/src/PreMonoidalCategories.v +++ b/src/PreMonoidalCategories.v @@ -924,5 +924,66 @@ Section PreMonoidalFullSubcategory. apply (pmon_cancell_central(PreMonoidalCat:=pm)). Defined. + Instance inclusion_first : ∀a : S, + FullSubcategoryInclusionFunctor S >>>> + - ⋉(FullSubcategoryInclusionFunctor S) a <~~~> + - ⋉a >>>> FullSubcategoryInclusionFunctor S + := { ni_iso := fun A => iso_id ((projT1 A)⊗(projT1 a)) }. + intros; simpl. + symmetry. + setoid_rewrite right_identity. + setoid_rewrite left_identity. + destruct A. + destruct B. + destruct a. + simpl. + reflexivity. + Defined. + + Instance inclusion_second : ∀a : S, + FullSubcategoryInclusionFunctor S >>>> + (FullSubcategoryInclusionFunctor S) a ⋊- <~~~> + a ⋊- >>>> FullSubcategoryInclusionFunctor S + := { ni_iso := fun A => iso_id ((projT1 a)⊗(projT1 A)) }. + intros; simpl. + symmetry. + setoid_rewrite right_identity. + setoid_rewrite left_identity. + destruct A. + destruct B. + destruct a. + simpl. + reflexivity. + Defined. + + (* Curiously, the inclusion functor for a PREmonoidal category isn't necessarily premonoidal (it might fail to preserve + * the center. But in the monoidal case we're okay *) + Instance PreMonoidalFullSubcategoryInclusionFunctor_PreMonoidal (mc:CommutativeCat pm) + : PreMonoidalFunctor PreMonoidalFullSubcategory_PreMonoidal pm (FullSubcategoryInclusionFunctor S) := + { mf_i := iso_id _ + ; mf_first := inclusion_first + ; mf_first := inclusion_second + }. + intros; destruct a; destruct b; reflexivity. + intros; destruct a; destruct b; simpl in *. + apply mc. + intros; destruct b; simpl. + setoid_rewrite right_identity. + setoid_rewrite fmor_preserves_id. + setoid_rewrite left_identity. + reflexivity. + intros; destruct a; simpl. + setoid_rewrite right_identity. + setoid_rewrite fmor_preserves_id. + setoid_rewrite left_identity. + reflexivity. + intros; destruct a; destruct b; destruct c; simpl. + setoid_rewrite right_identity. + setoid_rewrite fmor_preserves_id. + setoid_rewrite left_identity. + setoid_rewrite right_identity. + reflexivity. + Defined. + End PreMonoidalFullSubcategory. -- 1.7.10.4