# mathlibdocumentation

category_theory.closed.monoidal

# 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]
structure category_theory.closed {C : Type u} (X : C) :
Type (max u v)

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

Instances of this typeclass
Instances of other typeclasses for category_theory.closed
• category_theory.closed.has_sizeof_inst
@[class]
structure category_theory.monoidal_closed (C : Type u)  :
Type (max u v)
• closed' : Π (X : C),

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

Instances of this typeclass
Instances of other typeclasses for category_theory.monoidal_closed
• category_theory.monoidal_closed.has_sizeof_inst

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
def category_theory.unit_closed {C : Type u}  :

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

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

Equations

The adjunction between A ⊗ - and A ⟹ -.

Equations
def category_theory.ihom.ev {C : Type u} (A : C)  :

The evaluation natural transformation.

Equations
def category_theory.ihom.coev {C : Type u} (A : C)  :

The coevaluation natural transformation.

Equations
@[simp]
theorem category_theory.ihom.ihom_adjunction_counit {C : Type u} (A : C)  :
@[simp]
theorem category_theory.ihom.ihom_adjunction_unit {C : Type u} (A : C)  :
@[simp]
theorem category_theory.ihom.ev_naturality {C : Type u} (A : C) {X Y : C} (f : X Y) :
(𝟙 A f) = f
@[simp]
theorem category_theory.ihom.ev_naturality_assoc {C : Type u} (A : C) {X Y : C} (f : X Y) {X' : C} (f' : (𝟭 C).obj Y X') :
(𝟙 A f) f' = f f'
@[simp]
theorem category_theory.ihom.coev_naturality_assoc {C : Type u} (A : C) {X Y : C} (f : X Y) {X' : C} (f' : X') :
f f' = (𝟙 A f) f'
@[simp]
theorem category_theory.ihom.coev_naturality {C : Type u} (A : C) {X Y : C} (f : X Y) :
f = (𝟙 A f)
@[simp]
theorem category_theory.ihom.ev_coev {C : Type u} (A B : C)  :
(𝟙 A B) (A B) = 𝟙 (A B)
@[simp]
theorem category_theory.ihom.ev_coev_assoc {C : Type u} (A B : C) {X' : C} (f' : (𝟭 C).obj X') :
(𝟙 A B) (A B) f' = f'
@[simp]
theorem category_theory.ihom.coev_ev_assoc {C : Type u} (A B : C) {X' : C} (f' : ((𝟭 C).obj B) X') :
.obj B) B) f' = f'
@[simp]
theorem category_theory.ihom.coev_ev {C : Type u} (A B : C)  :
.obj B) B) = 𝟙 .obj B)
@[protected, instance]
Equations
def category_theory.monoidal_closed.curry {C : Type u} {A X Y : C}  :
(A Y X)(Y X)

Currying in a monoidal closed category.

Equations
def category_theory.monoidal_closed.uncurry {C : Type u} {A X Y : C}  :
(Y X)(A Y X)

Uncurrying in a monoidal closed category.

Equations
@[simp]
theorem category_theory.monoidal_closed.hom_equiv_apply_eq {C : Type u} {A X Y : C} (f : A Y X) :
@[simp]
theorem category_theory.monoidal_closed.hom_equiv_symm_apply_eq {C : Type u} {A X Y : C} (f : Y X) :
theorem category_theory.monoidal_closed.curry_natural_left {C : Type u} {A X X' Y : C} (f : X X') (g : A X' Y) :
theorem category_theory.monoidal_closed.curry_natural_left_assoc {C : Type u} {A X X' Y : C} (f : X X') (g : A X' Y) {X'_1 : C} (f' : Y X'_1) :
theorem category_theory.monoidal_closed.curry_natural_right {C : Type u} {A X Y Y' : C} (f : A X Y) (g : Y Y') :
theorem category_theory.monoidal_closed.curry_natural_right_assoc {C : Type u} {A X Y Y' : C} (f : A X Y) (g : Y Y') {X' : C} (f' : Y' X') :
=
theorem category_theory.monoidal_closed.uncurry_natural_right {C : Type u} {A X Y Y' : C} (f : X Y) (g : Y Y') :
theorem category_theory.monoidal_closed.uncurry_natural_right_assoc {C : Type u} {A X Y Y' : C} (f : X Y) (g : Y Y') {X' : C} (f' : Y' X') :
theorem category_theory.monoidal_closed.uncurry_natural_left {C : Type u} {A X X' Y : C} (f : X X') (g : X' Y) :
theorem category_theory.monoidal_closed.uncurry_natural_left_assoc {C : Type u} {A X X' Y : C} (f : X X') (g : X' Y) {X'_1 : C} (f' : Y X'_1) :
= (𝟙 A f)
@[simp]
theorem category_theory.monoidal_closed.uncurry_curry {C : Type u} {A X Y : C} (f : A X Y) :
@[simp]
theorem category_theory.monoidal_closed.curry_uncurry {C : Type u} {A X Y : C} (f : X Y) :
theorem category_theory.monoidal_closed.curry_eq_iff {C : Type u} {A X Y : C} (f : A Y X) (g : Y X) :
theorem category_theory.monoidal_closed.eq_curry_iff {C : Type u} {A X Y : C} (f : A Y X) (g : Y X) :
theorem category_theory.monoidal_closed.uncurry_eq {C : Type u} {A X Y : C} (g : Y X) :
= (𝟙 A g)
theorem category_theory.monoidal_closed.curry_eq {C : Type u} {A X Y : C} (g : A Y X) :
theorem category_theory.monoidal_closed.uncurry_id_eq_ev {C : Type u} (A X : C)  :
def category_theory.monoidal_closed.pre {C : Type u} {A B : C} (f : B A) :

Pre-compose an internal hom with an external hom.

Equations
theorem category_theory.monoidal_closed.id_tensor_pre_app_comp_ev {C : Type u} {A B : C} (f : B A) (X : C) :
(𝟙 B = (f 𝟙 .obj X))
theorem category_theory.monoidal_closed.uncurry_pre {C : Type u} {A B : C} (f : B A) (X : C) :
= (f 𝟙 .obj X))
theorem category_theory.monoidal_closed.coev_app_comp_pre_app {C : Type u} {A B : C} (X : C) (f : B A) :
(A X) = (f 𝟙 X)
@[simp]
theorem category_theory.monoidal_closed.pre_id {C : Type u} (A : C)  :
@[simp]
theorem category_theory.monoidal_closed.pre_map {C : Type u} {A₁ A₂ A₃ : C} (f : A₁ A₂) (g : A₂ A₃) :

The internal hom functor given by the monoidal closed structure.

Equations
noncomputable def category_theory.monoidal_closed.of_equiv {C : Type u} {D : Type u₂} (F : D)  :

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

Equations