d₁_eq — Mathlib

English

The formula for the first differential expresses d1 in terms of ε1 and the map d and ιTotal.

Русский

Формула для первого дифференциала выражает d1 через ε1 и отображение d и ιTotal.

LaTeX

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

Lean4

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

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