mathlib documentation

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} [category_theory.category C] [category_theory.monoidal_category C] (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]

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