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] :
C → Type (max u v)
An object X is (right) closed if (X ⊗ -) is a left adjoint.
Instances
@[class]
structure
category_theory.monoidal_closed
(C : Type u)
[category_theory.category C]
[category_theory.monoidal_category C] :
Type (max u v)
- closed : Π (X : C), category_theory.closed X
A monoidal category C is (right) monoidal closed if every object is (right) closed.
def
category_theory.unit_closed
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C] :
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
- category_theory.unit_closed = {is_adj := {right := 𝟭 C _inst_1, adj := category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (X _x : C), {to_fun := λ (a : (category_theory.monoidal_category.tensor_left (𝟙_ C)).obj X ⟶ _x), (λ_ X).inv ≫ a, inv_fun := λ (a : X ⟶ (𝟭 C).obj _x), (λ_ X).hom ≫ a, left_inv := _, right_inv := _}, hom_equiv_naturality_left_symm' := _, hom_equiv_naturality_right' := _}}}