whiskerEquivalence — Mathlib

English

If G maps cocones with certain preserving properties, and G.mapCocone c is universal, then c is universal as well.

Русский

Если отображение G сохраняет нужные пределы и отображает кокон, который является универсальным, то исходный кокон тоже универсален.

LaTeX

$$$[PreservesLimitsOfShape .. G]\\; [ReflectsColimitsOfShape .. G]\\; (IsUniversalColimit (G.mapCocone c)) \\Rightarrow IsUniversalColimit c$$

Lean4

theorem whiskerEquivalence {K : Type*} [Category K] (e : J ≌ K) {F : K ⥤ C} {c : Cocone F} (hc : IsVanKampenColimit c) :
    IsVanKampenColimit (c.whisker e.functor) := by
  intro F' c' α f e' hα
  convert
    hc (c'.whisker e.inverse) (whiskerLeft e.inverse α ≫ (e.invFunIdAssoc F).hom) f ?_
      ((hα.whiskerLeft _).comp (NatTrans.equifibered_of_isIso _)) using
    1
  · exact (IsColimit.whiskerEquivalenceEquiv e.symm).nonempty_congr
  · simp only [Functor.const_obj_obj, Functor.comp_obj, Cocone.whisker_pt, Cocone.whisker_ι, whiskerLeft_app,
      NatTrans.comp_app, Equivalence.invFunIdAssoc_hom_app, Functor.id_obj]
    constructor
    · intro H k
      rw [← Category.comp_id f]
      refine (H (e.inverse.obj k)).paste_vert ?_
      have : IsIso (𝟙 (Cocone.whisker e.functor c).pt) := inferInstance
      exact IsPullback.of_vert_isIso ⟨by simp⟩
    · intro H j
      have : α.app j = F'.map (e.unit.app _) ≫ α.app _ ≫ F.map (e.counit.app (e.functor.obj j)) := by
        simp [← Functor.map_comp]
      rw [← Category.id_comp f, this]
      refine IsPullback.paste_vert ?_ (H (e.functor.obj j))
      exact IsPullback.of_vert_isIso ⟨by simp⟩
  · ext k
    simpa using congr_app e' (e.inverse.obj k)

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