δ_eq_zero — Mathlib

English

There is a construction sending a morphism φ: F ⟶ G to the 0-th cocycle in Cocycle F G 0.

Русский

Существует конструктор, отправляющий морфизм φ: F ⟶ G в 0‑кокцикл Cocycle F G 0.

LaTeX

$$Cocycle.ofHom φ ∈ Cocycle F G 0$$

Lean4

@[simp]
theorem δ_eq_zero {n : ℤ} (z : Cocycle F G n) (m : ℤ) : δ n m (z : Cochain F G n) = 0 :=
  by
  by_cases h : n + 1 = m
  · rw [← mem_iff n m h]
    exact z.2
  · exact δ_shape n m h _

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