restrictionOpcyclesIso — Mathlib

Lean4
/-- The isomorphism `(K.restriction e).opcycles j ≅ K.opcycles j'` when `e.f j = j'`
and the predecessors `i` and `i'` of `j` and `j'` satisfy `e.f i = i'`. -/
noncomputable def restrictionOpcyclesIso : (K.restriction e).opcycles j ≅ K.opcycles j'
    where
  hom :=
    (K.restriction e).descOpcycles ((K.restrictionXIso e hj').hom ≫ K.pOpcycles j') _ hi
      (by rw [restriction_d_eq _ _ hi' hj', assoc, assoc, Iso.inv_hom_id_assoc, d_pOpcycles, comp_zero])
  inv :=
    K.descOpcycles ((K.restrictionXIso e hj').inv ≫ (K.restriction e).pOpcycles j) _ hi''
      (by rw [← cancel_epi (K.restrictionXIso e hi').hom, ← restriction_d_eq_assoc, comp_zero, d_pOpcycles])
  hom_inv_id := by simp [← cancel_epi ((K.restriction e).pOpcycles j)]
  inv_hom_id := by simp [← cancel_epi (K.pOpcycles j')]
Похожие утверждения