@[reducible, inline]

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

Equations

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

@[reducible, inline]

abbrev CategoryTheory.Enriched.Ehom (V : Type u) [CategoryTheory.Category.{u₁, u} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.MonoidalClosed V] (C : Type v) [CategoryTheory.EnrichedCategory V C] (x : C) (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) [CategoryTheory.Category.{u₁, u} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.MonoidalClosed V] (x : V) (y : V) : CategoryTheory.Enriched.Ihom V x y = CategoryTheory.Enriched.Ehom V V x y

Equations

• ⋯ = ⋯

structure CategoryTheory.Enriched.Precotensor {V : Type u} [CategoryTheory.Category.{u₁, u} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.MonoidalClosed V] {C : Type v} [CategoryTheory.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 ⟶ CategoryTheory.Enriched.Ehom V C self.obj x

def CategoryTheory.Enriched.Precotensor.coneNatTrans {V : Type u} [CategoryTheory.Category.{u₁, u} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.SymmetricCategory V] [CategoryTheory.MonoidalClosed V] {C : Type v} [CategoryTheory.EnrichedCategory V C] {v : V} {x : C} (vx : CategoryTheory.Enriched.Precotensor v x) (y : C) : CategoryTheory.Enriched.Ehom V C y vx.obj ⟶ CategoryTheory.Enriched.Ihom V v (CategoryTheory.Enriched.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} [CategoryTheory.Category.{u₁, u} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.SymmetricCategory V] [CategoryTheory.MonoidalClosed V] {C : Type v} [CategoryTheory.EnrichedCategory V C] {v : V} {x : C} (vx : CategoryTheory.Enriched.Precotensor v x) (y : C) : CategoryTheory.MonoidalClosed.uncurry (vx.coneNatTrans y) = CategoryTheory.CategoryStruct.comp (β_ v (CategoryTheory.EnrichedCategory.Hom y vx.obj)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (CategoryTheory.EnrichedCategory.Hom y vx.obj) vx.cone) (CategoryTheory.eComp V y vx.obj x))

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

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

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

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

theorem CategoryTheory.Enriched.Cotensor.NatTransInv_NatTrans_eq {V : Type u} [CategoryTheory.Category.{u₁, u} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.SymmetricCategory V] [CategoryTheory.MonoidalClosed V] {C : Type v} [CategoryTheory.EnrichedCategory V C] {v : V} {x : C} (self : CategoryTheory.Enriched.Cotensor v x) (y : C) : CategoryTheory.CategoryStruct.comp (self.coneNatTransInv y) (self.coneNatTrans y) = CategoryTheory.CategoryStruct.id (CategoryTheory.Enriched.Ihom V v (CategoryTheory.Enriched.Ehom V C y x))

theorem CategoryTheory.Enriched.Cotensor.NatTrans_NatTransInv_eq {V : Type u} [CategoryTheory.Category.{u₁, u} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.SymmetricCategory V] [CategoryTheory.MonoidalClosed V] {C : Type v} [CategoryTheory.EnrichedCategory V C] {v : V} {x : C} (self : CategoryTheory.Enriched.Cotensor v x) (y : C) : CategoryTheory.CategoryStruct.comp (self.coneNatTrans y) (self.coneNatTransInv y) = CategoryTheory.CategoryStruct.id (CategoryTheory.Enriched.Ehom V C y self.obj)

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

def CategoryTheory.Enriched.Cotensor.postcompose (V : Type u) [CategoryTheory.Category.{u₁, u} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.SymmetricCategory V] [CategoryTheory.MonoidalClosed V] {C : Type v} [CategoryTheory.EnrichedCategory V C] {x : C} {y : C} {v : V} (vx : CategoryTheory.Enriched.Cotensor v x) (vy : CategoryTheory.Enriched.Cotensor v y) : CategoryTheory.Enriched.Ehom V C x y ⟶ CategoryTheory.Enriched.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) [CategoryTheory.Category.{u₁, u} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.SymmetricCategory V] [CategoryTheory.MonoidalClosed V] {C : Type v} [CategoryTheory.EnrichedCategory V C] {x : C} {y : C} {v : V} (vx : CategoryTheory.Enriched.Cotensor v x) (vy : CategoryTheory.Enriched.Cotensor v y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Enriched.Cotensor.postcompose V vx vy) (vy.coneNatTrans vx.obj) = CategoryTheory.MonoidalClosed.curry (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight vx.cone (CategoryTheory.EnrichedCategory.Hom x y)) (CategoryTheory.eComp V vx.obj x y))

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

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

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

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

def CategoryTheory.Enriched.Cotensor.IhomPrecompose (V : Type u) [CategoryTheory.Category.{u₁, u} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.SymmetricCategory V] [CategoryTheory.MonoidalClosed V] {C : Type v} [CategoryTheory.EnrichedCategory V C] {x : C} {w : V} {v : V} (wx : CategoryTheory.Enriched.Cotensor w x) (vx : CategoryTheory.Enriched.Cotensor v x) : CategoryTheory.Enriched.Ihom V w v ⟶ CategoryTheory.Enriched.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) [CategoryTheory.Category.{u₁, u} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.SymmetricCategory V] [CategoryTheory.MonoidalClosed V] {C : Type v} [CategoryTheory.EnrichedCategory V C] {x : C} {w : V} {v : V} (wx : CategoryTheory.Enriched.Cotensor w x) (vx : CategoryTheory.Enriched.Cotensor v x) : CategoryTheory.Enriched.Ehom V V w v ⟶ CategoryTheory.Enriched.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) [CategoryTheory.Category.{u₁, u} V] [CategoryTheory.MonoidalCategory V] [CategoryTheory.SymmetricCategory V] [CategoryTheory.MonoidalClosed V] {C : Type v} [CategoryTheory.EnrichedCategory V C] {x : C} {w : V} {v : V} (wx : CategoryTheory.Enriched.Cotensor w x) (vx : CategoryTheory.Enriched.Cotensor v x) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Enriched.Cotensor.IhomPrecompose V wx vx) (wx.coneNatTrans vx.obj) = (CategoryTheory.ihom w).map vx.cone

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

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

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

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

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

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

Naturality of postcomposition with precoposition

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

• cotensor : (v : V) → (x : C) → CategoryTheory.Enriched.Cotensor v x

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

Equations

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