Closed monoidal categories #

Define (right) closed objects and (right) closed monoidal categories.

TODO #

Some of the theorems proved about cartesian closed categories should be generalised and moved to this file.

class CategoryTheory.Closed {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) :

Type (max u v)

An object X is (right) closed if (X ⊗ -) is a left adjoint.

rightAdj : CategoryTheory.Functor C C
a choice of a right adjoint for tensorLeft X
adj : CategoryTheory.MonoidalCategory.tensorLeft X ⊣ CategoryTheory.Closed.rightAdj X
tensorLeft X is a left adjoint

Instances

source

class CategoryTheory.MonoidalClosed (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] :

Type (max u v)

A monoidal category C is (right) monoidal closed if every object is (right) closed.

closed : (X : C) → CategoryTheory.Closed X

Instances

source

def CategoryTheory.tensorClosed {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {X Y : C} (hX : CategoryTheory.Closed X) (hY : CategoryTheory.Closed Y) :

CategoryTheory.Closed (CategoryTheory.MonoidalCategory.tensorObj X Y)

If X and Y are closed then X ⊗ Y is. This isn't an instance because it's not usually how we want to construct internal homs, we'll usually prove all objects are closed uniformly.

Equations

One or more equations did not get rendered due to their size.

source

def CategoryTheory.unitClosed {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] :

CategoryTheory.Closed (𝟙_ C)

The unit object is always closed. This isn't an instance because most of the time we'll prove closedness for all objects at once, rather than just for this one.

Equations

CategoryTheory.unitClosed = { rightAdj := CategoryTheory.Functor.id C, adj := CategoryTheory.Adjunction.id.ofNatIsoLeft (CategoryTheory.MonoidalCategory.leftUnitorNatIso C).symm }

source

def CategoryTheory.ihom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A : C) [CategoryTheory.Closed A] :

CategoryTheory.Functor C C

This is the internal hom A ⟶[C] -.

Equations

CategoryTheory.ihom A = CategoryTheory.Closed.rightAdj A

source

def CategoryTheory.ihom.adjunction {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A : C) [CategoryTheory.Closed A] :

CategoryTheory.MonoidalCategory.tensorLeft A ⊣ CategoryTheory.ihom A

The adjunction between A ⊗ - and A ⟹ -.

Equations

CategoryTheory.ihom.adjunction A = CategoryTheory.Closed.adj

source

def CategoryTheory.ihom.ev {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A : C) [CategoryTheory.Closed A] :

(CategoryTheory.ihom A).comp (CategoryTheory.MonoidalCategory.tensorLeft A) ⟶ CategoryTheory.Functor.id C

The evaluation natural transformation.

Equations

CategoryTheory.ihom.ev A = (CategoryTheory.ihom.adjunction A).counit

source

def CategoryTheory.ihom.coev {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A : C) [CategoryTheory.Closed A] :

CategoryTheory.Functor.id C ⟶ (CategoryTheory.MonoidalCategory.tensorLeft A).comp (CategoryTheory.ihom A)

The coevaluation natural transformation.

Equations

CategoryTheory.ihom.coev A = (CategoryTheory.ihom.adjunction A).unit

source

@[simp]

theorem CategoryTheory.ihom.ihom_adjunction_counit {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A : C) [CategoryTheory.Closed A] :

(CategoryTheory.ihom.adjunction A).counit = CategoryTheory.ihom.ev A

source

@[simp]

theorem CategoryTheory.ihom.ihom_adjunction_unit {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A : C) [CategoryTheory.Closed A] :

(CategoryTheory.ihom.adjunction A).unit = CategoryTheory.ihom.coev A

source

@[simp]

theorem CategoryTheory.ihom.ev_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A : C) [CategoryTheory.Closed A] {X Y : C} (f : X ⟶ Y) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A ((CategoryTheory.ihom A).map f)) ((CategoryTheory.ihom.ev A).app Y) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.ev A).app X) f

source

@[simp]

theorem CategoryTheory.ihom.ev_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A : C) [CategoryTheory.Closed A] {X Y : C} (f : X ⟶ Y) {Z : C} (h : Y ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A ((CategoryTheory.ihom A).map f)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.ev A).app Y) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.ev A).app X) (CategoryTheory.CategoryStruct.comp f h)

source

@[simp]

theorem CategoryTheory.ihom.coev_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A : C) [CategoryTheory.Closed A] {X Y : C} (f : X ⟶ Y) :

CategoryTheory.CategoryStruct.comp f ((CategoryTheory.ihom.coev A).app Y) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.coev A).app X) ((CategoryTheory.ihom A).map (CategoryTheory.MonoidalCategory.whiskerLeft A f))

source

@[simp]

theorem CategoryTheory.ihom.coev_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A : C) [CategoryTheory.Closed A] {X Y : C} (f : X ⟶ Y) {Z : C} (h : (CategoryTheory.ihom A).obj ((CategoryTheory.MonoidalCategory.tensorLeft A).obj Y) ⟶ Z) :

CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.coev A).app Y) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.coev A).app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom A).map (CategoryTheory.MonoidalCategory.whiskerLeft A f)) h)

source

def CategoryTheory.ihom.«term_⟶[_]_» :

Lean.TrailingParserDescr

A ⟶[C] B denotes the internal hom from A to B

Equations

One or more equations did not get rendered due to their size.

source

@[simp]

theorem CategoryTheory.ihom.ev_coev {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A B : C) [CategoryTheory.Closed A] :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A ((CategoryTheory.ihom.coev A).app B)) ((CategoryTheory.ihom.ev A).app (CategoryTheory.MonoidalCategory.tensorObj A B)) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj A B)

source

@[simp]

theorem CategoryTheory.ihom.ev_coev_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A B : C) [CategoryTheory.Closed A] {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj A B ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A ((CategoryTheory.ihom.coev A).app B)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.ev A).app (CategoryTheory.MonoidalCategory.tensorObj A B)) h) = h

source

@[simp]

theorem CategoryTheory.ihom.coev_ev {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A B : C) [CategoryTheory.Closed A] :

CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.coev A).app ((CategoryTheory.ihom A).obj B)) ((CategoryTheory.ihom A).map ((CategoryTheory.ihom.ev A).app B)) = CategoryTheory.CategoryStruct.id ((CategoryTheory.ihom A).obj B)

source

@[simp]

theorem CategoryTheory.ihom.coev_ev_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A B : C) [CategoryTheory.Closed A] {Z : C} (h : (CategoryTheory.ihom A).obj B ⟶ Z) :

CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.coev A).app ((CategoryTheory.ihom A).obj B)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom A).map ((CategoryTheory.ihom.ev A).app B)) h) = h

source

instance CategoryTheory.instPreservesColimitsTensorLeft {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A : C) [CategoryTheory.Closed A] :

CategoryTheory.Limits.PreservesColimits (CategoryTheory.MonoidalCategory.tensorLeft A)

Equations

⋯ = ⋯

source

def CategoryTheory.MonoidalClosed.curry {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {A X Y : C} [CategoryTheory.Closed A] :

(CategoryTheory.MonoidalCategory.tensorObj A Y ⟶ X) → (Y ⟶ (CategoryTheory.ihom A).obj X)

Currying in a monoidal closed category.

Equations

CategoryTheory.MonoidalClosed.curry = ⇑((CategoryTheory.ihom.adjunction A).homEquiv Y X)

source

def CategoryTheory.MonoidalClosed.uncurry {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {A X Y : C} [CategoryTheory.Closed A] :

(Y ⟶ (CategoryTheory.ihom A).obj X) → (CategoryTheory.MonoidalCategory.tensorObj A Y ⟶ X)

Uncurrying in a monoidal closed category.

Equations

CategoryTheory.MonoidalClosed.uncurry = ⇑((CategoryTheory.ihom.adjunction A).homEquiv Y X).symm

source

@[simp]

theorem CategoryTheory.MonoidalClosed.homEquiv_apply_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {A X Y : C} [CategoryTheory.Closed A] (f : CategoryTheory.MonoidalCategory.tensorObj A Y ⟶ X) :

((CategoryTheory.ihom.adjunction A).homEquiv Y X) f = CategoryTheory.MonoidalClosed.curry f

source

@[simp]

theorem CategoryTheory.MonoidalClosed.homEquiv_symm_apply_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {A X Y : C} [CategoryTheory.Closed A] (f : Y ⟶ (CategoryTheory.ihom A).obj X) :

((CategoryTheory.ihom.adjunction A).homEquiv Y X).symm f = CategoryTheory.MonoidalClosed.uncurry f

source

theorem CategoryTheory.MonoidalClosed.curry_natural_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {A X X' Y : C} [CategoryTheory.Closed A] (f : X ⟶ X') (g : CategoryTheory.MonoidalCategory.tensorObj A X' ⟶ Y) :

CategoryTheory.MonoidalClosed.curry (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A f) g) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.MonoidalClosed.curry g)

source

theorem CategoryTheory.MonoidalClosed.curry_natural_left_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {A X X' Y : C} [CategoryTheory.Closed A] (f : X ⟶ X') (g : CategoryTheory.MonoidalCategory.tensorObj A X' ⟶ Y) {Z : C} (h : (CategoryTheory.ihom A).obj Y ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.curry (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A f) g)) h = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.curry g) h)

source

theorem CategoryTheory.MonoidalClosed.curry_natural_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {A X Y Y' : C} [CategoryTheory.Closed A] (f : CategoryTheory.MonoidalCategory.tensorObj A X ⟶ Y) (g : Y ⟶ Y') :

CategoryTheory.MonoidalClosed.curry (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.curry f) ((CategoryTheory.ihom A).map g)

source

theorem CategoryTheory.MonoidalClosed.curry_natural_right_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {A X Y Y' : C} [CategoryTheory.Closed A] (f : CategoryTheory.MonoidalCategory.tensorObj A X ⟶ Y) (g : Y ⟶ Y') {Z : C} (h : (CategoryTheory.ihom A).obj Y' ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.curry (CategoryTheory.CategoryStruct.comp f g)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.curry f) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom A).map g) h)

source

theorem CategoryTheory.MonoidalClosed.uncurry_natural_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {A X Y Y' : C} [CategoryTheory.Closed A] (f : X ⟶ (CategoryTheory.ihom A).obj Y) (g : Y ⟶ Y') :

CategoryTheory.MonoidalClosed.uncurry (CategoryTheory.CategoryStruct.comp f ((CategoryTheory.ihom A).map g)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.uncurry f) g

source

theorem CategoryTheory.MonoidalClosed.uncurry_natural_right_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {A X Y Y' : C} [CategoryTheory.Closed A] (f : X ⟶ (CategoryTheory.ihom A).obj Y) (g : Y ⟶ Y') {Z : C} (h : Y' ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.uncurry (CategoryTheory.CategoryStruct.comp f ((CategoryTheory.ihom A).map g))) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.uncurry f) (CategoryTheory.CategoryStruct.comp g h)

source

theorem CategoryTheory.MonoidalClosed.uncurry_natural_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {A X X' Y : C} [CategoryTheory.Closed A] (f : X ⟶ X') (g : X' ⟶ (CategoryTheory.ihom A).obj Y) :

CategoryTheory.MonoidalClosed.uncurry (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A f) (CategoryTheory.MonoidalClosed.uncurry g)

source

theorem CategoryTheory.MonoidalClosed.uncurry_natural_left_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {A X X' Y : C} [CategoryTheory.Closed A] (f : X ⟶ X') (g : X' ⟶ (CategoryTheory.ihom A).obj Y) {Z : C} (h : Y ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.uncurry (CategoryTheory.CategoryStruct.comp f g)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.uncurry g) h)

source

@[simp]

theorem CategoryTheory.MonoidalClosed.uncurry_curry {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {A X Y : C} [CategoryTheory.Closed A] (f : CategoryTheory.MonoidalCategory.tensorObj A X ⟶ Y) :

CategoryTheory.MonoidalClosed.uncurry (CategoryTheory.MonoidalClosed.curry f) = f

source

@[simp]

theorem CategoryTheory.MonoidalClosed.curry_uncurry {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {A X Y : C} [CategoryTheory.Closed A] (f : X ⟶ (CategoryTheory.ihom A).obj Y) :

CategoryTheory.MonoidalClosed.curry (CategoryTheory.MonoidalClosed.uncurry f) = f

source

theorem CategoryTheory.MonoidalClosed.curry_eq_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {A X Y : C} [CategoryTheory.Closed A] (f : CategoryTheory.MonoidalCategory.tensorObj A Y ⟶ X) (g : Y ⟶ (CategoryTheory.ihom A).obj X) :

CategoryTheory.MonoidalClosed.curry f = g ↔ f = CategoryTheory.MonoidalClosed.uncurry g

source

theorem CategoryTheory.MonoidalClosed.eq_curry_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {A X Y : C} [CategoryTheory.Closed A] (f : CategoryTheory.MonoidalCategory.tensorObj A Y ⟶ X) (g : Y ⟶ (CategoryTheory.ihom A).obj X) :

g = CategoryTheory.MonoidalClosed.curry f ↔ CategoryTheory.MonoidalClosed.uncurry g = f

source

theorem CategoryTheory.MonoidalClosed.uncurry_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {A X Y : C} [CategoryTheory.Closed A] (g : Y ⟶ (CategoryTheory.ihom A).obj X) :

CategoryTheory.MonoidalClosed.uncurry g = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A g) ((CategoryTheory.ihom.ev A).app X)

source

theorem CategoryTheory.MonoidalClosed.curry_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {A X Y : C} [CategoryTheory.Closed A] (g : CategoryTheory.MonoidalCategory.tensorObj A Y ⟶ X) :

CategoryTheory.MonoidalClosed.curry g = CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.coev A).app Y) ((CategoryTheory.ihom A).map g)

source

theorem CategoryTheory.MonoidalClosed.curry_injective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {A X Y : C} [CategoryTheory.Closed A] :

Function.Injective CategoryTheory.MonoidalClosed.curry

source

theorem CategoryTheory.MonoidalClosed.uncurry_injective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {A X Y : C} [CategoryTheory.Closed A] :

Function.Injective CategoryTheory.MonoidalClosed.uncurry

source

theorem CategoryTheory.MonoidalClosed.uncurry_id_eq_ev {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A X : C) [CategoryTheory.Closed A] :

CategoryTheory.MonoidalClosed.uncurry (CategoryTheory.CategoryStruct.id ((CategoryTheory.ihom A).obj X)) = (CategoryTheory.ihom.ev A).app X

source

theorem CategoryTheory.MonoidalClosed.curry_id_eq_coev {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A X : C) [CategoryTheory.Closed A] :

CategoryTheory.MonoidalClosed.curry (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj A ((CategoryTheory.Functor.id C).obj X))) = (CategoryTheory.ihom.coev A).app X

source

def CategoryTheory.MonoidalClosed.unitNatIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Closed (𝟙_ C)] :

CategoryTheory.Functor.id C ≅ CategoryTheory.ihom (𝟙_ C)

The internal hom out of the unit is naturally isomorphic to the identity functor.

Equations

One or more equations did not get rendered due to their size.

source

def CategoryTheory.MonoidalClosed.pre {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {A B : C} [CategoryTheory.Closed A] [CategoryTheory.Closed B] (f : B ⟶ A) :

CategoryTheory.ihom A ⟶ CategoryTheory.ihom B

Pre-compose an internal hom with an external hom.

Equations

One or more equations did not get rendered due to their size.

source

@[simp]

theorem CategoryTheory.MonoidalClosed.id_tensor_pre_app_comp_ev {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {A B : C} [CategoryTheory.Closed A] [CategoryTheory.Closed B] (f : B ⟶ A) (X : C) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft B ((CategoryTheory.MonoidalClosed.pre f).app X)) ((CategoryTheory.ihom.ev B).app X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight f ((CategoryTheory.ihom A).obj X)) ((CategoryTheory.ihom.ev A).app X)

source

@[simp]

theorem CategoryTheory.MonoidalClosed.id_tensor_pre_app_comp_ev_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {A B : C} [CategoryTheory.Closed A] [CategoryTheory.Closed B] (f : B ⟶ A) (X : C) {Z : C} (h : X ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft B ((CategoryTheory.MonoidalClosed.pre f).app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.ev B).app X) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight f ((CategoryTheory.ihom A).obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.ev A).app X) h)

source

@[simp]

theorem CategoryTheory.MonoidalClosed.uncurry_pre {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {A B : C} [CategoryTheory.Closed A] [CategoryTheory.Closed B] (f : B ⟶ A) (X : C) :

CategoryTheory.MonoidalClosed.uncurry ((CategoryTheory.MonoidalClosed.pre f).app X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight f ((CategoryTheory.ihom A).obj X)) ((CategoryTheory.ihom.ev A).app X)

source

@[simp]

theorem CategoryTheory.MonoidalClosed.coev_app_comp_pre_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {A B : C} (X : C) [CategoryTheory.Closed A] [CategoryTheory.Closed B] (f : B ⟶ A) :

CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.coev A).app X) ((CategoryTheory.MonoidalClosed.pre f).app (CategoryTheory.MonoidalCategory.tensorObj A X)) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.coev B).app X) ((CategoryTheory.ihom B).map (CategoryTheory.MonoidalCategory.whiskerRight f X))

source

@[simp]

theorem CategoryTheory.MonoidalClosed.coev_app_comp_pre_app_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {A B : C} (X : C) [CategoryTheory.Closed A] [CategoryTheory.Closed B] (f : B ⟶ A) {Z : C} (h : (CategoryTheory.ihom B).obj (CategoryTheory.MonoidalCategory.tensorObj A X) ⟶ Z) :

CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.coev A).app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalClosed.pre f).app (CategoryTheory.MonoidalCategory.tensorObj A X)) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.coev B).app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom B).map (CategoryTheory.MonoidalCategory.whiskerRight f X)) h)

source

@[simp]

theorem CategoryTheory.MonoidalClosed.pre_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (A : C) [CategoryTheory.Closed A] :

CategoryTheory.MonoidalClosed.pre (CategoryTheory.CategoryStruct.id A) = CategoryTheory.CategoryStruct.id (CategoryTheory.ihom A)

source

@[simp]

theorem CategoryTheory.MonoidalClosed.pre_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {A₁ A₂ A₃ : C} [CategoryTheory.Closed A₁] [CategoryTheory.Closed A₂] [CategoryTheory.Closed A₃] (f : A₁ ⟶ A₂) (g : A₂ ⟶ A₃) :

CategoryTheory.MonoidalClosed.pre (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.pre g) (CategoryTheory.MonoidalClosed.pre f)

source

theorem CategoryTheory.MonoidalClosed.pre_comm_ihom_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {W X Y Z : C} [CategoryTheory.Closed W] [CategoryTheory.Closed X] (f : W ⟶ X) (g : Y ⟶ Z) :

CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalClosed.pre f).app Y) ((CategoryTheory.ihom W).map g) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom X).map g) ((CategoryTheory.MonoidalClosed.pre f).app Z)

source

def CategoryTheory.MonoidalClosed.internalHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalClosed C] :

CategoryTheory.Functor Cᵒᵖ (CategoryTheory.Functor C C)

The internal hom functor given by the monoidal closed structure.

Equations

One or more equations did not get rendered due to their size.

source

@[simp]

theorem CategoryTheory.MonoidalClosed.internalHom_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalClosed C] (X : Cᵒᵖ) :

CategoryTheory.MonoidalClosed.internalHom.obj X = CategoryTheory.ihom (Opposite.unop X)

source

@[simp]

theorem CategoryTheory.MonoidalClosed.internalHom_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalClosed C] {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) :

CategoryTheory.MonoidalClosed.internalHom.map f = CategoryTheory.MonoidalClosed.pre f.unop

source

noncomputable def CategoryTheory.MonoidalClosed.ofEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [F.Monoidal] [F.IsEquivalence] [CategoryTheory.MonoidalClosed D] :

CategoryTheory.MonoidalClosed C

Transport the property of being monoidal closed across a monoidal equivalence of categories

Equations

One or more equations did not get rendered due to their size.

source

theorem CategoryTheory.MonoidalClosed.ofEquiv_curry_def {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [F.Monoidal] [F.IsEquivalence] [CategoryTheory.MonoidalClosed D] {X Y Z : C} (f : CategoryTheory.MonoidalCategory.tensorObj X Y ⟶ Z) :

CategoryTheory.MonoidalClosed.curry f = (adj.homEquiv Y ((CategoryTheory.ihom (F.obj X)).obj (F.obj Z))) (CategoryTheory.MonoidalClosed.curry ((adj.toEquivalence.symm.toAdjunction.homEquiv (CategoryTheory.MonoidalCategory.tensorObj (F.obj X) (F.obj Y)) Z) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.Monoidal.commTensorLeft F X).compInverseIso.hom.app Y) f)))

Suppose we have a monoidal equivalence F : C ≌ D, with D monoidal closed. We can pull the monoidal closed instance back along the equivalence. For X, Y, Z : C, this lemma describes the resulting currying map Hom(X ⊗ Y, Z) → Hom(Y, (X ⟶[C] Z)). (X ⟶[C] Z is defined to be F⁻¹(F(X) ⟶[D] F(Z)), so currying in C is given by essentially conjugating currying in D by F.)

source

theorem CategoryTheory.MonoidalClosed.ofEquiv_uncurry_def {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C D) {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [F.Monoidal] [F.IsEquivalence] [CategoryTheory.MonoidalClosed D] {X Y Z : C} (f : Y ⟶ (CategoryTheory.ihom X).obj Z) :

CategoryTheory.MonoidalClosed.uncurry f = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.Monoidal.commTensorLeft F X).compInverseIso.inv.app Y) ((adj.toEquivalence.symm.toAdjunction.homEquiv ((F.comp (CategoryTheory.MonoidalCategory.tensorLeft (F.obj X))).obj Y) Z).symm (CategoryTheory.MonoidalClosed.uncurry ((adj.homEquiv Y ((CategoryTheory.ihom (F.obj X)).obj (adj.toEquivalence.symm.inverse.obj Z))).symm f)))

Suppose we have a monoidal equivalence F : C ≌ D, with D monoidal closed. We can pull the monoidal closed instance back along the equivalence. For X, Y, Z : C, this lemma describes the resulting uncurrying map Hom(Y, (X ⟶[C] Z)) → Hom(X ⊗ Y ⟶ Z). (X ⟶[C] Z is defined to be F⁻¹(F(X) ⟶[D] F(Z)), so uncurrying in C is given by essentially conjugating uncurrying in D by F.)

source

def CategoryTheory.MonoidalClosed.id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (x : C) [CategoryTheory.Closed x] :

𝟙_ C ⟶ (CategoryTheory.ihom x).obj x

The C-identity morphism 𝟙_ C ⟶ hom(x, x) used to equip C with the structure of a C-category

Equations

CategoryTheory.MonoidalClosed.id x = CategoryTheory.MonoidalClosed.curry (CategoryTheory.MonoidalCategory.rightUnitor x).hom

source

def CategoryTheory.MonoidalClosed.compTranspose {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (x y z : C) [CategoryTheory.Closed x] [CategoryTheory.Closed y] :

CategoryTheory.MonoidalCategory.tensorObj x (CategoryTheory.MonoidalCategory.tensorObj ((CategoryTheory.ihom x).obj y) ((CategoryTheory.ihom y).obj z)) ⟶ z

The uncurried composition morphism x ⊗ (hom(x, y) ⊗ hom(y, z)) ⟶ (x ⊗ hom(x, y)) ⊗ hom(y, z) ⟶ y ⊗ hom(y, z) ⟶ z. The C-composition morphism will be defined as the adjoint transpose of this map.

Equations