Theorems · Definition · category theory

CategoryTheory.IsVanKampenColimit

{J : Type v'} →
  [inst : CategoryTheory.Category.{u', v'} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor J 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.

Defined in

Mathlib.CategoryTheory.Limits.VanKampen

Cited by

26 results in Mathlib

Foundations

Depth 23 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Category