English
For a bicomplex K with total complex K.total c12, the degree-1 differential along the c12-direction is given by the horizontal differential d and the total-structure maps, up to the ε₁ sign: d1 c12 i1 i2 i12 = ε₁ c1 c2 c12 ⟨i1,i2⟩ · ( (d i1 i1').f i2 ∘ ιTotalOrZero c12 i1' i2 i12 ).
Русский
Для двумерного комплекса K с общим (тотальным) комплексом d1 по направлению c12 задаётся как горизонтальный дифференциал d, умноженный на соответствующую инклюзию total и с учётом знака ε₁: d1 = ε₁ ⟨i1,i2⟩ (d i1 i1')^f i2 ∘ ιTotalOrZero.
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 \big( ((K.d i_1 i_1').f i_2) \;\circ\; K.\iota^{TotalOrZero}_{c_{12}} i_1' i_2 i_{12} \big)$$$
Lean4
theorem d₁_eq' {i₁ i₁' : I₁} (h : c₁.Rel i₁ i₁') (i₂ : I₂) (i₁₂ : I₁₂) :
K.d₁ c₁₂ i₁ i₂ i₁₂ = ComplexShape.ε₁ c₁ c₂ c₁₂ ⟨i₁, i₂⟩ • ((K.d i₁ i₁').f i₂ ≫ K.ιTotalOrZero c₁₂ i₁' i₂ i₁₂) :=
totalAux.d₁_eq' _ _ h _ _
