Documentation

Mathlib.CategoryTheory.Monoidal.Closed.Enrichment

A closed monoidal category is enriched in itself #

From the data of a closed monoidal category C, we define a C-category structure for C. where the hom-object is given by the internal hom (coming from the closed structure).

We use scoped instance to avoid potential issues where C may also have a C-category structure coming from another source (e.g. the type of simplicial sets SSet.{v} has an instance of EnrichedCategory SSet.{v} as a category of simplicial objects; see Mathlib/AlgebraicTopology/SimplicialCategory/SimplicialObject.lean).

All structure field values are defined in Mathlib/CategoryTheory/Closed/Monoidal.lean.

source
@[instance_reducible]
def CategoryTheory.MonoidalClosed.enrichedCategorySelf (C : Type u) [Category.{v, u} C] [MonoidalCategory C] [MonoidalClosed C] :
EnrichedCategory C C

For C closed monoidal, build an instance of C as a C-category

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem CategoryTheory.MonoidalClosed.enrichedCategorySelf_hom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [MonoidalClosed C] (X Y : C) :
    (X ⟶[C] Y) = (ihom X).obj Y
    source
    theorem CategoryTheory.MonoidalClosed.enrichedCategorySelf_id {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [MonoidalClosed C] (X : C) :
    eId C X = id X
    source
    theorem CategoryTheory.MonoidalClosed.enrichedCategorySelf_comp {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [MonoidalClosed C] (X Y Z : C) :
    eComp C X Y Z = comp X Y Z
    source
    @[instance_reducible]
    def CategoryTheory.MonoidalClosed.enrichedOrdinaryCategorySelf (C : Type u) [Category.{v, u} C] [MonoidalCategory C] [MonoidalClosed C] :
    EnrichedOrdinaryCategory C C

    A monoidal closed category is an enriched ordinary category over itself.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem CategoryTheory.MonoidalClosed.enrichedOrdinaryCategorySelf_eHomWhiskerLeft (C : Type u) [Category.{v, u} C] [MonoidalCategory C] [MonoidalClosed C] (X : C) {Y₁ Y₂ : C} (g : Y₁ ⟶ Y₂) :
      eHomWhiskerLeft C X g = (ihom X).map g
      source
      theorem CategoryTheory.MonoidalClosed.enrichedOrdinaryCategorySelf_eHomWhiskerRight (C : Type u) [Category.{v, u} C] [MonoidalCategory C] [MonoidalClosed C] {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C) :
      eHomWhiskerRight C f Y = (pre f).app Y
      source
      theorem CategoryTheory.MonoidalClosed.enrichedOrdinaryCategorySelf_homEquiv (C : Type u) [Category.{v, u} C] [MonoidalCategory C] [MonoidalClosed C] {X Y : C} (f : X ⟶ Y) :
      (eHomEquiv C) f = curry' f
      source
      theorem CategoryTheory.MonoidalClosed.enrichedOrdinaryCategorySelf_homEquiv_symm (C : Type u) [Category.{v, u} C] [MonoidalCategory C] [MonoidalClosed C] {X Y : C} (g : MonoidalCategoryStruct.tensorUnit C ⟶ (ihom X).obj Y) :
      (eHomEquiv C).symm g = uncurry' g