English
Let e: c → c' be an embedding of complex shapes and let φ: K.restriction e ⟶ L with hφ: e.HasLift φ. For any i and i′ with e.f i = i′, the f-component at i′ of the lifted extension e.liftExtend φ hφ is an isomorphism if and only if φ.f i is an isomorphism.
Русский
Пусть e: c → c' — вложение между формами комплексов, φ: K.restriction e ⟶ L, и существует лезвие hφ: e.HasLift φ. Для любых i, i′ с e.f i = i′ сопоставление f в точке i′ у расширенного отображения e.liftExtend φ hφ является изоморфизмом тогда и только тогда, когда φ.f i является изоморфизмом.
LaTeX
$$$$ \forall i\, \forall i'\, (hi : e.f\, i = i'):\quad IsIso\big((e.liftExtend φ hφ).f i'\big) \iff IsIso(φ.f i) $$$$
Lean4
theorem isIso_liftExtend_f_iff (hi : e.f i = i') : IsIso ((e.liftExtend φ hφ).f i') ↔ IsIso (φ.f i) :=
(MorphismProperty.isomorphisms C).arrow_mk_iso_iff (e.liftExtendfArrowIso φ hφ hi)
