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

10 declarations, 0 contain sorry, 0 declared as axioms

Base change for the infinite adele ring

If v is an infinite place of a number field K, we have established in FLT.NumberField.Completion.Infinite a continuous L-algebra homomorphism NumberField.InfinitePlace.Completion.baseChangeEquiv : L ⊗[K] K_v ≃A[L] ∏ w ∣ v, L_w where the product is over all infinite places w of L lying above v.

In this file we analogously establish the base change for the infinite adele ring NumberField.InfiniteAdeleRing.baseChangeEquiv : L ⊗[K] K_∞ ≃A[L] L_∞ where K_∞ is the infinite adele ring of K and L_∞ that of L. There are two approaches:

(1) Piece together the local results on completions at infinite places to get a global result on infinite adele rings. (2) Follow the same path as that of the local result by establishing K∞ → L∞ and lifting it to a base change.

In this file we favour approach (1) because it bundles bijectivity and avoids having to reprove it. Regardless, we show that they are actually the same map in NumberField.InfiniteAdeleRing.baseChangeAlgEquiv_apply.

Diamonds

Global instances of the form Algebra K L → Algebra (f K) (f L) are avoided in this file. For example we do not define

instance [Algebra K L] : Algebra K∞ L∞ := ...

This is to prevent diamonds when K = K which was observed to cause timeouts in other files in a previous version of the repository. Instead, we add the Algebra K∞ L∞ assumption explicitly where needed.

This is in contrast to FLT.NumberField.Completion.Infinite where we do define such global instances Algebra v.Completion wv.1.Completion, but those are safe because wv : v.Extension L has a separate type to w : InfinitePlace L so no diamonds can arise.

However, we still need to make sure that the abstract K∞-algebra structure on L∞ agrees with the local structures which are already defined. This is provided by the compatibility typeclass Pi.FiberwiseSMul (fun a => a.comap (algebraMap K L)) Completion Completion which guarantees exactly this. Hence this also appears as an assumption where needed.

The desired instances are constructed later as scoped instances in FLT.NumberField.AdeleRing.

Main definitions:

NumberField.InfiniteAdeleRing.baseChange : the canonical map from K∞ to L∞.
NumberField.InfiniteAdeleRing.piEquiv : the K∞-linear homeomorphism K∞^[L:K] ≃[K∞] L∞.
NumberField.InfiniteAdeleRing.baseChangeAlgEquiv : the L-algebra isomorphism L ⊗[K] K∞ ≃ₐ[L] L∞. Note that this does not require Algebra K∞ L∞ or Pi.FiberwiseSMul ... assumptions.
NumberField.InfiniteAdeleRing.baseChangeEquiv : the L-algebra homeomorphism L ⊗[K] K∞ ≃A[L] L∞ induced by baseChange. This requires the Algebra K∞ L∞ and Pi.FiberwiseSMul ... assumptions to ensure the correct K∞-module topology on L∞.

Imports (8)

Imported by 2 files

def NumberField.InfiniteAdeleRing.baseChange The canonical map from the infinite adeles of K to the infinite adeles of L line 84 source
Source documentation
The canonical map from the infinite adeles of K to the infinite adeles of L

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, ContinuousSemialgHom, Algebra.algebraMap, NumberField.InfiniteAdeleRing
Proof uses: SemialgHom, NumberField.InfinitePlace, NumberField.InfinitePlace.Completion, Real, Subtype, Pi.semialgHomPi, NumberField.InfinitePlace.comap, NumberField.InfinitePlace.Completion.comapHom, ContinuousSemialgHom.mk
26 instances, coercions and auxiliary constants left out.
```
noncomputable def baseChange :
    K∞ →SA[algebraMap K L] L∞ where
…
```
theorem NumberField.InfiniteAdeleRing.baseChange_apply line 90 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, NumberField.InfiniteAdeleRing, NumberField.InfinitePlace, Eq, NumberField.InfinitePlace.Completion, ContinuousSemialgHom, Algebra.algebraMap, NumberField.InfiniteAdeleRing.baseChange, SemialgHom, NumberField.InfinitePlace.comap, Real, AbsoluteValue, Exists, RingHom, Complex, NumberField.place, NumberField.InfinitePlace.Completion.comapHom, rfl
33 instances, coercions and auxiliary constants left out.
instance NumberField.InfiniteAdeleRing.(instance at line 95) line 95 source
def NumberField.InfiniteAdeleRing.piEquiv The $K_{\infty}$-linear homeomorphism $K_{\infty}^{[L:K]} \cong L_{\infty}$ line 106 source
Source documentation
The $K_{\infty}$-linear homeomorphism $K_{\infty}^{[L:K]} \cong L_{\infty}$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, NumberField, NumberField.InfiniteAdeleRing, Pi.FiberwiseSMul, NumberField.InfinitePlace, NumberField.InfinitePlace.comap, Algebra.algebraMap, NumberField.InfinitePlace.Completion, Subtype, Eq, NumberField.LiesOver.instAlgebraCompletion, ContinuousLinearEquiv, RingHom.id, Fin, Module.finrank
Proof uses: ContinuousLinearEquiv.trans, ContinuousLinearEquiv.symm, ContinuousLinearEquiv.piScalarPiComm, ContinuousLinearEquiv.piScalarPiCongrFiberwise, NumberField.InfinitePlace.Extension, NumberField.InfinitePlace.Completion.piEquiv
53 instances, coercions and auxiliary constants left out.
```
noncomputable def piEquiv [Algebra K∞ L∞]
    [Pi.FiberwiseSMul (fun a : InfinitePlace L => a.comap (algebraMap K L)) Completion Completion] :
    (Fin (Module.finrank K L) → K∞) ≃L[K∞] L∞ :=
…
```
Mentions: Pi.FiberwiseSMul
instance NumberField.InfiniteAdeleRing.instIsModuleTopology_fLT line 115 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, NumberField, NumberField.InfiniteAdeleRing, Pi.FiberwiseSMul, NumberField.InfinitePlace, NumberField.InfinitePlace.comap, Algebra.algebraMap, NumberField.InfinitePlace.Completion, Subtype, Eq, NumberField.LiesOver.instAlgebraCompletion, IsModuleTopology
Proof uses: IsModuleTopology.iso, Fin, Module.finrank, NumberField.InfiniteAdeleRing.piEquiv
46 instances, coercions and auxiliary constants left out.
def NumberField.InfiniteAdeleRing.baseChangeAlgEquiv The $L$-algebra isomorphism $L\otimes_K K_{\infty} \cong L_{\infty}$ line 125 source
Source documentation
The $L$-algebra isomorphism $L\otimes_K K_{\infty} \cong L_{\infty}$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, NumberField, AlgEquiv, TensorProduct, NumberField.InfiniteAdeleRing
Proof uses: AlgEquiv.trans, NumberField.InfinitePlace, NumberField.InfinitePlace.Completion, Real, Subtype, Algebra.TensorProduct.piRight, Classical.propDecidable, Eq, AlgEquiv.symm, AbsoluteValue, Exists, RingHom, Complex, NumberField.place, AlgEquiv.piCongrFiberwise, NumberField.InfinitePlace.comap, Algebra.algebraMap, NumberField.InfinitePlace.Extension, ContinuousAlgEquiv.toAlgEquiv, NumberField.InfinitePlace.Completion.baseChangeEquiv
54 instances, coercions and auxiliary constants left out.
```
noncomputable def baseChangeAlgEquiv :
    L ⊗[K] K∞ ≃ₐ[L] L∞ :=
…
```
theorem NumberField.InfiniteAdeleRing.baseChangeAlgEquiv_tmul line 133 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, NumberField, NumberField.InfiniteAdeleRing, Eq, AlgEquiv, TensorProduct, NumberField.InfiniteAdeleRing.baseChangeAlgEquiv, TensorProduct.tmul, HMul.hMul, RingHom, Algebra.algebraMap, ContinuousSemialgHom, NumberField.InfiniteAdeleRing.baseChange
Proof uses: rfl
35 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
instance NumberField.InfiniteAdeleRing.(instance at line 137) line 137 source
instance NumberField.InfiniteAdeleRing.(instance at line 151) line 151 source
Source documentation
Take two arbitrary Algebra K L∞ and Algebra K∞ L∞ instances. Assume that Algebra K L∞ factors through (existing) Algebra K L and Algebra L L∞. Assume further that Algebra K∞ L∞ is determined by the fibers of restriction of infinite places of L to K via (x • y) v = x (v.comap (algebraMap K L)) • y v. Then the L algebra base change map is also linear in K∞.
```
instance [Algebra K∞ L∞]
    [Pi.FiberwiseSMul (fun a => a.comap (algebraMap K L)) Completion Completion] :
    IsBiscalar L K∞ (baseChangeAlgEquiv K L).toAlgHom where
…
```
Mentions: Pi.FiberwiseSMul, IsBiscalar, NumberField.InfiniteAdeleRing.baseChangeAlgEquiv
def NumberField.InfiniteAdeleRing.baseChangeEquiv line 171 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Algebra, NumberField, NumberField.InfiniteAdeleRing, Pi.FiberwiseSMul, NumberField.InfinitePlace, NumberField.InfinitePlace.comap, Algebra.algebraMap, NumberField.InfinitePlace.Completion, Subtype, Eq, NumberField.LiesOver.instAlgebraCompletion, ContinuousAlgEquiv, TensorProduct, TensorProduct.RightActions.instTopologicalSpaceOfFinite_fLT
Proof uses: IsModuleTopology.continuousAlgEquivOfIsBiscalar, TensorProduct.RightActions.instAlgebra_fLT, NumberField.InfiniteAdeleRing.baseChangeAlgEquiv
45 instances, coercions and auxiliary constants left out.