convolution₂' — Mathlib

English

Reiteration of the tensor-hom compatibility for ι on Day convolution structure.

Русский

Повторение совместимости тензор-гом для ι в структуре Day-конволюции.

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') ⊗ d'')`
is a (triple) Day convolution of `(ι C V).obj d`, `(ι C V).obj d'` and
`(ι C V).obj d''`. -/
def convolution₂' (d d' d'' : D) : DayConvolution ((ι C V D |>.obj d) ⊛ (ι C V D |>.obj d')) (ι C V D |>.obj d'') :=
  convolution C V D _ _

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