limIso

Mathlib.CategoryTheory.Limits.Final

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.Initial.limIso

Lean4

/-- A pointfree version of `limitIso`, stating that whiskering by `F` followed by taking the
limit is isomorpic to taking the limit on the codomain of `F`. -/
def limIso [HasLimitsOfShape D E] [HasLimitsOfShape C E] : (whiskeringLeft _ _ _).obj F ⋙ lim ≅ lim (J := D) (C := E) :=
  Iso.symm <|
    NatIso.ofComponents (fun G => (limitIso F G).symm) fun f =>
      by
      simp only [comp_obj, whiskeringLeft_obj_obj, lim_obj, comp_map, whiskeringLeft_obj_map, lim_map, Iso.symm_hom,
        limitIso_inv]
      ext
      simp

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru