restrictionCyclesIso — Mathlib

Lean4
/-- The isomorphism `(K.restriction e).cycles j ≅ K.cycles j'` when `e.f j = j'`
and the successors `k` and `k'` of `j` and `j'` satisfy `e.f k = k'`. -/
noncomputable def restrictionCyclesIso : (K.restriction e).cycles j ≅ K.cycles j'
    where
  hom :=
    K.liftCycles ((K.restriction e).iCycles j ≫ (K.restrictionXIso e hj').hom) _ hk''
      (by
        rw [assoc, ← cancel_mono (K.restrictionXIso e hk').inv, assoc, assoc, ← restriction_d_eq, iCycles_d, zero_comp])
  inv :=
    (K.restriction e).liftCycles (K.iCycles j' ≫ (K.restrictionXIso e hj').inv) _ hk
      (by rw [assoc, restriction_d_eq _ _ hj' hk', Iso.inv_hom_id_assoc, iCycles_d_assoc, zero_comp])
  hom_inv_id := by simp [← cancel_mono ((K.restriction e).iCycles j)]
  inv_hom_id := by simp [← cancel_mono (K.iCycles j')]
Похожие утверждения