Examples

We discuss some examples of Haar characters.

LemmaMeasureTheory.ringHaarChar_real#

If \(R=\mathbb{R}\) then \(\delta_R(u)=|u|\).

Proof

Take \(\mu\) to be Lebesgue measure and \(X=[0,1]\). We have \(\delta(u)=\mu(uX)\). If \(u>0\) then \(u[0,1]=[0,u]\) which has measure \(u=|u|\), and if \(u<0\) then \(u*[0,1]=[u,0]\) which has measure \(-u=|u|\).

Lean

Formalized as MeasureTheory.ringHaarChar_real.

Sources
LeanMeasureTheory.ringHaarChar_real
Uses 1 · Used by 1
Proof usesMeasureTheory.ringHaarChar_mul_volume
Used byMeasureTheory.ringHaarChar_adeles_rat

LemmaMeasureTheory.ringHaarChar_complex#

If \(R=\mathbb{C}\) then \(\delta_R(u)=|u|^2\).

Proof

Multiplication by a positive real \(r\) sends a unit square to a square of area \(r^2=|r|^2\). Multiplication by \(e^{i\theta}\) is a rotation and thus does not change area. The general case follows.

Lean

Formalized as MeasureTheory.ringHaarChar_complex.

Sources
LeanMeasureTheory.ringHaarChar_complex
Uses 1
Proof usesMeasureTheory.ringHaarChar_mul_volume

LemmaMeasureTheory.ringHaarChar_padic#

If \(R=\mathbb{Q}_p\) then \(\delta_R(u)=|u|_p\), the usual \(p\)-adic norm.

Proof

Normalise Haar measure so that \(\mu(\mathbb{Z}_p)=1\). If \(u\) is a \(p\)-adic unit then \(u\mathbb{Z}_p=\mathbb{Z}_p\) so multiplication by \(u\) didn't change Haar measure. If however \(u=p\) then \(u\mathbb{Z}_p\) has index \(p\) in \(\mathbb{Z}_p\) and, because \(\mu(i+p\mathbb{Z}_p)=\mu(p\mathbb{Z}_p)\) we have that \(\mu(\mathbb{Z}_p)=p\mu(p\mathbb{Z}_p)\) and thus \(\delta(p)=p^{-1}\). These elements generate \(\mathbb{Q}_p^\times\) and two characters which agree on generators of a group must agree on the group.

Lean

Formalized as MeasureTheory.ringHaarChar_padic.

Sources
LeanMeasureTheory.ringHaarChar_padic
Uses 1 · Used by 1
Proof usesMeasureTheory.ringHaarChar_mul_volume
Used byMeasureTheory.ringHaarChar_adeles_rat

Remark. If \(R\) is a finite extension of \(\mathbb{Q}_p\) then \(\delta_R(u)\) is the norm on \(R\) normalised in the following way: \(\delta_R(\varpi)=q^{-1}\), where \(\varpi\) is a uniformiser and \(q\) is the size of the (finite) residue field. In fact the same is true for any nonarchimedean local field. The proof is the same as for \(\mathbb{Q}_p\). Right now this is difficult to state in Lean because there is still some discussion about the definition of a nonarchimedean local field.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.