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

class CategoryTheory.Limits.MonoCoprod (C : Type u_1) [CategoryTheory.Category.{u_2, u_1} C] : Prop

This condition expresses that inclusion morphisms into coproducts are monomorphisms.

• binaryCofan_inl ⦃A B : C⦄ (c : CategoryTheory.Limits.BinaryCofan A B) : CategoryTheory.Limits.IsColimit c → CategoryTheory.Mono c.inl

  the left inclusion of a colimit binary cofan is mono

@[instance 100]

instance CategoryTheory.Limits.monoCoprodOfHasZeroMorphisms {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] : CategoryTheory.Limits.MonoCoprod C

theorem CategoryTheory.Limits.MonoCoprod.binaryCofan_inr {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {A B : C} [CategoryTheory.Limits.MonoCoprod C] (c : CategoryTheory.Limits.BinaryCofan A B) (hc : CategoryTheory.Limits.IsColimit c) : CategoryTheory.Mono c.inr

instance CategoryTheory.Limits.MonoCoprod.instMonoInl {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {A B : C} [CategoryTheory.Limits.MonoCoprod C] [CategoryTheory.Limits.HasBinaryCoproduct A B] : CategoryTheory.Mono CategoryTheory.Limits.coprod.inl

instance CategoryTheory.Limits.MonoCoprod.instMonoInr {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {A 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 B : C} {c₁ c₂ : CategoryTheory.Limits.BinaryCofan A B} (hc₁ : CategoryTheory.Limits.IsColimit c₁) (hc₂ : CategoryTheory.Limits.IsColimit c₂) : CategoryTheory.Mono c₁.inl ↔ CategoryTheory.Mono c₂.inl

theorem CategoryTheory.Limits.MonoCoprod.mk' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] (h : ∀ (A B : C), ∃ (c : CategoryTheory.Limits.BinaryCofan A B) (x : CategoryTheory.Limits.IsColimit c), CategoryTheory.Mono c.inl) : CategoryTheory.Limits.MonoCoprod C

instance CategoryTheory.Limits.MonoCoprod.monoCoprodType : CategoryTheory.Limits.MonoCoprod (Type u)

def CategoryTheory.Limits.MonoCoprod.binaryCofanSum {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {I₁ : Type u_2} {I₂ : Type u_3} {X : I₁ ⊕ I₂ → C} (c : CategoryTheory.Limits.Cofan X) (c₁ : CategoryTheory.Limits.Cofan (X ∘ Sum.inl)) (c₂ : CategoryTheory.Limits.Cofan (X ∘ Sum.inr)) (hc₁ : CategoryTheory.Limits.IsColimit c₁) (hc₂ : CategoryTheory.Limits.IsColimit c₂) : CategoryTheory.Limits.BinaryCofan c₁.pt c₂.pt

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.

def CategoryTheory.Limits.MonoCoprod.isColimitBinaryCofanSum {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {I₁ : Type u_2} {I₂ : Type u_3} {X : I₁ ⊕ I₂ → C} (c : CategoryTheory.Limits.Cofan X) (c₁ : CategoryTheory.Limits.Cofan (X ∘ Sum.inl)) (c₂ : CategoryTheory.Limits.Cofan (X ∘ Sum.inr)) (hc : CategoryTheory.Limits.IsColimit c) (hc₁ : CategoryTheory.Limits.IsColimit c₁) (hc₂ : CategoryTheory.Limits.IsColimit c₂) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.MonoCoprod.binaryCofanSum c c₁ c₂ 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.

theorem CategoryTheory.Limits.MonoCoprod.mono_binaryCofanSum_inl {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {I₁ : Type u_2} {I₂ : Type u_3} {X : I₁ ⊕ I₂ → C} (c : CategoryTheory.Limits.Cofan X) (c₁ : CategoryTheory.Limits.Cofan (X ∘ Sum.inl)) (c₂ : CategoryTheory.Limits.Cofan (X ∘ Sum.inr)) (hc : CategoryTheory.Limits.IsColimit c) (hc₁ : CategoryTheory.Limits.IsColimit c₁) (hc₂ : CategoryTheory.Limits.IsColimit c₂) [CategoryTheory.Limits.MonoCoprod C] : CategoryTheory.Mono (CategoryTheory.Limits.MonoCoprod.binaryCofanSum c c₁ c₂ hc₁ hc₂).inl

theorem CategoryTheory.Limits.MonoCoprod.mono_binaryCofanSum_inr {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {I₁ : Type u_2} {I₂ : Type u_3} {X : I₁ ⊕ I₂ → C} (c : CategoryTheory.Limits.Cofan X) (c₁ : CategoryTheory.Limits.Cofan (X ∘ Sum.inl)) (c₂ : CategoryTheory.Limits.Cofan (X ∘ Sum.inr)) (hc : CategoryTheory.Limits.IsColimit c) (hc₁ : CategoryTheory.Limits.IsColimit c₁) (hc₂ : CategoryTheory.Limits.IsColimit c₂) [CategoryTheory.Limits.MonoCoprod C] : CategoryTheory.Mono (CategoryTheory.Limits.MonoCoprod.binaryCofanSum c c₁ c₂ hc₁ hc₂).inr

theorem CategoryTheory.Limits.MonoCoprod.mono_binaryCofanSum_inl' {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {I₁ : Type u_2} {I₂ : Type u_3} {X : I₁ ⊕ I₂ → C} (c : CategoryTheory.Limits.Cofan X) (c₁ : CategoryTheory.Limits.Cofan (X ∘ Sum.inl)) (c₂ : CategoryTheory.Limits.Cofan (X ∘ Sum.inr)) (hc : CategoryTheory.Limits.IsColimit c) (hc₁ : CategoryTheory.Limits.IsColimit c₁) (hc₂ : CategoryTheory.Limits.IsColimit c₂) [CategoryTheory.Limits.MonoCoprod C] (inl : c₁.pt ⟶ c.pt) (hinl : ∀ (i₁ : I₁), CategoryTheory.CategoryStruct.comp (c₁.inj i₁) inl = c.inj (Sum.inl i₁)) : CategoryTheory.Mono inl

theorem CategoryTheory.Limits.MonoCoprod.mono_binaryCofanSum_inr' {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {I₁ : Type u_2} {I₂ : Type u_3} {X : I₁ ⊕ I₂ → C} (c : CategoryTheory.Limits.Cofan X) (c₁ : CategoryTheory.Limits.Cofan (X ∘ Sum.inl)) (c₂ : CategoryTheory.Limits.Cofan (X ∘ Sum.inr)) (hc : CategoryTheory.Limits.IsColimit c) (hc₁ : CategoryTheory.Limits.IsColimit c₁) (hc₂ : CategoryTheory.Limits.IsColimit c₂) [CategoryTheory.Limits.MonoCoprod C] (inr : c₂.pt ⟶ c.pt) (hinr : ∀ (i₂ : I₂), CategoryTheory.CategoryStruct.comp (c₂.inj i₂) inr = c.inj (Sum.inr i₂)) : CategoryTheory.Mono inr

theorem CategoryTheory.Limits.MonoCoprod.mono_of_injective_aux {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.MonoCoprod C] {I : Type u_2} {J : Type u_3} (X : I → C) (ι : J → I) (hι : Function.Injective ι) (c : CategoryTheory.Limits.Cofan X) (c₁ : CategoryTheory.Limits.Cofan (X ∘ ι)) (hc : CategoryTheory.Limits.IsColimit c) (hc₁ : CategoryTheory.Limits.IsColimit c₁) (c₂ : CategoryTheory.Limits.Cofan fun (k : ↑(Set.range ι)ᶜ) => X ↑k) (hc₂ : CategoryTheory.Limits.IsColimit c₂) : CategoryTheory.Mono (CategoryTheory.Limits.Cofan.IsColimit.desc hc₁ fun (i : J) => c.inj (ι i))

theorem CategoryTheory.Limits.MonoCoprod.mono_of_injective {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.MonoCoprod C] {I : Type u_2} {J : Type u_3} (X : I → C) (ι : J → I) (hι : Function.Injective ι) (c : CategoryTheory.Limits.Cofan X) (c₁ : CategoryTheory.Limits.Cofan (X ∘ ι)) (hc : CategoryTheory.Limits.IsColimit c) (hc₁ : CategoryTheory.Limits.IsColimit c₁) [CategoryTheory.Limits.HasCoproduct fun (k : ↑(Set.range ι)ᶜ) => X ↑k] : CategoryTheory.Mono (CategoryTheory.Limits.Cofan.IsColimit.desc hc₁ fun (i : J) => c.inj (ι i))

theorem CategoryTheory.Limits.MonoCoprod.mono_of_injective' {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.MonoCoprod C] {I : Type u_2} {J : Type u_3} (X : I → C) (ι : J → I) (hι : Function.Injective ι) [CategoryTheory.Limits.HasCoproduct (X ∘ ι)] [CategoryTheory.Limits.HasCoproduct X] [CategoryTheory.Limits.HasCoproduct fun (k : ↑(Set.range ι)ᶜ) => X ↑k] : CategoryTheory.Mono (CategoryTheory.Limits.Sigma.desc fun (j : J) => CategoryTheory.Limits.Sigma.ι X (ι j))

theorem CategoryTheory.Limits.MonoCoprod.mono_map'_of_injective {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Limits.MonoCoprod C] {I : Type u_2} {J : Type u_3} (X : I → C) (ι : J → I) (hι : Function.Injective ι) [CategoryTheory.Limits.HasCoproduct (X ∘ ι)] [CategoryTheory.Limits.HasCoproduct X] [CategoryTheory.Limits.HasCoproduct fun (k : ↑(Set.range ι)ᶜ) => X ↑k] : CategoryTheory.Mono (CategoryTheory.Limits.Sigma.map' ι fun (j : J) => CategoryTheory.CategoryStruct.id ((X ∘ ι) j))

theorem CategoryTheory.Limits.MonoCoprod.mono_inj {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.MonoCoprod C] {I : Type u_2} (X : I → C) (c : CategoryTheory.Limits.Cofan X) (h : CategoryTheory.Limits.IsColimit c) (i : I) [CategoryTheory.Limits.HasCoproduct fun (k : ↑(Set.range fun (x : Unit) => i)ᶜ) => X ↑k] : CategoryTheory.Mono (c.inj i)

instance CategoryTheory.Limits.MonoCoprod.mono_ι {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.MonoCoprod C] {I : Type u_2} (X : I → C) [CategoryTheory.Limits.HasCoproduct X] (i : I) [CategoryTheory.Limits.HasCoproduct fun (k : ↑(Set.range fun (x : Unit) => i)ᶜ) => X ↑k] : CategoryTheory.Mono (CategoryTheory.Limits.Sigma.ι X i)

theorem CategoryTheory.Limits.MonoCoprod.monoCoprod_of_preservesCoprod_of_reflectsMono {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {D : Type u_2} [CategoryTheory.Category.{u_3, u_2} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.MonoCoprod D] [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F] [F.ReflectsMonomorphisms] : CategoryTheory.Limits.MonoCoprod C

instance CategoryTheory.Limits.MonoCoprod.instOfPreservesColimitsOfShapeDiscreteWalkingPairOfReflectsMonomorphismsForget {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.ConcreteCategory C] [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) (CategoryTheory.forget C)] [(CategoryTheory.forget C).ReflectsMonomorphisms] : CategoryTheory.Limits.MonoCoprod C