# mathlibdocumentation

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 #

• Adapt this to the infinitary (small) version: This is one of the conditions in Giraud's theorem characterising sheaf topoi.
• Construct examples (and counterexamples?), eg Type, Vec.
• Define extensive categories, and show every extensive category has disjoint coproducts.
• Define coherent categories and use this to define positive coherent categories.
@[class]
structure category_theory.limits.coproduct_disjoint {C : Type u} (X₁ X₂ : C) :
Type (max u v)
• is_initial_of_is_pullback_of_is_coproduct : Π {X Z : C} {pX₁ : X₁ X} {pX₂ : X₂ X} {f : Z X₁} {g : Z X₂}, Π {comm : f pX₁ = g pX₂},
• mono_inl : ∀ (X : C) (X₁_1 : X₁ X) (X₂_1 : X₂ X),
• mono_inr : ∀ (X : C) (X₁_1 : X₁ X) (X₂_1 : X₂ X),

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
def category_theory.limits.is_initial_of_is_pullback_of_is_coproduct {C : Type u} {Z X₁ X₂ X : C} {pX₁ : X₁ X} {pX₂ : X₂ X} {f : Z X₁} {g : Z X₂} {comm : f pX₁ = g pX₂}  :

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
def category_theory.limits.is_initial_of_is_pullback_of_coproduct {C : Type u} {Z X₁ X₂ : C} {f : Z X₁} {g : Z X₂}  :

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

Z ⟶ X₁ ↓ ↓ X₂ ⟶ X₁ ⨿ X₂

Z is initial.

Equations
def category_theory.limits.is_initial_of_pullback_of_is_coproduct {C : Type u} {X X₁ X₂ : C} {pX₁ : X₁ X} {pX₂ : X₂ X} [ pX₂]  :

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

If the coproduct of X₁ and X₂ is disjoint, the pullback of X₁ ⟶ X₁ ⨿ X₂ and X₂ ⟶ X₁ ⨿ X₂ is initial.

Equations
@[instance]
@[instance]
@[class]
structure category_theory.limits.coproducts_disjoint (C : Type u)  :
Type (max u v)
• coproduct_disjoint : Π (X Y : C),

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.