Extensive categories #
Main definitions #
CategoryTheory.IsVanKampenColimit
: A (colimit) cocone over a diagramF : J ⥤ C
is van Kampen if for every coconec'
over the pullback of the diagramF' : J ⥤ C'
,c'
is colimiting iffc'
is the pullback ofc
.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.
TODO #
Show that the following are finitary extensive:
- the categories of sheaves over a site
Scheme
AffineScheme
(CommRingᵒᵖ
)
References #
- https://ncatlab.org/nlab/show/extensive+category
- [Carboni et al, Introduction to extensive and distributive categories][CARBONI1993145]
A natural transformation is equifibered if every commutative square of the following form is a pullback.
F(X) → F(Y)
↓ ↓
G(X) → G(Y)
Instances For
A (colimit) cocone over a diagram F : J ⥤ C
is universal if it is stable under pullbacks.
Instances For
A (colimit) cocone over a diagram F : J ⥤ C
is van Kampen if for every cocone c'
over the
pullback of the diagram F' : J ⥤ C'
, c'
is colimiting iff c'
is the pullback of c
.
TODO: Show that this is iff the functor C ⥤ Catᵒᵖ
sending x
to C/x
preserves it.
TODO: Show that this is iff the inclusion functor C ⥤ Span(C)
preserves it.
Instances For
A van Kampen colimit is a colimit.
Instances For
- hasFiniteCoproducts : CategoryTheory.Limits.HasFiniteCoproducts 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
A category is (finitary) extensive if it has finite coproducts, and binary coproducts are van Kampen.
TODO: Show that this is iff all finite coproducts are van Kampen.
Instances
(Implementation) An auxiliary lemma for the proof that TopCat
is finitary extensive.