d_fst_v — Mathlib

English

A cochain γ in Cochain K (mappingCone φ) i is determined by its compositions with inl φ and inr φ; equality of such compositions yields equality of γ.

Русский

Коцепь γ в Cochain K (mappingCone φ) i определяется по своим композициям с inl φ и inr φ; равенство таких композиции эквивалентно равенству γ.

LaTeX

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

Lean4

@[reassoc]
theorem d_fst_v (i j k : ℤ) (hij : i + 1 = j) (hjk : j + 1 = k) :
    (mappingCone φ).d i j ≫ (fst φ).1.v j k hjk = -(fst φ).1.v i j hij ≫ F.d j k := by apply homotopyCofiber.d_fstX

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