uliftFunctorCompForgetIso

Mathlib.Topology.Category.TopCat.ULift

URI: https://scilib.ai/kg/mathlib#TopCat.uliftFunctorCompForgetIso

Lean4

/-- The `ULift` functor on categories of topological spaces is compatible
with the one defined on categories of types. -/
@[simps!]
def uliftFunctorCompForgetIso :
    uliftFunctor.{v, u} ⋙ forget TopCat.{max u v} ≅ forget TopCat.{u} ⋙ CategoryTheory.uliftFunctor.{v, u} :=
  Iso.refl _

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

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

Разделы

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

Аффилиация

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