English
An instance-level left Kan extension property for the product of DayConvolutions with an external product, ensuring the left Kan extension structure is preserved under external product with a fixed functor.
Русский
Свойство левого Кан-расширения для произведения DayConvolution с внешним произведением, сохраняющее структуру левого Кан-расширения при внешнем произведении с фиксированным функтором.
LaTeX
$$$ (F ⊠ G) ⊛ H \\text{ IsLeftKanExtension } | extensionUnitRight (G ⊛ H) (unit G H) F$$$
Lean4
instance : (U ⊠ F).IsLeftKanExtension <| extensionUnitLeft U (φ U) F :=
isPointwiseLeftKanExtensionExtensionUnitLeft U (φ U) F isPointwiseLeftKanExtensionCan |>.isLeftKanExtension
