δ_ofHom — Mathlib

English

For any morphism φ: F → G between cochain complexes, the differential δ at (0, p) applied to the cochain ofHom of φ is zero: δ_{0,p}(Cochain.ofHom φ) = 0.

Русский

Пусть φ: F → G — морфизм между коцепными комплексами. Тогда δ_{0,p}(Cochain.ofHom φ) = 0 для любого p.

LaTeX

$$$\delta_{0\,p}(\operatorname{Cochain.ofHom} \phi) = 0$$$

Lean4

@[simp]
theorem δ_ofHom {p : ℤ} (φ : F ⟶ G) : δ 0 p (Cochain.ofHom φ) = 0 :=
  by
  by_cases h : p = 1
  · subst h
    ext
    simp
  · rw [δ_shape]
    cutsat

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