δ_shape — Mathlib

English

If the degree relation does not hold (n + 1 ≠ m), the differential δ(n,m,z) vanishes: δ(n,m,z) = 0.

Русский

Если отношение степеней не выполняется (n+1 ≠ m), дифференциал обнуляется: δ(n,m,z) = 0.

LaTeX

$$$\\\\text{If } n+1 \\\\neq m, \\\\ δ(n,m,z) = 0.$$$

Lean4

theorem δ_shape (hnm : ¬n + 1 = m) (z : Cochain F G n) : δ n m z = 0 :=
  by
  ext p q hpq
  dsimp only [δ]
  rw [Cochain.mk_v, Cochain.zero_v, F.shape, G.shape, comp_zero, zero_add, zero_comp, smul_zero]
  all_goals
    simp only [ComplexShape.up_Rel]
    exact fun _ => hnm (by cutsat)

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