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.
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
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
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
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
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
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
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
Alias of CategoryTheory.Limits.IsInitial.ofBinaryCoproductDisjointOfIsLimit
.
If X ← Z → Y
is a pullback diagram over X ⨿ Y
, Z
is initial.
Equations
Instances For
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
Alias of CategoryTheory.Limits.IsInitial.ofBinaryCoproductDisjoint
.
X ×[X ⨿ Y] Y
is initial.
Equations
Instances For
Alias of CategoryTheory.Mono.of_binaryCoproductDisjoint_left
.
Alias of CategoryTheory.Mono.of_binaryCoproductDisjoint_right
.
C
has disjoint coproducts if every coproduct is disjoint.
- coproductDisjoint (X : ι → C) : CoproductDisjoint X
Instances
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.
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.