English
The second differential d23 in the complex of inhomogeneous cochains is the map sending a function f: G×G → A to the function on G×G×G given by (g1,g2,g3) ↦ ρ_A(g1)(f(g2,g3)) − f(g1g2,g3) + f(g1,g2g3) − f(g1,g2).
Русский
Второй дифференциал d23 в комплексe иногомогенных коцепей — это отображение, которое отправляет f: G×G → A в функцию на G×G×G, заданную (g1,g2,g3) ↦ ρ_A(g1)(f(g2,g3)) − f(g1g2,g3) + f(g1,g2g3) − f(g1,g2).
LaTeX
$$$\\displaystyle d_{23} : (G \\times G \\to A) \\to (G \\times G \\times G \\to A),\\qquad (d_{23} f)(g_1,g_2,g_3) = \\rho_A(g_1)(f(g_2,g_3)) - f(g_1g_2,g_3) + f(g_1,g_2g_3) - f(g_1,g_2).$$$
Lean4
/-- The 2nd differential in the complex of inhomogeneous cochains of `A : Rep k G`, as a
`k`-linear map `Fun(G × G, A) → Fun(G × G × G, A)`. It sends
`(f, (g₁, g₂, g₃)) ↦ ρ_A(g₁)(f(g₂, g₃)) - f(g₁g₂, g₃) + f(g₁, g₂g₃) - f(g₁, g₂).` -/
@[simps!]
def d₂₃ : ModuleCat.of k (G × G → A) ⟶ ModuleCat.of k (G × G × G → A) :=
ModuleCat.ofHom
{ toFun f g := A.ρ g.1 (f (g.2.1, g.2.2)) - f (g.1 * g.2.1, g.2.2) + f (g.1, g.2.1 * g.2.2) - f (g.1, g.2.1)
map_add' x
y :=
funext fun g => by
dsimp
rw [map_add, add_sub_add_comm (A.ρ _ _), add_sub_assoc, add_sub_add_comm, add_add_add_comm, add_sub_assoc,
add_sub_assoc]
map_smul' r x := funext fun g => by dsimp; simp only [map_smul, smul_add, smul_sub] }
