prevD_succ_cochainComplex — Mathlib

English

For a family of maps f, the operator prevD at i+1 applied to f equals f(i+1) followed by the differential on Q, i.e., prevD(i+1) f = f(i+1) ∘ Q.d(i,i+1).

Русский

Для семейства отображений f операция prevD на i+1 применяемая к f равна f(i+1) затем дифференциалу Q: prevD(i+1) f = f(i+1) ∘ Q.d(i,i+1).

LaTeX

$$prevD(i+1) f = f(i+1) ≫ Q.d(i,i+1).$$

Lean4

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

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