English
For an isomorphism α, IsVanKampenColimit ((Cocones.precompose α).obj c) iff IsVanKampenColimit c.
Русский
При изоморфизме α верно: IsVanKampenColimit ((Cocones.precompose α).obj c) ⇔ IsVanKampenColimit c.
LaTeX
$$$IsVanKampenColimit((\\mathrm{Cocones.precompose}(\\alpha)).{ }_{{}}\\!\\!\\!\\!.obj c) \\iff IsVanKampenColimit(c)$$$
Lean4
theorem isVanKampenColimit_of_evaluation [HasPullbacks D] [HasColimitsOfShape J D] (F : J ⥤ C ⥤ D) (c : Cocone F)
(hc : ∀ x : C, IsVanKampenColimit (((evaluation C D).obj x).mapCocone c)) : IsVanKampenColimit c :=
by
intro F' c' α f e hα
have := fun x =>
hc x (((evaluation C D).obj x).mapCocone c') (whiskerRight α _) (((evaluation C D).obj x).map f)
(by
ext y
dsimp
exact NatTrans.congr_app (NatTrans.congr_app e y) x)
(hα.whiskerRight _)
constructor
· rintro ⟨hc'⟩ j
refine ⟨⟨(NatTrans.congr_app e j).symm⟩, ⟨evaluationJointlyReflectsLimits _ ?_⟩⟩
refine fun x => (isLimitMapConePullbackConeEquiv _ _).symm ?_
exact ((this x).mp ⟨isColimitOfPreserves _ hc'⟩ _).isLimit
·
exact fun H =>
⟨evaluationJointlyReflectsColimits _ fun x => ((this x).mpr fun j => (H j).map ((evaluation C D).obj x)).some⟩
