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
- binaryCofan_inl : ∀ ⦃A B : C⦄ (c : CategoryTheory.Limits.BinaryCofan A B), CategoryTheory.Limits.IsColimit c → CategoryTheory.Mono (CategoryTheory.Limits.BinaryCofan.inl c)
the left inclusion of a colimit binary cofan is mono
This condition expresses that inclusion morphisms into coproducts are monomorphisms.
Instances
theorem
CategoryTheory.Limits.MonoCoprod.binaryCofan_inr
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{A : C}
{B : C}
[CategoryTheory.Limits.MonoCoprod C]
(c : CategoryTheory.Limits.BinaryCofan A B)
(hc : CategoryTheory.Limits.IsColimit c)
:
instance
CategoryTheory.Limits.MonoCoprod.instMonoCoprodInl
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{A : C}
{B : C}
[CategoryTheory.Limits.MonoCoprod C]
[CategoryTheory.Limits.HasBinaryCoproduct A B]
:
CategoryTheory.Mono CategoryTheory.Limits.coprod.inl
instance
CategoryTheory.Limits.MonoCoprod.instMonoCoprodInr
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{A : C}
{B : C}
[CategoryTheory.Limits.MonoCoprod C]
[CategoryTheory.Limits.HasBinaryCoproduct A B]
:
CategoryTheory.Mono CategoryTheory.Limits.coprod.inr
theorem
CategoryTheory.Limits.MonoCoprod.mono_inl_iff
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{A : C}
{B : C}
{c₁ : CategoryTheory.Limits.BinaryCofan A B}
{c₂ : CategoryTheory.Limits.BinaryCofan A B}
(hc₁ : CategoryTheory.Limits.IsColimit c₁)
(hc₂ : CategoryTheory.Limits.IsColimit c₂)
:
theorem
CategoryTheory.Limits.MonoCoprod.mk'
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
(h : ∀ (A B : C), ∃ c x, CategoryTheory.Mono (CategoryTheory.Limits.BinaryCofan.inl c))
: