# 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.

More generally, we deduce that when suitable coproducts exists, then if X : I → C and ι : J → I is an injective map, then the canonical morphism ∐ (X ∘ ι) ⟶ ∐ X is a monomorphism. It also follows that for any i : I, Sigma.ι X i : X i ⟶ ∐ 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.

• binaryCofan_inl : ∀ ⦃A B : C⦄ (c : ),

the left inclusion of a colimit binary cofan is mono

Instances
theorem CategoryTheory.Limits.MonoCoprod.binaryCofan_inl {C : Type u_1} [] [self : ] ⦃A : C ⦃B : C (c : ) :

the left inclusion of a colimit binary cofan is mono

@[instance 100]
Equations
• =
theorem CategoryTheory.Limits.MonoCoprod.binaryCofan_inr {C : Type u_1} [] {A : C} {B : C} (c : ) (hc : ) :
instance CategoryTheory.Limits.MonoCoprod.instMonoInl {C : Type u_1} [] {A : C} {B : C} :
CategoryTheory.Mono CategoryTheory.Limits.coprod.inl
Equations
• =
instance CategoryTheory.Limits.MonoCoprod.instMonoInr {C : Type u_1} [] {A : C} {B : C} :
CategoryTheory.Mono CategoryTheory.Limits.coprod.inr
Equations
• =
theorem CategoryTheory.Limits.MonoCoprod.mono_inl_iff {C : Type u_1} [] {A : C} {B : C} {c₁ : } {c₂ : } (hc₁ : ) (hc₂ : ) :
theorem CategoryTheory.Limits.MonoCoprod.mk' {C : Type u_1} [] (h : ∀ (A B : C), ∃ (c : ) (x : ), CategoryTheory.Mono c.inl) :
def CategoryTheory.Limits.MonoCoprod.binaryCofanSum {C : Type u_1} [] {I₁ : Type u_2} {I₂ : Type u_3} {X : I₁ I₂C} (c : ) (c₁ : CategoryTheory.Limits.Cofan (X Sum.inl)) (c₂ : CategoryTheory.Limits.Cofan (X Sum.inr)) (hc₁ : ) (hc₂ : ) :

Given a family of objects X : I₁ ⊕ I₂ → C, a cofan of X, and two colimit cofans of X ∘ Sum.inl and X ∘ Sum.inr, this is a cofan for c₁.pt and c₂.pt whose point is c.pt.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Limits.MonoCoprod.isColimitBinaryCofanSum {C : Type u_1} [] {I₁ : Type u_2} {I₂ : Type u_3} {X : I₁ I₂C} (c : ) (c₁ : CategoryTheory.Limits.Cofan (X Sum.inl)) (c₂ : CategoryTheory.Limits.Cofan (X Sum.inr)) (hc : ) (hc₁ : ) (hc₂ : ) :

The binary cofan binaryCofanSum c c₁ c₂ hc₁ hc₂ is colimit.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Limits.MonoCoprod.mono_binaryCofanSum_inl {C : Type u_1} [] {I₁ : Type u_2} {I₂ : Type u_3} {X : I₁ I₂C} (c : ) (c₁ : CategoryTheory.Limits.Cofan (X Sum.inl)) (c₂ : CategoryTheory.Limits.Cofan (X Sum.inr)) (hc : ) (hc₁ : ) (hc₂ : ) :
theorem CategoryTheory.Limits.MonoCoprod.mono_binaryCofanSum_inr {C : Type u_1} [] {I₁ : Type u_2} {I₂ : Type u_3} {X : I₁ I₂C} (c : ) (c₁ : CategoryTheory.Limits.Cofan (X Sum.inl)) (c₂ : CategoryTheory.Limits.Cofan (X Sum.inr)) (hc : ) (hc₁ : ) (hc₂ : ) :
theorem CategoryTheory.Limits.MonoCoprod.mono_binaryCofanSum_inl' {C : Type u_1} [] {I₁ : Type u_2} {I₂ : Type u_3} {X : I₁ I₂C} (c : ) (c₁ : CategoryTheory.Limits.Cofan (X Sum.inl)) (c₂ : CategoryTheory.Limits.Cofan (X Sum.inr)) (hc : ) (hc₁ : ) (hc₂ : ) (inl : c₁.pt c.pt) (hinl : ∀ (i₁ : I₁), CategoryTheory.CategoryStruct.comp (c₁.inj i₁) inl = c.inj (Sum.inl i₁)) :
theorem CategoryTheory.Limits.MonoCoprod.mono_binaryCofanSum_inr' {C : Type u_1} [] {I₁ : Type u_2} {I₂ : Type u_3} {X : I₁ I₂C} (c : ) (c₁ : CategoryTheory.Limits.Cofan (X Sum.inl)) (c₂ : CategoryTheory.Limits.Cofan (X Sum.inr)) (hc : ) (hc₁ : ) (hc₂ : ) (inr : c₂.pt c.pt) (hinr : ∀ (i₂ : I₂), CategoryTheory.CategoryStruct.comp (c₂.inj i₂) inr = c.inj (Sum.inr i₂)) :
theorem CategoryTheory.Limits.MonoCoprod.mono_of_injective_aux {C : Type u_1} [] {I : Type u_2} {J : Type u_3} (X : IC) (ι : JI) (hι : ) (c : ) (c₁ : ) (hc : ) (hc₁ : ) (c₂ : CategoryTheory.Limits.Cofan fun (k : ()) => X k) (hc₂ : ) :
theorem CategoryTheory.Limits.MonoCoprod.mono_of_injective {C : Type u_1} [] {I : Type u_2} {J : Type u_3} (X : IC) (ι : JI) (hι : ) (c : ) (c₁ : ) (hc : ) (hc₁ : ) [CategoryTheory.Limits.HasCoproduct fun (k : ()) => X k] :
theorem CategoryTheory.Limits.MonoCoprod.mono_of_injective' {C : Type u_1} [] {I : Type u_2} {J : Type u_3} (X : IC) (ι : JI) (hι : ) [] [CategoryTheory.Limits.HasCoproduct fun (k : ()) => X k] :
theorem CategoryTheory.Limits.MonoCoprod.mono_map'_of_injective {C : Type u_1} [] {I : Type u_2} {J : Type u_3} (X : IC) (ι : JI) (hι : ) [] [CategoryTheory.Limits.HasCoproduct fun (k : ()) => X k] :
theorem CategoryTheory.Limits.MonoCoprod.mono_inj {C : Type u_1} [] {I : Type u_2} (X : IC) (c : ) (i : I) [CategoryTheory.Limits.HasCoproduct fun (k : (Set.range fun (x : Unit) => i)) => X k] :
instance CategoryTheory.Limits.MonoCoprod.mono_ι {C : Type u_1} [] {I : Type u_2} (X : IC) (i : I) [CategoryTheory.Limits.HasCoproduct fun (k : (Set.range fun (x : Unit) => i)) => X k] :
Equations
• =
theorem CategoryTheory.Limits.MonoCoprod.monoCoprod_of_preservesCoprod_of_reflectsMono {C : Type u_1} [] {D : Type u_2} [] (F : ) [F.ReflectsMonomorphisms] :
Equations
• =