Lean4
/-- Given `φ : K ⟶ L`, `K⟦(1 : ℤ)⟧` is homotopy equivalent to
the mapping cone of `inr φ : L ⟶ mappingCone φ`. -/
noncomputable def rotateHomotopyEquiv : HomotopyEquiv (K⟦(1 : ℤ)⟧) (mappingCone (inr φ))
where
hom :=
lift (inr φ) (-(Cocycle.ofHom φ).leftShift 1 1 (zero_add 1)) (-(inl φ).leftShift 1 0 (neg_add_cancel 1))
(by
-- the following list of lemmas has been obtained by doing
-- simp? [Cochain.δ_leftShift _ 1 0 1 (neg_add_cancel 1) 0 (zero_add 1)]
simp only [Int.reduceNeg, δ_neg, Cochain.δ_leftShift _ 1 0 1 (neg_add_cancel 1) 0 (zero_add 1),
Int.negOnePow_one, δ_inl, Cochain.ofHom_comp, Cochain.leftShift_comp_zero_cochain, Units.neg_smul, one_smul,
neg_neg, Cocycle.coe_neg, Cocycle.leftShift_coe, Cocycle.ofHom_coe, Cochain.neg_comp, add_neg_cancel])
inv := desc (inr φ) 0 (triangle φ).mor₃ (by simp only [δ_zero, inr_triangleδ, Cochain.ofHom_zero])
homotopyHomInvId :=
Homotopy.ofEq
(by
ext n
simp only [shiftFunctor_obj_X', Int.reduceNeg, HomologicalComplex.comp_f, lift_desc_f _ _ _ _ _ _ _ _ _ rfl,
Cocycle.coe_neg, Cocycle.leftShift_coe, Cocycle.ofHom_coe, Cochain.neg_v, Cochain.zero_v, comp_zero,
(inl φ).leftShift_v 1 0 _ _ n _ (n + 1) (by simp only [add_neg_cancel_right]), shiftFunctor_obj_X, mul_zero,
sub_self, Int.zero_ediv, add_zero, Int.negOnePow_zero, shiftFunctorObjXIso, HomologicalComplex.XIsoOfEq_rfl,
Iso.refl_hom, id_comp, one_smul, Preadditive.neg_comp, inl_v_triangle_mor₃_f, Iso.refl_inv, neg_neg, zero_add,
HomologicalComplex.id_f])
homotopyInvHomId :=
(Cochain.equivHomotopy _ _).symm
⟨-(snd (inr φ)).comp ((snd φ).comp (inl (inr φ)) (zero_add (-1))) (zero_add (-1)),
by
ext n
simp only [Int.reduceNeg, Cochain.ofHom_comp, ofHom_desc, ofHom_lift, Cocycle.coe_neg, Cocycle.leftShift_coe,
Cocycle.ofHom_coe, Cochain.comp_zero_cochain_v, shiftFunctor_obj_X', δ_neg,
δ_zero_cochain_comp _ _ _ (neg_add_cancel 1), δ_inl, Int.negOnePow_neg, Int.negOnePow_one, δ_snd,
Cochain.neg_comp, Cochain.comp_assoc_of_second_is_zero_cochain, smul_neg, Units.neg_smul, one_smul, neg_neg,
Cochain.comp_add, inr_snd_assoc, neg_add_rev, Cochain.add_v, Cochain.neg_v,
Cochain.comp_v _ _ (add_neg_cancel 1) n (n + 1) n rfl (by omega), Cochain.zero_cochain_comp_v,
Cochain.ofHom_v, HomologicalComplex.id_f, ext_to_iff _ _ (n + 1) rfl, assoc, liftCochain_v_fst_v,
(Cochain.ofHom φ).leftShift_v 1 1 (zero_add 1) n (n + 1) rfl (n + 1) (by omega), shiftFunctor_obj_X, mul_one,
sub_self, mul_zero, Int.zero_ediv, add_zero, shiftFunctorObjXIso, HomologicalComplex.XIsoOfEq_rfl,
Iso.refl_hom, id_comp, Preadditive.add_comp, Preadditive.neg_comp, inl_v_fst_v, comp_id, inr_f_fst_v,
comp_zero, neg_zero, neg_add_cancel_comm, ext_from_iff _ (n + 1) _ rfl, inl_v_descCochain_v_assoc,
Cochain.zero_v, zero_comp, Preadditive.comp_neg, inl_v_snd_v_assoc, inr_f_descCochain_v_assoc,
inr_f_snd_v_assoc, inl_v_triangle_mor₃_f_assoc, triangle_obj₁, Iso.refl_inv, inl_v_fst_v_assoc,
inr_f_triangle_mor₃_f_assoc, inr_f_fst_v_assoc, and_self, liftCochain_v_snd_v,
(inl φ).leftShift_v 1 0 (neg_add_cancel 1) n n (add_zero n) (n + 1) (by omega), Int.negOnePow_zero,
inl_v_snd_v, inr_f_snd_v, zero_add, inl_v_descCochain_v, inr_f_descCochain_v, inl_v_triangle_mor₃_f,
inr_f_triangle_mor₃_f, neg_add_cancel]⟩
