Lean4
/-- Given an embedding `e : c.Embedding c'` of complexes shapes, this is the
morphism `K.extend e ⟶ L.extend e` induced by a morphism `K ⟶ L` in
`HomologicalComplex C c`. -/
noncomputable def extendMap : K.extend e ⟶ L.extend e
where
f _ := extend.mapX φ _
comm' i' j'
_ := by
by_cases hi : ∃ i, e.f i = i'
· obtain ⟨i, hi⟩ := hi
by_cases hj : ∃ j, e.f j = j'
· obtain ⟨j, hj⟩ := hj
rw [K.extend_d_eq e hi hj, L.extend_d_eq e hi hj, extend.mapX_some φ (e.r_eq_some hi),
extend.mapX_some φ (e.r_eq_some hj)]
simp only [extendXIso, assoc, Iso.inv_hom_id_assoc, Hom.comm_assoc]
· have hj' := e.r_eq_none j' (fun j'' hj'' => hj ⟨j'', hj''⟩)
dsimp [extend]
rw [extend.d_none_eq_zero' _ _ _ hj', extend.d_none_eq_zero' _ _ _ hj', comp_zero, zero_comp]
· have hi' := e.r_eq_none i' (fun i'' hi'' => hi ⟨i'', hi''⟩)
dsimp [extend]
rw [extend.d_none_eq_zero _ _ _ hi', extend.d_none_eq_zero _ _ _ hi', comp_zero, zero_comp]
