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.
a choice of a left adjoint for
tensorLeft X
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
- CategoryTheory.tensorClosed hX hY = { isAdj := CategoryTheory.Adjunction.leftAdjointOfNatIso (CategoryTheory.MonoidalCategory.tensorLeftTensor X Y).symm }
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
- One or more equations did not get rendered due to their size.
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.IsLeftAdjoint.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.tensorHom (CategoryTheory.CategoryStruct.id A)
((CategoryTheory.ihom A).toPrefunctor.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.tensorHom (CategoryTheory.CategoryStruct.id A)
((CategoryTheory.ihom A).toPrefunctor.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).toPrefunctor.obj ((CategoryTheory.MonoidalCategory.tensorLeft A).toPrefunctor.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).toPrefunctor.map
(CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id 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).toPrefunctor.map
(CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id 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]
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id A)
((CategoryTheory.ihom.coev A).app B))
((CategoryTheory.ihom.ev A).app (CategoryTheory.MonoidalCategory.tensorObj A B)) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj A B)
@[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).toPrefunctor.obj B ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.coev A).app ((CategoryTheory.ihom A).toPrefunctor.obj B))
(CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom A).toPrefunctor.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).toPrefunctor.obj B))
((CategoryTheory.ihom A).toPrefunctor.map ((CategoryTheory.ihom.ev A).app B)) = CategoryTheory.CategoryStruct.id ((CategoryTheory.ihom A).toPrefunctor.obj B)
instance
CategoryTheory.instPreservesColimitsTensorLeft
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.MonoidalCategory C]
(A : C)
[CategoryTheory.Closed A]
:
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).toPrefunctor.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).toPrefunctor.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).toPrefunctor.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).toPrefunctor.obj Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalClosed.curry
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id A) f) g))
h = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.curry g) h)
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).toPrefunctor.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')
:
CategoryTheory.MonoidalClosed.curry (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.curry f)
((CategoryTheory.ihom A).toPrefunctor.map g)
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).toPrefunctor.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).toPrefunctor.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).toPrefunctor.obj Y)
{Z : C}
(h : Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.uncurry (CategoryTheory.CategoryStruct.comp f g)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id A) f)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.uncurry g) h)
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).toPrefunctor.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).toPrefunctor.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).toPrefunctor.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).toPrefunctor.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).toPrefunctor.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).toPrefunctor.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).toPrefunctor.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]
:
CategoryTheory.MonoidalClosed.curry
(CategoryTheory.CategoryStruct.id
(CategoryTheory.MonoidalCategory.tensorObj A ((CategoryTheory.Functor.id C).toPrefunctor.obj X))) = (CategoryTheory.ihom.coev A).app X
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.tensorHom (CategoryTheory.CategoryStruct.id B)
((CategoryTheory.MonoidalClosed.pre f).app X))
(CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.ev B).app X) h) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.tensorHom f
(CategoryTheory.CategoryStruct.id ((CategoryTheory.ihom A).toPrefunctor.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.tensorHom (CategoryTheory.CategoryStruct.id B)
((CategoryTheory.MonoidalClosed.pre f).app X))
((CategoryTheory.ihom.ev B).app X) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.tensorHom f
(CategoryTheory.CategoryStruct.id ((CategoryTheory.ihom A).toPrefunctor.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)
:
CategoryTheory.MonoidalClosed.uncurry ((CategoryTheory.MonoidalClosed.pre f).app X) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalCategory.tensorHom f
(CategoryTheory.CategoryStruct.id ((CategoryTheory.ihom A).toPrefunctor.obj X)))
((CategoryTheory.ihom.ev A).app X)
@[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).toPrefunctor.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).toPrefunctor.map
(CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id 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).toPrefunctor.map
(CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id 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).toPrefunctor.map g) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom X).toPrefunctor.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.toPrefunctor.obj X = CategoryTheory.ihom X.unop
@[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.toPrefunctor.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)
[CategoryTheory.IsEquivalence F.toFunctor]
[h : 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)
[CategoryTheory.IsEquivalence F.toFunctor]
[CategoryTheory.MonoidalClosed D]
{X : C}
{Y : C}
{Z : C}
(f : CategoryTheory.MonoidalCategory.tensorObj X Y ⟶ Z)
:
CategoryTheory.MonoidalClosed.curry f = ((CategoryTheory.Functor.adjunction F.toFunctor).homEquiv Y
((CategoryTheory.ihom (F.toPrefunctor.obj X)).toPrefunctor.obj
((CategoryTheory.Functor.inv (CategoryTheory.Functor.inv F.toFunctor)).toPrefunctor.obj Z)))
(CategoryTheory.MonoidalClosed.curry
(((CategoryTheory.Functor.adjunction (CategoryTheory.Functor.inv F.toFunctor)).homEquiv
(CategoryTheory.MonoidalCategory.tensorObj (F.toPrefunctor.obj X) (F.toPrefunctor.obj Y)) Z)
(CategoryTheory.CategoryStruct.comp
((CategoryTheory.Iso.compInvIso (CategoryTheory.MonoidalFunctor.commTensorLeft F 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
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)
[CategoryTheory.IsEquivalence F.toFunctor]
[CategoryTheory.MonoidalClosed D]
{X : C}
{Y : C}
{Z : C}
(f : Y ⟶ (CategoryTheory.ihom X).toPrefunctor.obj Z)
:
CategoryTheory.MonoidalClosed.uncurry f = CategoryTheory.CategoryStruct.comp
((CategoryTheory.Iso.compInvIso (CategoryTheory.MonoidalFunctor.commTensorLeft F X)).inv.app Y)
(((CategoryTheory.Functor.adjunction (CategoryTheory.Functor.inv F.toFunctor)).homEquiv
(CategoryTheory.MonoidalCategory.tensorObj (F.toPrefunctor.obj X) (F.toPrefunctor.obj Y)) Z).symm
(CategoryTheory.MonoidalClosed.uncurry
(((CategoryTheory.Functor.adjunction F.toFunctor).homEquiv Y
((CategoryTheory.ihom (F.toPrefunctor.obj X)).toPrefunctor.obj (F.toPrefunctor.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.)