# mathlib3documentation

category_theory.extensive

# 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 #

def category_theory.nat_trans.equifibered {J : Type v'} {C : Type u} {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
theorem category_theory.nat_trans.equifibered_of_is_iso {J : Type v'} {C : Type u} {F G : J C} (α : F G)  :
theorem category_theory.nat_trans.equifibered.comp {J : Type v'} {C : Type u} {F G H : J C} {α : F G} {β : G H}  :
def category_theory.is_universal_colimit {J : Type v'} {C : Type u} {F : J C}  :
Prop

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

Equations
def category_theory.is_van_kampen_colimit {J : Type v'} {C : Type u} {F : J C}  :
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
theorem category_theory.is_van_kampen_colimit.is_universal {J : Type v'} {C : Type u} {F : J C}  :
noncomputable def category_theory.is_van_kampen_colimit.is_colimit {J : Type v'} {C : Type u} {F : J C}  :

A van Kampen colimit is a colimit.

Equations
@[class]
structure category_theory.finitary_extensive (C : Type u)  :
Prop
• has_finite_coproducts :
• 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 of this typeclass
theorem category_theory.map_pair_equifibered {C : Type u} (α : F F') :
theorem category_theory.binary_cofan.is_van_kampen_iff {C : Type u} {X Y : C}  :
{X' Y' : C} (c' : (αX : X' X) (αY : Y' Y) (f : c'.X c.X), αX c.inl = c'.inl f αY c.inr = c'.inr f f c.inl f c.inr)
theorem category_theory.binary_cofan.is_van_kampen_mk {C : Type u} {X Y : C} (cofans : Π (X Y : C), ) (colimits : Π (X Y : C), category_theory.limits.is_colimit (cofans X Y)) (cones : Π {X Y Z : C} (f : X Z) (g : Y Z), ) (limits : Π {X Y Z : C} (f : X Z) (g : Y Z), category_theory.limits.is_limit (cones f g)) (h₁ : {X' Y' : C} (αX : X' X) (αY : Y' Y) (f : (cofans X' Y').X c.X), αX c.inl = (cofans X' Y').inl f αY c.inr = (cofans X' Y').inr f category_theory.is_pullback (cofans X' Y').inl αX f c.inl category_theory.is_pullback (cofans X' Y').inr αY f c.inr) (h₂ : Π {Z : C} (f : Z c.X), category_theory.limits.is_colimit (category_theory.limits.binary_cofan.mk (cones f c.inl).fst (cones f c.inr).fst)) :
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]

(Implementation) An auxiliary lemma for the proof that Top is finitary extensive.

Equations
@[protected, instance]
theorem category_theory.nat_trans.equifibered.whisker_right {J : Type v'} {C : Type u} {D : Type u''} {F G : J C} {α : F G} (H : C D)  :
theorem category_theory.is_van_kampen_colimit.of_iso {J : Type v'} {C : Type u} {F : J C} {c c' : category_theory.limits.cocone F} (e : c c') :
theorem category_theory.is_van_kampen_colimit_of_evaluation {J : Type v'} {C : Type u} {D : Type u''} (F : J C D) (hc : (x : C), ) :
@[protected, instance]