Lean4
/-- The right homology data which allows to show that `K.πTruncGE e`
induces an isomorphism in homology in degrees `j'` such that `e.f j = j'` for some `j`. -/
@[simps]
noncomputable def rightHomologyMapData {i j k : ι} {j' : ι'} (hj' : e.f j = j') (hi : c.prev j = i) (hk : c.next j = k)
(hj : e.BoundaryGE j) :
ShortComplex.RightHomologyMapData ((shortComplexFunctor C c' j').map (K.πTruncGE e))
(ShortComplex.RightHomologyData.canonical (K.sc j'))
(extend.rightHomologyData (K.truncGE' e) e hj' hi rfl hk rfl (truncGE'.homologyData K e i j k hk hj' hj).right)
where
φQ := (K.truncGE'XIsoOpcycles e hj' hj).inv
φH := 𝟙 _
commp := by
change K.pOpcycles j' ≫ _ = _
simp [truncGE'.homologyData, πTruncGE, e.liftExtend_f _ _ hj',
K.restrictionToTruncGE'_f_eq_iso_hom_pOpcycles_iso_inv e hj' hj]
commg' := by
have hk' : e.f k = c'.next j' := by rw [← hj', e.next_f hk]
dsimp
rw [extend.rightHomologyData_g' _ _ _ _ _ _ _ _ hk', πTruncGE, e.liftExtend_f _ _ hk',
truncGE'.homologyData_right_g']
by_cases hjk : c.Rel j k
· simp [K.truncGE'_d_eq_fromOpcycles e hjk hj' hk' hj,
K.restrictionToTruncGE'_f_eq_iso_hom_iso_inv e hk' (e.not_boundaryGE_next hjk)]
rfl
· obtain rfl : k = j := by rw [← c.next_eq_self j (by simpa only [hk] using hjk), hk]
rw [shape _ _ _ hjk, zero_comp, comp_zero, K.restrictionToTruncGE'_f_eq_iso_hom_pOpcycles_iso_inv e hk' hj]
simp only [restriction_X, restrictionXIso, eqToIso.inv, eqToIso.hom, assoc, eqToHom_trans_assoc, eqToHom_refl,
id_comp]
change 0 = K.fromOpcycles _ _ ≫ _
rw [← cancel_epi (K.pOpcycles _), comp_zero, p_fromOpcycles_assoc, d_pOpcycles_assoc, zero_comp]
