δ_zero_cocycle_comp — Mathlib

English

For a morphism f: F ⟶ G and a cochain z: G ⟶ K of degree n, δ(n,m) applied after composing with Cochain.ofHom f equals composing with Cochain.ofHom f after applying δ to z.

Русский

Для морфизма f: F ⟶ G и коцепна z: G ⟶ K степенью n, δ(n,m) после композиции с Cochain.ofHom f равен композиции с Cochain.ofHom f после применения δ к z.

LaTeX

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

Lean4

@[simp]
theorem δ_zero_cocycle_comp {n : ℤ} (z₁ : Cocycle F G 0) (z₂ : Cochain G K n) (m : ℤ) :
    δ n m (z₁.1.comp z₂ (zero_add n)) = z₁.1.comp (δ n m z₂) (zero_add m) :=
  by
  by_cases hnm : n + 1 = m
  · simp [δ_zero_cochain_comp _ _ _ hnm]
  · simp [δ_shape _ _ hnm]

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