Extensive categories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main definitions #

category_theory.is_van_kampen_colimit: 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.
category_theory.finitary_extensive: A category is (finitary) extensive if it has finite coproducts, and binary coproducts are van Kampen.

Main Results #

category_theory.has_strict_initial_objects_of_finitary_extensive: The initial object in extensive categories is strict.
category_theory.finitary_extensive.mono_inr_of_is_colimit: Coproduct injections are monic in extensive categories.
category_theory.binary_cofan.is_pullback_initial_to_of_is_van_kampen: In extensive categories, sums are disjoint, i.e. the pullback of X ⟶ X ⨿ Y and Y ⟶ X ⨿ Y is the initial object.
category_theory.types.finitary_extensive: 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 #

source

def category_theory.nat_trans.equifibered {J : Type v'} [category_theory.category J] {C : Type u} [category_theory.category C] {F G : 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)

Equations

category_theory.nat_trans.equifibered α = ∀ ⦃i j : J⦄ (f : i ⟶ j), category_theory.is_pullback (F.map f) (α.app i) (α.app j) (G.map f)

source

theorem category_theory.nat_trans.equifibered_of_is_iso {J : Type v'} [category_theory.category J] {C : Type u} [category_theory.category C] {F G : J ⥤ C} (α : F ⟶ G) [category_theory.is_iso α] :

category_theory.nat_trans.equifibered α

source

theorem category_theory.nat_trans.equifibered.comp {J : Type v'} [category_theory.category J] {C : Type u} [category_theory.category C] {F G H : J ⥤ C} {α : F ⟶ G} {β : G ⟶ H} (hα : category_theory.nat_trans.equifibered α) (hβ : category_theory.nat_trans.equifibered β) :

category_theory.nat_trans.equifibered (α ≫ β)

source

def category_theory.is_universal_colimit {J : Type v'} [category_theory.category J] {C : Type u} [category_theory.category C] {F : J ⥤ C} (c : category_theory.limits.cocone F) :

Prop

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

Equations

category_theory.is_universal_colimit c = ∀ ⦃F' : J ⥤ C⦄ (c' : category_theory.limits.cocone F') (α : F' ⟶ F) (f : c'.X ⟶ c.X), α ≫ c.ι = c'.ι ≫ (category_theory.functor.const J).map f → category_theory.nat_trans.equifibered α → (∀ (j : J), category_theory.is_pullback (c'.ι.app j) (α.app j) f (c.ι.app j)) → nonempty (category_theory.limits.is_colimit c')

source

def category_theory.is_van_kampen_colimit {J : Type v'} [category_theory.category J] {C : Type u} [category_theory.category C] {F : J ⥤ C} (c : category_theory.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.

Equations