restrictionHomologyIso — Mathlib

Lean4

/-- The isomorphism `(K.restriction e).homology j ≅ K.homology j'` when `e.f j = j'`,
the predecessors `i` and `i'` of `j` and `j'` satisfy `e.f i = i'`,
and the successors `k` and `k'` of `j` and `j'` satisfy `e.f k = k'` -/
noncomputable def restrictionHomologyIso : (K.restriction e).homology j ≅ K.homology j' :=
  have : ((K.restriction e).sc' i j k).HasHomology := by subst hi hk; assumption
  have : (K.sc' i' j' k').HasHomology := by subst hi'' hk''; assumption
  (K.restriction e).homologyIsoSc' i j k hi hk ≪≫
    ShortComplex.homologyMapIso (restriction.sc'Iso K e i j k hi' hj' hk' hi'' hk'') ≪≫
      (K.homologyIsoSc' i' j' k' hi'' hk'').symm

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