homotopicMapsNatIso

Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

URI: https://scilib.ai/kg/mathlib#FundamentalGroupoidFunctor.homotopicMapsNatIso

Lean4

/-- Given a homotopy H : f ∼ g, we have an associated natural isomorphism between the induced
functors `f` and `g` -/
-- Porting note: couldn't use category arrow `\hom` in statement, needed to expand

def homotopicMapsNatIso : @Quiver.Hom _ Functor.category.toQuiver (πₘ (TopCat.ofHom f)) (πₘ (TopCat.ofHom g))
    where
  app x := ⟦H.evalAt x.as⟧
  naturality x y p := by erw [(H.eq_diag_path p).1, (H.eq_diag_path p).2]

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

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

Разделы

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

Аффилиация

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