prevD_chainComplex — Mathlib

English

For a function f assigning maps between X_i and X_j of a chain of complexes P and Q, the dNext operator at i+1 is the composition of the differential P.d_{i+1,i} with f_i,i+1.

Русский

Для отображения f между компонентами цепочного комплекса P и Q оператор dNext на i+1 равен композиции дифференциала P.d_{i+1,i} с f_{i,i+1}.

LaTeX

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

Lean4

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

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