convolution — Mathlib

English

Compatibility of the induced ι-map with tensoring in the Day convolution context; maps commute with tensoring.

Русский

Совместимость отображения ι с тензоризацией в контексте Day-конволюции; отображения commute с тензоризацией.

LaTeX

$$$ (ι C V D).map (f \otimes_ m f') = DayConvolution.map ((ι C V D).map f) ((ι C V D).map f') $$$

Lean4

/-- In a `LawfulDayConvolutionMonoidalCategoryStruct`, `ι.obj (d ⊗ d')` is a
Day convolution of `(ι C V).obj d` and `(ι C V).d'`. -/
def convolution (d d' : D) : DayConvolution (ι C V D |>.obj d) (ι C V D |>.obj d')
    where
  convolution := (ι C V D).obj (d ⊗ d')
  unit := convolutionExtensionUnit C V d d'
  isPointwiseLeftKanExtensionUnit := isPointwiseLeftKanExtensionConvolutionExtensionUnit d d'

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