compUniqFunctor

Mathlib.CategoryTheory.Localization.Predicate

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Localization.compUniqFunctor

Lean4

/-- The functor of equivalence of localized categories given by `Localization.uniq` is
compatible with the localization functors. -/
def compUniqFunctor : L₁ ⋙ (uniq L₁ L₂ W').functor ≅ L₂ :=
  calc
    L₁ ⋙ (uniq L₁ L₂ W').functor ≅ (L₁ ⋙ (equivalenceFromModel L₁ W').inverse) ⋙ (equivalenceFromModel L₂ W').functor :=
      (associator _ _ _).symm
    _ ≅ W'.Q ⋙ (equivalenceFromModel L₂ W').functor := (isoWhiskerRight (compEquivalenceFromModelInverseIso L₁ W') _)
    _ ≅ L₂ := qCompEquivalenceFromModelFunctorIso L₂ W'

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

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

Разделы

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

Аффилиация

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