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.
- hasPullbackInl : ∀ {X Y Z : C} (f : Z ⟶ X ⨿ Y), CategoryTheory.Limits.HasPullback CategoryTheory.Limits.coprod.inl f
Instances
A functor preserves pullback of inclusions if it preserves all pullbacks along coproduct injections.
- preservesPullbackInl : {X Y Z : C} → (f : Z ⟶ X ⨿ Y) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan CategoryTheory.Limits.coprod.inl f) F
Instances
A category is (finitary) pre-extensive if it has finite coproducts, and binary coproducts are universal.
- hasFiniteCoproducts : CategoryTheory.Limits.HasFiniteCoproducts C
- hasPullbacksOfInclusions : CategoryTheory.HasPullbacksOfInclusions C
- universal' : ∀ {X Y : C} (c : CategoryTheory.Limits.BinaryCofan X Y), CategoryTheory.Limits.IsColimit c → CategoryTheory.IsUniversalColimit c
In a finitary extensive category, all coproducts are van Kampen
Instances
In a finitary extensive category, all coproducts are van Kampen
A category is (finitary) extensive if it has finite coproducts, and binary coproducts are van Kampen.
- hasFiniteCoproducts : CategoryTheory.Limits.HasFiniteCoproducts C
- hasPullbacksOfInclusions : CategoryTheory.HasPullbacksOfInclusions C
- van_kampen' : ∀ {X Y : C} (c : CategoryTheory.Limits.BinaryCofan X Y), CategoryTheory.Limits.IsColimit c → CategoryTheory.IsVanKampenColimit c
In a finitary extensive category, all coproducts are van Kampen
Instances
In a finitary extensive category, all coproducts are van Kampen
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- CategoryTheory.PreservesPullbacksOfInclusions.instOfPreservesLimitsOfShapeWalkingCospan F = CategoryTheory.PreservesPullbacksOfInclusions.mk
Equations
- CategoryTheory.PreservesPullbacksOfInclusions.preservesPullbackInl' F f = CategoryTheory.Limits.preservesPullbackSymmetry F CategoryTheory.Limits.coprod.inl f
Equations
- One or more equations did not get rendered due to their size.
Equations
- CategoryTheory.PreservesPullbacksOfInclusions.preservesPullbackInr F f = CategoryTheory.Limits.preservesPullbackSymmetry F f CategoryTheory.Limits.coprod.inr
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
(Implementation) An auxiliary lemma for the proof that TopCat
is finitary extensive.
Equations
- CategoryTheory.finitaryExtensiveTopCatAux Z f = ⋯.some
Instances For
Equations
- ⋯ = ⋯
Equations
- One or more equations did not get rendered due to their size.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯