Evaluation, coevaluation and precomposition in a closed monoidal full subcategory

If P is a monoidal property of objects of a closed monoidal category C that is closed under internal Homs, Mathlib makes the full subcategory of P closed monoidal (CategoryTheory.ObjectProperty.fullMonoidalClosedSubcategory), with internal Homs computed in C (CategoryTheory.ObjectProperty.ihom_obj, CategoryTheory.ObjectProperty.ihom_map_hom). This file records that its evaluation, coevaluation and precomposition maps are also those of C, so that computations with internal Homs in the subcategory reduce to computations in C.

Main declarations

• CategoryTheory.ObjectProperty.ihom_ev_app_hom and CategoryTheory.ObjectProperty.ihom_coev_app_hom: evaluation and coevaluation;
• CategoryTheory.ObjectProperty.pre_app_hom: precomposition with a morphism of the subcategory.

@[simp]

theorem CategoryTheory.ObjectProperty.ihom_ev_app_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [MonoidalClosed C] (P : ObjectProperty C) [P.IsMonoidal] [P.IsMonoidalClosed] (X Y : P.FullSubcategory) : ((ihom.ev X).app Y).hom = (ihom.ev X.obj).app Y.obj

Evaluation in the closed monoidal full subcategory is evaluation in the ambient category.

@[simp]

theorem CategoryTheory.ObjectProperty.ihom_coev_app_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [MonoidalClosed C] (P : ObjectProperty C) [P.IsMonoidal] [P.IsMonoidalClosed] (X Y : P.FullSubcategory) : ((ihom.coev X).app Y).hom = (ihom.coev X.obj).app Y.obj

Coevaluation in the closed monoidal full subcategory is coevaluation in the ambient category.

@[simp]

theorem CategoryTheory.ObjectProperty.pre_app_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [MonoidalClosed C] {P : ObjectProperty C} [P.IsMonoidal] [P.IsMonoidalClosed] {X X' : P.FullSubcategory} (f : X ⟶ X') (Y : P.FullSubcategory) : ((MonoidalClosed.pre f).app Y).hom = (MonoidalClosed.pre f.hom).app Y.obj

Precomposition of internal Homs in the closed monoidal full subcategory is precomposition in the ambient category.