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
CategoryTheory.Closed
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
(X : C)
:
Type (max u v)
An object X is (right) closed if (X ⊗ -) is a left adjoint.
- rightAdj : CategoryTheory.Functor C C
a choice of a right adjoint for
tensorLeft X tensorLeft Xis a left adjoint
Instances
class
CategoryTheory.MonoidalClosed
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
:
Type (max u v)
A monoidal category C is (right) monoidal closed if every object is (right) closed.
- closed : (X : C) → CategoryTheory.Closed X
Instances
def
CategoryTheory.tensorClosed
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{X : C}
{Y : C}
(hX : CategoryTheory.Closed X)
(hY : CategoryTheory.Closed 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
- One or more equations did not get rendered due to their size.
Instances For
def
CategoryTheory.unitClosed
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
:
CategoryTheory.Closed (𝟙_ 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
- CategoryTheory.unitClosed = { rightAdj := CategoryTheory.Functor.id C, adj := CategoryTheory.Adjunction.id.ofNatIsoLeft (CategoryTheory.MonoidalCategory.leftUnitorNatIso C).symm }
Instances For
def
CategoryTheory.ihom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
(A : C)
[CategoryTheory.Closed A]
:
This is the internal hom A ⟶[C] -.
Equations
Instances For
def
CategoryTheory.ihom.adjunction
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
(A : C)
[CategoryTheory.Closed A]
:
The adjunction between A ⊗ - and A ⟹ -.
Equations
- CategoryTheory.ihom.adjunction A = CategoryTheory.Closed.adj
Instances For
def
CategoryTheory.ihom.ev
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
(A : C)
[CategoryTheory.Closed A]
:
The evaluation natural transformation.
Equations
- CategoryTheory.ihom.ev A = (CategoryTheory.ihom.adjunction A).counit
Instances For
def
CategoryTheory.ihom.coev
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
(A : C)
[CategoryTheory.Closed A]
:
The coevaluation natural transformation.
Equations
Instances For
@[simp]
theorem
CategoryTheory.ihom.ihom_adjunction_counit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
(A : C)
[CategoryTheory.Closed A]
:
(CategoryTheory.ihom.adjunction A).counit = CategoryTheory.ihom.ev A
@[simp]
theorem
CategoryTheory.ihom.ihom_adjunction_unit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
(A : C)
[CategoryTheory.Closed A]
:
@[simp]
theorem
CategoryTheory.ihom.ev_naturality_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
(A : C)
[CategoryTheory.Closed A]
{X : C}
{Y : C}
(f : X ⟶ Y)
{Z : C}
(h : Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A ((CategoryTheory.ihom A).map f))
(CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.ev A).app Y) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.ev A).app X) (CategoryTheory.CategoryStruct.comp f h)
@[simp]
theorem
CategoryTheory.ihom.ev_naturality
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
(A : C)
[CategoryTheory.Closed A]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A ((CategoryTheory.ihom A).map f))
((CategoryTheory.ihom.ev A).app Y) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.ev A).app X) f
@[simp]
theorem
CategoryTheory.ihom.coev_naturality_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
(A : C)
[CategoryTheory.Closed A]
{X : C}
{Y : C}
(f : X ⟶ Y)
{Z : C}
(h : (CategoryTheory.ihom A).obj ((CategoryTheory.MonoidalCategory.tensorLeft A).obj Y) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.coev A).app Y) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.coev A).app X)
(CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom A).map (CategoryTheory.MonoidalCategory.whiskerLeft A f))
h)
@[simp]
theorem
CategoryTheory.ihom.coev_naturality
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
(A : C)
[CategoryTheory.Closed A]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
CategoryTheory.CategoryStruct.comp f ((CategoryTheory.ihom.coev A).app Y) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.coev A).app X)
((CategoryTheory.ihom A).map (CategoryTheory.MonoidalCategory.whiskerLeft A f))
A ⟶[C] B denotes the internal hom from A to B
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.ihom.ev_coev_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
(A : C)
(B : C)
[CategoryTheory.Closed A]
{Z : C}
(h : CategoryTheory.MonoidalCategory.tensorObj A B ⟶ Z)
:
@[simp]
theorem
CategoryTheory.ihom.ev_coev
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
(A : C)
(B : C)
[CategoryTheory.Closed A]
:
@[simp]
theorem
CategoryTheory.ihom.coev_ev_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
(A : C)
(B : C)
[CategoryTheory.Closed A]
{Z : C}
(h : (CategoryTheory.ihom A).obj B ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.coev A).app ((CategoryTheory.ihom A).obj B))
(CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom A).map ((CategoryTheory.ihom.ev A).app B)) h) = h
@[simp]
theorem
CategoryTheory.ihom.coev_ev
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
(A : C)
(B : C)
[CategoryTheory.Closed A]
:
CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.coev A).app ((CategoryTheory.ihom A).obj B))
((CategoryTheory.ihom A).map ((CategoryTheory.ihom.ev A).app B)) = CategoryTheory.CategoryStruct.id ((CategoryTheory.ihom A).obj B)
instance
CategoryTheory.instPreservesColimitsTensorLeft
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
(A : C)
[CategoryTheory.Closed A]
:
Equations
- CategoryTheory.instPreservesColimitsTensorLeft A = (CategoryTheory.ihom.adjunction A).leftAdjointPreservesColimits
def
CategoryTheory.MonoidalClosed.curry
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{A : C}
{X : C}
{Y : C}
[CategoryTheory.Closed A]
:
(CategoryTheory.MonoidalCategory.tensorObj A Y ⟶ X) → (Y ⟶ (CategoryTheory.ihom A).obj X)
Currying in a monoidal closed category.
Equations
- CategoryTheory.MonoidalClosed.curry = ⇑((CategoryTheory.ihom.adjunction A).homEquiv Y X)
Instances For
def
CategoryTheory.MonoidalClosed.uncurry
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{A : C}
{X : C}
{Y : C}
[CategoryTheory.Closed A]
:
(Y ⟶ (CategoryTheory.ihom A).obj X) → (CategoryTheory.MonoidalCategory.tensorObj A Y ⟶ X)
Uncurrying in a monoidal closed category.
Equations
- CategoryTheory.MonoidalClosed.uncurry = ⇑((CategoryTheory.ihom.adjunction A).homEquiv Y X).symm
Instances For
@[simp]
theorem
CategoryTheory.MonoidalClosed.homEquiv_apply_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{A : C}
{X : C}
{Y : C}
[CategoryTheory.Closed A]
(f : CategoryTheory.MonoidalCategory.tensorObj A Y ⟶ X)
:
((CategoryTheory.ihom.adjunction A).homEquiv Y X) f = CategoryTheory.MonoidalClosed.curry f
@[simp]
theorem
CategoryTheory.MonoidalClosed.homEquiv_symm_apply_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{A : C}
{X : C}
{Y : C}
[CategoryTheory.Closed A]
(f : Y ⟶ (CategoryTheory.ihom A).obj X)
:
((CategoryTheory.ihom.adjunction A).homEquiv Y X).symm f = CategoryTheory.MonoidalClosed.uncurry f
theorem
CategoryTheory.MonoidalClosed.curry_natural_left_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{A : C}
{X : C}
{X' : C}
{Y : C}
[CategoryTheory.Closed A]
(f : X ⟶ X')
(g : CategoryTheory.MonoidalCategory.tensorObj A X' ⟶ Y)
{Z : C}
(h : (CategoryTheory.ihom A).obj Y ⟶ Z)
:
theorem
CategoryTheory.MonoidalClosed.curry_natural_left
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{A : C}
{X : C}
{X' : C}
{Y : C}
[CategoryTheory.Closed A]
(f : X ⟶ X')
(g : CategoryTheory.MonoidalCategory.tensorObj A X' ⟶ Y)
:
theorem
CategoryTheory.MonoidalClosed.curry_natural_right_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{A : C}
{X : C}
{Y : C}
{Y' : C}
[CategoryTheory.Closed A]
(f : CategoryTheory.MonoidalCategory.tensorObj A X ⟶ Y)
(g : Y ⟶ Y')
{Z : C}
(h : (CategoryTheory.ihom A).obj Y' ⟶ Z)
:
theorem
CategoryTheory.MonoidalClosed.curry_natural_right
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{A : C}
{X : C}
{Y : C}
{Y' : C}
[CategoryTheory.Closed A]
(f : CategoryTheory.MonoidalCategory.tensorObj A X ⟶ Y)
(g : Y ⟶ Y')
:
theorem
CategoryTheory.MonoidalClosed.uncurry_natural_right_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{A : C}
{X : C}
{Y : C}
{Y' : C}
[CategoryTheory.Closed A]
(f : X ⟶ (CategoryTheory.ihom A).obj Y)
(g : Y ⟶ Y')
{Z : C}
(h : Y' ⟶ Z)
:
theorem
CategoryTheory.MonoidalClosed.uncurry_natural_right
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{A : C}
{X : C}
{Y : C}
{Y' : C}
[CategoryTheory.Closed A]
(f : X ⟶ (CategoryTheory.ihom A).obj Y)
(g : Y ⟶ Y')
:
theorem
CategoryTheory.MonoidalClosed.uncurry_natural_left_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{A : C}
{X : C}
{X' : C}
{Y : C}
[CategoryTheory.Closed A]
(f : X ⟶ X')
(g : X' ⟶ (CategoryTheory.ihom A).obj Y)
{Z : C}
(h : Y ⟶ Z)
:
theorem
CategoryTheory.MonoidalClosed.uncurry_natural_left
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{A : C}
{X : C}
{X' : C}
{Y : C}
[CategoryTheory.Closed A]
(f : X ⟶ X')
(g : X' ⟶ (CategoryTheory.ihom A).obj Y)
:
@[simp]
theorem
CategoryTheory.MonoidalClosed.uncurry_curry
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{A : C}
{X : C}
{Y : C}
[CategoryTheory.Closed A]
(f : CategoryTheory.MonoidalCategory.tensorObj A X ⟶ Y)
:
@[simp]
theorem
CategoryTheory.MonoidalClosed.curry_uncurry
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{A : C}
{X : C}
{Y : C}
[CategoryTheory.Closed A]
(f : X ⟶ (CategoryTheory.ihom A).obj Y)
:
theorem
CategoryTheory.MonoidalClosed.curry_eq_iff
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{A : C}
{X : C}
{Y : C}
[CategoryTheory.Closed A]
(f : CategoryTheory.MonoidalCategory.tensorObj A Y ⟶ X)
(g : Y ⟶ (CategoryTheory.ihom A).obj X)
:
theorem
CategoryTheory.MonoidalClosed.eq_curry_iff
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{A : C}
{X : C}
{Y : C}
[CategoryTheory.Closed A]
(f : CategoryTheory.MonoidalCategory.tensorObj A Y ⟶ X)
(g : Y ⟶ (CategoryTheory.ihom A).obj X)
:
theorem
CategoryTheory.MonoidalClosed.uncurry_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{A : C}
{X : C}
{Y : C}
[CategoryTheory.Closed A]
(g : Y ⟶ (CategoryTheory.ihom A).obj X)
:
theorem
CategoryTheory.MonoidalClosed.curry_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{A : C}
{X : C}
{Y : C}
[CategoryTheory.Closed A]
(g : CategoryTheory.MonoidalCategory.tensorObj A Y ⟶ X)
:
CategoryTheory.MonoidalClosed.curry g = CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.coev A).app Y) ((CategoryTheory.ihom A).map g)
theorem
CategoryTheory.MonoidalClosed.curry_injective
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{A : C}
{X : C}
{Y : C}
[CategoryTheory.Closed A]
:
Function.Injective CategoryTheory.MonoidalClosed.curry
theorem
CategoryTheory.MonoidalClosed.uncurry_injective
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{A : C}
{X : C}
{Y : C}
[CategoryTheory.Closed A]
:
Function.Injective CategoryTheory.MonoidalClosed.uncurry
theorem
CategoryTheory.MonoidalClosed.uncurry_id_eq_ev
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
(A : C)
(X : C)
[CategoryTheory.Closed A]
:
CategoryTheory.MonoidalClosed.uncurry (CategoryTheory.CategoryStruct.id ((CategoryTheory.ihom A).obj X)) = (CategoryTheory.ihom.ev A).app X
theorem
CategoryTheory.MonoidalClosed.curry_id_eq_coev
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
(A : C)
(X : C)
[CategoryTheory.Closed A]
:
def
CategoryTheory.MonoidalClosed.unitNatIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.Closed (𝟙_ C)]
:
The internal hom out of the unit is naturally isomorphic to the identity functor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
CategoryTheory.MonoidalClosed.pre
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{A : C}
{B : C}
[CategoryTheory.Closed A]
[CategoryTheory.Closed B]
(f : B ⟶ A)
:
Pre-compose an internal hom with an external hom.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.MonoidalClosed.id_tensor_pre_app_comp_ev_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{A : C}
{B : C}
[CategoryTheory.Closed A]
[CategoryTheory.Closed B]
(f : B ⟶ A)
(X : C)
{Z : C}
(h : X ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.whiskerLeft B ((CategoryTheory.MonoidalClosed.pre f).app X))
(CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.ev B).app X) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight f ((CategoryTheory.ihom A).obj X))
(CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.ev A).app X) h)
@[simp]
theorem
CategoryTheory.MonoidalClosed.id_tensor_pre_app_comp_ev
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{A : C}
{B : C}
[CategoryTheory.Closed A]
[CategoryTheory.Closed B]
(f : B ⟶ A)
(X : C)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.whiskerLeft B ((CategoryTheory.MonoidalClosed.pre f).app X))
((CategoryTheory.ihom.ev B).app X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight f ((CategoryTheory.ihom A).obj X))
((CategoryTheory.ihom.ev A).app X)
@[simp]
theorem
CategoryTheory.MonoidalClosed.uncurry_pre
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{A : C}
{B : C}
[CategoryTheory.Closed A]
[CategoryTheory.Closed B]
(f : B ⟶ A)
(X : C)
:
@[simp]
theorem
CategoryTheory.MonoidalClosed.coev_app_comp_pre_app_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{A : C}
{B : C}
(X : C)
[CategoryTheory.Closed A]
[CategoryTheory.Closed B]
(f : B ⟶ A)
{Z : C}
(h : (CategoryTheory.ihom B).obj (CategoryTheory.MonoidalCategory.tensorObj A X) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.coev A).app X)
(CategoryTheory.CategoryStruct.comp
((CategoryTheory.MonoidalClosed.pre f).app (CategoryTheory.MonoidalCategory.tensorObj A X)) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.coev B).app X)
(CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom B).map (CategoryTheory.MonoidalCategory.whiskerRight f X))
h)
@[simp]
theorem
CategoryTheory.MonoidalClosed.coev_app_comp_pre_app
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{A : C}
{B : C}
(X : C)
[CategoryTheory.Closed A]
[CategoryTheory.Closed B]
(f : B ⟶ A)
:
CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.coev A).app X)
((CategoryTheory.MonoidalClosed.pre f).app (CategoryTheory.MonoidalCategory.tensorObj A X)) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.coev B).app X)
((CategoryTheory.ihom B).map (CategoryTheory.MonoidalCategory.whiskerRight f X))
@[simp]
@[simp]
theorem
CategoryTheory.MonoidalClosed.pre_map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{A₁ : C}
{A₂ : C}
{A₃ : C}
[CategoryTheory.Closed A₁]
[CategoryTheory.Closed A₂]
[CategoryTheory.Closed A₃]
(f : A₁ ⟶ A₂)
(g : A₂ ⟶ A₃)
:
theorem
CategoryTheory.MonoidalClosed.pre_comm_ihom_map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{W : C}
{X : C}
{Y : C}
{Z : C}
[CategoryTheory.Closed W]
[CategoryTheory.Closed X]
(f : W ⟶ X)
(g : Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalClosed.pre f).app Y) ((CategoryTheory.ihom W).map g) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom X).map g) ((CategoryTheory.MonoidalClosed.pre f).app Z)
@[simp]
theorem
CategoryTheory.MonoidalClosed.internalHom_obj
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.MonoidalClosed C]
(X : Cᵒᵖ)
:
CategoryTheory.MonoidalClosed.internalHom.obj X = CategoryTheory.ihom (Opposite.unop X)
@[simp]
theorem
CategoryTheory.MonoidalClosed.internalHom_map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.MonoidalClosed C]
:
∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), CategoryTheory.MonoidalClosed.internalHom.map f = CategoryTheory.MonoidalClosed.pre f.unop
def
CategoryTheory.MonoidalClosed.internalHom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.MonoidalClosed C]
:
The internal hom functor given by the monoidal closed structure.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.MonoidalClosed.ofEquiv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
(F : CategoryTheory.MonoidalFunctor C D)
{G : CategoryTheory.Functor D C}
(adj : F.toFunctor ⊣ G)
[F.IsEquivalence]
[CategoryTheory.MonoidalClosed D]
:
Transport the property of being monoidal closed across a monoidal equivalence of categories
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.MonoidalClosed.ofEquiv_curry_def
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
(F : CategoryTheory.MonoidalFunctor C D)
{G : CategoryTheory.Functor D C}
(adj : F.toFunctor ⊣ G)
[F.IsEquivalence]
[CategoryTheory.MonoidalClosed D]
{X : C}
{Y : C}
{Z : C}
(f : CategoryTheory.MonoidalCategory.tensorObj X Y ⟶ Z)
:
CategoryTheory.MonoidalClosed.curry f = (adj.homEquiv Y ((CategoryTheory.ihom (F.obj X)).obj (F.obj Z)))
(CategoryTheory.MonoidalClosed.curry
((adj.toEquivalence.symm.toAdjunction.homEquiv (CategoryTheory.MonoidalCategory.tensorObj (F.obj X) (F.obj Y)) Z)
(CategoryTheory.CategoryStruct.comp ((F.commTensorLeft X).compInverseIso.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
CategoryTheory.MonoidalClosed.ofEquiv_uncurry_def
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.MonoidalCategory D]
(F : CategoryTheory.MonoidalFunctor C D)
{G : CategoryTheory.Functor D C}
(adj : F.toFunctor ⊣ G)
[F.IsEquivalence]
[CategoryTheory.MonoidalClosed D]
{X : C}
{Y : C}
{Z : C}
(f : Y ⟶ (CategoryTheory.ihom X).obj Z)
:
CategoryTheory.MonoidalClosed.uncurry f = CategoryTheory.CategoryStruct.comp ((F.commTensorLeft X).compInverseIso.inv.app Y)
((adj.toEquivalence.symm.toAdjunction.homEquiv
((F.comp (CategoryTheory.MonoidalCategory.tensorLeft (F.obj X))).obj Y) Z).symm
(CategoryTheory.MonoidalClosed.uncurry
((adj.homEquiv Y ((CategoryTheory.ihom (F.obj X)).obj (adj.toEquivalence.symm.inverse.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.)
def
CategoryTheory.MonoidalClosed.id
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
(x : C)
[CategoryTheory.Closed x]
:
𝟙_ C ⟶ (CategoryTheory.ihom x).obj x
The C-identity morphism
𝟙_ C ⟶ hom(x, x)
used to equip C with the structure of a C-category
Equations
Instances For
def
CategoryTheory.MonoidalClosed.compTranspose
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
(x : C)
(y : C)
(z : C)
[CategoryTheory.Closed x]
[CategoryTheory.Closed y]
:
CategoryTheory.MonoidalCategory.tensorObj x
(CategoryTheory.MonoidalCategory.tensorObj ((CategoryTheory.ihom x).obj y) ((CategoryTheory.ihom y).obj z)) ⟶ z
The uncurried composition morphism
x ⊗ (hom(x, y) ⊗ hom(y, z)) ⟶ (x ⊗ hom(x, y)) ⊗ hom(y, z) ⟶ y ⊗ hom(y, z) ⟶ z.
The C-composition morphism will be defined as the adjoint transpose of this map.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
CategoryTheory.MonoidalClosed.comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
(x : C)
(y : C)
(z : C)
[CategoryTheory.Closed x]
[CategoryTheory.Closed y]
:
CategoryTheory.MonoidalCategory.tensorObj ((CategoryTheory.ihom x).obj y) ((CategoryTheory.ihom y).obj z) ⟶ (CategoryTheory.ihom x).obj z
The C-composition morphism
hom(x, y) ⊗ hom(y, z) ⟶ hom(x, z)
used to equip C with the structure of a C-category
Equations
Instances For
theorem
CategoryTheory.MonoidalClosed.id_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
(x : C)
[CategoryTheory.Closed x]
:
Unfold the definition of id.
This exists to streamline the proofs of MonoidalClosed.id_comp and MonoidalClosed.comp_id
theorem
CategoryTheory.MonoidalClosed.compTranspose_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
(x : C)
(y : C)
(z : C)
[CategoryTheory.Closed x]
[CategoryTheory.Closed y]
:
CategoryTheory.MonoidalClosed.compTranspose x y z = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.associator x ((CategoryTheory.ihom x).obj y) ((CategoryTheory.ihom y).obj z)).inv
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.whiskerRight ((CategoryTheory.ihom.ev x).app y) ((CategoryTheory.ihom y).obj z))
((CategoryTheory.ihom.ev y).app z))
Unfold the definition of compTranspose.
This exists to streamline the proof of MonoidalClosed.assoc
theorem
CategoryTheory.MonoidalClosed.comp_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
(x : C)
(y : C)
(z : C)
[CategoryTheory.Closed x]
[CategoryTheory.Closed y]
:
Unfold the definition of comp.
This exists to streamline the proof of MonoidalClosed.assoc
The proofs of associativity and unitality use the following outline:
- Take adjoint transpose on each side of the equality (uncurry_injective)
- Do whatever rewrites/simps are necessary to apply uncurry_curry
- Conclude with simp
@[simp]
theorem
CategoryTheory.MonoidalClosed.id_comp_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
(x : C)
(y : C)
[CategoryTheory.Closed x]
{Z : C}
(h : (CategoryTheory.ihom x).obj y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor ((CategoryTheory.ihom x).obj y)).inv
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalClosed.id x)
((CategoryTheory.ihom x).obj y))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.comp x x y) h)) = h
@[simp]
theorem
CategoryTheory.MonoidalClosed.id_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
(x : C)
(y : C)
[CategoryTheory.Closed x]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor ((CategoryTheory.ihom x).obj y)).inv
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalClosed.id x)
((CategoryTheory.ihom x).obj y))
(CategoryTheory.MonoidalClosed.comp x x y)) = CategoryTheory.CategoryStruct.id ((CategoryTheory.ihom x).obj y)
Left unitality of the enriched structure
@[simp]
theorem
CategoryTheory.MonoidalClosed.comp_id_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
(x : C)
(y : C)
[CategoryTheory.Closed x]
[CategoryTheory.Closed y]
{Z : C}
(h : (CategoryTheory.ihom x).obj y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor ((CategoryTheory.ihom x).obj y)).inv
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.whiskerLeft ((CategoryTheory.ihom x).obj y) (CategoryTheory.MonoidalClosed.id y))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.comp x y y) h)) = h
@[simp]
theorem
CategoryTheory.MonoidalClosed.comp_id
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
(x : C)
(y : C)
[CategoryTheory.Closed x]
[CategoryTheory.Closed y]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor ((CategoryTheory.ihom x).obj y)).inv
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.whiskerLeft ((CategoryTheory.ihom x).obj y) (CategoryTheory.MonoidalClosed.id y))
(CategoryTheory.MonoidalClosed.comp x y y)) = CategoryTheory.CategoryStruct.id ((CategoryTheory.ihom x).obj y)
Right unitality of the enriched structure
theorem
CategoryTheory.MonoidalClosed.assoc_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
(w : C)
(x : C)
(y : C)
(z : C)
[CategoryTheory.Closed w]
[CategoryTheory.Closed x]
[CategoryTheory.Closed y]
{Z : C}
(h : (CategoryTheory.ihom w).obj z ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.associator ((CategoryTheory.ihom w).obj x) ((CategoryTheory.ihom x).obj y)
((CategoryTheory.ihom y).obj z)).inv
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalClosed.comp w x y)
((CategoryTheory.ihom y).obj z))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.comp w y z) h)) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.whiskerLeft ((CategoryTheory.ihom w).obj x)
(CategoryTheory.MonoidalClosed.comp x y z))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.comp w x z) h)
theorem
CategoryTheory.MonoidalClosed.assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
(w : C)
(x : C)
(y : C)
(z : C)
[CategoryTheory.Closed w]
[CategoryTheory.Closed x]
[CategoryTheory.Closed y]
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.associator ((CategoryTheory.ihom w).obj x) ((CategoryTheory.ihom x).obj y)
((CategoryTheory.ihom y).obj z)).inv
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalClosed.comp w x y)
((CategoryTheory.ihom y).obj z))
(CategoryTheory.MonoidalClosed.comp w y z)) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.whiskerLeft ((CategoryTheory.ihom w).obj x)
(CategoryTheory.MonoidalClosed.comp x y z))
(CategoryTheory.MonoidalClosed.comp w x z)
Associativity of the enriched structure