Disjoint coproducts #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source

@[class]

structure category_theory.limits.coproduct_disjoint {C : Type u} [category_theory.category C] (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₂}, category_theory.limits.is_colimit (category_theory.limits.binary_cofan.mk pX₁ pX₂) → Π {comm : f ≫ pX₁ = g ≫ pX₂}, category_theory.limits.is_limit (category_theory.limits.pullback_cone.mk f g comm) → category_theory.limits.is_initial Z
mono_inl : ∀ (X : C) (X₁_1 : X₁ ⟶ X) (X₂_1 : X₂ ⟶ X), category_theory.limits.is_colimit (category_theory.limits.binary_cofan.mk X₁_1 X₂_1) → category_theory.mono X₁_1
mono_inr : ∀ (X : C) (X₁_1 : X₁ ⟶ X) (X₂_1 : X₂ ⟶ X), category_theory.limits.is_colimit (category_theory.limits.binary_cofan.mk X₁_1 X₂_1) → category_theory.mono X₂_1

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

category_theory.limits.coproducts_disjoint.coproduct_disjoint

Instances of other typeclasses for category_theory.limits.coproduct_disjoint

category_theory.limits.coproduct_disjoint.has_sizeof_inst

source

def category_theory.limits.is_initial_of_is_pullback_of_is_coproduct {C : Type u} [category_theory.category C] {Z X₁ X₂ X : C} [category_theory.limits.coproduct_disjoint X₁ X₂] {pX₁ : X₁ ⟶ X} {pX₂ : X₂ ⟶ X} (cX : category_theory.limits.is_colimit (category_theory.limits.binary_cofan.mk pX₁ pX₂)) {f : Z ⟶ X₁} {g : Z ⟶ X₂} {comm : f ≫ pX₁ = g ≫ pX₂} (cZ : category_theory.limits.is_limit (category_theory.limits.pullback_cone.mk f g comm)) :

category_theory.limits.is_initial Z

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

category_theory.limits.is_initial_of_is_pullback_of_is_coproduct cX cZ = category_theory.limits.coproduct_disjoint.is_initial_of_is_pullback_of_is_coproduct cX cZ

source

noncomputable def category_theory.limits.is_initial_of_is_pullback_of_coproduct {C : Type u} [category_theory.category C] {Z X₁ X₂ : C} [category_theory.limits.has_binary_coproduct X₁ X₂] [category_theory.limits.coproduct_disjoint X₁ X₂] {f : Z ⟶ X₁} {g : Z ⟶ X₂} {comm : f ≫ category_theory.limits.coprod.inl = g ≫ category_theory.limits.coprod.inr} (cZ : category_theory.limits.is_limit (category_theory.limits.pullback_cone.mk f g comm)) :

category_theory.limits.is_initial Z

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

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

Z is initial.

Equations

category_theory.limits.is_initial_of_is_pullback_of_coproduct cZ = category_theory.limits.coproduct_disjoint.is_initial_of_is_pullback_of_is_coproduct (category_theory.limits.coprod_is_coprod X₁ X₂) cZ

source

noncomputable def category_theory.limits.is_initial_of_pullback_of_is_coproduct {C : Type u} [category_theory.category C] {X X₁ X₂ : C} [category_theory.limits.coproduct_disjoint X₁ X₂] {pX₁ : X₁ ⟶ X} {pX₂ : X₂ ⟶ X} [category_theory.limits.has_pullback pX₁ pX₂] (cX : category_theory.limits.is_colimit (category_theory.limits.binary_cofan.mk pX₁ pX₂)) :

category_theory.limits.is_initial (category_theory.limits.pullback pX₁ 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

category_theory.limits.is_initial_of_pullback_of_is_coproduct cX = category_theory.limits.coproduct_disjoint.is_initial_of_is_pullback_of_is_coproduct cX (category_theory.limits.pullback_is_pullback pX₁ pX₂)

source

noncomputable def category_theory.limits.is_initial_of_pullback_of_coproduct {C : Type u} [category_theory.category C] {X₁ X₂ : C} [category_theory.limits.has_binary_coproduct X₁ X₂] [category_theory.limits.coproduct_disjoint X₁ X₂] [category_theory.limits.has_pullback category_theory.limits.coprod.inl category_theory.limits.coprod.inr] :

category_theory.limits.is_initial (category_theory.limits.pullback category_theory.limits.coprod.inl category_theory.limits.coprod.inr)

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

Equations

category_theory.limits.is_initial_of_pullback_of_coproduct = category_theory.limits.is_initial_of_is_pullback_of_coproduct (category_theory.limits.pullback_is_pullback category_theory.limits.coprod.inl category_theory.limits.coprod.inr)

source

@[protected, instance]

def category_theory.limits.coprod.inl.category_theory.mono {C : Type u} [category_theory.category C] {X₁ X₂ : C} [category_theory.limits.has_binary_coproduct X₁ X₂] [category_theory.limits.coproduct_disjoint X₁ X₂] :

category_theory.mono category_theory.limits.coprod.inl

source

@[protected, instance]

def category_theory.limits.coprod.inr.category_theory.mono {C : Type u} [category_theory.category C] {X₁ X₂ : C} [category_theory.limits.has_binary_coproduct X₁ X₂] [category_theory.limits.coproduct_disjoint X₁ X₂] :

category_theory.mono category_theory.limits.coprod.inr

source

@[class]

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

Type (max u v)

coproduct_disjoint : Π (X Y : C), category_theory.limits.coproduct_disjoint X Y

C has disjoint coproducts if every coproduct is disjoint.

Instances for category_theory.limits.coproducts_disjoint

category_theory.limits.coproducts_disjoint.has_sizeof_inst

source

theorem category_theory.limits.initial_mono_class_of_disjoint_coproducts {C : Type u} [category_theory.category C] [category_theory.limits.coproducts_disjoint C] :

category_theory.limits.initial_mono_class C

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.