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 #
- The coproduct coprojections are monic in a cartesian distributive category.
TODO #
Every cartesian distributive category is finitary distributive, meaning that the left tensor product functor
X ⊗ -
preserves all finite coproducts.Show that any extensive distributive category can be embedded into a topos.
References #
A category C
with finite products is cartesian distributive if is monoidal distributive
with respect to the cartesian monoidal structure.
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.