dNext_cochainComplex — Mathlib

English

In a cochain complex, the differential operator dNext acts on a family of degreewise defined maps by composing with the target differential on the right, i.e., dNext j f = P.d(j, j+1) ∘ f(j+1, j).

Русский

В надцепочечном комплексе дифференциал dNext действует на семейство отображений так, что dNext j f = P.d(j, j+1) ∘ f(j+1, j).

LaTeX

$$$dNext(j)\\, f = P.d(j, j+1) \\circ f(j+1, j).$$$

Lean4

theorem dNext_cochainComplex (f : ∀ i j, P.X i ⟶ Q.X j) (j : ℕ) : dNext j f = P.d _ _ ≫ f (j + 1) j :=
  by
  dsimp [dNext]
  have : (ComplexShape.up ℕ).next j = j + 1 := CochainComplex.next ℕ j
  congr 2
    -- This is not a simp lemma; the LHS already simplifies.

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