inl_v_descCochain_v — Mathlib

English

The differential on mappingCone composed with snd components equals φ.f plus the snd-component composed with G’s differential.

Русский

Дифференциал конуса отображения через snd-компонент равен φ.f плюс snd-компонента по дифференциалу G.

LaTeX

$$$(mappingCone φ).d_{i,j} ∘ (snd φ)_{j,i} = φ.f_j + (snd φ)_{i,i} ∘ G_{i,j}.$$$

Lean4

@[reassoc (attr := simp)]
theorem inl_v_descCochain_v (p₁ p₂ p₃ : ℤ) (h₁₂ : p₁ + (-1) = p₂) (h₂₃ : p₂ + n = p₃) :
    (inl φ).v p₁ p₂ h₁₂ ≫ (descCochain φ α β h).v p₂ p₃ h₂₃ =
      α.v p₁ p₃ (by rw [← h₂₃, ← h₁₂, ← h, add_comm m, add_assoc, neg_add_cancel_left]) :=
  by
  simpa only [Cochain.comp_v _ _ (show -1 + n = m by cutsat) p₁ p₂ p₃ (by cutsat) (by cutsat)] using
    Cochain.congr_v (inl_descCochain φ α β h) p₁ p₃ (by cutsat)

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