chainsIso₁ — Mathlib

English

The differential applied to a delta at a single group element g and a A-element a yields ρ_A(g^{-1}) a − a.

Русский

Действие дифференциала на элементе-дельте, соответствующем g и a ∈ A, даёт ρ_A(g^{-1})a − a.

LaTeX

$$$d_{10} A (\text{single } g a) = A.\rho(g^{-1}) a - a$$$

Lean4

/-- The 1st object in the complex of inhomogeneous chains of `A : Rep k G` is isomorphic
to `G →₀ A` as a `k`-module. -/
def chainsIso₁ : (inhomogeneousChains A).X 1 ≅ ModuleCat.of k (G →₀ A) :=
  (Finsupp.domLCongr (Equiv.funUnique (Fin 1) G)).toModuleIso

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