ElevenTwelfths.Arithmetic

ElevenTwelfths
Arithmetic

import Mathlib.NumberTheory.NumberField.Cyclotomic.PID
import Mathlib.NumberTheory.NumberField.Cyclotomic.Three
import Mathlib.RingTheory.Ideal.Norm.AbsNorm
import Mathlib.RingTheory.UniqueFactorizationDomain.Moebius

Eisenstein arithmetic used by the 11/12 argument

This file fixes the number field and its ring of integers. In particular, 𝒪 is not an abstract parameter: it is the ring of integers of the third cyclotomic field, hence a model of the Eisenstein integers.

The analytic core is indexed by ideals, so the public element notation uses the ideal Mobius function evaluated on the principal ideal (n). The predicate primary chooses the distinguished associate congruent to 1 modulo 3; the norm is the absolute norm of the same principal ideal. This keeps the readable element sum and the ideal-indexed proof on literally the same arithmetic coefficients.

namespace ElevenTwelfths

The Eisenstein number field ℚ(ζ₃).

abbrev K := CyclotomicField 3 ℚ

The Eisenstein integers, realized as the ring of integers of ℚ(ζ₃).

abbrev 𝒪 := NumberField.RingOfIntegers K

local instance : IsCyclotomicExtension {3} ℚ K :=
  CyclotomicField.isCyclotomicExtension 3 ℚ

local instance : IsPrincipalIdealRing 𝒪 :=
  IsCyclotomicExtension.Rat.three_pid K

The chosen primitive cube root of unity in the Eisenstein integers.

noncomputable def ω : 𝒪 :=
  (IsCyclotomicExtension.zeta_spec 3 ℚ K).toInteger

A generator of the unique ramified prime ideal above 3.

noncomputable def 𝔓 : 𝒪 := ω - 1

An Eisenstein integer is primary when it is 1 modulo 3.

def primary (n : 𝒪) : Prop := (3 : 𝒪) ∣ n - 1

The ramified-prime formulation of the primary congruence.

theorem primary_iff_ramified (n : 𝒪) : primary n ↔ 𝔓 ^ 2 ∣ n - 1 := byn:𝒪⊢ primary n ↔ 𝔓 ^ 2 ∣ n - 1
  have hs : ω ^ 2 = -ω - 1 := by
    simpa only [IsUnit.unit_spec, ω] using
      IsCyclotomicExtension.Rat.Three.eta_sq (IsCyclotomicExtension.zeta_spec 3 ℚ K)n:𝒪hs:ω ^ 2 = -ω - 1⊢ primary n ↔ 𝔓 ^ 2 ∣ n - 1
  have hp : 𝔓 ^ 2 = (3 : 𝒪) * (-ω) := by
    dsimp [𝔓]n:𝒪hs:ω ^ 2 = -ω - 1⊢ (ω - 1) ^ 2 = 3 * -ω
    calc (ω - 1) ^ 2 = ω ^ 2 - 2 * ω + 1 := byn:𝒪hs:ω ^ 2 = -ω - 1⊢ (ω - 1) ^ 2 = ω ^ 2 - 2 * ω + 1 ringAll goals completed! 🐙
         _ = 3 * (-ω) := byn:𝒪hs:ω ^ 2 = -ω - 1⊢ ω ^ 2 - 2 * ω + 1 = 3 * -ω rw [hsn:𝒪hs:ω ^ 2 = -ω - 1⊢ -ω - 1 - 2 * ω + 1 = 3 * -ω]n:𝒪hs:ω ^ 2 = -ω - 1⊢ -ω - 1 - 2 * ω + 1 = 3 * -ω; ringn:𝒪hs:ω ^ 2 = -ω - 1hp:𝔓 ^ 2 = 3 * -ω⊢ primary n ↔ 𝔓 ^ 2 ∣ n - 1
  have hu : IsUnit (-ω) :=
    ((IsCyclotomicExtension.zeta_spec 3 ℚ K).toInteger_isPrimitiveRoot.isUnit
      (byn:𝒪hs:ω ^ 2 = -ω - 1hp:𝔓 ^ 2 = 3 * -ω⊢ 3 ≠ 0 decideAll goals completed! 🐙)).negn:𝒪hs:ω ^ 2 = -ω - 1hp:𝔓 ^ 2 = 3 * -ωhu:IsUnit (-ω)⊢ primary n ↔ 𝔓 ^ 2 ∣ n - 1
  rw [primary,n:𝒪hs:ω ^ 2 = -ω - 1hp:𝔓 ^ 2 = 3 * -ωhu:IsUnit (-ω)⊢ 3 ∣ n - 1 ↔ 𝔓 ^ 2 ∣ n - 1 hp,n:𝒪hs:ω ^ 2 = -ω - 1hp:𝔓 ^ 2 = 3 * -ωhu:IsUnit (-ω)⊢ 3 ∣ n - 1 ↔ 3 * -ω ∣ n - 1 IsUnit.mul_right_dvd hun:𝒪hs:ω ^ 2 = -ω - 1hp:𝔓 ^ 2 = 3 * -ωhu:IsUnit (-ω)⊢ 3 ∣ n - 1 ↔ 3 ∣ n - 1]All goals completed! 🐙

The absolute norm of an Eisenstein integer.

noncomputable def 𝒩 (n : 𝒪) : ℕ :=
  Ideal.absNorm (Ideal.span {n})

The ideal Mobius coefficient of the principal ideal generated by n. Primary restriction removes the remaining choice of associate.

noncomputable def μ_K (n : 𝒪) : ℤ :=
  UniqueFactorizationMonoid.moebius (Ideal.span {n})

Elementwise coprimality in the Eisenstein integers.

def eisensteinCoprime (a b : 𝒪) : Prop := IsCoprime a b

@[simp] theorem 𝒩_zero : 𝒩 0 = 0 := by⊢ 𝒩 0 = 0
  simp [𝒩]All goals completed! 🐙

theorem 𝒩_ne_zero {n : 𝒪} (hn : n ≠ 0) : 𝒩 n ≠ 0 := byn:𝒪hn:n ≠ 0⊢ 𝒩 n ≠ 0
  intro hnormn:𝒪hn:n ≠ 0hnorm:𝒩 n = 0⊢ False
  apply hnn:𝒪hn:n ≠ 0hnorm:𝒩 n = 0⊢ n = 0
  exact Ideal.span_singleton_eq_bot.mp (Ideal.absNorm_eq_zero_iff.mp hnorm)All goals completed! 🐙

@[simp] theorem μ_K_zero : μ_K 0 = 0 := by⊢ μ_K 0 = 0
  rw [μ_K,⊢ UniqueFactorizationMonoid.moebius (Ideal.span {0}) = 0 show Ideal.span ({0} : Set 𝒪) = 0 by⊢ μ_K 0 = 0 simpAll goals completed! 🐙]⊢ UniqueFactorizationMonoid.moebius 0 = 0
  exact UniqueFactorizationMonoid.moebius_zeroAll goals completed! 🐙

end ElevenTwelfths