d_fst_v' — Mathlib

English

Dual statement to Ext_to_cochain for cochains on mapping cone: equality is detected by precomposition with inl and inr via the mapping cone's desc/ fst structure.

Русский

Дуальная формула к Ext_to_cochain для коцепей над mapping cone: равенство обнаруживается через префиксацию inl и inr с помощью desc/fst структур конуса отображения.

LaTeX

$$$\forall γ_1, γ_2:\ Cochain (mappingCone φ) K j:\ (γ_1=γ_2) \iff (inl φ)\circ γ_1 = (inl φ)\circ γ_2 \land (Cochain.ofHom (inr φ))\circ γ_1 = (Cochain.ofHom (inr φ))\circ γ_2.$$$

Lean4

@[reassoc (attr := simp)]
theorem d_fst_v' (i j : ℤ) (hij : i + 1 = j) :
    (mappingCone φ).d (i - 1) i ≫ (fst φ).1.v i j hij = -(fst φ).1.v (i - 1) i (by cutsat) ≫ F.d i j :=
  d_fst_v φ (i - 1) i j (by cutsat) hij

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