Extensive categories #

Main definitions #

CategoryTheory.IsVanKampenColimit: 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.
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 of X ⟶ X ⨿ Y and Y ⟶ 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]

source

def CategoryTheory.NatTrans.Equifibered {J : Type v'} [CategoryTheory.Category.{u', v'} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor J C} (α : F ⟶ G) :

Prop

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

source

theorem CategoryTheory.NatTrans.equifibered_of_isIso {J : Type v'} [CategoryTheory.Category.{u', v'} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor J C} (α : F ⟶ G) [CategoryTheory.IsIso α] :

CategoryTheory.NatTrans.Equifibered α

source

theorem CategoryTheory.NatTrans.Equifibered.comp {J : Type v'} [CategoryTheory.Category.{u', v'} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C} {G : CategoryTheory.Functor J C} {H : CategoryTheory.Functor J C} {α : F ⟶ G} {β : G ⟶ H} (hα : CategoryTheory.NatTrans.Equifibered α) (hβ : CategoryTheory.NatTrans.Equifibered β) :

CategoryTheory.NatTrans.Equifibered (CategoryTheory.CategoryStruct.comp α β)

source

def CategoryTheory.IsUniversalColimit {J : Type v'} [CategoryTheory.Category.{u', v'} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) :

Prop

A (colimit) cocone over a diagram F : J ⥤ C is universal if it is stable under pullbacks.

Instances For

source

def CategoryTheory.IsVanKampenColimit {J : Type v'} [CategoryTheory.Category.{u', v'} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) :

Prop

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

source