forgetCreatesLimits

Mathlib.Topology.Category.Compactum

URI: https://scilib.ai/kg/mathlib#CompHaus.forgetCreatesLimits

Lean4

noncomputable instance forgetCreatesLimits : CreatesLimits (forget CompHaus) :=
  by
  let e : forget CompHaus ≅ compactumToCompHaus.inv ⋙ Compactum.forget :=
    (((forget CompHaus).leftUnitor.symm ≪≫
          Functor.isoWhiskerRight compactumToCompHaus.asEquivalence.symm.unitIso (forget CompHaus)) ≪≫
        compactumToCompHaus.inv.associator compactumToCompHaus (forget CompHaus)) ≪≫
      Functor.isoWhiskerLeft _ compactumToCompHausCompForget
  exact createsLimitsOfNatIso e.symm

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

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

Разделы

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

Аффилиация

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