@[reducible, inline]

abbrev CategoryTheory.Enriched.Ihom (V : Type u) [Category.{u₁, u} V] [MonoidalCategory V] [MonoidalClosed V] (x y : V) : V

Equations

• CategoryTheory.Enriched.Ihom V x y = (CategoryTheory.ihom x).obj y

@[reducible, inline]

abbrev CategoryTheory.Enriched.Ehom (V : Type u) [Category.{u₁, u} V] [MonoidalCategory V] [MonoidalClosed V] (C : Type v) [EnrichedCategory V C] (x y : C) : V

Equations

• CategoryTheory.Enriched.Ehom V C x y = CategoryTheory.EnrichedCategory.Hom x y

def CategoryTheory.Enriched.Ihom_Ehom_eq (V : Type u) [Category.{u₁, u} V] [MonoidalCategory V] [MonoidalClosed V] (x y : V) : Ihom V x y = Ehom V V x y

Equations

• ⋯ = ⋯

structure CategoryTheory.Enriched.Precotensor {V : Type u} [Category.{u₁, u} V] [MonoidalCategory V] [MonoidalClosed V] {C : Type v} [EnrichedCategory V C] (v : V) (x : C) : Type (max u₁ v)

The structure of the cotensoring of x : C by v : V

• obj : C
• cone : v ⟶ Ehom V C self.obj x

def CategoryTheory.Enriched.Precotensor.coneNatTrans {V : Type u} [Category.{u₁, u} V] [MonoidalCategory V] [SymmetricCategory V] [MonoidalClosed V] {C : Type v} [EnrichedCategory V C] {v : V} {x : C} (vx : Precotensor v x) (y : C) : Ehom V C y vx.obj ⟶ Ihom V v (Ehom V C y x)

The adjoint tranpose of precotensor_eval

Equations

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

theorem CategoryTheory.Enriched.Precotensor.coneNatTrans_eq {V : Type u} [Category.{u₁, u} V] [MonoidalCategory V] [SymmetricCategory V] [MonoidalClosed V] {C : Type v} [EnrichedCategory V C] {v : V} {x : C} (vx : Precotensor v x) (y : C) : MonoidalClosed.uncurry (vx.coneNatTrans y) = CategoryStruct.comp (β_ v (EnrichedCategory.Hom y vx.obj)).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (EnrichedCategory.Hom y vx.obj) vx.cone) (eComp V y vx.obj x))

theorem CategoryTheory.Enriched.Precotensor.coneNatTrans_braid_eq {V : Type u} [Category.{u₁, u} V] [MonoidalCategory V] [SymmetricCategory V] [MonoidalClosed V] {C : Type v} [EnrichedCategory V C] {v : V} {x : C} (vx : Precotensor v x) (y : C) : CategoryStruct.comp (β_ (Ehom V C y vx.obj) v).hom (MonoidalClosed.uncurry (vx.coneNatTrans y)) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (EnrichedCategory.Hom y vx.obj) vx.cone) (eComp V y vx.obj x)

structure CategoryTheory.Enriched.Cotensor {V : Type u} [Category.{u₁, u} V] [MonoidalCategory V] [SymmetricCategory V] [MonoidalClosed V] {C : Type v} [EnrichedCategory V C] (v : V) (x : C) extends CategoryTheory.Enriched.Precotensor v x : Type (max u₁ v)

A Cotensor is a Precotensor such that coneNatTransInv is an inverse to coneNatTrans.

• obj : C
• cone : v ⟶ Ehom V C self.obj x
• coneNatTransInv (y : C) : Ihom V v (Ehom V C y x) ⟶ Ehom V C y self.obj
• NatTransInv_NatTrans_eq (y : C) : CategoryStruct.comp (self.coneNatTransInv y) (self.coneNatTrans y) = CategoryStruct.id (Ihom V v (Ehom V C y x))
• NatTrans_NatTransInv_eq (y : C) : CategoryStruct.comp (self.coneNatTrans y) (self.coneNatTransInv y) = CategoryStruct.id (Ehom V C y self.obj)

instance CategoryTheory.Enriched.instIsIsoConeNatTransInv {V : Type u} [Category.{u₁, u} V] [MonoidalCategory V] [SymmetricCategory V] [MonoidalClosed V] {C : Type v} [EnrichedCategory V C] {v : V} {x : C} {vx : Cotensor v x} {y : C} : IsIso (vx.coneNatTransInv y)

instance CategoryTheory.Enriched.instIsIsoConeNatTrans {V : Type u} [Category.{u₁, u} V] [MonoidalCategory V] [SymmetricCategory V] [MonoidalClosed V] {C : Type v} [EnrichedCategory V C] {v : V} {x : C} {vx : Cotensor v x} {y : C} : IsIso (vx.coneNatTrans y)

def CategoryTheory.Enriched.Cotensor.postcompose (V : Type u) [Category.{u₁, u} V] [MonoidalCategory V] [SymmetricCategory V] [MonoidalClosed V] {C : Type v} [EnrichedCategory V C] {x y : C} {v : V} (vx : Cotensor v x) (vy : Cotensor v y) : Ehom V C x y ⟶ Ehom V C vx.obj vy.obj

Equations

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

theorem CategoryTheory.Enriched.Cotensor.postcompose_coneNatTrans_eq (V : Type u) [Category.{u₁, u} V] [MonoidalCategory V] [SymmetricCategory V] [MonoidalClosed V] {C : Type v} [EnrichedCategory V C] {x y : C} {v : V} (vx : Cotensor v x) (vy : Cotensor v y) : CategoryStruct.comp (postcompose V vx vy) (vy.coneNatTrans vx.obj) = MonoidalClosed.curry (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight vx.cone (EnrichedCategory.Hom x y)) (eComp V vx.obj x y))

theorem CategoryTheory.Enriched.Cotensor.uncurry_postcompose_coneNatTrans_eq (V : Type u) [Category.{u₁, u} V] [MonoidalCategory V] [SymmetricCategory V] [MonoidalClosed V] {C : Type v} [EnrichedCategory V C] {x y : C} {v : V} (vx : Cotensor v x) (vy : Cotensor v y) : MonoidalClosed.uncurry (CategoryStruct.comp (postcompose V vx vy) (vy.coneNatTrans vx.obj)) = CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight vx.cone (EnrichedCategory.Hom x y)) (eComp V vx.obj x y)

theorem CategoryTheory.Enriched.Cotensor.postcompose_selfEval_comp_eq (V : Type u) [Category.{u₁, u} V] [MonoidalCategory V] [SymmetricCategory V] [MonoidalClosed V] {C : Type v} [EnrichedCategory V C] {x y : C} {v : V} (vx : Cotensor v x) (vy : Cotensor v y) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (postcompose V vx vy) v) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (Ehom V C vx.obj vy.obj) vy.cone) (eComp V vx.obj vy.obj y)) = CategoryStruct.comp (β_ (EnrichedCategory.Hom x y) v).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight vx.cone (EnrichedCategory.Hom x y)) (eComp V vx.obj x y))

theorem CategoryTheory.Enriched.Cotensor.postcompose_comp_eq (V : Type u) [Category.{u₁, u} V] [MonoidalCategory V] [SymmetricCategory V] [MonoidalClosed V] {C : Type v} [EnrichedCategory V C] {x y z : C} {v : V} (vx : Cotensor v x) (vy : Cotensor v y) (vz : Cotensor v z) : CategoryStruct.comp (eComp V x y z) (postcompose V vx vz) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (postcompose V vx vy) (postcompose V vy vz)) (eComp V vx.obj vy.obj vz.obj)

theorem CategoryTheory.Enriched.Cotensor.postcompose_id_eq (V : Type u) [Category.{u₁, u} V] [MonoidalCategory V] [SymmetricCategory V] [MonoidalClosed V] {C : Type v} [EnrichedCategory V C] {x : C} {v : V} (vx : Cotensor v x) : CategoryStruct.comp (eId V x) (postcompose V vx vx) = eId V vx.obj

def CategoryTheory.Enriched.Cotensor.IhomPrecompose (V : Type u) [Category.{u₁, u} V] [MonoidalCategory V] [SymmetricCategory V] [MonoidalClosed V] {C : Type v} [EnrichedCategory V C] {x : C} {w v : V} (wx : Cotensor w x) (vx : Cotensor v x) : Ihom V w v ⟶ Ehom V C vx.obj wx.obj

Equations

• CategoryTheory.Enriched.Cotensor.IhomPrecompose V wx vx = CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom w).map vx.cone) (wx.coneNatTransInv vx.obj)

def CategoryTheory.Enriched.Cotensor.EhomPrecompose (V : Type u) [Category.{u₁, u} V] [MonoidalCategory V] [SymmetricCategory V] [MonoidalClosed V] {C : Type v} [EnrichedCategory V C] {x : C} {w v : V} (wx : Cotensor w x) (vx : Cotensor v x) : Ehom V V w v ⟶ Ehom V C vx.obj wx.obj

Equations

• CategoryTheory.Enriched.Cotensor.EhomPrecompose V wx vx = CategoryTheory.Enriched.Cotensor.IhomPrecompose V wx vx

theorem CategoryTheory.Enriched.Cotensor.IhomPrecompose_coneNatTrans_eq (V : Type u) [Category.{u₁, u} V] [MonoidalCategory V] [SymmetricCategory V] [MonoidalClosed V] {C : Type v} [EnrichedCategory V C] {x : C} {w v : V} (wx : Cotensor w x) (vx : Cotensor v x) : CategoryStruct.comp (IhomPrecompose V wx vx) (wx.coneNatTrans vx.obj) = (ihom w).map vx.cone

theorem CategoryTheory.Enriched.Cotensor.EhomPrecompose_coneNatTrans_eq (V : Type u) [Category.{u₁, u} V] [MonoidalCategory V] [SymmetricCategory V] [MonoidalClosed V] {C : Type v} [EnrichedCategory V C] {x : C} {w v : V} (wx : Cotensor w x) (vx : Cotensor v x) : CategoryStruct.comp (EhomPrecompose V wx vx) (wx.coneNatTrans vx.obj) = (ihom w).map vx.cone

theorem CategoryTheory.Enriched.Cotensor.IhomPrecompose_selfEval_comp_eq (V : Type u) [Category.{u₁, u} V] [MonoidalCategory V] [SymmetricCategory V] [MonoidalClosed V] {C : Type v} [EnrichedCategory V C] {x : C} {w v : V} (wx : Cotensor w x) (vx : Cotensor v x) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (IhomPrecompose V wx vx) w) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (Ehom V C vx.obj wx.obj) wx.cone) (eComp V vx.obj wx.obj x)) = CategoryStruct.comp (β_ ((ihom w).obj v) w).hom (CategoryStruct.comp ((ihom.ev w).app v) vx.cone)

theorem CategoryTheory.Enriched.Cotensor.EhomPrecompose_selfEval_comp_eq (V : Type u) [Category.{u₁, u} V] [MonoidalCategory V] [SymmetricCategory V] [MonoidalClosed V] {C : Type v} [EnrichedCategory V C] {x : C} {w v : V} (wx : Cotensor w x) (vx : Cotensor v x) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight (EhomPrecompose V wx vx) w) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft (Ehom V C vx.obj wx.obj) wx.cone) (eComp V vx.obj wx.obj x)) = CategoryStruct.comp (β_ ((ihom w).obj v) w).hom (CategoryStruct.comp ((ihom.ev w).app v) vx.cone)

theorem CategoryTheory.Enriched.Cotensor.precompose_comp_eq (V : Type u) [Category.{u₁, u} V] [MonoidalCategory V] [SymmetricCategory V] [MonoidalClosed V] {C : Type v} [EnrichedCategory V C] {x : C} {u v w : V} (ux : Cotensor u x) (vx : Cotensor v x) (wx : Cotensor w x) : CategoryStruct.comp (eComp V u v w) (EhomPrecompose V ux wx) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (EhomPrecompose V ux vx) (EhomPrecompose V vx wx)) (CategoryStruct.comp (β_ (Ehom V C vx.obj ux.obj) (Ehom V C wx.obj vx.obj)).hom (eComp V wx.obj vx.obj ux.obj))

theorem CategoryTheory.Enriched.Cotensor.precompose_id_eq (V : Type u) [Category.{u₁, u} V] [MonoidalCategory V] [SymmetricCategory V] [MonoidalClosed V] {C : Type v} [EnrichedCategory V C] {x : C} {v : V} (vx : Cotensor v x) : CategoryStruct.comp (eId V v) (EhomPrecompose V vx vx) = eId V vx.obj

theorem CategoryTheory.Enriched.Cotensor.post_pre_eq_pre_post (V : Type u) [Category.{u₁, u} V] [MonoidalCategory V] [SymmetricCategory V] [MonoidalClosed V] {C : Type v} [EnrichedCategory V C] {x y : C} {w v : V} (wx : Cotensor w x) (wy : Cotensor w y) (vx : Cotensor v x) (vy : Cotensor v y) : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (EhomPrecompose V wx vx) (postcompose V wx wy)) (eComp V vx.obj wx.obj wy.obj) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom (EhomPrecompose V wy vy) (postcompose V vx vy)) (CategoryStruct.comp (β_ (Ehom V C vy.obj wy.obj) (Ehom V C vx.obj vy.obj)).hom (eComp V vx.obj vy.obj wy.obj))

Naturality of postcomposition with precoposition

class CategoryTheory.Enriched.Cotensor.CotensoredCategory (V : Type u) [Category.{u₁, u} V] [MonoidalCategory V] [MonoidalClosed V] [SymmetricCategory V] (C : Type v) [EnrichedCategory V C] : Type (max (max u u₁) v)

• cotensor (v : V) (x : C) : Cotensor v x

def CategoryTheory.Enriched.Cotensor.cotensor_bifunc (V : Type u) [Category.{u₁, u} V] [MonoidalCategory V] [SymmetricCategory V] [MonoidalClosed V] {C : Type v} [EnrichedCategory V C] [CotensoredCategory V C] : EnrichedFunctor V (Vᵒᵖ ⊗[V] C) C

Equations

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