d_snd_v' — Mathlib

English

Another rephrasing of ext_cochain_to_iff for k-graded cochains; equality reduces to equality of their fst- and snd-projections.

Русский

Другая переработка ext_cochain_to_iff для k-градуированных коцепей; равенство сводится к равенству fst- и snd-проекций.

LaTeX

$$$\forall {K}, {γ_1 γ_2}: Cochain K (mappingCone φ) i:\ γ_1=γ_2 \iff (γ_1\circ fst φ)=(γ_2\circ fst φ)\land (γ_1\circ snd φ)=(γ_2\circ snd φ).$$$

Lean4

@[reassoc (attr := simp)]
theorem d_snd_v' (n : ℤ) :
    (mappingCone φ).d (n - 1) n ≫ (snd φ).v n n (add_zero n) =
      (fst φ : Cochain (mappingCone φ) F 1).v (n - 1) n (by cutsat) ≫ φ.f n +
        (snd φ).v (n - 1) (n - 1) (add_zero _) ≫ G.d (n - 1) n :=
  by apply d_snd_v

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