of_isIso_coprodComparisonTensorRight

English

If, for every X,Y,Z, the coprodComparison map from (tensorRight X) to (Y,Z) is an isomorphism, then the monoidal category is right distributive.

Русский

Если для любых X,Y,Z отображение coprodComparison (tensorRight X) Y Z является изоморфизмом, то монодальная категория правая распределительная.

LaTeX

$$$\\forall X,Y,Z, IsIso(\\operatorname{coprodComparison}(\\otimes_{R} X) Y Z) \\Rightarrow IsMonoidalRightDistrib C$$$

Lean4

theorem of_isIso_coprodComparisonTensorRight [i : ∀ {X Y Z : C}, IsIso (coprodComparison (tensorRight X) Y Z)] :
    IsMonoidalRightDistrib C where
  preservesBinaryCoproducts_tensorRight _ := ⟨preservesBinaryCoproducts_of_isIso_coprodComparison _ |>.preservesColimit⟩

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