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

Given a category with chosen finite products, the cartesian monoidal structure is provided by the instance monoidalOfChosenFiniteProducts. A cartesian distributive category is then defined as a monoidal distributive category with respect to this monoidal structure.

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

• J.R.B.Cockett, Introduction to distributive categories, 1993
• Carboni et al, Introduction to extensive and distributive categories

@[reducible, inline]

abbrev CategoryTheory.IsCartesianDistributive (C : Type u) [Category.{v, u} C] [ChosenFiniteProducts C] [Limits.HasBinaryCoproducts C] : Prop

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

Equations

• CategoryTheory.IsCartesianDistributive C = CategoryTheory.IsMonoidalDistrib C

theorem CategoryTheory.IsCartesianDistributive.of_isMonoidalLeftDistrib (C : Type u) [Category.{v, u} C] [ChosenFiniteProducts C] [Limits.HasBinaryCoproducts C] [IsMonoidalLeftDistrib C] : IsCartesianDistributive C

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.

instance CategoryTheory.IsCartesianDistributive.monoCoprod (C : Type u) [Category.{v, u} C] [ChosenFiniteProducts C] [Limits.HasBinaryCoproducts C] [IsCartesianDistributive C] : Limits.MonoCoprod C

The coproduct coprojections are monic in a cartesian distributive category.