of_endofunctors — Mathlib

English

The category of endofunctors with composition as tensor product inherits left distributivity from the base category provided the base category has binary coproducts.

Русский

Категория концевых функторов с умножением как тензорная операция наследует левое распределение от базовой категории при условии наличия бинарных копроизведений.

LaTeX

$$IsMonoidalLeftDistrib (C ⥤ C)$$

Lean4

/-- The monoidal structure on the category of endofunctors is left distributive. -/
instance of_endofunctors : IsMonoidalLeftDistrib (C ⥤ C) where
  preservesBinaryCoproducts_tensorLeft
    F := inferInstanceAs (PreservesColimitsOfShape _ ((Functor.whiskeringLeft C C C).obj F))

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