English
The horizontal and vertical signs anticommute: for suitably related indices i1,i1', i2,i2', the product ε2(i1,i2)ε1(i1,i2) equals minus ε1(i1',i2)ε2(i1,i2).
Русский
Знаки горизонтального и вертикального дифференциалов антикоммютируют: для связанных индексов выполняется тождество ε₂(i1,i2)ε₁(i1,i2) = − ε₁(i1',i2)ε₂(i1,i2).
LaTeX
$$$\\forall {i_1,i_1'\\in I_1} {i_2,i_2'\\in I_2}\\; c_1.Rel(i_1,i_1') \\land c_2.Rel(i_2,i_2') \\Rightarrow \\\\varepsilon_2(c_1,c_2,c_{12})(\\langle i_1,i_2\\rangle)\\cdot \\varepsilon_1(c_1,c_2,c_{12})(\\langle i_1,i_2'\\rangle) = -\\varepsilon_1(c_1,c_2,c_{12})(\\langle i_1',i_2\\rangle)\\cdot \\varepsilon_2(c_1,c_2,c_{12})(\\langle i_1,i_2\\rangle)$$$$
Lean4
theorem ε₂_ε₁ {i₁ i₁' : I₁} {i₂ i₂' : I₂} (h₁ : c₁.Rel i₁ i₁') (h₂ : c₂.Rel i₂ i₂') :
ε₂ c₁ c₂ c₁₂ ⟨i₁, i₂⟩ * ε₁ c₁ c₂ c₁₂ ⟨i₁, i₂'⟩ = -ε₁ c₁ c₂ c₁₂ ⟨i₁, i₂⟩ * ε₂ c₁ c₂ c₁₂ ⟨i₁', i₂⟩ :=
TotalComplexShape.ε₂_ε₁ h₁ h₂
