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} [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.

Instances
    theorem CategoryTheory.Limits.CoproductDisjoint.mono_inl {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} [self : CategoryTheory.Limits.CoproductDisjoint X₁✝ X₂✝] (X : C) (X₁ : X₁✝ X) (X₂ : X₂✝ X) (_cX : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk X₁ X₂)) :
    theorem CategoryTheory.Limits.CoproductDisjoint.mono_inr {C : Type u} [CategoryTheory.Category.{v, u} C] {X₁ : C} {X₂ : C} [self : CategoryTheory.Limits.CoproductDisjoint X₁✝ X₂✝] (X : C) (X₁ : X₁✝ X) (X₂ : X₂✝ X) (_cX : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk X₁ X₂)) :

    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
    Instances For

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

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

      Z is initial.

      Equations
      Instances For

        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
        Instances For
          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.
          Instances For

            C has disjoint coproducts if every coproduct is disjoint.

            Instances

              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.