liftExtendfArrowIso

Mathlib.Algebra.Homology.Embedding.HomEquiv

URI: https://scilib.ai/kg/mathlib#ComplexShape.Embedding.liftExtendfArrowIso

Lean4

/-- Given `φ : K.restriction e ⟶ L` such that `hφ : e.HasLift φ`, this is
the isomorphisms in the category of arrows between the maps
`(e.liftExtend φ hφ).f i'` and `φ.f i` when `e.f i = i'`. -/
noncomputable def liftExtendfArrowIso : Arrow.mk ((e.liftExtend φ hφ).f i') ≅ Arrow.mk (φ.f i) :=
  Arrow.isoMk (K.restrictionXIso e hi).symm (L.extendXIso e hi) (by simp [e.liftExtend_f φ hφ hi])

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

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

Разделы

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

Аффилиация

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