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} (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₂} → {comm : } →
• mono_inl : ∀ (X : C) (X₁_1 : X₁ X) (X₂_1 : X₂ X),
• mono_inr : ∀ (X : C) (X₁_1 : X₁ X) (X₂_1 : X₂ X),
Instances
theorem CategoryTheory.Limits.CoproductDisjoint.mono_inl {C : Type u} {X₁ : C} {X₂ : C} [self : ] (X : C) (X₁ : X₁✝ X) (X₂ : X₂✝ X) :
theorem CategoryTheory.Limits.CoproductDisjoint.mono_inr {C : Type u} {X₁ : C} {X₂ : C} [self : ] (X : C) (X₁ : X₁✝ X) (X₂ : X₂✝ X) :
def CategoryTheory.Limits.isInitialOfIsPullbackOfIsCoproduct {C : Type u} {Z : C} {X₁ : C} {X₂ : C} {X : C} {pX₁ : X₁ X} {pX₂ : X₂ X} (cX : ) {f : Z X₁} {g : Z X₂} {comm : } (cZ : ) :

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
noncomputable def CategoryTheory.Limits.isInitialOfIsPullbackOfCoproduct {C : Type u} {Z : C} {X₁ : C} {X₂ : C} {f : Z X₁} {g : Z X₂} {comm : CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.coprod.inl = CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.coprod.inr} (cZ : ) :

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
noncomputable def CategoryTheory.Limits.isInitialOfPullbackOfIsCoproduct {C : Type u} {X : C} {X₁ : C} {X₂ : C} {pX₁ : X₁ X} {pX₂ : X₂ X} [] (cX : ) :

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} {X₁ : C} {X₂ : C} [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
instance CategoryTheory.Limits.instMonoInlOfCoproductDisjoint {C : Type u} {X₁ : C} {X₂ : C} :
CategoryTheory.Mono CategoryTheory.Limits.coprod.inl
Equations
• =
instance CategoryTheory.Limits.instMonoInrOfCoproductDisjoint {C : Type u} {X₁ : C} {X₂ : C} :
CategoryTheory.Mono CategoryTheory.Limits.coprod.inr
Equations
• =

C has disjoint coproducts if every coproduct is disjoint.

• CoproductDisjoint : (X Y : C) →
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.