instIsLeftKanExtensionDiscretePUnitFunctorTensorUnitνNatTrans

Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MonoidalCategory.DayFunctor.instIsLeftKanExtensionDiscretePUnitFunctorTensorUnitνNatTrans

English

Natural unit transformations exist through νNatTrans and convolution structure

Русский

Существуют естественные преобразования единицы через νNatTrans и структуру конволюции.

LaTeX

$$$\\nuNatTrans : \\text{Unit transformation} $$$

Lean4

instance : (𝟙_ (C ⊛⥤ V)).functor.IsLeftKanExtension (νNatTrans C V) :=
  isPointwiseLeftKanExtensionUnitUnit C V (C ⊛⥤ V) |>.isLeftKanExtension

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru