δ_comp_ofHom — Mathlib

English

For any z1: F ⟶ G of degree n, any f: G ⟶ K, and m, one has δ(n,m)(z1 ∘ Cochain.ofHom f) = (δ(n,m) z1) ∘ Cochain.ofHom f.

Русский

Для любого z1: F ⟶ G степенью n, для любого f: G ⟶ K и для любого m верно δ(n,m)(z1 ∘ Cochain.ofHom f) = (δ(n,m) z1) ∘ Cochain.ofHom f.

LaTeX

$$$\\delta(n,m)(z_1 \\circ \\mathrm{Cochain.ofHom}(f)) = (\\delta(n,m) z_1) \\circ \\mathrm{Cochain.ofHom}(f).$$$

Lean4

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

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