mathlib3 documentation


Categories where inclusions into coproducts are monomorphisms #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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


This condition expresses that inclusion morphisms into coproducts are monomorphisms.

Instances of this typeclass