isGE_shift — Mathlib

English

If K isGE at n, then shifting K by a yields GE at n′ when a+n′ = n.

Русский

Если K GE в n, то сдвиг K на a дает GE в n′ при a+n′ = n.

LaTeX

$$$ (n) [K.IsGE(n)] (a, n')\\, (h: a+n' = n) \\Rightarrow ((K⟦a⟧).IsGE(n')) $$$

Lean4

theorem isGE_shift (n : ℤ) [K.IsGE n] (a n' : ℤ) (h : a + n' = n) : (K⟦a⟧).IsGE n' :=
  by
  rw [isGE_iff]
  intro i hi
  rw [exactAt_iff_isZero_homology]
  exact
    IsZero.of_iso (K.isZero_of_isGE n (a + i) (by cutsat)) (((homologyFunctor C _ (0 : ℤ)).shiftIso a i _ rfl).app K)

Похожие утверждения