chainsIso₀ — Mathlib

English

The 0th differential in the inhomogeneous chain complex is the sum of all G-actions minus the identity, i.e., d1₀ maps a finite supported function f: G → A to ∑_g (ρ_A(g^{-1}) f(g) - f(g)).

Русский

Нулевой дифференциал в комплексe бесконечно однородных цепей есть сумма действия G по всем элементам минус единичный акт, то есть d1₀(f) = ∑_g (ρ_A(g^{-1}) f(g) - f(g)).

LaTeX

$$$d_{10} : (G \to_0 A) \to A = \mathrm{ModuleCat}.ofHom \big|\,\sum_{g \in G} (\rho_A(g^{-1}) - \mathrm{id}) \big|$$$

Lean4

/-- The 0th object in the complex of inhomogeneous chains of `A : Rep k G` is isomorphic
to `A` as a `k`-module. -/
def chainsIso₀ : (inhomogeneousChains A).X 0 ≅ A.V :=
  (LinearEquiv.finsuppUnique _ _ _).toModuleIso

Похожие утверждения