mathlib documentation

category_theory.extensive

Extensive categories #

Main definitions #

Main Results #

TODO #

Show that the following are finitary extensive:

References #

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

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

Equations

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
@[class]

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.binary_cofan.is_van_kampen_mk {C : Type u} [category_theory.category C] {X Y : C} (c : category_theory.limits.binary_cofan X Y) (cofans : Π (X Y : C), category_theory.limits.binary_cofan X Y) (colimits : Π (X Y : C), category_theory.limits.is_colimit (cofans X Y)) (cones : Π {X Y Z : C} (f : X Z) (g : Y Z), category_theory.limits.pullback_cone f g) (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)) :

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

Equations