d_snd_v — Mathlib

English

For f: (mappingCone φ).X j → A, there exist a,b with f = (inl φ).v j i hij ≫ a + (inr φ).f j ≫ b.

Русский

Для отображения f: (mappingCone φ).X_j → A существуют a,b с f = (inl φ).v j i hij ≫ a + (inr φ).f j ≫ b.

LaTeX

$$$\exists a:\, A\to F.X_i,\ b:\, A\to G.X_j:\ f = (inl φ)_{j,i hij} \circ a + (inr φ)_{j j} \circ b.$$$

Lean4

@[reassoc]
theorem d_snd_v (i j : ℤ) (hij : i + 1 = j) :
    (mappingCone φ).d i j ≫ (snd φ).v j j (add_zero _) =
      (fst φ).1.v i j hij ≫ φ.f j + (snd φ).v i i (add_zero i) ≫ G.d i j :=
  by
  dsimp [mappingCone, snd, fst]
  simp only [Cochain.ofHoms_v]
  apply homotopyCofiber.d_sndX

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