mathlib documentation

category_theory.limits.mono_coprod

Categories where inclusions into coproducts are monomorphisms #

If C is a category, the class mono_coprod C expresses that left inclusions A ⟶ A ⨿ B are monomorphisms when has_coproduct 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 mono_coprod, see https://ncatlab.org/toddtrimble/published/distributivity+implies+monicity+of+coproduct+inclusions

@[class]

This condition expresses that inclusion morphisms into coproducts are monomorphisms.

Instances of this typeclass