convolution₂ — Mathlib

English

Another compatibility lemma for the ι-map on tensor products landing in Day convolution.

Русский

Ещё одно свойство совместимости отображения ι на тензорных произведениях в Day-конволюции.

LaTeX

$$$ (ι C V D).map (f \otimes 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 _ _

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