of_isMonoidalLeftDistrib — Mathlib

English

A category is Cartesian distributive if it is left distributive; the right distributivity follows from symmetry of the Cartesian monoidal structure.

Русский

Категория является декартово распределимой, если она слева распределима; правое распределение следует из симметрии декартовой моноидальной структуры.

LaTeX

$$$\\text{If } IsMonoidalLeftDistrib\\, C \\text{ then } IsCartesianDistributive\\, C$$$

Lean4

/-- To show a category is Cartesian distributive it is enough to show it is left distributive.
The right distributivity is inferred from symmetry of the Cartesian monoidal structure. -/
theorem of_isMonoidalLeftDistrib [IsMonoidalLeftDistrib C] : IsCartesianDistributive C :=
  letI : BraidedCategory C := Nonempty.some inferInstance
  SymmetricCategory.isMonoidalDistrib_of_isMonoidalLeftDistrib

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