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} [Category.{v, u} C] [MonoidalCategory C] (X : C) : Type (max u v)

An object X is (right) closed if (X ⊗ -) is a left adjoint.

• rightAdj : Functor C C

  a choice of a right adjoint for tensorLeft X

• adj : MonoidalCategory.tensorLeft X ⊣ rightAdj X

  tensorLeft X is a left adjoint

class CategoryTheory.MonoidalClosed (C : Type u) [Category.{v, u} C] [MonoidalCategory C] : Type (max u v)

A monoidal category C is (right) monoidal closed if every object is (right) closed.

• closed (X : C) : Closed X

def CategoryTheory.tensorClosed {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X Y : C} (hX : Closed X) (hY : Closed Y) : Closed (MonoidalCategoryStruct.tensorObj 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

• One or more equations did not get rendered due to their size.

def CategoryTheory.unitClosed {C : Type u} [Category.{v, u} C] [MonoidalCategory C] : Closed (MonoidalCategoryStruct.tensorUnit 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 }

def CategoryTheory.ihom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A : C) [Closed A] : Functor C C

This is the internal hom A ⟶[C] -.

Equations

• CategoryTheory.ihom A = CategoryTheory.Closed.rightAdj A

def CategoryTheory.ihom.adjunction {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A : C) [Closed A] : MonoidalCategory.tensorLeft A ⊣ ihom A

The adjunction between A ⊗ - and A ⟹ -.

Equations

• CategoryTheory.ihom.adjunction A = CategoryTheory.Closed.adj

instance CategoryTheory.ihom.instIsLeftAdjointTensorLeft {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A : C) [Closed A] : (MonoidalCategory.tensorLeft A).IsLeftAdjoint

def CategoryTheory.ihom.ev {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A : C) [Closed A] : (ihom A).comp (MonoidalCategory.tensorLeft A) ⟶ Functor.id C

The evaluation natural transformation.

Equations

• CategoryTheory.ihom.ev A = (CategoryTheory.ihom.adjunction A).counit

def CategoryTheory.ihom.coev {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A : C) [Closed A] : Functor.id C ⟶ (MonoidalCategory.tensorLeft A).comp (ihom A)

The coevaluation natural transformation.

Equations

• CategoryTheory.ihom.coev A = (CategoryTheory.ihom.adjunction A).unit

@[simp]

theorem CategoryTheory.ihom.ihom_adjunction_counit {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A : C) [Closed A] : (adjunction A).counit = ev A

@[simp]

theorem CategoryTheory.ihom.ihom_adjunction_unit {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A : C) [Closed A] : (adjunction A).unit = coev A

@[simp]

theorem CategoryTheory.ihom.ev_naturality {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A : C) [Closed A] {X Y : C} (f : X ⟶ Y) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft A ((ihom A).map f)) ((ev A).app Y) = CategoryStruct.comp ((ev A).app X) f

@[simp]

theorem CategoryTheory.ihom.ev_naturality_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A : C) [Closed A] {X Y : C} (f : X ⟶ Y) {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft A ((ihom A).map f)) (CategoryStruct.comp ((ev A).app Y) h) = CategoryStruct.comp ((ev A).app X) (CategoryStruct.comp f h)

@[simp]

theorem CategoryTheory.ihom.coev_naturality {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A : C) [Closed A] {X Y : C} (f : X ⟶ Y) : CategoryStruct.comp f ((coev A).app Y) = CategoryStruct.comp ((coev A).app X) ((ihom A).map (MonoidalCategoryStruct.whiskerLeft A f))

@[simp]

theorem CategoryTheory.ihom.coev_naturality_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A : C) [Closed A] {X Y : C} (f : X ⟶ Y) {Z : C} (h : (ihom A).obj ((MonoidalCategory.tensorLeft A).obj Y) ⟶ Z) : CategoryStruct.comp f (CategoryStruct.comp ((coev A).app Y) h) = CategoryStruct.comp ((coev A).app X) (CategoryStruct.comp ((ihom A).map (MonoidalCategoryStruct.whiskerLeft A f)) h)

def CategoryTheory.ihom.«term_⟶[_]_» : Lean.TrailingParserDescr

A ⟶[C] B denotes the internal hom from A to B

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.ihom.ev_coev {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A B : C) [Closed A] : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft A ((coev A).app B)) ((ev A).app (MonoidalCategoryStruct.tensorObj A B)) = CategoryStruct.id (MonoidalCategoryStruct.tensorObj A B)

@[simp]

theorem CategoryTheory.ihom.ev_coev_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A B : C) [Closed A] {Z : C} (h : MonoidalCategoryStruct.tensorObj A B ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft A ((coev A).app B)) (CategoryStruct.comp ((ev A).app (MonoidalCategoryStruct.tensorObj A B)) h) = h

@[simp]

theorem CategoryTheory.ihom.coev_ev {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A B : C) [Closed A] : CategoryStruct.comp ((coev A).app ((ihom A).obj B)) ((ihom A).map ((ev A).app B)) = CategoryStruct.id ((ihom A).obj B)

@[simp]

theorem CategoryTheory.ihom.coev_ev_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A B : C) [Closed A] {Z : C} (h : (ihom A).obj B ⟶ Z) : CategoryStruct.comp ((coev A).app ((ihom A).obj B)) (CategoryStruct.comp ((ihom A).map ((ev A).app B)) h) = h

instance CategoryTheory.instPreservesColimitsTensorLeft {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A : C) [Closed A] : Limits.PreservesColimits (MonoidalCategory.tensorLeft A)

def CategoryTheory.MonoidalClosed.curry {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A X Y : C} [Closed A] : (MonoidalCategoryStruct.tensorObj A Y ⟶ X) → (Y ⟶ (ihom A).obj X)

Currying in a monoidal closed category.

Equations

• CategoryTheory.MonoidalClosed.curry = ⇑((CategoryTheory.ihom.adjunction A).homEquiv Y X)

def CategoryTheory.MonoidalClosed.uncurry {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A X Y : C} [Closed A] : (Y ⟶ (ihom A).obj X) → (MonoidalCategoryStruct.tensorObj A Y ⟶ X)

Uncurrying in a monoidal closed category.

Equations

• CategoryTheory.MonoidalClosed.uncurry = ⇑((CategoryTheory.ihom.adjunction A).homEquiv Y X).symm

theorem CategoryTheory.MonoidalClosed.homEquiv_apply_eq {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A X Y : C} [Closed A] (f : MonoidalCategoryStruct.tensorObj A Y ⟶ X) : ((ihom.adjunction A).homEquiv Y X) f = curry f

theorem CategoryTheory.MonoidalClosed.homEquiv_symm_apply_eq {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A X Y : C} [Closed A] (f : Y ⟶ (ihom A).obj X) : ((ihom.adjunction A).homEquiv Y X).symm f = uncurry f

theorem CategoryTheory.MonoidalClosed.curry_natural_left {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A X X' Y : C} [Closed A] (f : X ⟶ X') (g : MonoidalCategoryStruct.tensorObj A X' ⟶ Y) : curry (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft A f) g) = CategoryStruct.comp f (curry g)

theorem CategoryTheory.MonoidalClosed.curry_natural_left_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A X X' Y : C} [Closed A] (f : X ⟶ X') (g : MonoidalCategoryStruct.tensorObj A X' ⟶ Y) {Z : C} (h : (ihom A).obj Y ⟶ Z) : CategoryStruct.comp (curry (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft A f) g)) h = CategoryStruct.comp f (CategoryStruct.comp (curry g) h)

theorem CategoryTheory.MonoidalClosed.curry_natural_right {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A X Y Y' : C} [Closed A] (f : MonoidalCategoryStruct.tensorObj A X ⟶ Y) (g : Y ⟶ Y') : curry (CategoryStruct.comp f g) = CategoryStruct.comp (curry f) ((ihom A).map g)

theorem CategoryTheory.MonoidalClosed.curry_natural_right_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A X Y Y' : C} [Closed A] (f : MonoidalCategoryStruct.tensorObj A X ⟶ Y) (g : Y ⟶ Y') {Z : C} (h : (ihom A).obj Y' ⟶ Z) : CategoryStruct.comp (curry (CategoryStruct.comp f g)) h = CategoryStruct.comp (curry f) (CategoryStruct.comp ((ihom A).map g) h)

theorem CategoryTheory.MonoidalClosed.uncurry_natural_right {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A X Y Y' : C} [Closed A] (f : X ⟶ (ihom A).obj Y) (g : Y ⟶ Y') : uncurry (CategoryStruct.comp f ((ihom A).map g)) = CategoryStruct.comp (uncurry f) g

theorem CategoryTheory.MonoidalClosed.uncurry_natural_right_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A X Y Y' : C} [Closed A] (f : X ⟶ (ihom A).obj Y) (g : Y ⟶ Y') {Z : C} (h : Y' ⟶ Z) : CategoryStruct.comp (uncurry (CategoryStruct.comp f ((ihom A).map g))) h = CategoryStruct.comp (uncurry f) (CategoryStruct.comp g h)

theorem CategoryTheory.MonoidalClosed.uncurry_natural_left {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A X X' Y : C} [Closed A] (f : X ⟶ X') (g : X' ⟶ (ihom A).obj Y) : uncurry (CategoryStruct.comp f g) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft A f) (uncurry g)

theorem CategoryTheory.MonoidalClosed.uncurry_natural_left_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A X X' Y : C} [Closed A] (f : X ⟶ X') (g : X' ⟶ (ihom A).obj Y) {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (uncurry (CategoryStruct.comp f g)) h = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft A f) (CategoryStruct.comp (uncurry g) h)

@[simp]

theorem CategoryTheory.MonoidalClosed.uncurry_curry {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A X Y : C} [Closed A] (f : MonoidalCategoryStruct.tensorObj A X ⟶ Y) : uncurry (curry f) = f

@[simp]

theorem CategoryTheory.MonoidalClosed.curry_uncurry {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A X Y : C} [Closed A] (f : X ⟶ (ihom A).obj Y) : curry (uncurry f) = f

theorem CategoryTheory.MonoidalClosed.curry_eq_iff {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A X Y : C} [Closed A] (f : MonoidalCategoryStruct.tensorObj A Y ⟶ X) (g : Y ⟶ (ihom A).obj X) : curry f = g ↔ f = uncurry g

theorem CategoryTheory.MonoidalClosed.eq_curry_iff {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A X Y : C} [Closed A] (f : MonoidalCategoryStruct.tensorObj A Y ⟶ X) (g : Y ⟶ (ihom A).obj X) : g = curry f ↔ uncurry g = f

theorem CategoryTheory.MonoidalClosed.uncurry_eq {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A X Y : C} [Closed A] (g : Y ⟶ (ihom A).obj X) : uncurry g = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft A g) ((ihom.ev A).app X)

theorem CategoryTheory.MonoidalClosed.curry_eq {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A X Y : C} [Closed A] (g : MonoidalCategoryStruct.tensorObj A Y ⟶ X) : curry g = CategoryStruct.comp ((ihom.coev A).app Y) ((ihom A).map g)

theorem CategoryTheory.MonoidalClosed.curry_injective {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A X Y : C} [Closed A] : Function.Injective curry

theorem CategoryTheory.MonoidalClosed.uncurry_injective {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A X Y : C} [Closed A] : Function.Injective uncurry

theorem CategoryTheory.MonoidalClosed.uncurry_id_eq_ev {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A X : C) [Closed A] : uncurry (CategoryStruct.id ((ihom A).obj X)) = (ihom.ev A).app X

theorem CategoryTheory.MonoidalClosed.curry_id_eq_coev {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A X : C) [Closed A] : curry (CategoryStruct.id (MonoidalCategoryStruct.tensorObj A ((Functor.id C).obj X))) = (ihom.coev A).app X

@[simp]

theorem CategoryTheory.MonoidalClosed.whiskerLeft_curry_ihom_ev_app {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A X : C) {Y : C} [Closed A] (g : MonoidalCategoryStruct.tensorObj A Y ⟶ X) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft A (curry g)) ((ihom.ev A).app X) = g

@[simp]

theorem CategoryTheory.MonoidalClosed.whiskerLeft_curry_ihom_ev_app_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A X : C) {Y : C} [Closed A] (g : MonoidalCategoryStruct.tensorObj A Y ⟶ X) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft A (curry g)) (CategoryStruct.comp ((ihom.ev A).app X) h) = CategoryStruct.comp g h

theorem CategoryTheory.MonoidalClosed.uncurry_ihom_map {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A : C) {Y Y' : C} [Closed A] (g : Y ⟶ Y') : uncurry ((ihom A).map g) = CategoryStruct.comp ((ihom.ev A).app Y) g

def CategoryTheory.MonoidalClosed.unitNatIso {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Closed (MonoidalCategoryStruct.tensorUnit C)] : Functor.id C ≅ ihom (MonoidalCategoryStruct.tensorUnit 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.

def CategoryTheory.MonoidalClosed.pre {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A B : C} [Closed A] [Closed B] (f : B ⟶ A) : ihom A ⟶ ihom B

Pre-compose an internal hom with an external hom.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.MonoidalClosed.id_tensor_pre_app_comp_ev {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A B : C} [Closed A] [Closed B] (f : B ⟶ A) (X : C) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft B ((pre f).app X)) ((ihom.ev B).app X) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f ((ihom A).obj X)) ((ihom.ev A).app X)

@[simp]

theorem CategoryTheory.MonoidalClosed.id_tensor_pre_app_comp_ev_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A B : C} [Closed A] [Closed B] (f : B ⟶ A) (X : C) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft B ((pre f).app X)) (CategoryStruct.comp ((ihom.ev B).app X) h) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f ((ihom A).obj X)) (CategoryStruct.comp ((ihom.ev A).app X) h)

@[simp]

theorem CategoryTheory.MonoidalClosed.uncurry_pre {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A B : C} [Closed A] [Closed B] (f : B ⟶ A) (X : C) : uncurry ((pre f).app X) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f ((ihom A).obj X)) ((ihom.ev A).app X)

theorem CategoryTheory.MonoidalClosed.curry_pre_app {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A B : C} [Closed A] [Closed B] (f : B ⟶ A) {X Y : C} (g : MonoidalCategoryStruct.tensorObj A Y ⟶ X) : CategoryStruct.comp (curry g) ((pre f).app X) = curry (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f Y) g)

theorem CategoryTheory.MonoidalClosed.curry_pre_app_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A B : C} [Closed A] [Closed B] (f : B ⟶ A) {X Y : C} (g : MonoidalCategoryStruct.tensorObj A Y ⟶ X) {Z : C} (h : (ihom B).obj X ⟶ Z) : CategoryStruct.comp (curry g) (CategoryStruct.comp ((pre f).app X) h) = CategoryStruct.comp (curry (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight f Y) g)) h

@[simp]

theorem CategoryTheory.MonoidalClosed.coev_app_comp_pre_app {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A B : C} (X : C) [Closed A] [Closed B] (f : B ⟶ A) : CategoryStruct.comp ((ihom.coev A).app X) ((pre f).app (MonoidalCategoryStruct.tensorObj A X)) = CategoryStruct.comp ((ihom.coev B).app X) ((ihom B).map (MonoidalCategoryStruct.whiskerRight f X))

@[simp]

theorem CategoryTheory.MonoidalClosed.coev_app_comp_pre_app_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A B : C} (X : C) [Closed A] [Closed B] (f : B ⟶ A) {Z : C} (h : (ihom B).obj (MonoidalCategoryStruct.tensorObj A X) ⟶ Z) : CategoryStruct.comp ((ihom.coev A).app X) (CategoryStruct.comp ((pre f).app (MonoidalCategoryStruct.tensorObj A X)) h) = CategoryStruct.comp ((ihom.coev B).app X) (CategoryStruct.comp ((ihom B).map (MonoidalCategoryStruct.whiskerRight f X)) h)

theorem CategoryTheory.MonoidalClosed.uncurry_pre_app {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A B : C} (X : C) {Y : C} [Closed A] [Closed B] (f : Y ⟶ (ihom A).obj X) (g : B ⟶ A) : uncurry (CategoryStruct.comp f ((pre g).app X)) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight g Y) (uncurry f)

theorem CategoryTheory.MonoidalClosed.uncurry_pre_app_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A B : C} (X : C) {Y : C} [Closed A] [Closed B] (f : Y ⟶ (ihom A).obj X) (g : B ⟶ A) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (uncurry (CategoryStruct.comp f ((pre g).app X))) h = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight g Y) (CategoryStruct.comp (uncurry f) h)

@[simp]

theorem CategoryTheory.MonoidalClosed.pre_id {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A : C) [Closed A] : pre (CategoryStruct.id A) = CategoryStruct.id (ihom A)

@[simp]

theorem CategoryTheory.MonoidalClosed.pre_map {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A₁ A₂ A₃ : C} [Closed A₁] [Closed A₂] [Closed A₃] (f : A₁ ⟶ A₂) (g : A₂ ⟶ A₃) : pre (CategoryStruct.comp f g) = CategoryStruct.comp (pre g) (pre f)

theorem CategoryTheory.MonoidalClosed.pre_comm_ihom_map {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {W X Y Z : C} [Closed W] [Closed X] (f : W ⟶ X) (g : Y ⟶ Z) : CategoryStruct.comp ((pre f).app Y) ((ihom W).map g) = CategoryStruct.comp ((ihom X).map g) ((pre f).app Z)

def CategoryTheory.MonoidalClosed.internalHom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [MonoidalClosed C] : Functor Cᵒᵖ (Functor C C)

The internal hom functor given by the monoidal closed structure.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.MonoidalClosed.internalHom_obj {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [MonoidalClosed C] (X : Cᵒᵖ) : internalHom.obj X = ihom (Opposite.unop X)

@[simp]

theorem CategoryTheory.MonoidalClosed.internalHom_map {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [MonoidalClosed C] {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) : internalHom.map f = pre f.unop

noncomputable def CategoryTheory.MonoidalClosed.ofEquiv {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) {G : Functor D C} (adj : F ⊣ G) [F.Monoidal] [F.IsEquivalence] [MonoidalClosed D] : MonoidalClosed C

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.

theorem CategoryTheory.MonoidalClosed.ofEquiv_curry_def {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) {G : Functor D C} (adj : F ⊣ G) [F.Monoidal] [F.IsEquivalence] [MonoidalClosed D] {X Y Z : C} (f : MonoidalCategoryStruct.tensorObj X Y ⟶ Z) : curry f = (adj.homEquiv Y ((ihom (F.obj X)).obj (F.obj Z))) (curry ((adj.toEquivalence.symm.toAdjunction.homEquiv (MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)) Z) (CategoryStruct.comp ((Functor.Monoidal.commTensorLeft F 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} [Category.{v, u} C] [MonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [MonoidalCategory D] (F : Functor C D) {G : Functor D C} (adj : F ⊣ G) [F.Monoidal] [F.IsEquivalence] [MonoidalClosed D] {X Y Z : C} (f : Y ⟶ (ihom X).obj Z) : uncurry f = CategoryStruct.comp ((Functor.Monoidal.commTensorLeft F X).compInverseIso.inv.app Y) ((adj.toEquivalence.symm.toAdjunction.homEquiv ((F.comp (MonoidalCategory.tensorLeft (F.obj X))).obj Y) Z).symm (uncurry ((adj.homEquiv Y ((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} [Category.{v, u} C] [MonoidalCategory C] (x : C) [Closed x] : MonoidalCategoryStruct.tensorUnit C ⟶ (ihom x).obj x

The C-identity morphism 𝟙_ C ⟶ hom(x, x) used to equip C with the structure of a C-category

Equations

• CategoryTheory.MonoidalClosed.id x = CategoryTheory.MonoidalClosed.curry (CategoryTheory.MonoidalCategoryStruct.rightUnitor x).hom

def CategoryTheory.MonoidalClosed.compTranspose {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (x y z : C) [Closed x] [Closed y] : MonoidalCategoryStruct.tensorObj x (MonoidalCategoryStruct.tensorObj ((ihom x).obj y) ((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.

def CategoryTheory.MonoidalClosed.comp {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (x y z : C) [Closed x] [Closed y] : MonoidalCategoryStruct.tensorObj ((ihom x).obj y) ((ihom y).obj z) ⟶ (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

• CategoryTheory.MonoidalClosed.comp x y z = CategoryTheory.MonoidalClosed.curry (CategoryTheory.MonoidalClosed.compTranspose x y z)

theorem CategoryTheory.MonoidalClosed.id_eq {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (x : C) [Closed x] : id x = curry (MonoidalCategoryStruct.rightUnitor x).hom

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} [Category.{v, u} C] [MonoidalCategory C] (x y z : C) [Closed x] [Closed y] : compTranspose x y z = CategoryStruct.comp (MonoidalCategoryStruct.associator x ((ihom x).obj y) ((ihom y).obj z)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight ((ihom.ev x).app y) ((ihom y).obj z)) ((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} [Category.{v, u} C] [MonoidalCategory C] (x y z : C) [Closed x] [Closed y] : comp x y z = curry (compTranspose x y z)

Unfold the definition of comp. This exists to streamline the proof of MonoidalClosed.assoc

The proofs of associativity and unitality use the following outline:

1. Take adjoint transpose on each side of the equality (uncurry_injective)
2. Do whatever rewrites/simps are necessary to apply uncurry_curry
3. Conclude with simp

@[simp]

theorem CategoryTheory.MonoidalClosed.id_comp {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (x y : C) [Closed x] : CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor ((ihom x).obj y)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (id x) ((ihom x).obj y)) (comp x x y)) = CategoryStruct.id ((ihom x).obj y)

Left unitality of the enriched structure

@[simp]

theorem CategoryTheory.MonoidalClosed.id_comp_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (x y : C) [Closed x] {Z : C} (h : (ihom x).obj y ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor ((ihom x).obj y)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (id x) ((ihom x).obj y)) (CategoryStruct.comp (comp x x y) h)) = h

@[simp]

theorem CategoryTheory.MonoidalClosed.comp_id {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (x y : C) [Closed x] [Closed y] : CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor ((ihom x).obj y)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft ((ihom x).obj y) (id y)) (comp x y y)) = CategoryStruct.id ((ihom x).obj y)

Right unitality of the enriched structure

@[simp]

theorem CategoryTheory.MonoidalClosed.comp_id_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (x y : C) [Closed x] [Closed y] {Z : C} (h : (ihom x).obj y ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor ((ihom x).obj y)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft ((ihom x).obj y) (id y)) (CategoryStruct.comp (comp x y y) h)) = h

theorem CategoryTheory.MonoidalClosed.assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (w x y z : C) [Closed w] [Closed x] [Closed y] : CategoryStruct.comp (MonoidalCategoryStruct.associator ((ihom w).obj x) ((ihom x).obj y) ((ihom y).obj z)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (comp w x y) ((ihom y).obj z)) (comp w y z)) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft ((ihom w).obj x) (comp x y z)) (comp w x z)

Associativity of the enriched structure

theorem CategoryTheory.MonoidalClosed.assoc_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (w x y z : C) [Closed w] [Closed x] [Closed y] {Z : C} (h : (ihom w).obj z ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.associator ((ihom w).obj x) ((ihom x).obj y) ((ihom y).obj z)).inv (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (comp w x y) ((ihom y).obj z)) (CategoryStruct.comp (comp w y z) h)) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft ((ihom w).obj x) (comp x y z)) (CategoryStruct.comp (comp w x z) h)

def CategoryTheory.MonoidalClosed.curry' {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X Y : C} [Closed X] (f : X ⟶ Y) : MonoidalCategoryStruct.tensorUnit C ⟶ (ihom X).obj Y

The morphism 𝟙_ C ⟶ (ihom X).obj Y corresponding to a morphism X ⟶ Y.

Equations

• CategoryTheory.MonoidalClosed.curry' f = CategoryTheory.MonoidalClosed.curry (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom f)

def CategoryTheory.MonoidalClosed.uncurry' {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X Y : C} [Closed X] (g : MonoidalCategoryStruct.tensorUnit C ⟶ (ihom X).obj Y) : X ⟶ Y

The morphism X ⟶ Y corresponding to a morphism 𝟙_ C ⟶ (ihom X).obj Y.

Equations

• CategoryTheory.MonoidalClosed.uncurry' g = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv (CategoryTheory.MonoidalClosed.uncurry g)

@[simp]

theorem CategoryTheory.MonoidalClosed.curry'_uncurry' {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X Y : C} [Closed X] (g : MonoidalCategoryStruct.tensorUnit C ⟶ (ihom X).obj Y) : curry' (uncurry' g) = g

curry' and uncurry' are inverse bijections.

@[simp]

theorem CategoryTheory.MonoidalClosed.uncurry'_curry' {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X Y : C} [Closed X] (f : X ⟶ Y) : uncurry' (curry' f) = f

curry' and uncurry' are inverse bijections.

def CategoryTheory.MonoidalClosed.curryHomEquiv' {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X Y : C} [Closed X] : (X ⟶ Y) ≃ (MonoidalCategoryStruct.tensorUnit C ⟶ (ihom X).obj Y)

The bijection (X ⟶ Y) ≃ (𝟙_ C ⟶ (ihom X).obj Y) in a monoidal closed category.

Equations

• CategoryTheory.MonoidalClosed.curryHomEquiv' = { toFun := CategoryTheory.MonoidalClosed.curry', invFun := CategoryTheory.MonoidalClosed.uncurry', left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem CategoryTheory.MonoidalClosed.curryHomEquiv'_symm_apply {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X Y : C} [Closed X] (g : MonoidalCategoryStruct.tensorUnit C ⟶ (ihom X).obj Y) : curryHomEquiv'.symm g = uncurry' g

@[simp]

theorem CategoryTheory.MonoidalClosed.curryHomEquiv'_apply {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X Y : C} [Closed X] (f : X ⟶ Y) : curryHomEquiv' f = curry' f

theorem CategoryTheory.MonoidalClosed.curry'_injective {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X Y : C} [Closed X] {f f' : X ⟶ Y} (h : curry' f = curry' f') : f = f'

theorem CategoryTheory.MonoidalClosed.uncurry'_injective {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X Y : C} [Closed X] {f f' : MonoidalCategoryStruct.tensorUnit C ⟶ (ihom X).obj Y} (h : uncurry' f = uncurry' f') : f = f'

@[simp]

theorem CategoryTheory.MonoidalClosed.curry'_id {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (X : C) [Closed X] : curry' (CategoryStruct.id X) = id X

theorem CategoryTheory.MonoidalClosed.whiskerLeft_curry'_ihom_ev_app {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X Y : C} [Closed X] (f : X ⟶ Y) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X (curry' f)) ((ihom.ev X).app Y) = CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor X).hom f

theorem CategoryTheory.MonoidalClosed.whiskerLeft_curry'_ihom_ev_app_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X Y : C} [Closed X] (f : X ⟶ Y) {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X (curry' f)) (CategoryStruct.comp ((ihom.ev X).app Y) h) = CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor X).hom (CategoryStruct.comp f h)

theorem CategoryTheory.MonoidalClosed.curry'_whiskerRight_comp {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X Y Z : C} [Closed X] [Closed Y] (f : X ⟶ Y) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (curry' f) ((ihom Y).obj Z)) (comp X Y Z) = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor ((ihom Y).obj Z)).hom ((pre f).app Z)

theorem CategoryTheory.MonoidalClosed.curry'_whiskerRight_comp_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X Y Z : C} [Closed X] [Closed Y] (f : X ⟶ Y) {Z✝ : C} (h : (ihom X).obj Z ⟶ Z✝) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (curry' f) ((ihom Y).obj Z)) (CategoryStruct.comp (comp X Y Z) h) = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor ((ihom Y).obj Z)).hom (CategoryStruct.comp ((pre f).app Z) h)

theorem CategoryTheory.MonoidalClosed.whiskerLeft_curry'_comp {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X Y Z : C} [Closed X] [Closed Y] (f : Y ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft ((ihom X).obj Y) (curry' f)) (comp X Y Z) = CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor ((ihom X).obj Y)).hom ((ihom X).map f)

theorem CategoryTheory.MonoidalClosed.whiskerLeft_curry'_comp_assoc {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X Y Z : C} [Closed X] [Closed Y] (f : Y ⟶ Z) {Z✝ : C} (h : (ihom X).obj Z ⟶ Z✝) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft ((ihom X).obj Y) (curry' f)) (CategoryStruct.comp (comp X Y Z) h) = CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor ((ihom X).obj Y)).hom (CategoryStruct.comp ((ihom X).map f) h)

theorem CategoryTheory.MonoidalClosed.curry'_ihom_map {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X Y Z : C} [Closed X] (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryStruct.comp (curry' f) ((ihom X).map g) = curry' (CategoryStruct.comp f g)

theorem CategoryTheory.MonoidalClosed.curry'_comp {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {X Y Z : C} [Closed X] [Closed Y] (f : X ⟶ Y) (g : Y ⟶ Z) : curry' (CategoryStruct.comp f g) = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).inv (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (curry' f) (curry' g)) (comp X Y Z))