leftKanExtension — Mathlib

English

For DayConvolution F G, the convolution F ⊛ G is a left Kan extension of the unit F G with respect to the tensor product, expressing the universal property of the Day convolution.

Русский

Для DayConvolution F G конволюция F ⊛ G является левой Кан-расширением единицы F G по отношению к тензорному произведению, выражая универсальное свойство Day-конволюции.

LaTeX

$$$ (F \\ ⊛ G). \\text{IsLeftKanExtension} (\\text{unit } F G) $$$

Lean4

instance leftKanExtension [DayConvolution F G] : (F ⊛ G).IsLeftKanExtension (unit F G) :=
  isPointwiseLeftKanExtensionUnit F G |>.isLeftKanExtension

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