English
The second differential d32 is a linear map from G × G × G to G × G, sending a triple to a signed sum of four specified basis elements, encoding the boundary of 2-simplices in the inhomogeneous chain complex.
Русский
Второй дифференциал d32 — линейное отображение из тройки G × G × G в пару G × G, отправляющее тройку в линейную комбинацию из четырех заданных базисных элементов, кодирующее границу 2-семплиций в неоднородном цепном комплексе.
LaTeX
$$$d_{32}A(\mathrm{single}(g1,g2,g3) a) = \mathrm{single}(g2,g3)(A.ρ(g1^{-1})a) - \mathrm{single}(g1g2,g3)a + \mathrm{single}(g1,g2g3)a - \mathrm{single}(g1,g2)a$$$
Lean4
/-- The 2nd differential in the complex of inhomogeneous chains of `A : Rep k G`, as a
`k`-linear map `(G³ →₀ A) → (G² →₀ A)`. It is defined by
`a·(g₁, g₂, g₃) ↦ ρ_A(g₁⁻¹)(a)·(g₂, g₃) - a·(g₁g₂, g₃) + a·(g₁, g₂g₃) - a·(g₁, g₂)`. -/
def d₃₂ : ModuleCat.of k (G × G × G →₀ A) ⟶ ModuleCat.of k (G × G →₀ A) :=
ModuleCat.ofHom <|
lsum k fun g =>
lsingle (g.2.1, g.2.2) ∘ₗ A.ρ g.1⁻¹ - lsingle (g.1 * g.2.1, g.2.2) + lsingle (g.1, g.2.1 * g.2.2) -
lsingle (g.1, g.2.1)
