AdeleRing.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 1204 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Pinned FLT blueprint introduction

11 declarations, 0 contain sorry, 0 declared as axioms

Global units are in the determinant of the adelic Haar character

If K is a number field and B is a finite-dimensional K-algebra then B ⊗ 𝔸_K is a locally compact topological ring, so it admits a Haar character (B ⊗ 𝔸_K)ˣ → ℝ>0. In this file we show that the global units Bˣ are in the kernel of this character.

Imports (19)

Imported by 2 files

instance (instance at line 59) line 59 source
instance (instance at line 65) line 65 source
lemma MeasureTheory.ringHaarChar_adeles_rat line 70 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Units, NumberField.AdeleRing, NumberField.RingOfIntegers, Rat, Eq, NNReal, ContinuousMonoidHom, MeasureTheory.ringHaarChar, HMul.hMul, NumberField.InfiniteAdeleRing, Prod.fst, IsDedekindDomain.FiniteAdeleRing, MulEquiv, Prod, MulEquiv.prodUnits, finprod, IsDedekindDomain.HeightOneSpectrum, IsDedekindDomain.HeightOneSpectrum.adicCompletion, RestrictedProduct, Subgroup and 7 more
Proof uses: id, Eq.mpr, congrArg, MeasureTheory.ringHaarChar_prod', HMul, Eq.rec, Eq.refl, Fact, IsOpen, Fact.mk, NumberField.isOpenAdicCompletionIntegers, CompactSpace, Subtype, Membership.mem, MeasureTheory.addEquivAddHaarChar, AddSubgroup, Subring.toAddSubgroup, ValuationSubring.toSubring, WithZero, Multiplicative and 27 more
209 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.ringHaarChar_adeles_units_rat_eq_one line 88 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Units, Rat, Eq, NNReal, ContinuousMonoidHom, NumberField.AdeleRing, NumberField.RingOfIntegers, MeasureTheory.ringHaarChar, MonoidHom, Units.map, RingHom, Algebra.algebraMap, OfNat.ofNat
Proof uses: Eq.mpr, HMul.hMul, NumberField.InfiniteAdeleRing, Prod.fst, IsDedekindDomain.FiniteAdeleRing, MulEquiv, Prod, MulEquiv.prodUnits, finprod, IsDedekindDomain.HeightOneSpectrum, IsDedekindDomain.HeightOneSpectrum.adicCompletion, RestrictedProduct, Subgroup, Submonoid.units, Submonoid.ofClass, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Filter.cofinite, MulEquiv.restrictedProductUnits, Prod.snd and 130 more
305 instances, coercions and auxiliary constants left out.

Tactic trace: 25 steps
Open to load the checked before-and-after goal states.
def TensorProduct.RightActions.ContinuousLinearEquiv.baseChange The continuous A-linear map (A a topological ring, tensor products have the module topology) A ⊗[R] M ≃ A ⊗[R] N associated to an abstract R-linear isomorphism M ≃ N line 130 source
Source documentation
The continuous A-linear map (A a topological ring, tensor products have the module topology) A ⊗[R] M ≃ A ⊗[R] N associated to an abstract R-linear isomorphism M ≃ N.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, TopologicalSpace, AddCommGroup, Module, Module.Finite, LinearEquiv, RingHom.id, ContinuousLinearEquiv, TensorProduct, TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT, TensorProduct.RightActions.instModule_fLT
Proof uses: TensorProduct.RightActions.LinearEquiv.baseChange, ContinuousLinearEquiv.mk
18 instances, coercions and auxiliary constants left out.
```
noncomputable def TensorProduct.RightActions.ContinuousLinearEquiv.baseChange (R : Type*)
    [CommRing R]
    (A : Type*) [CommRing A] [Algebra R A] [TopologicalSpace A]
    (M N : Type*) [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
    [Module.Finite R M] [Module.Finite R N]
    (φ : M ≃ₗ[R] N) : (M ⊗[R] A) ≃L[A] (N ⊗[R] A) where
…
```
lemma ContinuousLinearEquiv.baseChange_apply line 141 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Algebra, TopologicalSpace, AddCommGroup, Module, Module.Finite, LinearEquiv, RingHom.id, Eq, TensorProduct, ContinuousLinearEquiv, TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT, TensorProduct.RightActions.instModule_fLT, TensorProduct.RightActions.ContinuousLinearEquiv.baseChange, TensorProduct.tmul
Proof uses: rfl
23 instances, coercions and auxiliary constants left out.
lemma LinearMap.toMatrix_basis mathlib? line 150 source
Source comment
mathlib?

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Fintype, Finite, DecidableEq, CommSemiring, Algebra, AddCommMonoid, Module, Module.Basis, LinearMap, RingHom.id, Eq, Matrix, LinearEquiv, TensorProduct, LinearMap.toMatrix, Algebra.TensorProduct.basis, LinearMap.baseChange, Matrix.map, RingHom, Algebra.algebraMap
Proof uses: Matrix.ext, of_eq_true, Eq.trans, True, congrFun', congrArg, LinearMap.toMatrix_baseChange, eq_self
46 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
lemma LinearMap.toMatrix_basis {R : Type*} (A : Type*) {M : Type*} {ι j : Type*} [Fintype ι]
    [Finite j] [DecidableEq ι] [CommSemiring R] [CommSemiring A]
    [Algebra R A] [AddCommMonoid M] [Module R M] (b : Module.Basis ι R M)
    {N : Type*} [AddCommMonoid N] [Module R N] (c : Module.Basis j R N) (φ : M →ₗ[R] N) :
    LinearMap.toMatrix (Algebra.TensorProduct.basis A b) (Algebra.TensorProduct.basis A c)
      (φ.baseChange A) = (LinearMap.toMatrix b c φ).map (algebraMap R A) := by
…
```
lemma MeasureTheory.addHaarScalarFactor_tensor_adeles_rat_eq_one line 160 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AddCommGroup, Module, Rat, FiniteDimensional, LinearEquiv, RingHom.id, MeasurableSpace, TensorProduct, NumberField.AdeleRing, NumberField.RingOfIntegers, BorelSpace, TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT, Eq, NNReal, MeasureTheory.addEquivAddHaarChar, TensorProduct.RightActions.instIsTopologicalAddGroup_fLT, TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT, ContinuousLinearEquiv.toContinuousAddEquiv, TensorProduct.RightActions.instModule_fLT, TensorProduct.RightActions.ContinuousLinearEquiv.baseChange and 1 more
Proof uses: Module.Basis, Fin, Module.finrank, Module.finBasis, TensorProduct.RightActions.Algebra.TensorProduct.basis, Eq.mpr, ContinuousMonoidHom, Units, MeasureTheory.ringHaarChar, MonoidHom, LinearEquiv.det, id, congrArg, MeasureTheory.addEquivAddHaarChar_eq_ringHaarChar_det_of_existsListTransvecEtc, TensorProduct.RightActions.instIsModuleTopology_fLT, Matrix.Pivot.ExistsListTransvecMulDiagonalMulListTransvec, RingHom, Matrix, RingHom.mapMatrix, Algebra.algebraMap and 61 more
153 instances, coercions and auxiliary constants left out.

Tactic trace: 15 steps
Open to load the checked before-and-after goal states.
lemma MeasureTheory.addHaarScalarFactor_tensor_adeles_eq_one line 189 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, AddCommGroup, Module, FiniteDimensional, LinearEquiv, RingHom.id, MeasurableSpace, TensorProduct, NumberField.AdeleRing, NumberField.RingOfIntegers, BorelSpace, TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT, Eq, NNReal, MeasureTheory.addEquivAddHaarChar, TensorProduct.RightActions.instIsTopologicalAddGroup_fLT, TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT, ContinuousLinearEquiv.toContinuousAddEquiv, TensorProduct.RightActions.instModule_fLT and 2 more
Proof uses: Rat, Module.compHom, Algebra.algebraMap, Module.Finite, FiniteDimensional.trans, IsScalarTower, TensorProduct.RightActions.instSMul_fLT, IsScalarTower.of_algebraMap_smul, congrFun, HSMul.hSMul, RingHom, rfl, ContinuousLinearEquiv, NumberField.AdeleRing.ModuleBaseChangeContinuousLinearEquiv, ContinuousAddEquiv, LinearEquiv.restrictScalars, borel, BorelSpace.mk, MeasureTheory.addEquivAddHaarChar_eq_addEquivAddHaarChar_of_continuousAddEquiv, Eq.mpr and 14 more
104 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma NumberField.AdeleRing.units_mem_ringHaarCharacter_ker Left multiplication by an element of Bˣ on B ⊗ 𝔸_K does not scale additive Haar measure line 221 source
Source documentation
Left multiplication by an element of Bˣ on B ⊗ 𝔸_K does not scale additive Haar measure. In other words, Bˣ is in the kernel of the ringHaarChar of B ⊗ 𝔸_K.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, FiniteDimensional, MeasurableSpace, TensorProduct, NumberField.AdeleRing, NumberField.RingOfIntegers, BorelSpace, TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT, Units, Membership.mem, Subgroup, MeasureTheory.ringHaarCharKer, TensorProduct.RightActions.instIsTopologicalRing_fLT_1, TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT, MonoidHom, Units.map, Algebra.TensorProduct.includeLeftRingHom
Proof uses: Eq.mpr, Eq, NNReal, ContinuousMonoidHom, MeasureTheory.ringHaarChar, OfNat.ofNat, id, congrArg, propext, MeasureTheory.mem_ringHaarChar_ker, MeasureTheory.addEquivAddHaarChar, ContinuousAddEquiv.mulLeft, MeasureTheory.ringHaarChar_apply, TensorProduct.RightActions.instIsTopologicalAddGroup_fLT, ContinuousLinearEquiv.toContinuousAddEquiv, TensorProduct.RightActions.instModule_fLT, TensorProduct.RightActions.ContinuousLinearEquiv.baseChange, LinearEquiv.mulLeft, eq_of_heq, HEq and 30 more
129 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
lemma NumberField.AdeleRing.units_mem_ringHaarCharacter_ker
    [MeasurableSpace (B ⊗[K] AdeleRing (𝓞 K) K)] [BorelSpace (B ⊗[K] AdeleRing (𝓞 K) K)]
    (b : Bˣ) :
    (Units.map Algebra.TensorProduct.includeLeftRingHom.toMonoidHom b :
      (B ⊗[K] AdeleRing (𝓞 K) K)ˣ) ∈
    ringHaarCharKer (B ⊗[K] AdeleRing (𝓞 K) K) := by
…
```
lemma NumberField.AdeleRing.addEquivAddHaarChar_mulRight_unit_eq_one Right multiplication by an element of Bˣ on B ⊗ 𝔸_K does not scale additive Haar measure line 239 source
Source documentation
Right multiplication by an element of Bˣ on B ⊗ 𝔸_K does not scale additive Haar measure.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, NumberField, Ring, Algebra, FiniteDimensional, MeasurableSpace, TensorProduct, NumberField.AdeleRing, NumberField.RingOfIntegers, BorelSpace, TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT, Units, Eq, NNReal, MeasureTheory.addEquivAddHaarChar, TensorProduct.RightActions.instIsTopologicalAddGroup_fLT, TensorProduct.RightActions.instLocallyCompactSpaceOfIsTopologicalRing_fLT, ContinuousAddEquiv.mulRight, TensorProduct.RightActions.instIsTopologicalRing_fLT_1, MonoidHom and 3 more
Proof uses: Eq.mpr, ContinuousLinearEquiv.toContinuousAddEquiv, TensorProduct.RightActions.instModule_fLT, TensorProduct.RightActions.ContinuousLinearEquiv.baseChange, LinearEquiv.mulRight, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm, AddGroup, TopologicalSpace, IsTopologicalAddGroup, LocallyCompactSpace, ContinuousAddEquiv, heq_of_eq, ContinuousAddEquiv.ext, id, TensorProduct.inductionOn, ContinuousLinearEquiv and 19 more
129 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
lemma NumberField.AdeleRing.addEquivAddHaarChar_mulRight_unit_eq_one
    [MeasurableSpace (B ⊗[K] AdeleRing (𝓞 K) K)] [BorelSpace (B ⊗[K] AdeleRing (𝓞 K) K)]
    (b : Bˣ) :
    addEquivAddHaarChar
      (ContinuousAddEquiv.mulRight
        (Units.map Algebra.TensorProduct.includeLeftRingHom.toMonoidHom b :
      (B ⊗[K] AdeleRing (𝓞 K) K)ˣ)) = 1 := by
…
```