Documentation

Mathlib.CategoryTheory.Extensive

Extensive categories #

Main definitions #

Main Results #

TODO #

Show that the following are finitary extensive:

References #

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 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
          theorem CategoryTheory.BinaryCofan.isVanKampen_mk {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (c : CategoryTheory.Limits.BinaryCofan X Y) (cofans : (X Y : C) → CategoryTheory.Limits.BinaryCofan X Y) (colimits : (X Y : C) → CategoryTheory.Limits.IsColimit (cofans X Y)) (cones : {X Y Z : C} → (f : X Z) → (g : Y Z) → CategoryTheory.Limits.PullbackCone f g) (limits : {X Y Z : C} → (f : X Z) → (g : Y Z) → CategoryTheory.Limits.IsLimit (cones X Y Z f g)) (h₁ : ∀ {X' Y' : C} (αX : X' X) (αY : Y' Y) (f : (cofans X' Y').pt c.pt), CategoryTheory.CategoryStruct.comp αX (CategoryTheory.Limits.BinaryCofan.inl c) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryCofan.inl (cofans X' Y')) fCategoryTheory.CategoryStruct.comp αY (CategoryTheory.Limits.BinaryCofan.inr c) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryCofan.inr (cofans X' Y')) fCategoryTheory.IsPullback (CategoryTheory.Limits.BinaryCofan.inl (cofans X' Y')) αX f (CategoryTheory.Limits.BinaryCofan.inl c) CategoryTheory.IsPullback (CategoryTheory.Limits.BinaryCofan.inr (cofans X' Y')) αY f (CategoryTheory.Limits.BinaryCofan.inr c)) (h₂ : {Z : C} → (f : Z c.pt) → CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk (CategoryTheory.Limits.PullbackCone.fst (cones Z ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left }) c.pt f (CategoryTheory.Limits.BinaryCofan.inl c))) (CategoryTheory.Limits.PullbackCone.fst (cones Z ((CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right }) c.pt f (CategoryTheory.Limits.BinaryCofan.inr c))))) :