`Definitions/Def_NumberField_AdelicHaar.lean`

definition module

Haar measure on adele rings and adelic $GL_{n}$

Let R be a Dedekind domain with fraction field K, and for v in the height-one spectrum of R write K_v = v.adicCompletion K and \mathcal{O}_v = v.adicCompletionIntegers K. The local section records: a Fact instance that each \mathcal{O}_v is open in K_v; exists_valued_algebraMap_sub_lt_one, that for every x \in \mathcal{O}_v there is a \in R with |a - x|_v < 1 (proved from density of K in K_v plus integral approximation); mem_maximalIdeal_iff_valued_lt_one, that d \in \mathfrak{m}_v iff |d|_v < 1; and consequently that R \to \mathcal{O}_v \to \mathcal{O}_v/\mathfrak{m}_v is surjective and kills v (residue_algebraMap_surjective, residue_algebraMap_eq_zero_of_mem). Under the extra hypotheses that R is free and finite as a \mathbb{Z}-module, the residue field of \mathcal{O}_v is therefore finite, whence K_v is a proper space and \mathcal{O}_v is compact (instances).

The adelic section registers Hausdorffness of FiniteAdeleRing R K, InfiniteAdeleRing K and AdeleRing R K, local compactness of the finite adeles (under the same \mathbb{Z}-finiteness hypotheses on R) and of AdeleRing R K when K is a number field. It then defines adeleBorel R K to be the Borel \sigma-algebra of \mathbb{A}_K (a reducible definition, deliberately not an instance), proves it is a BorelSpace, and defines adelicAddHaar R K as Mathlib's additive Haar measure for that \sigma-algebra, with isAddHaarMeasure_adelicAddHaar as its sole interface: it is translation invariant, finite on compacts and positive on nonempty opens. No normalisation is fixed and no volume is computed. Parallel declarations treat M_n(\mathbb{A}_K) (Hausdorff; locally compact for finite n) and, for n a Fintype with decidable equality, \mathrm{GL}_n(\mathbb{A}_K) with its unit-group topology: glBorel n R K, borelSpace_glBorel, local compactness, and a left Haar measure adelicGLHaar n R K characterised by isHaarMeasure_adelicGLHaar.

Relation to Mathlib

Built entirely on Mathlib: the adele and finite-adele rings, the restricted-product topology, Valued.integer criteria for properness and compactness, and Measure.addHaar/Measure.haar are Mathlib's. What is added here is the passage from a \mathbb{Z}-finite Dedekind domain to finiteness of the residue fields of the \mathcal{O}_v (hence properness of K_v), the resulting topological instances for \mathbb{A}_K, M_n(\mathbb{A}_K) and \mathrm{GL}_n(\mathbb{A}_K), and named Borel \sigma-algebras and Haar measures on \mathbb{A}_K and \mathrm{GL}_n(\mathbb{A}_K) under stable names; the \sigma-algebras are reducible definitions rather than registered MeasurableSpace instances.

Where it is used

These instances and measures are the substrate for every integral taken over adelic groups later in the argument: square-integrability conditions on automorphic forms, integrals against Haar measure on \mathrm{GL}_n(\mathbb{A}_K), and adelic volume arguments. All declarations are generic in the pair (R,K), so they apply both to a number field with its ring of integers and to the model AdeleRing ℤ ℚ.

References

A. Weil, Basic Number Theory, Grundlehren der mathematischen Wissenschaften 144, Springer, 1967
J. W. S. Cassels and A. Fröhlich (eds.), Algebraic Number Theory, Academic Press, 1967

References are suggested automatically and have not been individually verified.

English text generated automatically from the Lean source; the Lean statement is authoritative.

206 lines
25 declarations
used in the statements of 642 theorems and imported by 764 proofs
imports 0 definition modules

Source file: Definitions/Def_NumberField_AdelicHaar.lean

Imports

only Mathlib

Imported by

Declarations

instanceNumberField.AdelicHaar.fact_isOpen_adicCompletionIntegers
theoremNumberField.AdelicHaar.exists_valued_algebraMap_sub_lt_one
theoremNumberField.AdelicHaar.mem_maximalIdeal_iff_valued_lt_one
theoremNumberField.AdelicHaar.residue_algebraMap_surjective
theoremNumberField.AdelicHaar.residue_algebraMap_eq_zero_of_mem
instanceNumberField.AdelicHaar.finite_residueField_adicCompletionIntegers
instanceNumberField.AdelicHaar.properSpace_adicCompletion
instanceNumberField.AdelicHaar.compactSpace_adicCompletionIntegers
instanceNumberField.AdelicHaar.t2Space_finiteAdeleRing
instanceNumberField.AdelicHaar.t2Space_infiniteAdeleRing
instanceNumberField.AdelicHaar.t2Space_adeleRing
defNumberField.AdelicHaar.adeleBorel
theoremNumberField.AdelicHaar.borelSpace_adeleBorel
instanceNumberField.AdelicHaar.locallyCompactSpace_finiteAdeleRing
instanceNumberField.AdelicHaar.locallyCompactSpace_adeleRing
defNumberField.AdelicHaar.adelicAddHaar
theoremNumberField.AdelicHaar.isAddHaarMeasure_adelicAddHaar
instanceNumberField.AdelicHaar.t2Space_matrix_adeleRing
instanceNumberField.AdelicHaar.locallyCompactSpace_matrix_adeleRing
instanceNumberField.AdelicHaar.t2Space_gl_adeleRing
defNumberField.AdelicHaar.glBorel
theoremNumberField.AdelicHaar.borelSpace_glBorel
instanceNumberField.AdelicHaar.locallyCompactSpace_gl_adeleRing
defNumberField.AdelicHaar.adelicGLHaar
theoremNumberField.AdelicHaar.isHaarMeasure_adelicGLHaar

Source

import Mathlib.NumberTheory.NumberField.AdeleRing ↗
import Mathlib.NumberTheory.NumberField.Completion.FinitePlace ↗
import Mathlib.Topology.Algebra.Valued.LocallyCompact ↗

open IsDedekindDomain NumberField MeasureTheory
open scoped RestrictedProduct

noncomputable section

namespace NumberField.AdelicHaar

section Local

variable (R K : Type*) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K]
  [IsFractionRing R K] (v : HeightOneSpectrum R)

instance fact_isOpen_adicCompletionIntegers :
    Fact (∀ v : HeightOneSpectrum R,
      IsOpen (v.adicCompletionIntegers K : Set (v.adicCompletion K))) :=
  ⟨fun _ => Valued.isOpen_valuationSubring _⟩

theorem exists_valued_algebraMap_sub_lt_one (x : v.adicCompletionIntegers K) :
    ∃ a : R, Valued.v ((algebraMap R (v.adicCompletion K) a) - (x : v.adicCompletion K)) < 1 := by
  have hn : {z : v.adicCompletion K | Valued.v (z - (x : v.adicCompletion K)) < 1} ∈
      nhds (x : v.adicCompletion K) := by
    refine Valued.mem_nhds.mpr ⟨1, fun z hz => ?_⟩
    have hz' : Valued.v.restrict (z - (x : v.adicCompletion K)) < 1 := by
      rw [← Units.val_one]; exact hz
    exact (Valuation.restrict_lt_one_iff _).mp hz'
  obtain ⟨_, hz, y, rfl⟩ := mem_closure_iff_nhds.mp
    (HeightOneSpectrum.denseRange_algebraMap (K := K) (v := v) (x : v.adicCompletion K)) _ hn
  have hy1 : Valued.v (algebraMap K (v.adicCompletion K) y - (x : v.adicCompletion K)) < 1 := hz
  have hyint : v.valuation K y ≤ 1 := by
    have hx1 : Valued.v (x : v.adicCompletion K) ≤ 1 := x.2
    have h : Valued.v (algebraMap K (v.adicCompletion K) y) ≤ 1 := by
      have := Valuation.map_add (Valued.v : Valuation (v.adicCompletion K) _)
        (algebraMap K (v.adicCompletion K) y - (x : v.adicCompletion K)) (x : v.adicCompletion K)
      rw [sub_add_cancel] at this
      exact this.trans (max_le hy1.le hx1)
    rwa [show algebraMap K (v.adicCompletion K) y = (y : v.adicCompletion K) from rfl,
      HeightOneSpectrum.valuedAdicCompletion_eq_valuation'] at h
  obtain ⟨a, ha⟩ := HeightOneSpectrum.exists_valuation_sub_lt_of_integer v hyint 1
  refine ⟨a, ?_⟩
  have ha' : Valued.v ((algebraMap R (v.adicCompletion K) a) -
      algebraMap K (v.adicCompletion K) y) < 1 := by
    rw [IsScalarTower.algebraMap_apply R K (v.adicCompletion K) a, ← map_sub,
      show algebraMap K (v.adicCompletion K) (algebraMap R K a - y) =
        ((algebraMap R K a - y : K) : v.adicCompletion K) from rfl,
      HeightOneSpectrum.valuedAdicCompletion_eq_valuation']
    exact ha.trans_eq Units.val_one
  have := Valuation.map_add (Valued.v : Valuation (v.adicCompletion K) _)
    ((algebraMap R (v.adicCompletion K) a) - algebraMap K (v.adicCompletion K) y)
    (algebraMap K (v.adicCompletion K) y - (x : v.adicCompletion K))
  rw [sub_add_sub_cancel] at this
  exact lt_of_le_of_lt this (max_lt ha' hy1)

theorem mem_maximalIdeal_iff_valued_lt_one (d : v.adicCompletionIntegers K) :
    d ∈ IsLocalRing.maximalIdeal (v.adicCompletionIntegers K) ↔
      Valued.v (d : v.adicCompletion K) < 1 := by
  rw [IsLocalRing.mem_maximalIdeal, mem_nonunits_iff,
    HeightOneSpectrum.adicCompletionIntegers.isUnit_iff_valued_eq_one]
  have hd : Valued.v (d : v.adicCompletion K) ≤ 1 := d.2
  exact ⟨fun h => lt_of_le_of_ne hd h, fun h => ne_of_lt h⟩

theorem residue_algebraMap_surjective :
    Function.Surjective (fun a : R =>
      IsLocalRing.residue (v.adicCompletionIntegers K)
        (algebraMap R (v.adicCompletionIntegers K) a)) := by
  intro z
  obtain ⟨x, rfl⟩ := IsLocalRing.residue_surjective z
  obtain ⟨a, ha⟩ := exists_valued_algebraMap_sub_lt_one R K v x
  refine ⟨a, ?_⟩
  show Ideal.Quotient.mk _ _ = Ideal.Quotient.mk _ _
  rw [Ideal.Quotient.eq, mem_maximalIdeal_iff_valued_lt_one]
  simpa [HeightOneSpectrum.algebraMap_adicCompletion] using ha

theorem residue_algebraMap_eq_zero_of_mem {a : R} (ha : a ∈ v.asIdeal) :
    IsLocalRing.residue (v.adicCompletionIntegers K)
      (algebraMap R (v.adicCompletionIntegers K) a) = 0 := by
  rw [IsLocalRing.residue_eq_zero_iff, mem_maximalIdeal_iff_valued_lt_one]
  simp only [HeightOneSpectrum.algebraMap_adicCompletionIntegers_apply]
  rw [HeightOneSpectrum.valuedAdicCompletion_eq_valuation', HeightOneSpectrum.valuation_of_algebraMap]
  exact (HeightOneSpectrum.intValuation_lt_one_iff_mem v a).mpr ha

variable [Module.Free ℤ R] [Module.Finite ℤ R]

instance finite_residueField_adicCompletionIntegers :
    Finite (IsLocalRing.ResidueField (v.adicCompletionIntegers K)) := by
  haveI : Finite (R ⧸ v.asIdeal) := Ideal.finiteQuotientOfFreeOfNeBot v.asIdeal v.ne_bot
  let f : R ⧸ v.asIdeal → IsLocalRing.ResidueField (v.adicCompletionIntegers K) :=
    Ideal.Quotient.lift v.asIdeal
      ((IsLocalRing.residue (v.adicCompletionIntegers K)).comp
        (algebraMap R (v.adicCompletionIntegers K)))
      (fun a ha => residue_algebraMap_eq_zero_of_mem R K v ha)
  refine Finite.of_surjective f fun z => ?_
  obtain ⟨a, ha⟩ := residue_algebraMap_surjective R K v z
  exact ⟨Ideal.Quotient.mk _ a, ha⟩

open scoped Valued in

instance properSpace_adicCompletion : ProperSpace (v.adicCompletion K) := by
  haveI : IsDiscreteValuationRing 𝒪[v.adicCompletion K] :=
    inferInstanceAs (IsDiscreteValuationRing (v.adicCompletionIntegers K))
  haveI : Finite 𝓀[v.adicCompletion K] :=
    inferInstanceAs (Finite (IsLocalRing.ResidueField (v.adicCompletionIntegers K)))
  exact Valued.integer.properSpace_iff_completeSpace_and_isDiscreteValuationRing_integer_and_finite_residueField.mpr
    ⟨inferInstance, inferInstance, inferInstance⟩

open scoped Valued in

instance compactSpace_adicCompletionIntegers : CompactSpace (v.adicCompletionIntegers K) := by
  have h : CompactSpace 𝒪[v.adicCompletion K] :=
    Valued.integer.properSpace_iff_compactSpace_integer.mp inferInstance
  exact h

end Local

section Adele

variable (R K : Type*) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K]
  [IsFractionRing R K]

instance t2Space_finiteAdeleRing : T2Space (FiniteAdeleRing R K) :=
  inferInstanceAs (T2Space (Πʳ v : HeightOneSpectrum R, [v.adicCompletion K, v.adicCompletionIntegers K]))

instance t2Space_infiniteAdeleRing : T2Space (InfiniteAdeleRing K) :=
  inferInstanceAs (T2Space ((v : InfinitePlace K) → v.Completion))

instance t2Space_adeleRing : T2Space (AdeleRing R K) :=
  inferInstanceAs (T2Space (InfiniteAdeleRing K × FiniteAdeleRing R K))

@[reducible] def adeleBorel : MeasurableSpace (AdeleRing R K) := borel _

theorem borelSpace_adeleBorel : @BorelSpace (AdeleRing R K) _ (adeleBorel R K) :=
  @BorelSpace.mk _ _ (adeleBorel R K) rfl

variable [Module.Free ℤ R] [Module.Finite ℤ R]

instance locallyCompactSpace_finiteAdeleRing : LocallyCompactSpace (FiniteAdeleRing R K) :=
  inferInstanceAs (LocallyCompactSpace
    (Πʳ v : HeightOneSpectrum R, [v.adicCompletion K, v.adicCompletionIntegers K]))

instance locallyCompactSpace_adeleRing [NumberField K] : LocallyCompactSpace (AdeleRing R K) :=
  inferInstanceAs (LocallyCompactSpace (InfiniteAdeleRing K × FiniteAdeleRing R K))

def adelicAddHaar [NumberField K] : @Measure (AdeleRing R K) (adeleBorel R K) := by
  letI := adeleBorel R K
  haveI := borelSpace_adeleBorel R K
  exact Measure.addHaar

theorem isAddHaarMeasure_adelicAddHaar [NumberField K] :
    @Measure.IsAddHaarMeasure (AdeleRing R K) _ _ (adeleBorel R K) (adelicAddHaar R K) := by
  letI := adeleBorel R K
  haveI := borelSpace_adeleBorel R K
  exact Measure.isAddHaarMeasure_addHaarMeasure _

end Adele

section GeneralLinear

variable (n : Type*) (R K : Type*) [CommRing R] [IsDedekindDomain R] [Field K] [Algebra R K]
  [IsFractionRing R K]

instance t2Space_matrix_adeleRing : T2Space (Matrix n n (AdeleRing R K)) :=
  inferInstanceAs (T2Space (n → n → AdeleRing R K))

instance locallyCompactSpace_matrix_adeleRing [Finite n] [Module.Free ℤ R] [Module.Finite ℤ R]
    [NumberField K] : LocallyCompactSpace (Matrix n n (AdeleRing R K)) :=
  inferInstanceAs (LocallyCompactSpace (n → n → AdeleRing R K))

variable [Fintype n] [DecidableEq n]

instance t2Space_gl_adeleRing : T2Space (Matrix.GeneralLinearGroup n (AdeleRing R K)) :=
  inferInstance

@[reducible] def glBorel : MeasurableSpace (Matrix.GeneralLinearGroup n (AdeleRing R K)) :=
  borel _

theorem borelSpace_glBorel :
    @BorelSpace (Matrix.GeneralLinearGroup n (AdeleRing R K)) _ (glBorel n R K) :=
  @BorelSpace.mk _ _ (glBorel n R K) rfl

variable [Module.Free ℤ R] [Module.Finite ℤ R] [NumberField K]

instance locallyCompactSpace_gl_adeleRing :
    LocallyCompactSpace (Matrix.GeneralLinearGroup n (AdeleRing R K)) :=
  inferInstance

def adelicGLHaar : @Measure (Matrix.GeneralLinearGroup n (AdeleRing R K)) (glBorel n R K) := by
  letI := glBorel n R K
  haveI := borelSpace_glBorel n R K
  exact Measure.haar

theorem isHaarMeasure_adelicGLHaar :
    @Measure.IsHaarMeasure (Matrix.GeneralLinearGroup n (AdeleRing R K)) _ _ (glBorel n R K)
      (adelicGLHaar n R K) := by
  letI := glBorel n R K
  haveI := borelSpace_glBorel n R K
  exact Measure.isHaarMeasure_haarMeasure _

end GeneralLinear

end NumberField.AdelicHaar

end

Statements phrased using this module (642)

… and 492 more statements (search for the module name to find them).

Definitions/Def_NumberField_AdelicHaar.lean

Haar measure on adele rings and adelic GLn​