# mathlib3documentation

category_theory.closed.monoidal

# Closed monoidal categories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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

The evaluation natural transformation.

Equations

The coevaluation natural transformation.

Equations
@[simp]
@[simp]
@[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) :
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
@[simp]
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))
@[simp]
theorem category_theory.monoidal_closed.id_tensor_pre_app_comp_ev_assoc {C : Type u} {A B : C} (f : B A) (X : C) {X' : C} (f' : (𝟭 C).obj X X') :
(𝟙 B f' = (f 𝟙 .obj X)) f'
@[simp]
theorem category_theory.monoidal_closed.uncurry_pre {C : Type u} {A B : C} (f : B A) (X : C) :
= (f 𝟙 .obj X))
@[simp]
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.coev_app_comp_pre_app_assoc {C : Type u} {A B : C} (X : C) (f : B A) {X' : C} (f' : X') :
(A X) f' = (f 𝟙 X) f'
@[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₃) :
theorem category_theory.monoidal_closed.pre_comm_ihom_map {C : Type u} {W X Y Z : C} (f : W X) (g : Y Z) :
=
@[simp]
@[simp]

The internal hom functor given by the monoidal closed structure.

Equations

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

Equations
theorem category_theory.monoidal_closed.of_equiv_curry_def {C : Type u} {D : Type u₂} (F : D) {X Y Z : C} (f : X Y 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 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 category_theory.monoidal_closed.of_equiv_uncurry_def {C : Type u} {D : Type u₂} (F : D) {X Y Z : C} (f : Y 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.)