mathlib3 documentation

category_theory.limits.mono_coprod

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

source
@[class]
structure category_theory.limits.mono_coprod (C : Type u_1) [category_theory.category C] :
Prop

This condition expresses that inclusion morphisms into coproducts are monomorphisms.

Instances of this typeclass
source
@[protected, instance]
def category_theory.limits.mono_coprod_of_has_zero_morphisms {C : Type u_1} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] :
category_theory.limits.mono_coprod C
source
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) :
category_theory.mono c.inr
source
@[protected, instance]
def category_theory.limits.mono_coprod.category_theory.limits.coprod.inl.category_theory.mono {C : Type u_1} [category_theory.category C] {A B : C} [category_theory.limits.mono_coprod C] [category_theory.limits.has_binary_coproduct A B] :
category_theory.mono category_theory.limits.coprod.inl
source
@[protected, instance]
def category_theory.limits.mono_coprod.category_theory.limits.coprod.inr.category_theory.mono {C : Type u_1} [category_theory.category C] {A B : C} [category_theory.limits.mono_coprod C] [category_theory.limits.has_binary_coproduct A B] :
category_theory.mono category_theory.limits.coprod.inr
source
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₂) :
category_theory.mono c₁.inl ↔ category_theory.mono c₂.inl
source
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) :
category_theory.limits.mono_coprod C
source
@[protected, instance]
def category_theory.limits.mono_coprod.mono_coprod_type  :
category_theory.limits.mono_coprod (Type u)