mathlib3 documentation

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]

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]

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

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

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.)

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.)