mathlib documentation


Disjoint coproducts #

Defines disjoint coproducts: coproducts where the intersection is initial and the coprojections are monic. Shows that a category with disjoint coproducts is initial_mono_class.


structure category_theory.limits.coproduct_disjoint {C : Type u} [category_theory.category C] (X₁ X₂ : C) :
Type (max u v)

Given any pullback diagram of the form

Z ⟶ X₁ ↓ ↓ X₂ ⟶ X

where X₁ ⟶ X ← X₂ is a coproduct diagram, then Z is initial, and both X₁ ⟶ X and X₂ ⟶ X are mono.

Instances of this typeclass
Instances of other typeclasses for category_theory.limits.coproduct_disjoint
  • category_theory.limits.coproduct_disjoint.has_sizeof_inst

If the coproduct of X₁ and X₂ is disjoint, then given any pullback square

Z ⟶ X₁ ↓ ↓ X₂ ⟶ X

where X₁ ⟶ X ← X₂ is a coproduct, then Z is initial.


If the coproduct of X₁ and X₂ is disjoint, then provided X₁ ⟶ X ← X₂ is a coproduct the pullback is an initial object:


X₂ ⟶ X

structure category_theory.limits.coproducts_disjoint (C : Type u) [category_theory.category C] :
Type (max u v)

C has disjoint coproducts if every coproduct is disjoint.

Instances for category_theory.limits.coproducts_disjoint
  • category_theory.limits.coproducts_disjoint.has_sizeof_inst

If C has disjoint coproducts, any morphism out of initial is mono. Note it isn't true in general that C has strict initial objects, for instance consider the category of types and partial functions.