d₂_eq' — Mathlib

English

The second differential d2 is expressed via ε2 and the map d on the D2-graded component with inclusion ιTotalOrZero.

Русский

Второй дифференциал d2 выражается через ε2 и отображение d на компоненте D2 с включением ιTotalOrZero.

LaTeX

$$$K.d_2 c_{12} i_1 i_2 i_{12} = \\varepsilon_2 c_1 c_2 c_{12} \\langle i_1,i_2 \\rangle \\cdot (d i_2 i_2' \\circ ιTotalOrZero c_{12} i_1 i_2' i_{12} h)$$$

Lean4

theorem d₂_eq' (i₁ : I₁) {i₂ i₂' : I₂} (h : c₂.Rel i₂ i₂') (i₁₂ : I₁₂) :
    K.d₂ c₁₂ i₁ i₂ i₁₂ = ComplexShape.ε₂ c₁ c₂ c₁₂ ⟨i₁, i₂⟩ • ((K.X i₁).d i₂ i₂' ≫ K.ιTotalOrZero c₁₂ i₁ i₂' i₁₂) :=
  totalAux.d₂_eq' _ _ _ h _

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