# 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} (X : C) :
Type (max u v)

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

a choice of a right adjoint for tensorLeft X

• tensorLeft X is a left adjoint

Instances
class CategoryTheory.MonoidalClosed (C : Type u) :
Type (max u v)

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

• closed : (X : C) →
Instances
def CategoryTheory.tensorClosed {C : Type u} {X : C} {Y : C} (hX : ) (hY : ) :

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.
Instances For

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
Instances For
def CategoryTheory.ihom {C : Type u} (A : C) :

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

Equations
Instances For

The adjunction between A ⊗ - and A ⟹ -.

Equations
Instances For
def CategoryTheory.ihom.ev {C : Type u} (A : C) :

The evaluation natural transformation.

Equations
Instances For
def CategoryTheory.ihom.coev {C : Type u} (A : C) :

The coevaluation natural transformation.

Equations
Instances For
@[simp]
@[simp]
@[simp]
theorem CategoryTheory.ihom.ev_naturality_assoc {C : Type u} (A : C) {X : C} {Y : C} (f : X Y) {Z : C} (h : Y Z) :
@[simp]
theorem CategoryTheory.ihom.ev_naturality {C : Type u} (A : C) {X : C} {Y : C} (f : X Y) :
=
@[simp]
theorem CategoryTheory.ihom.coev_naturality_assoc {C : Type u} (A : C) {X : C} {Y : C} (f : X Y) {Z : C} (h : .obj () Z) :
@[simp]
theorem CategoryTheory.ihom.coev_naturality {C : Type u} (A : C) {X : C} {Y : C} (f : X Y) :
=

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.ihom.ev_coev_assoc {C : Type u} (A : C) (B : C) {Z : C} (h : ) :
= h
@[simp]
theorem CategoryTheory.ihom.ev_coev {C : Type u} (A : C) (B : C) :
@[simp]
theorem CategoryTheory.ihom.coev_ev_assoc {C : Type u} (A : C) (B : C) {Z : C} (h : .obj B Z) :
@[simp]
theorem CategoryTheory.ihom.coev_ev {C : Type u} (A : C) (B : C) :
CategoryTheory.CategoryStruct.comp (.app (.obj B)) (.map (.app B)) =
Equations
def CategoryTheory.MonoidalClosed.curry {C : Type u} {A : C} {X : C} {Y : C} :
(Y .obj X)

Currying in a monoidal closed category.

Equations
• CategoryTheory.MonoidalClosed.curry = (.homEquiv Y X)
Instances For
def CategoryTheory.MonoidalClosed.uncurry {C : Type u} {A : C} {X : C} {Y : C} :
(Y .obj X)

Uncurrying in a monoidal closed category.

Equations
• CategoryTheory.MonoidalClosed.uncurry = (.homEquiv Y X).symm
Instances For
@[simp]
theorem CategoryTheory.MonoidalClosed.homEquiv_apply_eq {C : Type u} {A : C} {X : C} {Y : C} (f : ) :
(.homEquiv Y X) f =
@[simp]
theorem CategoryTheory.MonoidalClosed.homEquiv_symm_apply_eq {C : Type u} {A : C} {X : C} {Y : C} (f : Y .obj X) :
(.homEquiv Y X).symm f =
theorem CategoryTheory.MonoidalClosed.curry_natural_left_assoc {C : Type u} {A : C} {X : C} {X' : C} {Y : C} (f : X X') (g : ) {Z : C} (h : .obj Y Z) :
theorem CategoryTheory.MonoidalClosed.curry_natural_left {C : Type u} {A : C} {X : C} {X' : C} {Y : C} (f : X X') (g : ) :
theorem CategoryTheory.MonoidalClosed.curry_natural_right_assoc {C : Type u} {A : C} {X : C} {Y : C} {Y' : C} (f : ) (g : Y Y') {Z : C} (h : .obj Y' Z) :
theorem CategoryTheory.MonoidalClosed.curry_natural_right {C : Type u} {A : C} {X : C} {Y : C} {Y' : C} (f : ) (g : Y Y') :
theorem CategoryTheory.MonoidalClosed.uncurry_natural_right_assoc {C : Type u} {A : C} {X : C} {Y : C} {Y' : C} (f : X .obj Y) (g : Y Y') {Z : C} (h : Y' Z) :
theorem CategoryTheory.MonoidalClosed.uncurry_natural_right {C : Type u} {A : C} {X : C} {Y : C} {Y' : C} (f : X .obj Y) (g : Y Y') :
theorem CategoryTheory.MonoidalClosed.uncurry_natural_left_assoc {C : Type u} {A : C} {X : C} {X' : C} {Y : C} (f : X X') (g : X' .obj Y) {Z : C} (h : Y Z) :
theorem CategoryTheory.MonoidalClosed.uncurry_natural_left {C : Type u} {A : C} {X : C} {X' : C} {Y : C} (f : X X') (g : X' .obj Y) :
@[simp]
theorem CategoryTheory.MonoidalClosed.uncurry_curry {C : Type u} {A : C} {X : C} {Y : C} (f : ) :
@[simp]
theorem CategoryTheory.MonoidalClosed.curry_uncurry {C : Type u} {A : C} {X : C} {Y : C} (f : X .obj Y) :
theorem CategoryTheory.MonoidalClosed.curry_eq_iff {C : Type u} {A : C} {X : C} {Y : C} (f : ) (g : Y .obj X) :
theorem CategoryTheory.MonoidalClosed.eq_curry_iff {C : Type u} {A : C} {X : C} {Y : C} (f : ) (g : Y .obj X) :
theorem CategoryTheory.MonoidalClosed.uncurry_eq {C : Type u} {A : C} {X : C} {Y : C} (g : Y .obj X) :
theorem CategoryTheory.MonoidalClosed.curry_eq {C : Type u} {A : C} {X : C} {Y : C} (g : ) :
theorem CategoryTheory.MonoidalClosed.curry_injective {C : Type u} {A : C} {X : C} {Y : C} :
Function.Injective CategoryTheory.MonoidalClosed.curry
theorem CategoryTheory.MonoidalClosed.uncurry_injective {C : Type u} {A : C} {X : C} {Y : C} :
Function.Injective CategoryTheory.MonoidalClosed.uncurry
theorem CategoryTheory.MonoidalClosed.curry_id_eq_coev {C : Type u} (A : C) (X : C) :
= .app X
def CategoryTheory.MonoidalClosed.pre {C : Type u} {A : C} {B : C} (f : B A) :

Pre-compose an internal hom with an external hom.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.MonoidalClosed.id_tensor_pre_app_comp_ev_assoc {C : Type u} {A : C} {B : C} (f : B A) (X : C) {Z : C} (h : X Z) :
=
@[simp]
theorem CategoryTheory.MonoidalClosed.id_tensor_pre_app_comp_ev {C : Type u} {A : C} {B : C} (f : B A) (X : C) :
=
@[simp]
theorem CategoryTheory.MonoidalClosed.uncurry_pre {C : Type u} {A : C} {B : C} (f : B A) (X : C) :
=
@[simp]
theorem CategoryTheory.MonoidalClosed.coev_app_comp_pre_app_assoc {C : Type u} {A : C} {B : C} (X : C) (f : B A) {Z : C} (h : Z) :
@[simp]
theorem CategoryTheory.MonoidalClosed.coev_app_comp_pre_app {C : Type u} {A : C} {B : C} (X : C) (f : B A) :
=
@[simp]
@[simp]
theorem CategoryTheory.MonoidalClosed.pre_map {C : Type u} {A₁ : C} {A₂ : C} {A₃ : C} (f : A₁ A₂) (g : A₂ A₃) :
theorem CategoryTheory.MonoidalClosed.pre_comm_ihom_map {C : Type u} {W : C} {X : C} {Y : C} {Z : C} (f : W X) (g : Y Z) :
@[simp]
theorem CategoryTheory.MonoidalClosed.internalHom_map {C : Type u} :
∀ {X Y : Cᵒᵖ} (f : X Y), CategoryTheory.MonoidalClosed.internalHom.map f =
@[simp]
theorem CategoryTheory.MonoidalClosed.internalHom_obj {C : Type u} (X : Cᵒᵖ) :
CategoryTheory.MonoidalClosed.internalHom.obj X = CategoryTheory.ihom X.unop

The internal hom functor given by the monoidal closed structure.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def CategoryTheory.MonoidalClosed.ofEquiv {C : Type u} {D : Type u₂} [] (F : ) {G : } (adj : F.toFunctor G) [F.IsEquivalence] :

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.
Instances For
theorem CategoryTheory.MonoidalClosed.ofEquiv_curry_def {C : Type u} {D : Type u₂} [] (F : ) {G : } (adj : F.toFunctor G) [F.IsEquivalence] {X : C} {Y : C} {Z : C} (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 ((F.commTensorLeft 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.)

theorem CategoryTheory.MonoidalClosed.ofEquiv_uncurry_def {C : Type u} {D : Type u₂} [] (F : ) {G : } (adj : F.toFunctor G) [F.IsEquivalence] {X : C} {Y : C} {Z : C} (f : Y .obj Z) :
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.)