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 : CategoryTheory.Limits.BinaryCofan A B), CategoryTheory.Limits.IsColimit c → CategoryTheory.Mono c.inl
the left inclusion of a colimit binary cofan is mono
Instances
theorem
CategoryTheory.Limits.MonoCoprod.binaryCofan_inl
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[self : CategoryTheory.Limits.MonoCoprod C]
⦃A : C⦄
⦃B : C⦄
(c : CategoryTheory.Limits.BinaryCofan A B)
:
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]
:
Equations
- ⋯ = ⋯
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 c.inr
instance
CategoryTheory.Limits.MonoCoprod.instMonoInl
{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
- ⋯ = ⋯
instance
CategoryTheory.Limits.MonoCoprod.instMonoInr
{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
- ⋯ = ⋯
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 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)
:
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.
Instances For
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₂)
:
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}
[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₁))
:
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₂))
:
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]
:
Equations
- ⋯ = ⋯
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]
:
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]
:
Equations
- ⋯ = ⋯