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

14 declarations, 4 contain sorry, 0 declared as axioms

Adelic Hurwitz quaternions

Base changes of the Hurwitz integers to ℚ and to ZHat, providing a quaternion algebra over the rationals and its profinite completion as free rank-4 modules over the corresponding base ring.

Main definitions

HurwitzRat: the rational quaternions ℚ + ℚi + ℚj + ℚk.
HurwitzHat: the profinite Hurwitz quaternions, a free rank-4 module over ZHat.

Imports (4)

Imported by 1 file

FLT.lean

def HurwitzHat The base change of the Hurwitz quaternions to ZHat line 32 source
Source documentation
The base change of the Hurwitz quaternions to ZHat.

standard axioms: Classical.choice, Quot.sound, propext what this means
Proof uses: TensorProduct, Int, Hurwitz, ZHat
10 instances, coercions and auxiliary constants left out.
```
noncomputable def HurwitzHat : Type := 𝓞 ⊗[ℤ] ZHat
…
```
Mentions: ZHat
instance HurwitzHat.(instance at line 39) line 39 source
def HurwitzRat The quaternion algebra ℚ + ℚi + ℚj + ℚk line 44 source
Source documentation
The quaternion algebra ℚ + ℚi + ℚj + ℚk.

standard axioms: Classical.choice, Quot.sound, propext what this means
Proof uses: TensorProduct, Int, Rat, Hurwitz
8 instances, coercions and auxiliary constants left out.
```
noncomputable def HurwitzRat : Type := ℚ ⊗[ℤ] 𝓞
…
```
instance HurwitzRat.(instance at line 51) line 51 source
def HurwitzRatHat The "profinite Hurwitz quaternions" over the finite adeles of ℚ; a free rank 4 module generated by 1, i, j, and (1+i+j+k)/2 line 59 source
Source documentation
The "profinite Hurwitz quaternions" over the finite adeles of ℚ; a free rank 4 module generated by 1, i, j, and (1+i+j+k)/2.

standard axioms: Classical.choice, Quot.sound, propext what this means
Proof uses: TensorProduct, Int, HurwitzRat, ZHat
12 instances, coercions and auxiliary constants left out.
```
noncomputable def HurwitzRatHat : Type := D ⊗[ℤ] ZHat
…
```
Mentions: ZHat
instance HurwitzRatHat.(instance at line 67) line 67 source
abbrev HurwitzRatHat.j₁ The inclusion from D=ℚ+ℚi+ℚj+ℚk to D ⊗ 𝔸, with 𝔸 the finite adeles of ℚ line 70 source
Source documentation
The inclusion from D=ℚ+ℚi+ℚj+ℚk to D ⊗ 𝔸, with 𝔸 the finite adeles of ℚ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AlgHom, Int, HurwitzRat, HurwitzRatHat
Proof uses: Algebra.TensorProduct.includeLeft, ZHat
14 instances, coercions and auxiliary constants left out.
```
noncomputable abbrev j₁ : D →ₐ[ℤ] D^ := Algebra.TensorProduct.includeLeft
```
lemma HurwitzRatHat.injective_hRat sorry line 73 source
depends on sorry what this means
Statement uses: Function.Injective, HurwitzRat, HurwitzRatHat, AlgHom, Int, HurwitzRatHat.j₁
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
15 instances, coercions and auxiliary constants left out.
instance HurwitzRatHat.(instance at line 77) line 77 source
Source comment
this stopped working in 4.29
```
noncomputable instance : Ring (ℚ ⊗[ℤ] 𝓞^) := Algebra.TensorProduct.instRing
```
instance HurwitzRatHat.(instance at line 80) line 80 source
Source comment
this stopped working in 4.29
```
noncomputable instance : Ring (D ⊗[ℤ] ZHat) := Algebra.TensorProduct.instRing
```
Mentions: ZHat
abbrev HurwitzRatHat.j₂ The inclusion from the profinite Hurwitz quaternions to to 𝔸+𝔸i+𝔸j+𝔸k, with 𝔸 the finite adeles of ℚ line 85 source
Source documentation
The inclusion from the profinite Hurwitz quaternions to to 𝔸+𝔸i+𝔸j+𝔸k, with 𝔸 the finite adeles of ℚ.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: AlgHom, Int, HurwitzHat, HurwitzRatHat
Proof uses: AlgHom.comp, TensorProduct, Rat, Hurwitz, ZHat, AlgEquiv.symm, Algebra.TensorProduct.assoc, Algebra.TensorProduct.includeRight
30 instances, coercions and auxiliary constants left out.
```
noncomputable abbrev j₂ : 𝓞^ →ₐ[ℤ] D^ :=
…
```
lemma HurwitzRatHat.injective_zHat sorry line 89 source
depends on sorry what this means
Statement uses: Function.Injective, HurwitzHat, HurwitzRatHat, AlgHom, Int, HurwitzRatHat.j₂
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
15 instances, coercions and auxiliary constants left out.
lemma HurwitzRatHat.canonicalForm should I rearrange tensors? sorry line 93 source
Source comment
should I rearrange tensors? Not sure if D^ should be (ℚ ⊗ 𝓞) ⊗ ℤhat or ℚ ⊗ (𝓞 ⊗ Zhat)

depends on sorry what this means
Statement uses: HurwitzRatHat, Exists, PNat, HurwitzHat, Eq, HMul.hMul, AlgHom, Int, HurwitzRat, HurwitzRatHat.j₁, TensorProduct.tmul, Rat, Hurwitz, Inv.inv, OfNat.ofNat, HurwitzRatHat.j₂
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Nat
47 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
lemma canonicalForm (z : D^) : ∃ (N : ℕ+) (z' : 𝓞^), z = j₁ ((N⁻¹ : ℚ) ⊗ₜ 1 : D) * j₂ z' := by
…
```
Mentions: HurwitzRatHat.j₁, HurwitzRatHat.j₂
lemma HurwitzRatHat.completed_units sorry line 96 source
depends on sorry what this means
Statement uses: Units, HurwitzRatHat, Exists, HurwitzRat, HurwitzHat, Eq, HMul.hMul, AlgHom, Int, HurwitzRatHat.j₁, HurwitzRatHat.j₂
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Nat
27 instances, coercions and auxiliary constants left out.