dNext_succ_chainComplex — Mathlib

English

The dNext operator evaluated at 0 is the zero morphism.

Русский

Оператор dNext в точке 0 равен нулевому морфизму.

LaTeX

$$$ dNext(0) f = 0 $$$

Lean4

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

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