of_isIso_coprodComparisonTensorLeft

English

The forward direction of the left distributivity isomorphism is the canonical coprod morphism coprod.desc (...).

Русский

Прямая часть изоморфизма левого распределения равна каноническому морфизму coprod.desc (...).

LaTeX

$$$(\\partial_L X Y Z).\\mathrm{hom} = \\mathrm{coprod.desc} (\\_ ◁ \\mathrm{coprod.inl}) (\\_ ◁ \\mathrm{coprod.inr})$$$

Lean4

theorem of_isIso_coprodComparisonTensorLeft [i : ∀ {X Y Z : C}, IsIso (coprodComparison (tensorLeft X) Y Z)] :
    IsMonoidalLeftDistrib C where
  preservesBinaryCoproducts_tensorLeft X := preservesBinaryCoproducts_of_isIso_coprodComparison (tensorLeft X)

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