Documentation

Mathlib.CategoryTheory.Distributive.Cartesian

Distributive categories #

Main definitions #

A category C with finite products and binary coproducts is called distributive if the canonical distributivity morphism (X ⨯ Y) ⨿ (X ⨯ Z) ⟶ X ⨯ (Y ⨿ Z) is an isomorphism for all objects X, Y, and Z in C.

Implementation Details #

A cartesian distributive category is defined as a cartesian monoidal category which is monoidal distributive.

Main results #

TODO #

References #

@[reducible, inline]

A category C with finite products is cartesian distributive if is monoidal distributive with respect to the cartesian monoidal structure.

Equations
Instances For

    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.

    The coproduct coprojections are monic in a cartesian distributive category.