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} [CategoryTheory.Category.{v, u} C] (X₁ : C) (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₂} → CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk pX₁ pX₂) → {comm : CategoryTheory.CategoryStruct.comp f pX₁ = CategoryTheory.CategoryStruct.comp g pX₂} → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk f g comm) → CategoryTheory.Limits.IsInitial Z
• mono_inl : ∀ (X : C) (X₁_1 : X₁ ⟶ X) (X₂_1 : X₂ ⟶ X), CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk X₁_1 X₂_1) → CategoryTheory.Mono X₁_1
• mono_inr : ∀ (X : C) (X₁_1 : X₁ ⟶ X) (X₂_1 : X₂ ⟶ X), CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk X₁_1 X₂_1) → CategoryTheory.Mono X₂_1

theorem CategoryTheory.Limits.CoproductDisjoint.mono_inl {C : Type u} : ∀ {inst : CategoryTheory.Category.{v, u} C} {X₁ X₂ : C} [self : CategoryTheory.Limits.CoproductDisjoint X₁ X₂] (X : C) (X₁_1 : X₁ ⟶ X) (X₂_1 : X₂ ⟶ X), CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk X₁_1 X₂_1) → CategoryTheory.Mono X₁_1

theorem CategoryTheory.Limits.CoproductDisjoint.mono_inr {C : Type u} : ∀ {inst : CategoryTheory.Category.{v, u} C} {X₁ X₂ : C} [self : CategoryTheory.Limits.CoproductDisjoint X₁ X₂] (X : C) (X₁_1 : X₁ ⟶ X) (X₂_1 : X₂ ⟶ X), CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk X₁_1 X₂_1) → CategoryTheory.Mono X₂_1

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

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

noncomputable def CategoryTheory.Limits.isInitialOfPullbackOfCoproduct {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} [CategoryTheory.Limits.HasBinaryCoproduct X₁ X₂] [CategoryTheory.Limits.CoproductDisjoint X₁ X₂] [CategoryTheory.Limits.HasPullback CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr] : CategoryTheory.Limits.IsInitial (CategoryTheory.Limits.pullback CategoryTheory.Limits.coprod.inl CategoryTheory.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

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

C has disjoint coproducts if every coproduct is disjoint.

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

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