convolutionUnit — Mathlib

English

Construction providing a Lawful Day convolution structure from given data.

Русский

Построение законной Day-конволюционной структуры из заданных данных.

LaTeX

$$$ \text{mkLawfulDayConvolutionMonoidalCategoryStruct }(C,V,D) : \text{LawfulDayConvolutionMonoidalCategoryStruct } C V D $$$

Lean4

/-- In a `LawfulDayConvolutionMonoidalCategoryStruct`, `ι.obj (𝟙_ D)`
is a Day convolution unit`. -/
def convolutionUnit : DayConvolutionUnit (ι C V D |>.obj <| 𝟙_ D)
    where
  can := unitUnit _ _ _
  isPointwiseLeftKanExtensionCan := isPointwiseLeftKanExtensionUnitUnit _ _ _

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