Documentation

Mathlib.CategoryTheory.Limits.MonoCoprod

Categories where inclusions into coproducts are monomorphisms #

If C is a category, the class MonoCoprod C expresses that left inclusions A ⟶ A ⨿ B are monomorphisms when HasCoproduct A B is satisfied. If it is so, it is shown that right inclusions are also monomorphisms.

TODO @joelriou: show that if X : I → C and ι : J → I is an injective map, then the canonical morphism ∐ (X ∘ ι) ⟶ ∐ X is a monomorphism.

TODO: define distributive categories, and show that they satisfy MonoCoprod, see https://ncatlab.org/toddtrimble/published/distributivity+implies+monicity+of+coproduct+inclusions

This condition expresses that inclusion morphisms into coproducts are monomorphisms.

Instances