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
https://ncatlab.org/toddtrimble/published/distributivity+implies+monicity+of+coproduct+inclusions
@[class]
- binary_cofan_inl : ∀ ⦃A B : C⦄ (c : category_theory.limits.binary_cofan A B), category_theory.limits.is_colimit c → category_theory.mono c.inl
This condition expresses that inclusion morphisms into coproducts are monomorphisms.
Instances of this typeclass
@[protected, instance]
theorem
category_theory.limits.mono_coprod.binary_cofan_inr
{C : Type u_1}
[category_theory.category C]
{A B : C}
[category_theory.limits.mono_coprod C]
(c : category_theory.limits.binary_cofan A B)
(hc : category_theory.limits.is_colimit c) :
@[protected, instance]
@[protected, instance]
theorem
category_theory.limits.mono_coprod.mono_inl_iff
{C : Type u_1}
[category_theory.category C]
{A B : C}
{c₁ c₂ : category_theory.limits.binary_cofan A B}
(hc₁ : category_theory.limits.is_colimit c₁)
(hc₂ : category_theory.limits.is_colimit c₂) :
theorem
category_theory.limits.mono_coprod.mk'
{C : Type u_1}
[category_theory.category C]
(h : ∀ (A B : C), ∃ (c : category_theory.limits.binary_cofan A B) (hc : category_theory.limits.is_colimit c), category_theory.mono c.inl) :
@[protected, instance]