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}
[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]
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.
Instances of this typeclass
- Module.category_theory.monoidal_closed
- category_theory.functor.monoidal_closed
- Rep.category_theory.monoidal_closed
- category_theory.monoidal_category.full_monoidal_closed_subcategory
- fgModule.category_theory.monoidal_closed
- category_theory.sort.cartesian_closed
- category_theory.functor.cartesian_closed
Instances of other typeclasses for category_theory.monoidal_closed
- category_theory.monoidal_closed.has_sizeof_inst
def
category_theory.tensor_closed
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{X Y : C}
(hX : category_theory.closed X)
(hY : category_theory.closed Y) :
category_theory.closed (X ⊗ Y)
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
- category_theory.tensor_closed hX hY = {is_adj := category_theory.adjunction.left_adjoint_of_nat_iso (category_theory.monoidal_category.tensor_left_tensor X Y).symm (category_theory.adjunction.left_adjoint_of_comp (category_theory.monoidal_category.tensor_left Y) (category_theory.monoidal_category.tensor_left X))}
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' := _}}}
def
category_theory.ihom
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(A : C)
[category_theory.closed A] :
C ⥤ C
This is the internal hom A ⟶[C] -.
def
category_theory.ihom.adjunction
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(A : C)
[category_theory.closed A] :
The adjunction between A ⊗ - and A ⟹ -.
def
category_theory.ihom.ev
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(A : C)
[category_theory.closed A] :
The evaluation natural transformation.
Equations
def
category_theory.ihom.coev
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(A : C)
[category_theory.closed A] :
The coevaluation natural transformation.
Equations
@[simp]
theorem
category_theory.ihom.ihom_adjunction_counit
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(A : C)
[category_theory.closed A] :
@[simp]
theorem
category_theory.ihom.ihom_adjunction_unit
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(A : C)
[category_theory.closed A] :
@[simp]
theorem
category_theory.ihom.ev_naturality
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(A : C)
[category_theory.closed A]
{X Y : C}
(f : X ⟶ Y) :
(𝟙 A ⊗ (category_theory.ihom A).map f) ≫ (category_theory.ihom.ev A).app Y = (category_theory.ihom.ev A).app X ≫ f
@[simp]
theorem
category_theory.ihom.ev_naturality_assoc
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(A : C)
[category_theory.closed A]
{X Y : C}
(f : X ⟶ Y)
{X' : C}
(f' : (𝟭 C).obj Y ⟶ X') :
(𝟙 A ⊗ (category_theory.ihom A).map f) ≫ (category_theory.ihom.ev A).app Y ≫ f' = (category_theory.ihom.ev A).app X ≫ f ≫ f'
@[simp]
theorem
category_theory.ihom.coev_naturality_assoc
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(A : C)
[category_theory.closed A]
{X Y : C}
(f : X ⟶ Y)
{X' : C}
(f' : (category_theory.monoidal_category.tensor_left A ⋙ category_theory.ihom A).obj Y ⟶ X') :
f ≫ (category_theory.ihom.coev A).app Y ≫ f' = (category_theory.ihom.coev A).app X ≫ (category_theory.ihom A).map (𝟙 A ⊗ f) ≫ f'
@[simp]
theorem
category_theory.ihom.coev_naturality
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(A : C)
[category_theory.closed A]
{X Y : C}
(f : X ⟶ Y) :
f ≫ (category_theory.ihom.coev A).app Y = (category_theory.ihom.coev A).app X ≫ (category_theory.ihom A).map (𝟙 A ⊗ f)
@[simp]
theorem
category_theory.ihom.ev_coev
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(A B : C)
[category_theory.closed A] :
@[simp]
theorem
category_theory.ihom.ev_coev_assoc
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(A B : C)
[category_theory.closed A]
{X' : C}
(f' : (𝟭 C).obj ((category_theory.monoidal_category.tensor_left A).obj B) ⟶ X') :
(𝟙 A ⊗ (category_theory.ihom.coev A).app B) ≫ (category_theory.ihom.ev A).app (A ⊗ B) ≫ f' = f'
@[simp]
theorem
category_theory.ihom.coev_ev_assoc
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(A B : C)
[category_theory.closed A]
{X' : C}
(f' : (category_theory.ihom A).obj ((𝟭 C).obj B) ⟶ X') :
(category_theory.ihom.coev A).app ((category_theory.ihom A).obj B) ≫ (category_theory.ihom A).map ((category_theory.ihom.ev A).app B) ≫ f' = f'
@[simp]
theorem
category_theory.ihom.coev_ev
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(A B : C)
[category_theory.closed A] :
(category_theory.ihom.coev A).app ((category_theory.ihom A).obj B) ≫ (category_theory.ihom A).map ((category_theory.ihom.ev A).app B) = 𝟙 ((category_theory.ihom A).obj B)
@[protected, instance]
def
category_theory.monoidal_closed.curry
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{A X Y : C}
[category_theory.closed A] :
Currying in a monoidal closed category.
Equations
def
category_theory.monoidal_closed.uncurry
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{A X Y : C}
[category_theory.closed A] :
Uncurrying in a monoidal closed category.
Equations
@[simp]
theorem
category_theory.monoidal_closed.hom_equiv_apply_eq
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{A X Y : C}
[category_theory.closed A]
(f : A ⊗ Y ⟶ X) :
@[simp]
theorem
category_theory.monoidal_closed.hom_equiv_symm_apply_eq
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{A X Y : C}
[category_theory.closed A]
(f : Y ⟶ (category_theory.ihom A).obj X) :
theorem
category_theory.monoidal_closed.curry_natural_left
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{A X X' Y : C}
[category_theory.closed A]
(f : X ⟶ X')
(g : A ⊗ X' ⟶ Y) :
category_theory.monoidal_closed.curry ((𝟙 A ⊗ f) ≫ g) = f ≫ category_theory.monoidal_closed.curry g
theorem
category_theory.monoidal_closed.curry_natural_left_assoc
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{A X X' Y : C}
[category_theory.closed A]
(f : X ⟶ X')
(g : A ⊗ X' ⟶ Y)
{X'_1 : C}
(f' : (category_theory.ihom A).obj Y ⟶ X'_1) :
category_theory.monoidal_closed.curry ((𝟙 A ⊗ f) ≫ g) ≫ f' = f ≫ category_theory.monoidal_closed.curry g ≫ f'
theorem
category_theory.monoidal_closed.curry_natural_right
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{A X Y Y' : C}
[category_theory.closed A]
(f : A ⊗ X ⟶ Y)
(g : Y ⟶ Y') :
theorem
category_theory.monoidal_closed.curry_natural_right_assoc
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{A X Y Y' : C}
[category_theory.closed A]
(f : A ⊗ X ⟶ Y)
(g : Y ⟶ Y')
{X' : C}
(f' : (category_theory.ihom A).obj Y' ⟶ X') :
category_theory.monoidal_closed.curry (f ≫ g) ≫ f' = category_theory.monoidal_closed.curry f ≫ (category_theory.ihom A).map g ≫ f'
theorem
category_theory.monoidal_closed.uncurry_natural_right
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{A X Y Y' : C}
[category_theory.closed A]
(f : X ⟶ (category_theory.ihom A).obj Y)
(g : Y ⟶ Y') :
theorem
category_theory.monoidal_closed.uncurry_natural_right_assoc
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{A X Y Y' : C}
[category_theory.closed A]
(f : X ⟶ (category_theory.ihom A).obj Y)
(g : Y ⟶ Y')
{X' : C}
(f' : Y' ⟶ X') :
category_theory.monoidal_closed.uncurry (f ≫ (category_theory.ihom A).map g) ≫ f' = category_theory.monoidal_closed.uncurry f ≫ g ≫ f'
theorem
category_theory.monoidal_closed.uncurry_natural_left
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{A X X' Y : C}
[category_theory.closed A]
(f : X ⟶ X')
(g : X' ⟶ (category_theory.ihom A).obj Y) :
theorem
category_theory.monoidal_closed.uncurry_natural_left_assoc
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{A X X' Y : C}
[category_theory.closed A]
(f : X ⟶ X')
(g : X' ⟶ (category_theory.ihom A).obj Y)
{X'_1 : C}
(f' : Y ⟶ X'_1) :
category_theory.monoidal_closed.uncurry (f ≫ g) ≫ f' = (𝟙 A ⊗ f) ≫ category_theory.monoidal_closed.uncurry g ≫ f'
@[simp]
theorem
category_theory.monoidal_closed.uncurry_curry
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{A X Y : C}
[category_theory.closed A]
(f : A ⊗ X ⟶ Y) :
@[simp]
theorem
category_theory.monoidal_closed.curry_uncurry
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{A X Y : C}
[category_theory.closed A]
(f : X ⟶ (category_theory.ihom A).obj Y) :
theorem
category_theory.monoidal_closed.curry_eq_iff
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{A X Y : C}
[category_theory.closed A]
(f : A ⊗ Y ⟶ X)
(g : Y ⟶ (category_theory.ihom A).obj X) :
theorem
category_theory.monoidal_closed.eq_curry_iff
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{A X Y : C}
[category_theory.closed A]
(f : A ⊗ Y ⟶ X)
(g : Y ⟶ (category_theory.ihom A).obj X) :
theorem
category_theory.monoidal_closed.uncurry_eq
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{A X Y : C}
[category_theory.closed A]
(g : Y ⟶ (category_theory.ihom A).obj X) :
category_theory.monoidal_closed.uncurry g = (𝟙 A ⊗ g) ≫ (category_theory.ihom.ev A).app X
theorem
category_theory.monoidal_closed.curry_eq
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{A X Y : C}
[category_theory.closed A]
(g : A ⊗ Y ⟶ X) :
theorem
category_theory.monoidal_closed.curry_injective
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{A X Y : C}
[category_theory.closed A] :
theorem
category_theory.monoidal_closed.uncurry_injective
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{A X Y : C}
[category_theory.closed A] :
theorem
category_theory.monoidal_closed.uncurry_id_eq_ev
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(A X : C)
[category_theory.closed A] :
theorem
category_theory.monoidal_closed.curry_id_eq_coev
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(A X : C)
[category_theory.closed A] :
category_theory.monoidal_closed.curry (𝟙 (A ⊗ (𝟭 C).obj X)) = (category_theory.ihom.coev A).app X
def
category_theory.monoidal_closed.pre
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{A B : C}
[category_theory.closed A]
[category_theory.closed B]
(f : B ⟶ A) :
Pre-compose an internal hom with an external hom.
@[simp]
theorem
category_theory.monoidal_closed.id_tensor_pre_app_comp_ev
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{A B : C}
[category_theory.closed A]
[category_theory.closed B]
(f : B ⟶ A)
(X : C) :
(𝟙 B ⊗ (category_theory.monoidal_closed.pre f).app X) ≫ (category_theory.ihom.ev B).app X = (f ⊗ 𝟙 ((category_theory.ihom A).obj X)) ≫ (category_theory.ihom.ev A).app X
@[simp]
theorem
category_theory.monoidal_closed.id_tensor_pre_app_comp_ev_assoc
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{A B : C}
[category_theory.closed A]
[category_theory.closed B]
(f : B ⟶ A)
(X : C)
{X' : C}
(f' : (𝟭 C).obj X ⟶ X') :
(𝟙 B ⊗ (category_theory.monoidal_closed.pre f).app X) ≫ (category_theory.ihom.ev B).app X ≫ f' = (f ⊗ 𝟙 ((category_theory.ihom A).obj X)) ≫ (category_theory.ihom.ev A).app X ≫ f'
@[simp]
theorem
category_theory.monoidal_closed.uncurry_pre
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{A B : C}
[category_theory.closed A]
[category_theory.closed B]
(f : B ⟶ A)
(X : C) :
category_theory.monoidal_closed.uncurry ((category_theory.monoidal_closed.pre f).app X) = (f ⊗ 𝟙 ((category_theory.ihom A).obj X)) ≫ (category_theory.ihom.ev A).app X
@[simp]
theorem
category_theory.monoidal_closed.coev_app_comp_pre_app
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{A B : C}
(X : C)
[category_theory.closed A]
[category_theory.closed B]
(f : B ⟶ A) :
(category_theory.ihom.coev A).app X ≫ (category_theory.monoidal_closed.pre f).app (A ⊗ X) = (category_theory.ihom.coev B).app X ≫ (category_theory.ihom B).map (f ⊗ 𝟙 X)
@[simp]
theorem
category_theory.monoidal_closed.coev_app_comp_pre_app_assoc
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{A B : C}
(X : C)
[category_theory.closed A]
[category_theory.closed B]
(f : B ⟶ A)
{X' : C}
(f' : (category_theory.ihom B).obj ((category_theory.monoidal_category.tensor_left A).obj X) ⟶ X') :
(category_theory.ihom.coev A).app X ≫ (category_theory.monoidal_closed.pre f).app (A ⊗ X) ≫ f' = (category_theory.ihom.coev B).app X ≫ (category_theory.ihom B).map (f ⊗ 𝟙 X) ≫ f'
@[simp]
theorem
category_theory.monoidal_closed.pre_id
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(A : C)
[category_theory.closed A] :
@[simp]
theorem
category_theory.monoidal_closed.pre_map
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{A₁ A₂ A₃ : C}
[category_theory.closed A₁]
[category_theory.closed A₂]
[category_theory.closed A₃]
(f : A₁ ⟶ A₂)
(g : A₂ ⟶ A₃) :
theorem
category_theory.monoidal_closed.pre_comm_ihom_map
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{W X Y Z : C}
[category_theory.closed W]
[category_theory.closed X]
(f : W ⟶ X)
(g : Y ⟶ Z) :
(category_theory.monoidal_closed.pre f).app Y ≫ (category_theory.ihom W).map g = (category_theory.ihom X).map g ≫ (category_theory.monoidal_closed.pre f).app Z
@[simp]
theorem
category_theory.monoidal_closed.internal_hom_map
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.monoidal_closed C]
(X Y : Cᵒᵖ)
(f : X ⟶ Y) :
@[simp]
def
category_theory.monoidal_closed.internal_hom
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.monoidal_closed C] :
The internal hom functor given by the monoidal closed structure.
Equations
- category_theory.monoidal_closed.internal_hom = {obj := λ (X : Cᵒᵖ), category_theory.ihom (opposite.unop X), map := λ (X Y : Cᵒᵖ) (f : X ⟶ Y), category_theory.monoidal_closed.pre f.unop, map_id' := _, map_comp' := _}
noncomputable
def
category_theory.monoidal_closed.of_equiv
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
(F : category_theory.monoidal_functor C D)
[category_theory.is_equivalence F.to_lax_monoidal_functor.to_functor]
[h : category_theory.monoidal_closed D] :
Transport the property of being monoidal closed across a monoidal equivalence of categories
Equations
- category_theory.monoidal_closed.of_equiv F = {closed' := λ (X : C), {is_adj := category_theory.adjunction.left_adjoint_of_nat_iso (category_theory.comp_inv_iso (F.comm_tensor_left X)) (category_theory.adjunction.left_adjoint_of_comp (F.to_lax_monoidal_functor.to_functor ⋙ category_theory.monoidal_category.tensor_left (F.to_lax_monoidal_functor.to_functor.obj X)) F.to_lax_monoidal_functor.to_functor.inv)}}
theorem
category_theory.monoidal_closed.of_equiv_curry_def
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
(F : category_theory.monoidal_functor C D)
[category_theory.is_equivalence F.to_lax_monoidal_functor.to_functor]
[h : category_theory.monoidal_closed D]
{X Y Z : C}
(f : X ⊗ Y ⟶ Z) :
category_theory.monoidal_closed.curry f = ⇑(F.to_lax_monoidal_functor.to_functor.adjunction.hom_equiv Y ((category_theory.ihom (F.to_lax_monoidal_functor.to_functor.obj X)).obj (F.to_lax_monoidal_functor.to_functor.inv.inv.obj Z))) (category_theory.monoidal_closed.curry (⇑(F.to_lax_monoidal_functor.to_functor.inv.adjunction.hom_equiv (F.to_lax_monoidal_functor.to_functor.obj X ⊗ F.to_lax_monoidal_functor.to_functor.obj Y) Z) ((category_theory.comp_inv_iso (F.comm_tensor_left X)).hom.app Y ≫ 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 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}
[category_theory.category C]
[category_theory.monoidal_category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
(F : category_theory.monoidal_functor C D)
[category_theory.is_equivalence F.to_lax_monoidal_functor.to_functor]
[h : category_theory.monoidal_closed D]
{X Y Z : C}
(f : Y ⟶ (category_theory.ihom X).obj Z) :
category_theory.monoidal_closed.uncurry f = (category_theory.comp_inv_iso (F.comm_tensor_left X)).inv.app Y ≫ ⇑((F.to_lax_monoidal_functor.to_functor.inv.adjunction.hom_equiv (F.to_lax_monoidal_functor.to_functor.obj X ⊗ F.to_lax_monoidal_functor.to_functor.obj Y) Z).symm) (category_theory.monoidal_closed.uncurry (⇑((F.to_lax_monoidal_functor.to_functor.adjunction.hom_equiv Y ((category_theory.ihom (F.to_lax_monoidal_functor.to_functor.obj X)).obj (F.to_lax_monoidal_functor.to_functor.obj Z))).symm) 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.)