Documentation

Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct

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 #

class CategoryTheory.Limits.CoproductDisjoint {C : Type u} [Category.{v, u} C] {ι : Type u_1} (X : ιC) :

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.

Instances
    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 jPullbackCone (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) :
    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)
    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) :

    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.

    Equations
    Instances For
      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)] :

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

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        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ᵢ.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          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) :

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

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[reducible, inline]

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

            Equations
            Instances For

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

              Equations
              Instances For

                X ×[X ⨿ Y] Y is initial.

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

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

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

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

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[deprecated CategoryTheory.Limits.IsInitial.ofBinaryCoproductDisjointOfIsColimitOfIsLimit (since := "2025-06-18")]

                      Alias of CategoryTheory.Limits.IsInitial.ofBinaryCoproductDisjointOfIsColimitOfIsLimit.


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

                      Equations
                      Instances For
                        @[deprecated CategoryTheory.Limits.IsInitial.ofBinaryCoproductDisjointOfIsLimit (since := "2025-06-18")]

                        Alias of CategoryTheory.Limits.IsInitial.ofBinaryCoproductDisjointOfIsLimit.


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

                        Equations
                        Instances For
                          @[deprecated CategoryTheory.Limits.IsInitial.ofBinaryCoproductDisjointOfIsColimit (since := "2025-06-18")]

                          Alias of CategoryTheory.Limits.IsInitial.ofBinaryCoproductDisjointOfIsColimit.


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

                          Equations
                          Instances For
                            @[deprecated CategoryTheory.Mono.of_binaryCoproductDisjoint_left (since := "2025-06-18")]
                            theorem CategoryTheory.Limits.CoproductDisjoint.mono_inl {C : Type u} [Category.{v, u} C] {X Y : C} [BinaryCoproductDisjoint X Y] {Z : C} {f : X Z} (g : Y Z) (hc : IsColimit (BinaryCofan.mk f g)) :

                            Alias of CategoryTheory.Mono.of_binaryCoproductDisjoint_left.

                            @[deprecated CategoryTheory.Mono.of_binaryCoproductDisjoint_right (since := "2025-06-18")]
                            theorem CategoryTheory.Limits.CoproductDisjoint.mono_inr {C : Type u} [Category.{v, u} C] {X Y : C} [BinaryCoproductDisjoint X Y] {Z : C} (f : X Z) {g : Y Z} (hc : IsColimit (BinaryCofan.mk f g)) :

                            Alias of CategoryTheory.Mono.of_binaryCoproductDisjoint_right.

                            C has disjoint coproducts if every coproduct is disjoint.

                            Instances
                              @[reducible, inline]

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

                              Equations
                              Instances For

                                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.

                                @[deprecated CategoryTheory.Limits.initialMonoClass_of_coproductsDisjoint (since := "2025-06-18")]

                                Alias of CategoryTheory.Limits.initialMonoClass_of_coproductsDisjoint.


                                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.