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][adhesive2004]

def CategoryTheory.NatTrans.Equifibered {J : Type v'} [CategoryTheory.Category.{u', v'} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C} {G : CategoryTheory.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.toPrefunctor.map f) (α.app i) (α.app j) (G.toPrefunctor.map f)

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

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

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

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

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

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

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

Equations

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

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

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

A van Kampen colimit is a colimit.

Equations

• CategoryTheory.IsVanKampenColimit.isColimit h = Nonempty.some (_ : Nonempty (CategoryTheory.Limits.IsColimit c))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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 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')) f → CategoryTheory.CategoryStruct.comp αY (CategoryTheory.Limits.BinaryCofan.inr c) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryCofan.inr (cofans X' Y')) f → CategoryTheory.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 f (CategoryTheory.Limits.BinaryCofan.inl c))) (CategoryTheory.Limits.PullbackCone.fst (cones f (CategoryTheory.Limits.BinaryCofan.inr c))))) : CategoryTheory.IsVanKampenColimit c

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

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

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

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

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

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

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