δ_comp_zero_cocycle — Mathlib

English

The operation δ(n,m) distributes over pre-composition with a 0-cocycle: δ(n,m)(z1 ∘ z2) = (δ(n,m) z1) ∘ z2, when z2 is a 0-cocycle and z1 is a cochain of degree n.

Русский

Операция δ(n,m) распределяется по предпроизведению с 0-коциклом: δ(n,m)(z1 ∘ z2) = (δ(n,m) z1) ∘ z2, когда z2 — 0-коцикл и z1 имеет степень n.

LaTeX

$$$\\delta(n,m)(z_1 \\circ z_2) = (\\delta(n,m) z_1) \\circ z_2,$ where $z_1$ is a cochain of degree $n$ and $z_2$ is a 0-cocycle.$$

Lean4

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

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