# Universal colimits and van Kampen colimits #

## Main definitions #

• CategoryTheory.IsUniversalColimit: A (colimit) cocone over a diagram F : J ⥤ C is universal if it is stable under pullbacks.
• CategoryTheory.IsVanKampenColimit: 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.

## References #

def CategoryTheory.NatTrans.Equifibered {J : Type v'} [] {C : Type u} {F : } {G : } (α : F G) :

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
Instances For
theorem CategoryTheory.NatTrans.equifibered_of_isIso {J : Type v'} [] {C : Type u} {F : } {G : } (α : F G) :
theorem CategoryTheory.NatTrans.Equifibered.comp {J : Type v'} [] {C : Type u} {F : } {G : } {H : } {α : F G} {β : G H} :
theorem CategoryTheory.NatTrans.Equifibered.whiskerRight {J : Type v'} [] {C : Type u} {D : Type u_2} [] {F : } {G : } {α : F G} (H : ) [(i j : J) → (f : j i) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (α.app i) (G.map f)) H] :
theorem CategoryTheory.NatTrans.Equifibered.whiskerLeft {J : Type v'} [] {C : Type u} {K : Type u_3} [] {F : } {G : } {α : F G} (H : ) :
theorem CategoryTheory.NatTrans.equifibered_of_discrete {C : Type u} {ι : Type u_3} {F : } {G : } (α : F G) :
def CategoryTheory.IsUniversalColimit {J : Type v'} [] {C : Type u} {F : } (c : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.IsVanKampenColimit {J : Type v'} [] {C : Type u} {F : } (c : ) :

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
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.IsVanKampenColimit.isUniversal {J : Type v'} [] {C : Type u} {F : } {c : } :
noncomputable def CategoryTheory.IsUniversalColimit.isColimit {J : Type v'} [] {C : Type u} {F : } {c : } :

A universal colimit is a colimit.

Equations
• h.isColimit = .some
Instances For
noncomputable def CategoryTheory.IsVanKampenColimit.isColimit {J : Type v'} [] {C : Type u} {F : } {c : } :

A van Kampen colimit is a colimit.

Equations
• h.isColimit = .isColimit
Instances For
theorem CategoryTheory.IsUniversalColimit.of_iso {J : Type v'} [] {C : Type u} {F : } {c : } {c' : } (e : c c') :
theorem CategoryTheory.IsVanKampenColimit.of_iso {J : Type v'} [] {C : Type u} {F : } {c : } {c' : } (e : c c') :
theorem CategoryTheory.IsVanKampenColimit.precompose_isIso {J : Type v'} [] {C : Type u} {F : } {G : } (α : F G) {c : } :
theorem CategoryTheory.IsUniversalColimit.precompose_isIso {J : Type v'} [] {C : Type u} {F : } {G : } (α : F G) {c : } :
theorem CategoryTheory.IsVanKampenColimit.precompose_isIso_iff {J : Type v'} [] {C : Type u} {F : } {G : } (α : F G) {c : } :
theorem CategoryTheory.IsUniversalColimit.of_mapCocone {J : Type v'} [] {C : Type u} {D : Type u_2} [] (G : ) {F : } {c : } (hc : CategoryTheory.IsUniversalColimit (G.mapCocone c)) :
theorem CategoryTheory.IsVanKampenColimit.of_mapCocone {J : Type v'} [] {C : Type u} {D : Type u_2} [] (G : ) {F : } {c : } [(i j : J) → (X : C) → (f : X F.obj j) → (g : i j) → ] [(i : J) → (X : C) → (f : X c.pt) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f (c.app i)) G] (H : CategoryTheory.IsVanKampenColimit (G.mapCocone c)) :
theorem CategoryTheory.IsVanKampenColimit.mapCocone_iff {J : Type v'} [] {C : Type u} {D : Type u_2} [] (G : ) {F : } {c : } [G.IsEquivalence] :
theorem CategoryTheory.IsUniversalColimit.whiskerEquivalence {J : Type v'} [] {C : Type u} {K : Type u_3} [] (e : J K) {F : } {c : } :
theorem CategoryTheory.IsUniversalColimit.whiskerEquivalence_iff {J : Type v'} [] {C : Type u} {K : Type u_3} [] (e : J K) {F : } {c : } :
theorem CategoryTheory.IsVanKampenColimit.whiskerEquivalence {J : Type v'} [] {C : Type u} {K : Type u_3} [] (e : J K) {F : } {c : } :
theorem CategoryTheory.IsVanKampenColimit.whiskerEquivalence_iff {J : Type v'} [] {C : Type u} {K : Type u_3} [] (e : J K) {F : } {c : } :
theorem CategoryTheory.isVanKampenColimit_of_evaluation {J : Type v'} [] {C : Type u} {D : Type u_2} [] (F : ) (c : ) (hc : ∀ (x : C), CategoryTheory.IsVanKampenColimit ((.obj x).mapCocone c)) :
theorem CategoryTheory.IsUniversalColimit.map_reflective {J : Type v'} [] {C : Type u} {D : Type u_2} [] {Gl : } {Gr : } (adj : Gl Gr) [Gr.Full] [Gr.Faithful] {F : } {c : CategoryTheory.Limits.Cocone (F.comp Gr)} [∀ (X : D) (f : X Gl.obj c.pt), CategoryTheory.Limits.HasPullback (Gr.map f) (adj.unit.app c.pt)] [(X : D) → (f : X Gl.obj c.pt) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (Gr.map f) (adj.unit.app c.pt)) Gl] :
theorem CategoryTheory.IsVanKampenColimit.map_reflective {J : Type v'} [] {C : Type u} {D : Type u_2} [] {Gl : } {Gr : } (adj : Gl Gr) [Gr.Full] [Gr.Faithful] {F : } {c : CategoryTheory.Limits.Cocone (F.comp Gr)} [∀ (X : D) (f : X Gl.obj c.pt), CategoryTheory.Limits.HasPullback (Gr.map f) (adj.unit.app c.pt)] [(X : D) → (f : X Gl.obj c.pt) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (Gr.map f) (adj.unit.app c.pt)) Gl] [(X : C) → (i : J) → (f : X c.pt) → CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f (c.app i)) Gl] :
theorem CategoryTheory.isVanKampenColimit_of_isEmpty {J : Type v'} [] {C : Type u} [] {F : } (c : ) (hc : ) :
theorem CategoryTheory.BinaryCofan.isVanKampen_iff {C : Type u} {X : C} {Y : C} (c : ) :
∀ {X' Y' : C} (c' : ) (αX : X' X) (αY : Y' Y) (f : c'.pt c.pt), = = ( CategoryTheory.IsPullback c'.inl αX f c.inl CategoryTheory.IsPullback c'.inr αY f c.inr)
theorem CategoryTheory.BinaryCofan.isVanKampen_mk {C : Type u} {X : C} {Y : C} (c : ) (cofans : (X Y : C) → ) (colimits : (X Y : C) → CategoryTheory.Limits.IsColimit (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) → CategoryTheory.Limits.IsLimit (cones f g)) (h₁ : ∀ {X' Y' : C} (αX : X' X) (αY : Y' Y) (f : (cofans X' Y').pt c.pt), = CategoryTheory.CategoryStruct.comp (cofans X' Y').inl f = CategoryTheory.CategoryStruct.comp (cofans X' Y').inr fCategoryTheory.IsPullback (cofans X' Y').inl αX f c.inl CategoryTheory.IsPullback (cofans X' Y').inr αY f c.inr) (h₂ : {Z : C} → (f : Z c.pt) → CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)) :
theorem CategoryTheory.isUniversalColimit_extendCofan {C : Type u} {n : } (f : Fin (n + 1)C) {c₁ : CategoryTheory.Limits.Cofan fun (i : Fin n) => f i.succ} {c₂ : CategoryTheory.Limits.BinaryCofan (f 0) c₁.pt} (t₁ : ) (t₂ : ) [∀ {Z : C} (i : Z c₂.pt), ] :
theorem CategoryTheory.isVanKampenColimit_extendCofan {C : Type u} {n : } (f : Fin (n + 1)C) {c₁ : CategoryTheory.Limits.Cofan fun (i : Fin n) => f i.succ} {c₂ : CategoryTheory.Limits.BinaryCofan (f 0) c₁.pt} (t₁ : ) (t₂ : ) [∀ {Z : C} (i : Z c₂.pt), ] :
theorem CategoryTheory.isPullback_of_cofan_isVanKampen {C : Type u} {ι : Type u_3} {X : ιC} {c : } (i : ι) (j : ι) [] :
CategoryTheory.IsPullback (if h : j = i then else ) (if h : j = i then else ) (c.inj i) (c.inj j)
theorem CategoryTheory.isPullback_initial_to_of_cofan_isVanKampen {C : Type u} {ι : Type u_3} {F : } {c : } (i : ) (j : ) (hi : i j) :
theorem CategoryTheory.mono_of_cofan_isVanKampen {C : Type u} {ι : Type u_3} {F : } {c : } (i : ) :
CategoryTheory.Mono (c.app i)