mkNatIso

Mathlib.CategoryTheory.FiberedCategory.BasedCategory

URI: https://scilib.ai/kg/mathlib#CategoryTheory.BasedNatIso.mkNatIso

Lean4

/-- The inverse of a based natural transformation whose underlying natural transformation is an
isomorphism. -/
def mkNatIso (α : F.toFunctor ≅ G.toFunctor) (isHomLift' : ∀ a : 𝒳.obj, IsHomLift 𝒴.p (𝟙 (𝒳.p.obj a)) (α.hom.app a)) :
    F ≅ G where
  hom := { toNatTrans := α.hom }
  inv :=
    { toNatTrans := α.inv
      isHomLift' := fun a ↦
        by
        have : 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (α.app a).hom := (Iso.app_hom α a) ▸ isHomLift' a
        rw [← Iso.app_inv]
        apply IsHomLift.lift_id_inv }

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

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

Разделы

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

Аффилиация

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