mathlib documentation

category_theory.limits.shapes.disjoint_coproduct

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.

TODO #

@[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

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.

Equations

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₂ ⟶ X

Equations
@[class]
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.

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.