δ_ofHom_comp — Mathlib

English

If z1 is a 0-cocycle and z2: G ⟶ K is a cochain of degree n, then δ(n,m)(z1.1.comp z2 (zero_add n)) = z1.1.comp (δ(n,m) z2)(zero_add m).

Русский

Если z1 — 0-коцикл, а z2: G ⟶ K — тк Cochain степени n, то δ(n,m)(z1.1.comp z2 (zero_add n)) = z1.1.comp (δ(n,m) z2)(zero_add m).

LaTeX

$$$\\delta(n,m)(z_1.1 \\circ z_2 \\circ (\\mathrm{zero\\_add}\\ n)) = z_1.1 \\circ (\\delta(n,m) z_2) \\circ (\\mathrm{zero\\_add}\\ m).$$$

Lean4

@[simp]
theorem δ_ofHom_comp {n : ℤ} (f : F ⟶ G) (z : Cochain G K n) (m : ℤ) :
    δ n m ((Cochain.ofHom f).comp z (zero_add n)) = (Cochain.ofHom f).comp (δ n m z) (zero_add m) := by
  rw [← Cocycle.ofHom_coe, δ_zero_cocycle_comp]

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