isVanKampenColimit_of_isEmpty — Mathlib

English

For an empty index J, if there is a strict initial object, the van Kampen colimit holds for the associated cocone.

Русский

Для пустого индекса J, при наличии строгого начального объекта, существует ван kampen колимит для связанного кокона.

LaTeX

$$$[HasStrictInitialObjects C] \\wedge [IsEmpty J] \\Rightarrow IsVanKampenColimit(\\mathrm{asEmptyCocone}(F))$$$

Lean4

theorem isVanKampenColimit_of_isEmpty [HasStrictInitialObjects C] [IsEmpty J] {F : J ⥤ C} (c : Cocone F)
    (hc : IsColimit c) : IsVanKampenColimit c :=
  by
  have : IsInitial c.pt :=
    by
    have :=
      (IsColimit.precomposeInvEquiv (Functor.uniqueFromEmpty _) _).symm
        (hc.whiskerEquivalence (equivalenceOfIsEmpty (Discrete PEmpty.{1}) J))
    exact IsColimit.ofIsoColimit this (Cocones.ext (Iso.refl c.pt) (fun {X} ↦ isEmptyElim X))
  replace this := IsInitial.isVanKampenColimit this
  apply (IsVanKampenColimit.whiskerEquivalence_iff (equivalenceOfIsEmpty (Discrete PEmpty.{1}) J)).mp
  exact
    (this.precompose_isIso
          (Functor.uniqueFromEmpty ((equivalenceOfIsEmpty (Discrete PEmpty.{1}) J).functor ⋙ F)).hom).of_iso
      (Cocones.ext (Iso.refl _) (by simp))

Похожие утверждения