Disjoint coproducts

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

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 CategoryTheory.Limits.CoproductDisjoint {C : Type u} [Category.{v, u} 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.

• isInitialOfIsPullbackOfIsCoproduct {X Z : C} {pX₁ : X₁ ⟶ X} {pX₂ : X₂ ⟶ X} {f : Z ⟶ X₁} {g : Z ⟶ X₂} (_cX : IsColimit (BinaryCofan.mk pX₁ pX₂)) {comm : CategoryStruct.comp f pX₁ = CategoryStruct.comp g pX₂} : IsLimit (PullbackCone.mk f g comm) → IsInitial Z
• mono_inl (X : C) (X₁ : X₁ ⟶ X) (X₂ : X₂ ⟶ X) (_cX : IsColimit (BinaryCofan.mk X₁ X₂)) : Mono X₁
• mono_inr (X : C) (X₁ : X₁ ⟶ X) (X₂ : X₂ ⟶ X) (_cX : IsColimit (BinaryCofan.mk X₁ X₂)) : Mono X₂

def CategoryTheory.Limits.isInitialOfIsPullbackOfIsCoproduct {C : Type u} [Category.{v, u} C] {Z X₁ X₂ X : C} [CoproductDisjoint X₁ X₂] {pX₁ : X₁ ⟶ X} {pX₂ : X₂ ⟶ X} (cX : IsColimit (BinaryCofan.mk pX₁ pX₂)) {f : Z ⟶ X₁} {g : Z ⟶ X₂} {comm : CategoryStruct.comp f pX₁ = CategoryStruct.comp g pX₂} (cZ : IsLimit (PullbackCone.mk f g comm)) : IsInitial 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

• CategoryTheory.Limits.isInitialOfIsPullbackOfIsCoproduct cX cZ = CategoryTheory.Limits.CoproductDisjoint.isInitialOfIsPullbackOfIsCoproduct cX cZ

noncomputable def CategoryTheory.Limits.isInitialOfIsPullbackOfCoproduct {C : Type u} [Category.{v, u} C] {Z X₁ X₂ : C} [HasBinaryCoproduct X₁ X₂] [CoproductDisjoint X₁ X₂] {f : Z ⟶ X₁} {g : Z ⟶ X₂} {comm : CategoryStruct.comp f coprod.inl = CategoryStruct.comp g coprod.inr} (cZ : IsLimit (PullbackCone.mk f g comm)) : IsInitial Z

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

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

Z is initial.

Equations

• CategoryTheory.Limits.isInitialOfIsPullbackOfCoproduct cZ = CategoryTheory.Limits.CoproductDisjoint.isInitialOfIsPullbackOfIsCoproduct (CategoryTheory.Limits.coprodIsCoprod X₁ X₂) cZ

noncomputable def CategoryTheory.Limits.isInitialOfPullbackOfIsCoproduct {C : Type u} [Category.{v, u} C] {X X₁ X₂ : C} [CoproductDisjoint X₁ X₂] {pX₁ : X₁ ⟶ X} {pX₂ : X₂ ⟶ X} [HasPullback pX₁ pX₂] (cX : IsColimit (BinaryCofan.mk pX₁ pX₂)) : IsInitial (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

• CategoryTheory.Limits.isInitialOfPullbackOfIsCoproduct cX = CategoryTheory.Limits.CoproductDisjoint.isInitialOfIsPullbackOfIsCoproduct cX (CategoryTheory.Limits.pullbackIsPullback pX₁ pX₂)

noncomputable def CategoryTheory.Limits.isInitialOfPullbackOfCoproduct {C : Type u} [Category.{v, u} C] {X₁ X₂ : C} [HasBinaryCoproduct X₁ X₂] [CoproductDisjoint X₁ X₂] [HasPullback coprod.inl coprod.inr] : IsInitial (pullback coprod.inl coprod.inr)

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

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.Limits.instMonoInlOfCoproductDisjoint {C : Type u} [Category.{v, u} C] {X₁ X₂ : C} [HasBinaryCoproduct X₁ X₂] [CoproductDisjoint X₁ X₂] : Mono coprod.inl

instance CategoryTheory.Limits.instMonoInrOfCoproductDisjoint {C : Type u} [Category.{v, u} C] {X₁ X₂ : C} [HasBinaryCoproduct X₁ X₂] [CoproductDisjoint X₁ X₂] : Mono coprod.inr

class CategoryTheory.Limits.CoproductsDisjoint (C : Type u) [Category.{v, u} C] : Type (max u v)

C has disjoint coproducts if every coproduct is disjoint.

• CoproductDisjoint (X Y : C) : Limits.CoproductDisjoint X Y

theorem CategoryTheory.Limits.initialMonoClass_of_disjoint_coproducts {C : Type u} [Category.{v, u} C] [CoproductsDisjoint C] : InitialMonoClass 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.