shift_v' — Mathlib

English

There is a closed form for the v-component of the shifted cochain γ.shift a: (γ.shift a).v p q hpq = γ.v(p+a,q+a) with hpq adjusted accordingly; this is a convenient simplification used in proofs.

Русский

Существует явное выражение для компоненты v сдвинутого коцепного γ.shift a: (γ.shift a).v p q hpq = γ.v(p+a,q+a) с соответствующей корректировкой hpq.

LaTeX

$$$(\\gamma.shift a).v_{p q}^{hpq} = γ.v_{p+a, q+a}^{hpq'}$$$

Lean4

theorem shift_v' (a : ℤ) (p q : ℤ) (hpq : p + n = q) : (γ.shift a).v p q hpq = γ.v (p + a) (q + a) (by cutsat) := by
  simp only [shift_v γ a p q hpq _ _ rfl rfl, shiftFunctor_obj_X, shiftFunctorObjXIso, HomologicalComplex.XIsoOfEq_rfl,
    Iso.refl_hom, Iso.refl_inv, comp_id, id_comp]

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