Documentation

Mathlib.CategoryTheory.Limits.MonoCoprod

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

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

Instances
    source
    instance CategoryTheory.Limits.monoCoprodOfHasZeroMorphisms {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] :
    CategoryTheory.Limits.MonoCoprod C
    Equations
    source
    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) :
    CategoryTheory.Mono (CategoryTheory.Limits.BinaryCofan.inr c)
    source
    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
    Equations
    • One or more equations did not get rendered due to their size.
    source
    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
    Equations
    • One or more equations did not get rendered due to their size.
    source
    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₂) :
    CategoryTheory.Mono (CategoryTheory.Limits.BinaryCofan.inl c₁) ↔ CategoryTheory.Mono (CategoryTheory.Limits.BinaryCofan.inl c₂)
    source
    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 (CategoryTheory.Limits.BinaryCofan.inl c)) :
    CategoryTheory.Limits.MonoCoprod C
    source
    instance CategoryTheory.Limits.MonoCoprod.monoCoprodType :
    CategoryTheory.Limits.MonoCoprod (Type u)
    Equations