Structures · Category theory
CategoryTheory.Limits.CoproductDisjoint
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.
- Shape
- One type argument · adds nonempty_isInitial_of_ne, mono_inj
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by11
- CategoryTheory.Mono.of_coproductDisjoint
- CategoryTheory.Limits.IsInitial.ofCoproductDisjointOfIsColimit
- CategoryTheory.Limits.CoproductDisjoint.mono_inj
- CategoryTheory.Mono.ι_of_coproductDisjoint
- CategoryTheory.Limits.CoproductDisjoint.isPullback_of_isInitial
- CategoryTheory.Limits.CoproductDisjoint.nonempty_isInitial_of_ne
- CategoryTheory.Limits.IsInitial.ofCoproductDisjointOfIsColimit.congr_simp
- CategoryTheory.Limits.IsInitial.ofCoproductDisjoint
- CategoryTheory.Limits.IsInitial.ofCoproductDisjointOfIsLimit
- CategoryTheory.Limits.IsInitial.ofCoproductDisjointOfIsColimitOfIsLimit
- CategoryTheory.Limits.IsInitial.ofCoproductDisjointOfCommSq
Ancestors0
No ancestors.