FiniteAdeleRing.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

22 declarations, 0 contain sorry, 0 declared as axioms

Finite Adele Ring

Material destined for Mathlib.

Imports (5)

Imported by 5 files

lemma IsDedekindDomain.FiniteAdeleRing.prop line 27 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Field, IsDedekindDomain, Algebra, IsFractionRing, IsDedekindDomain.FiniteAdeleRing, Filter.Eventually, IsDedekindDomain.HeightOneSpectrum, Membership.mem, IsDedekindDomain.HeightOneSpectrum.adicCompletion, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Filter.cofinite
Proof uses: Subtype.property, Set
17 instances, coercions and auxiliary constants left out.
abbrev IsDedekindDomain.FiniteAdeleRing.structureMap The structure map Π 𝒪ᵥ → 𝔸ᶠ as a ring hom line 31 source
Source documentation
The structure map Π 𝒪ᵥ → 𝔸ᶠ as a ring hom.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Field, IsDedekindDomain, Algebra, IsFractionRing, RingHom, IsDedekindDomain.HeightOneSpectrum, Subtype, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, IsDedekindDomain.FiniteAdeleRing
Proof uses: RestrictedProduct.structureMapRingHom, Filter.cofinite
25 instances, coercions and auxiliary constants left out.
```
noncomputable abbrev structureMap :
    (Π v : HeightOneSpectrum R, v.adicCompletionIntegers K) →+* 𝔸ᶠ[R, K] :=
…
```
lemma IsDedekindDomain.FiniteAdeleRing.structureMap_apply_apply line 36 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Field, IsDedekindDomain, Algebra, IsFractionRing, IsDedekindDomain.HeightOneSpectrum, Subtype, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Eq, IsDedekindDomain.FiniteAdeleRing, RingHom, IsDedekindDomain.FiniteAdeleRing.structureMap
Proof uses: rfl
39 instances, coercions and auxiliary constants left out.
abbrev IsDedekindDomain.FiniteAdeleRing.integralAdeles The integral adele subring inside the finite adele ring line 39 source
Source documentation
The integral adele subring inside the finite adele ring.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Field, IsDedekindDomain, Algebra, IsFractionRing, Subring, IsDedekindDomain.FiniteAdeleRing
Proof uses: RingHom.range, IsDedekindDomain.HeightOneSpectrum, Subtype, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Membership.mem, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, IsDedekindDomain.FiniteAdeleRing.structureMap
19 instances, coercions and auxiliary constants left out.
```
noncomputable abbrev integralAdeles : Subring (FiniteAdeleRing R K) :=
…
```
lemma IsDedekindDomain.FiniteAdeleRing.one_apply line 44 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Field, IsDedekindDomain, Algebra, IsFractionRing, IsDedekindDomain.HeightOneSpectrum, Eq, IsDedekindDomain.HeightOneSpectrum.adicCompletion, IsDedekindDomain.FiniteAdeleRing, OfNat.ofNat
Proof uses: rfl
27 instances, coercions and auxiliary constants left out.
lemma IsDedekindDomain.FiniteAdeleRing.mul_apply line 46 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Field, IsDedekindDomain, Algebra, IsFractionRing, IsDedekindDomain.FiniteAdeleRing, IsDedekindDomain.HeightOneSpectrum, Eq, IsDedekindDomain.HeightOneSpectrum.adicCompletion, HMul.hMul
Proof uses: rfl
21 instances, coercions and auxiliary constants left out.
lemma IsDedekindDomain.FiniteAdeleRing.add_apply line 49 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Field, IsDedekindDomain, Algebra, IsFractionRing, IsDedekindDomain.FiniteAdeleRing, IsDedekindDomain.HeightOneSpectrum, Eq, IsDedekindDomain.HeightOneSpectrum.adicCompletion, HAdd.hAdd
Proof uses: rfl
21 instances, coercions and auxiliary constants left out.
lemma IsDedekindDomain.FiniteAdeleRing.sub_apply line 52 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Field, IsDedekindDomain, Algebra, IsFractionRing, IsDedekindDomain.FiniteAdeleRing, IsDedekindDomain.HeightOneSpectrum, Eq, IsDedekindDomain.HeightOneSpectrum.adicCompletion, HSub.hSub
Proof uses: rfl
29 instances, coercions and auxiliary constants left out.
lemma IsDedekindDomain.FiniteAdeleRing.neg_apply line 55 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Field, IsDedekindDomain, Algebra, IsFractionRing, IsDedekindDomain.FiniteAdeleRing, IsDedekindDomain.HeightOneSpectrum, Eq, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Neg.neg
Proof uses: rfl
31 instances, coercions and auxiliary constants left out.
abbrev IsDedekindDomain.FiniteAdeleRing.mk Constructor for FiniteAdeleRing R K line 59 source
Source documentation
Constructor for FiniteAdeleRing R K. An abbrev.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Field, IsDedekindDomain, Algebra, IsFractionRing, IsDedekindDomain.HeightOneSpectrum, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Filter.Eventually, Membership.mem, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Filter.cofinite, IsDedekindDomain.FiniteAdeleRing
Proof uses: Subtype.mk, Set
16 instances, coercions and auxiliary constants left out.
```
abbrev mk (f : ∀ v, HeightOneSpectrum.adicCompletion K v)
    (h : ∀ᶠ (i : HeightOneSpectrum R) in Filter.cofinite,
    f i ∈ (fun v ↦ ↑(HeightOneSpectrum.adicCompletionIntegers K v)) i) : FiniteAdeleRing R K :=
…
```
lemma IsDedekindDomain.FiniteAdeleRing.mk_apply line 65 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Field, IsDedekindDomain, Algebra, IsFractionRing, IsDedekindDomain.HeightOneSpectrum, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Filter.Eventually, Membership.mem, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Filter.cofinite, Eq, IsDedekindDomain.FiniteAdeleRing, IsDedekindDomain.FiniteAdeleRing.mk
Proof uses: rfl
18 instances, coercions and auxiliary constants left out.
def IsDedekindDomain.FiniteAdeleRing.evalAlgebraMap The K-algebra map 𝔸_K^f → Kᵥ from the finite adele ring of K to a completion line 74 source
Source documentation
The K-algebra map 𝔸_K^f → Kᵥ from the finite adele ring of K to a completion.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Field, IsDedekindDomain, Algebra, IsFractionRing, IsDedekindDomain.HeightOneSpectrum, AlgHom, IsDedekindDomain.FiniteAdeleRing, IsDedekindDomain.HeightOneSpectrum.adicCompletion
Proof uses: ContinuousAddMonoidHom, RestrictedProduct, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Filter.cofinite, RestrictedProduct.evalContinuousAddMonoidHom, AlgHom.mk, RingHom.mk, MonoidHom.mk, OneHom.mk, ZeroHom.toFun, ContinuousAddMonoidHom.toAddMonoidHom
41 instances, coercions and auxiliary constants left out.
```
noncomputable def evalAlgebraMap (j : HeightOneSpectrum R) :
    FiniteAdeleRing R K →ₐ[K] j.adicCompletion K := {
…
```
def IsDedekindDomain.FiniteAdeleRing.evalContinuousAlgebraMap The continuous K-algebra map 𝔸_K^f → Kᵥ from the finite adele ring of K to a completion line 85 source
Source documentation
The continuous K-algebra map 𝔸_K^f → Kᵥ from the finite adele ring of K to a completion.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Field, IsDedekindDomain, Algebra, IsFractionRing, IsDedekindDomain.HeightOneSpectrum, ContinuousAlgHom, IsDedekindDomain.FiniteAdeleRing, IsDedekindDomain.HeightOneSpectrum.adicCompletion
Proof uses: ContinuousAddMonoidHom, RestrictedProduct, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Filter.cofinite, RestrictedProduct.evalContinuousAddMonoidHom, AlgHom, IsDedekindDomain.FiniteAdeleRing.evalAlgebraMap, ContinuousAlgHom.mk, AlgHom.mk, RingHom.mk, MonoidHom.mk, OneHom.mk, ZeroHom.toFun, ContinuousAddMonoidHom.toAddMonoidHom
46 instances, coercions and auxiliary constants left out.
```
noncomputable def evalContinuousAlgebraMap (j : HeightOneSpectrum R) :
    FiniteAdeleRing R K →A[K] j.adicCompletion K := {
…
```
def IsDedekindDomain.FiniteAdeleRing.singleLinearMap The continuous K-linear inclusion Kᵥ → 𝔸_K^f from a completion to the finite K-adeles line 98 source
Source documentation
The continuous K-linear inclusion Kᵥ → 𝔸_K^f from a completion to the finite K-adeles.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Field, IsDedekindDomain, Algebra, IsFractionRing, DecidableEq, IsDedekindDomain.HeightOneSpectrum, LinearMap, RingHom.id, IsDedekindDomain.HeightOneSpectrum.adicCompletion, IsDedekindDomain.FiniteAdeleRing
Proof uses: ContinuousAddMonoidHom, RestrictedProduct, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Filter.cofinite, RestrictedProduct.singleContinuousAddMonoidHom, LinearMap.mk, AddHom.mk, ZeroHom.toFun, ContinuousAddMonoidHom.toAddMonoidHom
41 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
noncomputable def singleLinearMap (j : HeightOneSpectrum R) :
    j.adicCompletion K →ₗ[K] FiniteAdeleRing R K := {
…
```
def IsDedekindDomain.FiniteAdeleRing.singleMulHom The continuous K-linear inclusion Kᵥ → 𝔸_K^f from a completion to the finite K-adeles line 117 source
Source documentation
The continuous K-linear inclusion Kᵥ → 𝔸_K^f from a completion to the finite K-adeles.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Field, IsDedekindDomain, Algebra, IsFractionRing, DecidableEq, IsDedekindDomain.HeightOneSpectrum, MulHom, IsDedekindDomain.HeightOneSpectrum.adicCompletion, IsDedekindDomain.FiniteAdeleRing
Proof uses: ContinuousAddMonoidHom, RestrictedProduct, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Filter.cofinite, RestrictedProduct.singleContinuousAddMonoidHom, MulHom.mk, ZeroHom.toFun, ContinuousAddMonoidHom.toAddMonoidHom
30 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
noncomputable def singleMulHom (j : HeightOneSpectrum R) :
    j.adicCompletion K →ₙ* FiniteAdeleRing R K := {
…
```
def IsDedekindDomain.FiniteAdeleRing.singleContinuousLinearMap The continuous K-linear inclusion Kᵥ → 𝔸_K^f from a completion to the finite K-adeles line 133 source
Source documentation
The continuous K-linear inclusion Kᵥ → 𝔸_K^f from a completion to the finite K-adeles.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Field, IsDedekindDomain, Algebra, IsFractionRing, DecidableEq, IsDedekindDomain.HeightOneSpectrum, ContinuousLinearMap, RingHom.id, IsDedekindDomain.HeightOneSpectrum.adicCompletion, IsDedekindDomain.FiniteAdeleRing
Proof uses: ContinuousAddMonoidHom, RestrictedProduct, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Filter.cofinite, RestrictedProduct.singleContinuousAddMonoidHom, ContinuousLinearMap.mk, LinearMap.mk, AddHom.mk, ZeroHom.toFun, ContinuousAddMonoidHom.toAddMonoidHom
46 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
noncomputable def singleContinuousLinearMap (j : HeightOneSpectrum R) :
    j.adicCompletion K →L[K] FiniteAdeleRing R K := {
…
```
lemma IsDedekindDomain.FiniteAdeleRing.evalContinuousAlgebraMap_singleContinuousLinearMap line 151 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Field, IsDedekindDomain, Algebra, IsFractionRing, DecidableEq, IsDedekindDomain.HeightOneSpectrum, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Eq, ContinuousAlgHom, IsDedekindDomain.FiniteAdeleRing, IsDedekindDomain.FiniteAdeleRing.evalContinuousAlgebraMap, ContinuousLinearMap, RingHom.id, IsDedekindDomain.FiniteAdeleRing.singleContinuousLinearMap
Proof uses: Pi.single_eq_same
25 instances, coercions and auxiliary constants left out.
lemma IsDedekindDomain.FiniteAdeleRing.evalAlgebraMap_singleLinearMap line 157 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Field, IsDedekindDomain, Algebra, IsFractionRing, DecidableEq, IsDedekindDomain.HeightOneSpectrum, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Eq, AlgHom, IsDedekindDomain.FiniteAdeleRing, IsDedekindDomain.FiniteAdeleRing.evalAlgebraMap, LinearMap, RingHom.id, IsDedekindDomain.FiniteAdeleRing.singleLinearMap
Proof uses: Pi.single_eq_same
22 instances, coercions and auxiliary constants left out.
def IsDedekindDomain.FiniteAdeleRing.localIdempotent localIdempotent R K p is the finite adele which is 1 at p and 0 elsewhere line 166 source
Source documentation
localIdempotent R K p is the finite adele which is 1 at p and 0 elsewhere.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Field, IsDedekindDomain, Algebra, IsFractionRing, DecidableEq, IsDedekindDomain.HeightOneSpectrum, IsDedekindDomain.FiniteAdeleRing
Proof uses: Subtype.mk, IsDedekindDomain.HeightOneSpectrum.adicCompletion, Filter.Eventually, Membership.mem, Set, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Filter.cofinite, Pi.single, OfNat.ofNat
21 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
noncomputable def localIdempotent (p : HeightOneSpectrum R) : FiniteAdeleRing R K :=
…
```
lemma IsDedekindDomain.FiniteAdeleRing.eval_localIdempotent line 174 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Field, IsDedekindDomain, Algebra, IsFractionRing, DecidableEq, IsDedekindDomain.HeightOneSpectrum, Eq, IsDedekindDomain.HeightOneSpectrum.adicCompletion, ContinuousAlgHom, IsDedekindDomain.FiniteAdeleRing, IsDedekindDomain.FiniteAdeleRing.evalContinuousAlgebraMap, IsDedekindDomain.FiniteAdeleRing.localIdempotent, OfNat.ofNat
Proof uses: Pi.single_eq_same
33 instances, coercions and auxiliary constants left out.
lemma IsDedekindDomain.FiniteAdeleRing.singleContinuousAlgebraMap_comp_evalContinuousLinearMap The composite 𝔸_K^f --(eval)--> Kᵥ --(single)--> 𝔸_K^f is multiplication by the local idempotent at v line 184 source
Source documentation
The composite 𝔸_K^f --(eval)--> Kᵥ --(single)--> 𝔸_K^f is multiplication by the local idempotent at v.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Field, IsDedekindDomain, Algebra, IsFractionRing, DecidableEq, IsDedekindDomain.HeightOneSpectrum, Eq, LinearMap, RingHom.id, IsDedekindDomain.FiniteAdeleRing, ContinuousLinearMap.comp, IsDedekindDomain.HeightOneSpectrum.adicCompletion, IsDedekindDomain.FiniteAdeleRing.singleContinuousLinearMap, ContinuousAlgHom.toContinuousLinearMap, IsDedekindDomain.FiniteAdeleRing.evalContinuousAlgebraMap, LinearMap.lsmul, IsDedekindDomain.FiniteAdeleRing.localIdempotent
Proof uses: LinearMap.ext, IsDedekindDomain.FiniteAdeleRing.ext, id, Ne, Or, Pi.single, HMul.hMul, OfNat.ofNat, RestrictedProduct, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Filter.cofinite, eq_or_ne, of_eq_true, Eq.trans, True, congr, congrArg, Pi.single_eq_same, congrFun' and 5 more
96 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
lemma singleContinuousAlgebraMap_comp_evalContinuousLinearMap (j : HeightOneSpectrum R) :
    ((singleContinuousLinearMap R K j).comp
    (evalContinuousAlgebraMap R K j).toContinuousLinearMap).toLinearMap =
    LinearMap.lsmul (FiniteAdeleRing R K) (FiniteAdeleRing R K) (localIdempotent R K j) := by
…
```
Mentions: IsDedekindDomain.FiniteAdeleRing.singleContinuousLinearMap, IsDedekindDomain.FiniteAdeleRing.evalContinuousAlgebraMap, IsDedekindDomain.FiniteAdeleRing.localIdempotent
lemma IsDedekindDomain.FiniteAdeleRing.exists_mul_mem_integralAdeles line 196 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, Field, IsDedekindDomain, Algebra, IsFractionRing, IsDedekindDomain.FiniteAdeleRing, Exists, Units, And, Membership.mem, Subring, IsDedekindDomain.FiniteAdeleRing.integralAdeles, HMul.hMul, Set.Finite, IsDedekindDomain.HeightOneSpectrum, Set.ofPred, Ne, IsDedekindDomain.HeightOneSpectrum.adicCompletion, OfNat.ofNat
Proof uses: Subtype, ValuationSubring, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Submonoid, nonZeroDivisors, Eq, HDiv.hDiv, RingHom, Algebra.algebraMap, Exists.intro, IsUnit.unit, IsDedekindDomain.FiniteAdeleRing.structureMap, ite, Classical.propDecidable, Iff.mpr, IsUnit, Filter.Eventually, WithZero, Multiplicative, Int and 45 more
114 instances, coercions and auxiliary constants left out.

Tactic trace: 23 steps
Open to load the checked before-and-after goal states.