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?), e.g. 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] {ι : Type u_1} (X : ι → C) : Prop

We say the coproduct of the family Xᵢ is disjoint, if whenever we have a pullback diagram of the form

Z  ⟶ X₁
↓    ↓
X₂ ⟶ ∐ X

Z is initial.

• nonempty_isInitial_of_ne {c : Cofan X} (hc : IsColimit c) {i j : ι} : i ≠ j → ∀ (s : PullbackCone (c.inj i) (c.inj j)) (a : IsLimit s), Nonempty (IsInitial s.pt)
• mono_inj {c : Cofan X} (hc : IsColimit c) (i : ι) : Mono (c.inj i)

theorem CategoryTheory.Limits.CoproductDisjoint.of_cofan {C : Type u} [Category.{v, u} C] {ι : Type u_1} {X : ι → C} {c : Cofan X} (hc : IsColimit c) [∀ (i : ι), Mono (c.inj i)] (s : {i j : ι} → i ≠ j → PullbackCone (c.inj i) (c.inj j)) (hs : {i j : ι} → (hij : i ≠ j) → IsLimit (s hij)) (H : {i j : ι} → (hij : i ≠ j) → IsInitial (s hij).pt) : CoproductDisjoint X

theorem CategoryTheory.Limits.CoproductDisjoint.of_hasCoproduct {C : Type u} [Category.{v, u} C] {ι : Type u_1} {X : ι → C} [HasCoproduct X] [∀ (i : ι), Mono (Sigma.ι X i)] (s : {i j : ι} → i ≠ j → PullbackCone (Sigma.ι X i) (Sigma.ι X j)) (hs : {i j : ι} → (hij : i ≠ j) → IsLimit (s hij)) (H : {i j : ι} → (hij : i ≠ j) → IsInitial (s hij).pt) : CoproductDisjoint X

theorem CategoryTheory.Mono.of_coproductDisjoint {C : Type u} [Category.{v, u} C] {ι : Type u_1} {X : ι → C} [Limits.CoproductDisjoint X] {c : Limits.Cofan X} (hc : Limits.IsColimit c) (i : ι) : Mono (c.inj i)

instance CategoryTheory.Mono.ι_of_coproductDisjoint {C : Type u} [Category.{v, u} C] {ι : Type u_1} {X : ι → C} [Limits.CoproductDisjoint X] [Limits.HasCoproduct X] (i : ι) : Mono (Limits.Sigma.ι X i)

noncomputable def CategoryTheory.Limits.IsInitial.ofCoproductDisjointOfIsColimitOfIsLimit {C : Type u} [Category.{v, u} C] {ι : Type u_1} {X : ι → C} [CoproductDisjoint X] {i j : ι} (hij : i ≠ j) {c : Cofan X} (hc : IsColimit c) {s : PullbackCone (c.inj i) (c.inj j)} (hs : IsLimit s) : IsInitial s.pt

If i ≠ j and Xᵢ ← Y → Xⱼ is a pullback diagram over Z, where Z is the coproduct of the Xᵢ, then Y is initial.

noncomputable def CategoryTheory.Limits.IsInitial.ofCoproductDisjoint {C : Type u} [Category.{v, u} C] {ι : Type u_1} {X : ι → C} [CoproductDisjoint X] {i j : ι} (hij : i ≠ j) [HasCoproduct X] [HasPullback (Sigma.ι X i) (Sigma.ι X j)] : IsInitial (pullback (Sigma.ι X i) (Sigma.ι X j))

If i ≠ j, the pullback Xᵢ ×[∐ X] Xⱼ is initial.

noncomputable def CategoryTheory.Limits.IsInitial.ofCoproductDisjointOfIsColimit {C : Type u} [Category.{v, u} C] {ι : Type u_1} {X : ι → C} [CoproductDisjoint X] {i j : ι} (hij : i ≠ j) {Z : C} {f : (i : ι) → X i ⟶ Z} [HasPullback (f i) (f j)] (hc : IsColimit (Cofan.mk Z f)) : IsInitial (pullback (f i) (f j))

If i ≠ j, the pullback Xᵢ ×[Z] Xⱼ is initial, if Z is the coproduct of the Xᵢ.

noncomputable def CategoryTheory.Limits.IsInitial.ofCoproductDisjointOfIsLimit {C : Type u} [Category.{v, u} C] {ι : Type u_1} {X : ι → C} [CoproductDisjoint X] {i j : ι} (hij : i ≠ j) [HasCoproduct X] {s : PullbackCone (Sigma.ι X i) (Sigma.ι X j)} (hs : IsLimit s) : IsInitial s.pt

If i ≠ j and Xᵢ ← Y → Xⱼ is a pullback diagram over ∐ X, Y is initial.

noncomputable def CategoryTheory.Limits.IsInitial.ofCoproductDisjointOfCommSq {C : Type u} [Category.{v, u} C] {ι : Type u_1} {X : ι → C} [CoproductDisjoint X] {i j : ι} (hij : i ≠ j) [HasStrictInitialObjects C] {c : Cofan X} (hc : IsColimit c) {Z : C} (fst : Z ⟶ X i) (snd : Z ⟶ X j) (h : CategoryStruct.comp fst (c.inj i) = CategoryStruct.comp snd (c.inj j)) [HasPullback (c.inj i) (c.inj j)] : IsInitial Z

If C has strict initial objects and there is a commutative square Xᵢ ← Z → Xⱼ over ∐ X, then Z is initial.

@[reducible, inline]

abbrev CategoryTheory.Limits.BinaryCoproductDisjoint {C : Type u} [Category.{v, u} C] (X Y : C) : Prop

The binary coproduct of X and Y is disjoint if the coproduct of the family {X, Y} is disjoint.

theorem CategoryTheory.Limits.BinaryCoproductDisjoint.of_binaryCofan {C : Type u} [Category.{v, u} C] {X Y : C} {c : BinaryCofan X Y} (hc : IsColimit c) [Mono c.inl] [Mono c.inr] {s : PullbackCone c.inl c.inr} (hs : IsLimit s) (H : IsInitial s.pt) : BinaryCoproductDisjoint X Y

theorem CategoryTheory.Mono.cofanInl_of_binaryCoproductDisjoint {C : Type u} [Category.{v, u} C] {X Y : C} [Limits.BinaryCoproductDisjoint X Y] {c : Limits.BinaryCofan X Y} (hc : Limits.IsColimit c) : Mono c.inl

theorem CategoryTheory.Mono.cofanInr_of_binaryCoproductDisjoint {C : Type u} [Category.{v, u} C] {X Y : C} [Limits.BinaryCoproductDisjoint X Y] {c : Limits.BinaryCofan X Y} (hc : Limits.IsColimit c) : Mono c.inr

theorem CategoryTheory.Mono.of_binaryCoproductDisjoint_left {C : Type u} [Category.{v, u} C] {X Y : C} [Limits.BinaryCoproductDisjoint X Y] {Z : C} {f : X ⟶ Z} (g : Y ⟶ Z) (hc : Limits.IsColimit (Limits.BinaryCofan.mk f g)) : Mono f

theorem CategoryTheory.Mono.of_binaryCoproductDisjoint_right {C : Type u} [Category.{v, u} C] {X Y : C} [Limits.BinaryCoproductDisjoint X Y] {Z : C} (f : X ⟶ Z) {g : Y ⟶ Z} (hc : Limits.IsColimit (Limits.BinaryCofan.mk f g)) : Mono g

instance CategoryTheory.Mono.inl_of_binaryCoproductDisjoint {C : Type u} [Category.{v, u} C] {X Y : C} [Limits.BinaryCoproductDisjoint X Y] [Limits.HasBinaryCoproduct X Y] : Mono Limits.coprod.inl

instance CategoryTheory.Mono.inr_of_binaryCoproductDisjoint {C : Type u} [Category.{v, u} C] {X Y : C} [Limits.BinaryCoproductDisjoint X Y] [Limits.HasBinaryCoproduct X Y] : Mono Limits.coprod.inr

noncomputable def CategoryTheory.Limits.IsInitial.ofBinaryCoproductDisjointOfIsColimitOfIsLimit {C : Type u} [Category.{v, u} C] {X Y : C} [BinaryCoproductDisjoint X Y] {c : BinaryCofan X Y} (hc : IsColimit c) {s : PullbackCone c.inl c.inr} (hs : IsLimit s) : IsInitial s.pt

If X ← Z → Y is a pullback diagram over W, where W is the coproduct of X and Y, then Z is initial.

noncomputable def CategoryTheory.Limits.IsInitial.ofBinaryCoproductDisjoint {C : Type u} [Category.{v, u} C] {X Y : C} [BinaryCoproductDisjoint X Y] [HasBinaryCoproduct X Y] [HasPullback coprod.inl coprod.inr] : IsInitial (pullback coprod.inl coprod.inr)

X ×[X ⨿ Y] Y is initial.

noncomputable def CategoryTheory.Limits.IsInitial.ofBinaryCoproductDisjointOfIsColimit {C : Type u} [Category.{v, u} C] {X Y : C} [BinaryCoproductDisjoint X Y] {Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} [HasPullback f g] (hc : IsColimit (BinaryCofan.mk f g)) : IsInitial (pullback f g)

The pullback X ×[W] Y is initial, if W is the coproduct of X and Y.

noncomputable def CategoryTheory.Limits.IsInitial.ofBinaryCoproductDisjointOfIsLimit {C : Type u} [Category.{v, u} C] {X Y : C} [BinaryCoproductDisjoint X Y] [HasBinaryCoproduct X Y] (s : PullbackCone coprod.inl coprod.inr) (hs : IsLimit s) : IsInitial s.pt

If X ← Z → Y is a pullback diagram over X ⨿ Y, Z is initial.

class CategoryTheory.Limits.CoproductsOfShapeDisjoint (C : Type u_1) [Category.{v_1, u_1} C] (ι : Type u_2) : Prop

C has disjoint coproducts if every coproduct is disjoint.

• coproductDisjoint (X : ι → C) : CoproductDisjoint X

@[reducible, inline]

abbrev CategoryTheory.Limits.BinaryCoproductsDisjoint (C : Type u_1) [Category.{v_1, u_1} C] : Prop

C has disjoint binary coproducts if every binary coproduct is disjoint.

theorem CategoryTheory.Limits.BinaryCoproductsDisjoint.mk {C : Type u} [Category.{v, u} C] (H : ∀ (X Y : C), BinaryCoproductDisjoint X Y) : BinaryCoproductsDisjoint C

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