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.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_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
@[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)
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.)