English
If h is a homotopy between φ1 and φ2, then for any n ∈ ℤ there is a homotopy between φ1⟦n⟧' and φ2⟦n⟧' given by h.hom scaled by n via n.negOnePow.
Русский
Если h — гомотопия между φ1 и φ2, то для любого n ∈ ℤ существует гомотопия между φ1⟦n⟧' и φ2⟦n⟧', полученная через умножение h.hom на n через n.negOnePow.
LaTeX
$$$$\text{Homotopy shift}:\; h:\mathrm{Homotopy}(\phi_1,\phi_2) \Rightarrow \mathrm{Homotopy}(\phi_1⟦n⟧', \phi_2⟦n⟧').$$$$
Lean4
/-- If `h : Homotopy φ₁ φ₂` and `n : ℤ`, this is the induced homotopy
between `φ₁⟦n⟧'` and `φ₂⟦n⟧'`. -/
def shift {K L : CochainComplex C ℤ} {φ₁ φ₂ : K ⟶ L} (h : Homotopy φ₁ φ₂) (n : ℤ) : Homotopy (φ₁⟦n⟧') (φ₂⟦n⟧')
where
hom _ _ := n.negOnePow • h.hom _ _
zero i j
hij := by
dsimp
rw [h.zero, smul_zero]
intro hij'
dsimp at hij hij'
omega
comm := fun i =>
by
rw [dNext_eq _ (show (ComplexShape.up ℤ).Rel i (i + 1) by simp),
prevD_eq _ (show (ComplexShape.up ℤ).Rel (i - 1) i by simp)]
dsimp
simpa only [Linear.units_smul_comp, Linear.comp_units_smul, smul_smul, Int.units_mul_self, one_smul,
dNext_eq _ (show (ComplexShape.up ℤ).Rel (i + n) (i + 1 + n) by dsimp; omega),
prevD_eq _ (show (ComplexShape.up ℤ).Rel (i - 1 + n) (i + n) by dsimp; omega)] using h.comm (i + n)
