inl_v_snd_v — Mathlib

English

The shift operation on cocycles moves both sides of the mapping cone construction by a fixed integer, preserving the cocycle condition in the shifted setup.

Русский

Сдвиг кокцикла перемещает обе стороны конструирования mapping cone на заданное целое число, сохраняя кокцикл-условие в смещённой постановке.

LaTeX

$$$\mathrm{shift}: \text{Cocycle}(K,L,n) \to \text{Cocycle}(K⟦a⟧,L⟦a⟧,n).$$$

Lean4

@[reassoc (attr := simp)]
theorem inl_v_snd_v (p q : ℤ) (hpq : p + (-1) = q) : (inl φ).v p q hpq ≫ (snd φ).v q q (add_zero q) = 0 := by
  simp [inl, snd]

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