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

• https://ncatlab.org/nlab/show/van+Kampen+colimit
• Stephen Lack and Paweł Sobociński, Adhesive Categories

def CategoryTheory.NatTrans.Equifibered {J : Type v'} [Category.{u', v'} J] {C : Type u} [Category.{v, u} C] {F G : Functor 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

• CategoryTheory.NatTrans.Equifibered α = ∀ ⦃i j : J⦄ (f : i ⟶ j), CategoryTheory.IsPullback (F.map f) (α.app i) (α.app j) (G.map f)

theorem CategoryTheory.NatTrans.equifibered_of_isIso {J : Type v'} [Category.{u', v'} J] {C : Type u} [Category.{v, u} C] {F G : Functor J C} (α : F ⟶ G) [IsIso α] : Equifibered α

theorem CategoryTheory.NatTrans.Equifibered.comp {J : Type v'} [Category.{u', v'} J] {C : Type u} [Category.{v, u} C] {F G H : Functor J C} {α : F ⟶ G} {β : G ⟶ H} (hα : Equifibered α) (hβ : Equifibered β) : Equifibered (CategoryStruct.comp α β)

theorem CategoryTheory.NatTrans.Equifibered.whiskerRight {J : Type v'} [Category.{u', v'} J] {C : Type u} [Category.{v, u} C] {D : Type u_2} [Category.{u_3, u_2} D] {F G : Functor J C} {α : F ⟶ G} (hα : Equifibered α) (H : Functor C D) [∀ (i j : J) (f : j ⟶ i), Limits.PreservesLimit (Limits.cospan (α.app i) (G.map f)) H] : Equifibered (CategoryTheory.whiskerRight α H)

theorem CategoryTheory.NatTrans.Equifibered.whiskerLeft {J : Type v'} [Category.{u', v'} J] {C : Type u} [Category.{v, u} C] {K : Type u_3} [Category.{u_4, u_3} K] {F G : Functor J C} {α : F ⟶ G} (hα : Equifibered α) (H : Functor K J) : Equifibered (CategoryTheory.whiskerLeft H α)

theorem CategoryTheory.mapPair_equifibered {C : Type u} [Category.{v, u} C] {F F' : Functor (Discrete Limits.WalkingPair) C} (α : F ⟶ F') : NatTrans.Equifibered α

theorem CategoryTheory.NatTrans.equifibered_of_discrete {C : Type u} [Category.{v, u} C] {ι : Type u_3} {F G : Functor (Discrete ι) C} (α : F ⟶ G) : Equifibered α

def CategoryTheory.IsUniversalColimit {J : Type v'} [Category.{u', v'} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} (c : Limits.Cocone F) : Prop

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.

def CategoryTheory.IsVanKampenColimit {J : Type v'} [Category.{u', v'} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} (c : 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.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.IsVanKampenColimit.isUniversal {J : Type v'} [Category.{u', v'} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} {c : Limits.Cocone F} (H : IsVanKampenColimit c) : IsUniversalColimit c

noncomputable def CategoryTheory.IsUniversalColimit.isColimit {J : Type v'} [Category.{u', v'} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} {c : Limits.Cocone F} (h : IsUniversalColimit c) : Limits.IsColimit c

A universal colimit is a colimit.

Equations

• h.isColimit = ⋯.some

noncomputable def CategoryTheory.IsVanKampenColimit.isColimit {J : Type v'} [Category.{u', v'} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} {c : Limits.Cocone F} (h : IsVanKampenColimit c) : Limits.IsColimit c

A van Kampen colimit is a colimit.

Equations

• h.isColimit = ⋯.isColimit

theorem CategoryTheory.IsInitial.isVanKampenColimit {C : Type u} [Category.{v, u} C] [Limits.HasStrictInitialObjects C] {X : C} (h : Limits.IsInitial X) : IsVanKampenColimit (Limits.asEmptyCocone X)

theorem CategoryTheory.IsUniversalColimit.of_iso {J : Type v'} [Category.{u', v'} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} {c c' : Limits.Cocone F} (hc : IsUniversalColimit c) (e : c ≅ c') : IsUniversalColimit c'

theorem CategoryTheory.IsVanKampenColimit.of_iso {J : Type v'} [Category.{u', v'} J] {C : Type u} [Category.{v, u} C] {F : Functor J C} {c c' : Limits.Cocone F} (H : IsVanKampenColimit c) (e : c ≅ c') : IsVanKampenColimit c'

theorem CategoryTheory.IsVanKampenColimit.precompose_isIso {J : Type v'} [Category.{u', v'} J] {C : Type u} [Category.{v, u} C] {F G : Functor J C} (α : F ⟶ G) [IsIso α] {c : Limits.Cocone G} (hc : IsVanKampenColimit c) : IsVanKampenColimit ((Limits.Cocones.precompose α).obj c)

theorem CategoryTheory.IsUniversalColimit.precompose_isIso {J : Type v'} [Category.{u', v'} J] {C : Type u} [Category.{v, u} C] {F G : Functor J C} (α : F ⟶ G) [IsIso α] {c : Limits.Cocone G} (hc : IsUniversalColimit c) : IsUniversalColimit ((Limits.Cocones.precompose α).obj c)

theorem CategoryTheory.IsVanKampenColimit.precompose_isIso_iff {J : Type v'} [Category.{u', v'} J] {C : Type u} [Category.{v, u} C] {F G : Functor J C} (α : F ⟶ G) [IsIso α] {c : Limits.Cocone G} : IsVanKampenColimit ((Limits.Cocones.precompose α).obj c) ↔ IsVanKampenColimit c

theorem CategoryTheory.IsUniversalColimit.of_mapCocone {J : Type v'} [Category.{u', v'} J] {C : Type u} [Category.{v, u} C] {D : Type u_2} [Category.{u_3, u_2} D] (G : Functor C D) {F : Functor J C} {c : Limits.Cocone F} [Limits.PreservesLimitsOfShape Limits.WalkingCospan G] [Limits.ReflectsColimitsOfShape J G] (hc : IsUniversalColimit (G.mapCocone c)) : IsUniversalColimit c

theorem CategoryTheory.IsVanKampenColimit.of_mapCocone {J : Type v'} [Category.{u', v'} J] {C : Type u} [Category.{v, u} C] {D : Type u_2} [Category.{u_3, u_2} D] (G : Functor C D) {F : Functor J C} {c : Limits.Cocone F} [∀ (i j : J) (X : C) (f : X ⟶ F.obj j) (g : i ⟶ j), Limits.PreservesLimit (Limits.cospan f (F.map g)) G] [∀ (i : J) (X : C) (f : X ⟶ c.pt), Limits.PreservesLimit (Limits.cospan f (c.ι.app i)) G] [Limits.ReflectsLimitsOfShape Limits.WalkingCospan G] [Limits.PreservesColimitsOfShape J G] [Limits.ReflectsColimitsOfShape J G] (H : IsVanKampenColimit (G.mapCocone c)) : IsVanKampenColimit c

theorem CategoryTheory.IsVanKampenColimit.mapCocone_iff {J : Type v'} [Category.{u', v'} J] {C : Type u} [Category.{v, u} C] {D : Type u_2} [Category.{u_3, u_2} D] (G : Functor C D) {F : Functor J C} {c : Limits.Cocone F} [G.IsEquivalence] : IsVanKampenColimit (G.mapCocone c) ↔ IsVanKampenColimit c

theorem CategoryTheory.IsUniversalColimit.whiskerEquivalence {J : Type v'} [Category.{u', v'} J] {C : Type u} [Category.{v, u} C] {K : Type u_3} [Category.{u_4, u_3} K] (e : J ≌ K) {F : Functor K C} {c : Limits.Cocone F} (hc : IsUniversalColimit c) : IsUniversalColimit (Limits.Cocone.whisker e.functor c)

theorem CategoryTheory.IsUniversalColimit.whiskerEquivalence_iff {J : Type v'} [Category.{u', v'} J] {C : Type u} [Category.{v, u} C] {K : Type u_3} [Category.{u_4, u_3} K] (e : J ≌ K) {F : Functor K C} {c : Limits.Cocone F} : IsUniversalColimit (Limits.Cocone.whisker e.functor c) ↔ IsUniversalColimit c

theorem CategoryTheory.IsVanKampenColimit.whiskerEquivalence {J : Type v'} [Category.{u', v'} J] {C : Type u} [Category.{v, u} C] {K : Type u_3} [Category.{u_4, u_3} K] (e : J ≌ K) {F : Functor K C} {c : Limits.Cocone F} (hc : IsVanKampenColimit c) : IsVanKampenColimit (Limits.Cocone.whisker e.functor c)

theorem CategoryTheory.IsVanKampenColimit.whiskerEquivalence_iff {J : Type v'} [Category.{u', v'} J] {C : Type u} [Category.{v, u} C] {K : Type u_3} [Category.{u_4, u_3} K] (e : J ≌ K) {F : Functor K C} {c : Limits.Cocone F} : IsVanKampenColimit (Limits.Cocone.whisker e.functor c) ↔ IsVanKampenColimit c

theorem CategoryTheory.isVanKampenColimit_of_evaluation {J : Type v'} [Category.{u', v'} J] {C : Type u} [Category.{v, u} C] {D : Type u_2} [Category.{u_3, u_2} D] [Limits.HasPullbacks D] [Limits.HasColimitsOfShape J D] (F : Functor J (Functor C D)) (c : Limits.Cocone F) (hc : ∀ (x : C), IsVanKampenColimit (((evaluation C D).obj x).mapCocone c)) : IsVanKampenColimit c

theorem CategoryTheory.IsUniversalColimit.map_reflective {J : Type v'} [Category.{u', v'} J] {C : Type u} [Category.{v, u} C] {D : Type u_2} [Category.{u_3, u_2} D] {Gl : Functor C D} {Gr : Functor D C} (adj : Gl ⊣ Gr) [Gr.Full] [Gr.Faithful] {F : Functor J D} {c : Limits.Cocone (F.comp Gr)} (H : IsUniversalColimit c) [∀ (X : D) (f : X ⟶ Gl.obj c.pt), Limits.HasPullback (Gr.map f) (adj.unit.app c.pt)] [∀ (X : D) (f : X ⟶ Gl.obj c.pt), Limits.PreservesLimit (Limits.cospan (Gr.map f) (adj.unit.app c.pt)) Gl] : IsUniversalColimit (Gl.mapCocone c)

theorem CategoryTheory.IsVanKampenColimit.map_reflective {J : Type v'} [Category.{u', v'} J] {C : Type u} [Category.{v, u} C] {D : Type u_2} [Category.{u_3, u_2} D] [Limits.HasColimitsOfShape J C] {Gl : Functor C D} {Gr : Functor D C} (adj : Gl ⊣ Gr) [Gr.Full] [Gr.Faithful] {F : Functor J D} {c : Limits.Cocone (F.comp Gr)} (H : IsVanKampenColimit c) [∀ (X : D) (f : X ⟶ Gl.obj c.pt), Limits.HasPullback (Gr.map f) (adj.unit.app c.pt)] [∀ (X : D) (f : X ⟶ Gl.obj c.pt), Limits.PreservesLimit (Limits.cospan (Gr.map f) (adj.unit.app c.pt)) Gl] [∀ (X : C) (i : J) (f : X ⟶ c.pt), Limits.PreservesLimit (Limits.cospan f (c.ι.app i)) Gl] : IsVanKampenColimit (Gl.mapCocone c)

theorem CategoryTheory.hasStrictInitial_of_isUniversal {C : Type u} [Category.{v, u} C] [Limits.HasInitial C] (H : IsUniversalColimit (Limits.BinaryCofan.mk (CategoryStruct.id (⊥_ C)) (CategoryStruct.id (⊥_ C)))) : Limits.HasStrictInitialObjects C

theorem CategoryTheory.isVanKampenColimit_of_isEmpty {J : Type v'} [Category.{u', v'} J] {C : Type u} [Category.{v, u} C] [Limits.HasStrictInitialObjects C] [IsEmpty J] {F : Functor J C} (c : Limits.Cocone F) (hc : Limits.IsColimit c) : IsVanKampenColimit c

theorem CategoryTheory.BinaryCofan.isVanKampen_iff {C : Type u} [Category.{v, u} C] {X Y : C} (c : Limits.BinaryCofan X Y) : IsVanKampenColimit c ↔ ∀ {X' Y' : C} (c' : Limits.BinaryCofan X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt), CategoryStruct.comp αX c.inl = CategoryStruct.comp c'.inl f → CategoryStruct.comp αY c.inr = CategoryStruct.comp c'.inr f → (Nonempty (Limits.IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr)

theorem CategoryTheory.BinaryCofan.isVanKampen_mk {C : Type u} [Category.{v, u} C] {X Y : C} (c : Limits.BinaryCofan X Y) (cofans : (X Y : C) → Limits.BinaryCofan X Y) (colimits : (X Y : C) → Limits.IsColimit (cofans X Y)) (cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → Limits.PullbackCone f g) (limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → Limits.IsLimit (cones f g)) (h₁ : ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt), CategoryStruct.comp αX c.inl = CategoryStruct.comp (cofans X' Y').inl f → CategoryStruct.comp αY c.inr = CategoryStruct.comp (cofans X' Y').inr f → IsPullback (cofans X' Y').inl αX f c.inl ∧ IsPullback (cofans X' Y').inr αY f c.inr) (h₂ : {Z : C} → (f : Z ⟶ c.pt) → Limits.IsColimit (Limits.BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)) : IsVanKampenColimit c

theorem CategoryTheory.BinaryCofan.mono_inr_of_isVanKampen {C : Type u} [Category.{v, u} C] [Limits.HasInitial C] {X Y : C} {c : Limits.BinaryCofan X Y} (h : IsVanKampenColimit c) : Mono c.inr

theorem CategoryTheory.BinaryCofan.isPullback_initial_to_of_isVanKampen {C : Type u} [Category.{v, u} C] {X Y : C} [Limits.HasInitial C] {c : Limits.BinaryCofan X Y} (h : IsVanKampenColimit c) : IsPullback (Limits.initial.to ((Limits.pair X Y).obj { as := Limits.WalkingPair.left })) (Limits.initial.to ((Limits.pair X Y).obj { as := Limits.WalkingPair.right })) c.inl c.inr

theorem CategoryTheory.isUniversalColimit_extendCofan {C : Type u} [Category.{v, u} C] {n : ℕ} (f : Fin (n + 1) → C) {c₁ : Limits.Cofan fun (i : Fin n) => f i.succ} {c₂ : Limits.BinaryCofan (f 0) c₁.pt} (t₁ : IsUniversalColimit c₁) (t₂ : IsUniversalColimit c₂) [∀ {Z : C} (i : Z ⟶ c₂.pt), Limits.HasPullback c₂.inr i] : IsUniversalColimit (extendCofan c₁ c₂)

theorem CategoryTheory.isVanKampenColimit_extendCofan {C : Type u} [Category.{v, u} C] {n : ℕ} (f : Fin (n + 1) → C) {c₁ : Limits.Cofan fun (i : Fin n) => f i.succ} {c₂ : Limits.BinaryCofan (f 0) c₁.pt} (t₁ : IsVanKampenColimit c₁) (t₂ : IsVanKampenColimit c₂) [∀ {Z : C} (i : Z ⟶ c₂.pt), Limits.HasPullback c₂.inr i] [Limits.HasFiniteCoproducts C] : IsVanKampenColimit (extendCofan c₁ c₂)

theorem CategoryTheory.isPullback_of_cofan_isVanKampen {C : Type u} [Category.{v, u} C] [Limits.HasInitial C] {ι : Type u_3} {X : ι → C} {c : Limits.Cofan X} (hc : IsVanKampenColimit c) (i j : ι) [DecidableEq ι] : IsPullback (if h : j = i then eqToHom ⋯ else CategoryStruct.comp (eqToHom ⋯) (Limits.initial.to (X i))) (if h : j = i then eqToHom ⋯ else CategoryStruct.comp (eqToHom ⋯) (Limits.initial.to (X j))) (c.inj i) (c.inj j)

theorem CategoryTheory.isPullback_initial_to_of_cofan_isVanKampen {C : Type u} [Category.{v, u} C] [Limits.HasInitial C] {ι : Type u_3} {F : Functor (Discrete ι) C} {c : Limits.Cocone F} (hc : IsVanKampenColimit c) (i j : Discrete ι) (hi : i ≠ j) : IsPullback (Limits.initial.to (F.obj i)) (Limits.initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)

theorem CategoryTheory.mono_of_cofan_isVanKampen {C : Type u} [Category.{v, u} C] [Limits.HasInitial C] {ι : Type u_3} {F : Functor (Discrete ι) C} {c : Limits.Cocone F} (hc : IsVanKampenColimit c) (i : Discrete ι) : Mono (c.ι.app i)