d₁₀ — Mathlib

English

The 0th differential in the inhomogeneous chains of A is the map from (G →₀ A) to A given by d1₀ = ∑_{g∈G} (ρ_A(g^{-1}) − id).

Русский

Нулевой дифференциал в комплексе бесконечно однородных цепей A есть отображение (G →₀ A) → A, заданное d1₀ = ∑_{g∈G} (ρ_A(g^{-1}) − id).

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 differential in the complex of inhomogeneous chains of `A : Rep k G`, as a
`k`-linear map `(G →₀ A) → A`. It is defined by `single g a ↦ ρ_A(g⁻¹)(a) - a.` -/
def d₁₀ : ModuleCat.of k (G →₀ A) ⟶ A.V :=
  ModuleCat.ofHom <| lsum k fun g => A.ρ g⁻¹ - LinearMap.id

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