Extensive categories #
Main definitions #
CategoryTheory.FinitaryExtensive
: A category is (finitary) extensive if it has finite coproducts, and binary coproducts are van Kampen.
Main Results #
CategoryTheory.hasStrictInitialObjects_of_finitaryExtensive
: The initial object in extensive categories is strict.CategoryTheory.FinitaryExtensive.mono_inr_of_isColimit
: Coproduct injections are monic in extensive categories.CategoryTheory.BinaryCofan.isPullback_initial_to_of_isVanKampen
: In extensive categories, sums are disjoint, i.e. the pullback ofX ⟶ X ⨿ Y
andY ⟶ X ⨿ Y
is the initial object.CategoryTheory.types.finitaryExtensive
: The category of types is extensive.CategoryTheory.FinitaryExtensive_TopCat
: The categoryTop
is extensive.CategoryTheory.FinitaryExtensive_functor
: The categoryC ⥤ D
is extensive ifD
has all pullbacks and is extensive.CategoryTheory.FinitaryExtensive.isVanKampen_finiteCoproducts
: Finite coproducts in a finitary extensive category are van Kampen.
TODO #
Show that the following are finitary extensive:
Scheme
AffineScheme
(CommRingᵒᵖ
)
References #
- https://ncatlab.org/nlab/show/extensive+category
- Carboni et al, Introduction to extensive and distributive categories
A category has pullback of inclusions if it has all pullbacks along coproduct injections.
Instances
A functor preserves pullback of inclusions if it preserves all pullbacks along coproduct injections.
- preservesPullbackInl {X Y Z : C} (f : Z ⟶ X ⨿ Y) : Limits.PreservesLimit (Limits.cospan Limits.coprod.inl f) F
Instances
A category is (finitary) pre-extensive if it has finite coproducts, and binary coproducts are universal.
- hasFiniteCoproducts : Limits.HasFiniteCoproducts C
- hasPullbacksOfInclusions : HasPullbacksOfInclusions C
- universal' {X Y : C} (c : Limits.BinaryCofan X Y) : ∀ (a : Limits.IsColimit c), IsUniversalColimit c
In a finitary extensive category, all coproducts are van Kampen
Instances
A category is (finitary) extensive if it has finite coproducts, and binary coproducts are van Kampen.
- hasFiniteCoproducts : Limits.HasFiniteCoproducts C
- hasPullbacksOfInclusions : HasPullbacksOfInclusions C
- van_kampen' {X Y : C} (c : Limits.BinaryCofan X Y) : ∀ (a : Limits.IsColimit c), IsVanKampenColimit c
In a finitary extensive category, all coproducts are van Kampen
Instances
(Implementation) An auxiliary lemma for the proof that TopCat
is finitary extensive.
Equations
Instances For
Alias of CategoryTheory.FinitaryPreExtensive.isIso_sigmaDesc_fst
.
If C
has pullbacks and is finitary (pre-)extensive, pullbacks distribute over finite
coproducts, i.e., ∐ (Xᵢ ×[S] Xⱼ) ≅ (∐ Xᵢ) ×[S] (∐ Xⱼ)
.
For an IsPullback
version, see FinitaryPreExtensive.isPullback_sigmaDesc
.
If C
has pullbacks and is finitary (pre-)extensive, pullbacks distribute over finite
coproducts, i.e., ∐ (Xᵢ ×[S] Xⱼ) ≅ (∐ Xᵢ) ×[S] (∐ Xⱼ)
.
For a variant, see FinitaryPreExtensive.isIso_sigmaDesc_map
.