English
The first differential d21 is a k-linear map from the free k-module on pairs (g1,g2) with coefficients in A to the free k-module on G with coefficients in A, given by the explicit alternating sum
Русский
Первый дифференциал d21 — это k-линейное отображение от свободного модуля на пары (g1,g2) с коэффициентами в A к свободному модулю на элементы G с коэффициентами в A, заданное явной чередующей суммой.
LaTeX
$$$d_{21}A\colon \; M_k(G\times G \to A) \to M_k(G\to A)$ with formula$$
Lean4
/-- The 1st 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₂) ↦ ρ_A(g₁⁻¹)(a)·g₂ - a·g₁g₂ + a·g₁`. -/
def d₂₁ : ModuleCat.of k (G × G →₀ A) ⟶ ModuleCat.of k (G →₀ A) :=
ModuleCat.ofHom <| lsum k fun g => lsingle g.2 ∘ₗ A.ρ g.1⁻¹ - lsingle (g.1 * g.2) + lsingle g.1
