3.3. The Iwasawa algebra
We now recast measures algebraically. The prototype is the classical fact for a finite abelian group.
If G is a finite abelian group, the map [g] \mapsto \delta_g induces an
isomorphism \Z[G] \cong \sM(G, \Z) between the group algebra and the space of
measures on G (discrete topology). It uses Definition 3.2.3.
A measure \mu on the finite set G is determined by its values
c_g = \mu(\one_{\set g}), and \mu = \sum_g c_g \delta_g; matching \delta_g
with the basis element [g] of \Z[G] gives a bijection that is visibly
\Z-linear and multiplicative for the convolution/group multiplication.
- No associated Lean code or declarations.
For G profinite abelian there is a natural isomorphism
\sM(G, \OL) \cong \varprojlim_H \OL[G/H],
the limit running over open subgroups H \leq G. This builds on
Proposition 3.2.4 and Proposition 3.3.1.
By Proposition 3.2.4, \sM(G,\OL) \cong \sMlc(G,\OL). Every locally
constant function factors through some finite quotient G/H, so
\cClc(G,\OL) \cong \varinjlim_H \cC(G/H, \OL). Dualising turns the direct limit
into an inverse limit,
\sM(G, \OL) \cong \varprojlim_H \sM(G/H, \OL), and each finite-level term is
\sM(G/H, \OL) \cong \OL[G/H] by Proposition 3.3.1 (over
\OL). Explicitly, a measure \mu maps to
\big(\sum_{[a] \in G/H} \mu(aH)\,[a]\big)_H, additivity guaranteeing
compatibility under the projection maps; conversely the coefficients of the
finite-level elements recover the set-function \mu(aH).
The Iwasawa algebra of G is the profinite completion of the group algebra,
\Lam(G) := \varprojlim_H \OL[G/H],
the inverse limit over open subgroups H \leq G (the coefficient field L is
suppressed from the notation). By Proposition 3.3.2 it is
canonically isomorphic to \sM(G, \OL).
Transporting the \OL-algebra structure of \Lam(G) to \sM(G, \OL) via
Definition 3.3.3, the product is convolution of measures: for
\mu, \lambda \in \sM(G, \OL),
\int_G \phi \cdot (\mu * \lambda) = \int_G \left(\int_G \phi(x+y) \cdot \lambda(y)\right) \cdot \mu(x).
This makes Proposition 3.3.2 an isomorphism of \OL-algebras,
and sends the Dirac measures \delta_a (for a \in \Zp) to the group-like
elements [a] = ([a + p^n\Zp])_n \in \Lam(\Zp).
Lean code for Definition3.3.4●1 theorem
Associated Lean declarations
-
PadicMeasure.mul_apply[complete]
-
PadicMeasure.mul_apply[complete]
-
theoremdefined in PadicLFunctions/Measure/Convolution.leancomplete
theorem PadicMeasure.mul_apply (p : ℕ) [hp : Fact (Nat.Prime p)] (μ ν : PadicMeasure p ℤ_[p]) (f : C(ℤ_[p], ℤ_[p])) : (μ * ν) f = μ (PadicMeasure.convInner p ν f)
theorem PadicMeasure.mul_apply (p : ℕ) [hp : Fact (Nat.Prime p)] (μ ν : PadicMeasure p ℤ_[p]) (f : C(ℤ_[p], ℤ_[p])) : (μ * ν) f = μ (PadicMeasure.convInner p ν f)
**The convolution formula** (RJW Rem. 3.11, TeX line 909): `∫ φ d(μ*ν) = ∫ (∫ φ(x+y) dν(y)) dμ(x)`. Proved by checking Mahler coefficients (Chu–Vandermonde: `binom(x+y, n) = ∑_{i+j=n} binom(x,i)·binom(y,j)`, mathlib's `Ring.add_choose_eq`); injectivity of the Mahler transform extends the identity from the Mahler basis to all continuous functions.