From fa3aa4aa09b498b2e78b1d7b77c23420be455a66 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 18:26:26 -0400 Subject: [PATCH 1/3] feat(foundations): Galois rings, ring Lagrange interpolation and the p-adic valuation of Q[X]/(f) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit T2.2 of #1538 (Theorem D.1 of OpenAI2026ETH, §D.4.1, pp. 57-58). - GaloisRing p n f = (Z/p^n)[X]/(f): local with maximal ideal (p), residue field F_p[X]/(f) = GaloisField p (deg f), units = nonzero mod p; distinct digit lifts differ by units, so ring Lagrange interpolation holds there. - Lagrange.ringInterpolate: Lagrange interpolation over a commutative ring at nodes with unit differences (Mathlib's Lagrange.interpolate needs a field). - AdjoinRoot.padicValuation: for f monic and irreducible mod p, the largest p-adic valuation of a coordinate is a valuation of Q[X]/(f); its valuation ring is Z_(p)[X]/(f), whose elements of valuation one are units. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 3 + .../Data/Polynomial/RingLagrange.lean | 154 ++++++++ .../Padics/AdjoinRootValuation.lean | 303 +++++++++++++++ .../Foundations/RingTheory/GaloisRing.lean | 351 ++++++++++++++++++ .../Data/Polynomial/RingLagrange.lean | 54 +++ .../Padics/AdjoinRootValuation.lean | 98 +++++ .../Foundations/RingTheory/GaloisRing.lean | 111 ++++++ 7 files changed, 1074 insertions(+) create mode 100644 Complexity/Foundations/Data/Polynomial/RingLagrange.lean create mode 100644 Complexity/Foundations/NumberTheory/Padics/AdjoinRootValuation.lean create mode 100644 Complexity/Foundations/RingTheory/GaloisRing.lean create mode 100644 ComplexityTests/Foundations/Data/Polynomial/RingLagrange.lean create mode 100644 ComplexityTests/Foundations/NumberTheory/Padics/AdjoinRootValuation.lean create mode 100644 ComplexityTests/Foundations/RingTheory/GaloisRing.lean diff --git a/Complexity.lean b/Complexity.lean index 1cd97a465..7ae579ac4 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2679,6 +2679,7 @@ public import Complexity.Foundations.Data.Polynomial.CoeffNorm1 public import Complexity.Foundations.Data.Polynomial.HermiteInterpolation public import Complexity.Foundations.Data.Polynomial.ParityAmplifier public import Complexity.Foundations.Data.Polynomial.ParityAmplifierDegree +public import Complexity.Foundations.Data.Polynomial.RingLagrange public import Complexity.Foundations.Data.Polynomial.SignQueries public import Complexity.Foundations.Data.Polynomial.StagedJetArithmetic public import Complexity.Foundations.Data.Rat.Basic @@ -2748,6 +2749,7 @@ public import Complexity.Foundations.NumberTheory.AKS.Criterion public import Complexity.Foundations.NumberTheory.AKS.Introspective public import Complexity.Foundations.NumberTheory.AKS.SmallR public import Complexity.Foundations.NumberTheory.Harmonic +public import Complexity.Foundations.NumberTheory.Padics.AdjoinRootValuation public import Complexity.Foundations.NumberTheory.PrimeCounting public import Complexity.Foundations.NumberTheory.PrimeWindow public import Complexity.Foundations.NumberTheory.SqrtPrimeWindow @@ -2777,6 +2779,7 @@ public import Complexity.Foundations.Relation.InductiveCounting public import Complexity.Foundations.Relation.RelatesWithinSteps public import Complexity.Foundations.RingTheory.CyclicIntRing public import Complexity.Foundations.RingTheory.CyclicIntRing.Coefficients +public import Complexity.Foundations.RingTheory.GaloisRing public import Complexity.Foundations.Semantics.Stateful.Amortized public import Complexity.Foundations.Semantics.Stateful.Basic public import Complexity.Foundations.Semantics.Stateful.Composition diff --git a/Complexity/Foundations/Data/Polynomial/RingLagrange.lean b/Complexity/Foundations/Data/Polynomial/RingLagrange.lean new file mode 100644 index 000000000..2ee13b010 --- /dev/null +++ b/Complexity/Foundations/Data/Polynomial/RingLagrange.lean @@ -0,0 +1,154 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate (Mathlib, `Mathlib/LinearAlgebra/Lagrange.lean`) + +public import Complexity.Init +public import Mathlib.LinearAlgebra.Lagrange + +/-! +# Lagrange interpolation over a commutative ring + +Mathlib's `Lagrange.interpolate` works over a field. Over a commutative ring `R`, interpolation at +nodes `v i`, `i ∈ s`, still works when the nodes have *unit differences*: every `v i - v j` with +`i ≠ j` is a unit. Galois rings such as `(ℤ / 2 ^ p)[U] / (f)` are the motivating example; they +are not domains, but lifts of distinct residue-field elements differ by units. + +The Lagrange basis polynomial at `i` is `∏_{j ∈ s, j ≠ i} (X - v j) / (v i - v j)`, where the +division is multiplication by `Ring.inverse (v i - v j)` (`Lagrange.ringBasis`). It is one at +`v i` and zero at the other nodes, so `Lagrange.ringInterpolate s v r = ∑ i ∈ s, r i • basis i` +takes the value `r i` at `v i`. A polynomial of degree less than `#s` that vanishes at all nodes is +zero, because the factors `X - v i` are pairwise coprime; hence every polynomial of degree less +than `#s` is the interpolant of its values (`Lagrange.eq_ringInterpolate`). Over a field these +are Mathlib's `Lagrange.basis` and `Lagrange.interpolate` +(`Lagrange.ringInterpolate_eq_interpolate`). + +## Main definitions + +* `Lagrange.ringBasis`: the Lagrange basis polynomial, with `Ring.inverse` for division. +* `Lagrange.ringInterpolate`: Lagrange interpolation over a commutative ring, as a linear map. + +## Main results + +* `Lagrange.eval_ringInterpolate_at_node`: the interpolant takes the prescribed values. +* `Lagrange.degree_ringInterpolate_lt`: it has degree less than the number of nodes. +* `Lagrange.eq_zero_of_degree_lt_of_eval_eq_zero`: uniqueness at nodes with unit differences. +* `Lagrange.eq_ringInterpolate`: a polynomial of degree less than `#s` is the interpolant of its + values. +* `Lagrange.ringInterpolate_eq_interpolate`: over a field, this is `Lagrange.interpolate`. +-/ + +public section + +namespace Lagrange + +open Polynomial Finset + +variable {R : Type*} [CommRing R] {ι : Type*} [DecidableEq ι] {s : Finset ι} {v : ι → R} + {i j : ι} + +/-- The Lagrange basis polynomial `∏_{j ∈ s, j ≠ i} (X - v j) / (v i - v j)` over a commutative +ring, where division by `v i - v j` is multiplication by `Ring.inverse (v i - v j)`. When the nodes +have unit differences it is one at `v i` and zero at the other nodes. -/ +@[expose] noncomputable def ringBasis (s : Finset ι) (v : ι → R) (i : ι) : R[X] := + ∏ j ∈ s.erase i, C (Ring.inverse (v i - v j)) * (X - C (v j)) + +/-- **Lagrange interpolation over a commutative ring**: `∑ i ∈ s, r i • ringBasis s v i`. At nodes +with unit differences, it is the unique polynomial of degree less than `#s` taking the value `r i` +at `v i`. -/ +@[expose] noncomputable def ringInterpolate (s : Finset ι) (v : ι → R) : (ι → R) →ₗ[R] R[X] where + toFun r := ∑ i ∈ s, C (r i) * ringBasis s v i + map_add' r r' := by + simp only [Pi.add_apply, C_add, add_mul, sum_add_distrib] + map_smul' c r := by + simp only [Pi.smul_apply, smul_eq_mul, C_mul, RingHom.id_apply, smul_sum, mul_assoc, + smul_eq_C_mul] + +theorem ringInterpolate_apply (s : Finset ι) (v : ι → R) (r : ι → R) : + ringInterpolate s v r = ∑ i ∈ s, C (r i) * ringBasis s v i := + rfl + +/-- The basis polynomial at `i` is one at its own node. -/ +theorem eval_ringBasis_self (hvs : (s : Set ι).Pairwise fun i j => IsUnit (v i - v j)) + (hi : i ∈ s) : (ringBasis s v i).eval (v i) = 1 := by + rw [ringBasis, eval_prod] + refine prod_eq_one fun j hj => ?_ + obtain ⟨hji, hj⟩ := mem_erase.mp hj + rw [eval_mul, eval_C, eval_sub, eval_X, eval_C] + exact Ring.inverse_mul_cancel _ (hvs hi hj (Ne.symm hji)) + +/-- The basis polynomial at `i` vanishes at every other node. -/ +theorem eval_ringBasis_of_ne (hij : i ≠ j) (hj : j ∈ s) : (ringBasis s v i).eval (v j) = 0 := by + rw [ringBasis, eval_prod] + refine prod_eq_zero (mem_erase.mpr ⟨Ne.symm hij, hj⟩) ?_ + simp only [eval_mul, eval_sub, eval_X, eval_C, sub_self, mul_zero] + +theorem natDegree_ringBasis_le (s : Finset ι) (v : ι → R) (i : ι) : + (ringBasis s v i).natDegree ≤ #(s.erase i) := by + refine (natDegree_prod_le _ _).trans + ((sum_le_sum fun j _ => ?_).trans_eq (card_eq_sum_ones _).symm) + exact (natDegree_C_mul_le _ _).trans (natDegree_X_sub_C_le _) + +/-- The basis polynomial at a node has degree less than the number of nodes. -/ +theorem degree_ringBasis_lt (hi : i ∈ s) : (ringBasis s v i).degree < #s := by + refine (degree_le_natDegree).trans_lt ?_ + have h := natDegree_ringBasis_le s v i + rw [card_erase_of_mem hi] at h + have hs : 0 < #s := card_pos.mpr ⟨i, hi⟩ + exact_mod_cast (show (ringBasis s v i).natDegree < #s by omega) + +/-- The interpolant has degree less than the number of nodes. -/ +theorem degree_ringInterpolate_lt (r : ι → R) : (ringInterpolate s v r).degree < #s := by + rw [← mem_degreeLT, ringInterpolate_apply] + refine Submodule.sum_mem _ fun i hi => ?_ + rw [← smul_eq_C_mul] + exact Submodule.smul_mem _ _ (mem_degreeLT.mpr (degree_ringBasis_lt hi)) + +/-- **The interpolant takes the prescribed values** at nodes with unit differences. -/ +theorem eval_ringInterpolate_at_node (hvs : (s : Set ι).Pairwise fun i j => IsUnit (v i - v j)) + (r : ι → R) (hi : i ∈ s) : (ringInterpolate s v r).eval (v i) = r i := by + rw [ringInterpolate_apply, eval_finsetSum, sum_eq_single_of_mem i hi, eval_mul, eval_C, + eval_ringBasis_self hvs hi, mul_one] + intro j _ hji + rw [eval_mul, eval_ringBasis_of_ne hji hi, mul_zero] + +omit [DecidableEq ι] in +/-- **Uniqueness of interpolation over a commutative ring.** A polynomial of degree less than +`#s` that vanishes at nodes with unit differences is zero: the factors `X - v i` are pairwise +coprime, so their product, of degree `#s`, divides it. -/ +theorem eq_zero_of_degree_lt_of_eval_eq_zero + (hvs : (s : Set ι).Pairwise fun i j => IsUnit (v i - v j)) {f : R[X]} (hf : f.degree < #s) + (h0 : ∀ i ∈ s, f.eval (v i) = 0) : f = 0 := by + nontriviality R + by_contra hne + have hdvd : nodal s v ∣ f := by + rw [nodal] + refine prod_dvd_of_coprime (fun i hi j hj hij => ?_) fun i hi => ?_ + · exact isCoprime_X_sub_C_of_isUnit_sub (hvs hi hj hij) + · exact dvd_iff_isRoot.mpr (h0 i hi) + exact nodal_monic.not_dvd_of_degree_lt hne (by rwa [degree_nodal]) hdvd + +/-- **Every polynomial of degree less than `#s` is the interpolant of its values** at nodes with +unit differences. -/ +theorem eq_ringInterpolate (hvs : (s : Set ι).Pairwise fun i j => IsUnit (v i - v j)) + {f : R[X]} (hf : f.degree < #s) : f = ringInterpolate s v (fun i => f.eval (v i)) := by + refine sub_eq_zero.mp (eq_zero_of_degree_lt_of_eval_eq_zero hvs + ((degree_sub_le _ _).trans_lt (max_lt hf (degree_ringInterpolate_lt _))) fun i hi => ?_) + rw [eval_sub, eval_ringInterpolate_at_node hvs _ hi, sub_self] + +/-- Over a field, `ringBasis` is Mathlib's `Lagrange.basis`. -/ +theorem ringBasis_eq_basis {F : Type*} [Field F] (s : Finset ι) (v : ι → F) (i : ι) : + ringBasis s v i = Lagrange.basis s v i := by + simp only [ringBasis, Lagrange.basis, basisDivisor, Ring.inverse_eq_inv'] + +/-- Over a field, `ringInterpolate` is Mathlib's `Lagrange.interpolate`. -/ +theorem ringInterpolate_eq_interpolate {F : Type*} [Field F] (s : Finset ι) (v : ι → F) : + ringInterpolate s v = interpolate s v := by + ext r : 1 + simp only [ringInterpolate_apply, interpolate_apply, ringBasis_eq_basis] + +end Lagrange diff --git a/Complexity/Foundations/NumberTheory/Padics/AdjoinRootValuation.lean b/Complexity/Foundations/NumberTheory/Padics/AdjoinRootValuation.lean new file mode 100644 index 000000000..707dad117 --- /dev/null +++ b/Complexity/Foundations/NumberTheory/Padics/AdjoinRootValuation.lean @@ -0,0 +1,303 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate (Mathlib, `Mathlib/NumberTheory/Padics/`) + +public import Complexity.Init +public import Mathlib.NumberTheory.Padics.PadicNumbers +public import Mathlib.RingTheory.AdjoinRoot +public import Mathlib.RingTheory.Valuation.Integers +import Complexity.Foundations.RingTheory.GaloisRing +import Mathlib.Algebra.GCDMonoid.IntegrallyClosed +import Mathlib.Algebra.Polynomial.Eval.Irreducible +import Mathlib.RingTheory.Localization.Integral +import Mathlib.RingTheory.Polynomial.Content +import Mathlib.RingTheory.Polynomial.GaussLemma + +/-! +# The `p`-adic valuation of `ℚ[X] / (f)` for `f` irreducible modulo `p` + +Let `p` be a prime and `f` a monic integer polynomial that is irreducible modulo `p`. Then `f` is +irreducible over `ℚ` (`AdjoinRoot.irreducible_map_rat`), so `K = ℚ[X] / (f)` is a field. Give each +element of `K` its coordinates in the basis `1, X, …, X ^ (deg f - 1)`, and let `v x` be the +largest `p`-adic valuation `Rat.padicValuation p` of a coordinate; written additively, `v x` is the +least `p`-adic order of a coordinate. This file proves that `v` is a valuation of `K` +(`AdjoinRoot.padicValuation`): it is multiplicative and ultrametric. + +Multiplicativity is the substantial point. Every element of `K` is a rational multiple +`r • x₀` of the image `x₀` of an element of `ℤ[X] / (f)` that is nonzero modulo `p`, and such +`x₀` have `v x₀ = 1`. Reduction modulo `p` is a ring map into the field `𝔽_p[X] / (f)`, so a +product of two such elements is again nonzero modulo `p`. + +The valuation ring `O = {x | v x ≤ 1}` of `v` consists of the elements whose coordinates have no +`p` in their denominators, that is `ℤ_(p)[X] / (f)` (`AdjoinRoot.mem_integer_padicValuation_iff`), +and an element of `O` with `v x = 1`, one that is nonzero modulo `p`, is a unit of `O` +(`AdjoinRoot.isUnit_of_padicValuation_eq_one`). + +This is the 2-adic valuation `v₂` of the coefficient field `K = ℚ[U] / (f)` of [OpenAI2026ETH] +(§D.4.1, p. 57), with `v₂ x = n` corresponding to `v x = exp (-n)`. + +## Main definitions + +* `AdjoinRoot.padicValuation`: the `p`-adic valuation of `ℚ[X] / (f)`. + +## Main results + +* `AdjoinRoot.irreducible_map_rat`: `f` is irreducible over `ℚ`. +* `AdjoinRoot.padicValuation_apply`: `v x` is the largest valuation of a coordinate of `x`. +* `AdjoinRoot.padicValuation_algebraMap`: `v` extends `Rat.padicValuation p`. +* `AdjoinRoot.padicValuation_map_eq_one_iff`: an element of `ℤ[X] / (f)` has valuation one + exactly when it is nonzero modulo `p`. +* `AdjoinRoot.mem_integer_padicValuation_iff`: the valuation ring is `ℤ_(p)[X] / (f)`. +* `AdjoinRoot.isUnit_of_padicValuation_eq_one`: elements of valuation one are units of it. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], §D.4.1, p. 57. +-/ + +public section + +open Polynomial +open scoped WithZero + +namespace AdjoinRoot + +variable (p : ℕ) [hp : Fact p.Prime] {f : ℤ[X]} + +/-- **Irreducible modulo `p` implies irreducible over `ℚ`**, for monic `f`. -/ +theorem irreducible_map_rat (hf : f.Monic) + (hirr : Irreducible (f.map (Int.castRingHom (ZMod p)))) : + Irreducible (f.map (Int.castRingHom ℚ)) := + (hf.irreducible_iff_irreducible_map_fraction_map (K := ℚ)).mp + (Monic.irreducible_of_irreducible_map _ _ hf hirr) + +variable {p} + +/-- The reduced representative has degree below `deg g`. -/ +private theorem degree_modByMonicHom_lt {R : Type*} [CommRing R] [Nontrivial R] {g : R[X]} + (hg : g.Monic) (x : AdjoinRoot g) : (modByMonicHom hg x).degree < g.degree := by + obtain ⟨Q, rfl⟩ := mk_surjective x + rw [modByMonicHom_mk] + exact degree_modByMonic_lt _ hg + +variable (p) in +/-- The largest `p`-adic valuation of a coordinate of `x` in the basis `1, X, …, X ^ (deg f - 1)`. +-/ +private noncomputable def coordVal (hf : f.Monic) (x : AdjoinRoot (f.map (Int.castRingHom ℚ))) : + ℤᵐ⁰ := + (Finset.range f.natDegree).sup fun i => + Rat.padicValuation p ((modByMonicHom (hf.map (Int.castRingHom ℚ)) x).coeff i) + +private theorem coordVal_smul_le (hf : f.Monic) (r : ℚ) + (x : AdjoinRoot (f.map (Int.castRingHom ℚ))) : + coordVal p hf (r • x) ≤ Rat.padicValuation p r * coordVal p hf x := by + refine Finset.sup_le fun i hi => ?_ + rw [LinearMap.map_smul_of_tower, coeff_smul, smul_eq_mul, map_mul] + exact mul_le_mul_right (Finset.le_sup (f := fun i => Rat.padicValuation p + ((modByMonicHom (hf.map (Int.castRingHom ℚ)) x).coeff i)) hi) _ + +/-- The coordinates scale with rational scalars. -/ +private theorem coordVal_smul (hf : f.Monic) (r : ℚ) + (x : AdjoinRoot (f.map (Int.castRingHom ℚ))) : + coordVal p hf (r • x) = Rat.padicValuation p r * coordVal p hf x := by + refine le_antisymm (coordVal_smul_le hf r x) ?_ + rcases eq_or_ne r 0 with rfl | hr + · simp + have h := coordVal_smul_le (p := p) hf r⁻¹ (r • x) + rw [inv_smul_smul₀ hr, map_inv₀] at h + calc + Rat.padicValuation p r * coordVal p hf x + ≤ Rat.padicValuation p r * ((Rat.padicValuation p r)⁻¹ * coordVal p hf (r • x)) := + mul_le_mul_right h _ + _ = coordVal p hf (r • x) := by + rw [← mul_assoc, mul_inv_cancel₀ ((Rat.padicValuation p).ne_zero_iff.mpr hr), one_mul] + +/-- The image of `ℤ[X] / (f)` in `ℚ[X] / (f)`. -/ +private noncomputable abbrev toRat (f : ℤ[X]) : + AdjoinRoot f →+* AdjoinRoot (f.map (Int.castRingHom ℚ)) := + map (Int.castRingHom ℚ) f _ dvd_rfl + +/-- Reduction of `ℤ[X] / (f)` modulo `p`. -/ +private noncomputable abbrev toZMod (p : ℕ) (f : ℤ[X]) : + AdjoinRoot f →+* AdjoinRoot (f.map (Int.castRingHom (ZMod p))) := + map (Int.castRingHom (ZMod p)) f _ dvd_rfl + +/-- The coordinates of the image of `ℤ[X] / (f)` are the integer coordinates. -/ +private theorem modByMonicHom_toRat (hf : f.Monic) (o : AdjoinRoot f) : + modByMonicHom (hf.map (Int.castRingHom ℚ)) (toRat f o) = + (modByMonicHom hf o).map (Int.castRingHom ℚ) := by + obtain ⟨Q, rfl⟩ := mk_surjective o + rw [toRat, map_mk, modByMonicHom_mk, modByMonicHom_mk, map_modByMonic _ hf] + +/-- **Images of `ℤ[X] / (f)` have valuation one exactly when they are nonzero modulo `p`**, and at +most one in any case. -/ +private theorem coordVal_toRat_eq_one_iff (hf : f.Monic) (o : AdjoinRoot f) : + coordVal p hf (toRat f o) ≤ 1 ∧ + (coordVal p hf (toRat f o) = 1 ↔ toZMod p f o ≠ 0) := by + set Q := modByMonicHom hf o + have hQdeg : ∀ i, f.natDegree ≤ i → Q.coeff i = 0 := fun i hi => + coeff_eq_zero_of_degree_lt ((degree_modByMonicHom_lt hf o).trans_le + ((degree_le_natDegree).trans (by exact_mod_cast hi))) + have hval : ∀ i, Rat.padicValuation p ((modByMonicHom (hf.map (Int.castRingHom ℚ)) + (toRat f o)).coeff i) = Int.padicValuation p (Q.coeff i) := fun i => by + rw [modByMonicHom_toRat, coeff_map, eq_intCast, Rat.padicValuation_cast] + have hle : coordVal p hf (toRat f o) ≤ 1 := + Finset.sup_le fun i _ => (hval i).trans_le (Int.padicValuation_le_one p _) + refine ⟨hle, ?_⟩ + rw [Ne, toZMod, map_eq_zero_iff _ hf dvd_rfl rfl] + simp only [eq_intCast, ZMod.intCast_zmod_eq_zero_iff_dvd] + constructor + · intro h1 hdvd + have hlt : coordVal p hf (toRat f o) < 1 := by + refine (Finset.sup_lt_iff (bot_lt_iff_ne_bot.mpr (by simp))).mpr fun i _ => ?_ + rw [hval] + exact Int.padicValuation_lt_one_iff.mpr (hdvd i) + exact hlt.ne h1 + · intro hndvd + obtain ⟨i, hi⟩ := not_forall.mp hndvd + have hie : i < f.natDegree := by + by_contra hie + exact hi (by rw [hQdeg i (not_lt.mp hie)]; exact dvd_zero _) + refine le_antisymm hle ?_ + rw [← Int.padicValuation_eq_one_iff.mpr hi, ← hval] + exact Finset.le_sup (f := fun i => Rat.padicValuation p + ((modByMonicHom (hf.map (Int.castRingHom ℚ)) (toRat f o)).coeff i)) (Finset.mem_range.mpr hie) + +/-- **Every element is a rational multiple of an integral element that is nonzero modulo `p`.** +Clear the denominators of the coordinates and divide by the content. -/ +private theorem exists_eq_smul_toRat (hf : f.Monic) + (hirr : Irreducible (f.map (Int.castRingHom (ZMod p)))) + (x : AdjoinRoot (f.map (Int.castRingHom ℚ))) : + ∃ r : ℚ, ∃ o : AdjoinRoot f, toZMod p f o ≠ 0 ∧ x = r • toRat f o := by + have := Fact.mk hirr + set P := modByMonicHom (hf.map (Int.castRingHom ℚ)) x + have hx : mk _ P = x := mk_leftInverse _ x + rcases eq_or_ne P 0 with hP | hP + · refine ⟨0, 1, by rw [map_one]; exact one_ne_zero, ?_⟩ + rw [zero_smul, ← hx, hP, map_zero] + obtain ⟨b, hb, hQ₀'⟩ := IsLocalization.integerNormalization_spec (nonZeroDivisors ℤ) P + set Q₀ := IsLocalization.integerNormalization (nonZeroDivisors ℤ) P + have hb0 : (b : ℚ) ≠ 0 := by exact_mod_cast nonZeroDivisors.ne_zero hb + have hQ₀ : Q₀.map (Int.castRingHom ℚ) = C (b : ℚ) * P := by + rw [← algebraMap_int_eq, hQ₀', ← Int.cast_smul_eq_zsmul ℚ, smul_eq_C_mul] + have hQ₀ne : Q₀ ≠ 0 := by + rintro h + rw [h, Polynomial.map_zero] at hQ₀ + exact mul_ne_zero (C_ne_zero.mpr hb0) hP hQ₀.symm + set Q₁ := Q₀.primPart + have hdeg : Q₁.degree < (f.map (Int.castRingHom (ZMod p))).degree := by + rw [hf.degree_map, degree_eq_natDegree (primPart_ne_zero Q₀), natDegree_primPart] + have hPdeg : P.degree < f.degree := + (hf.degree_map (Int.castRingHom ℚ)) ▸ degree_modByMonicHom_lt (hf.map _) x + have : Q₀.degree < f.degree := by + refine lt_of_le_of_lt ?_ hPdeg + rw [← degree_map_eq_of_injective (RingHom.injective_int (Int.castRingHom ℚ)) Q₀, hQ₀] + exact degree_mul_le_of_le (degree_C_le) le_rfl |>.trans (by simp) + rwa [degree_eq_natDegree hQ₀ne] at this + have hred : (Q₁.map (Int.castRingHom (ZMod p))) ≠ 0 := by + intro h0 + have hdvd : C (p : ℤ) ∣ Q₁ := (C_dvd_iff_dvd_coeff _ _).mpr fun i => by + rw [← ZMod.intCast_zmod_eq_zero_iff_dvd, ← eq_intCast (Int.castRingHom (ZMod p)), ← coeff_map, + h0, coeff_zero] + have hu := isPrimitive_primPart Q₀ (p : ℤ) hdvd + rw [Int.isUnit_iff_natAbs_eq, Int.natAbs_natCast] at hu + exact hp.out.one_lt.ne' hu + refine ⟨Q₀.content / b, mk f Q₁, ?_, ?_⟩ + · rw [toZMod, map_mk, Ne, mk_eq_zero] + exact (hf.map _).not_dvd_of_degree_lt hred ((degree_map_le).trans_lt hdeg) + · rw [toRat, map_mk, ← hx, Algebra.smul_def, algebraMap_eq, ← mk_C, ← map_mul] + congr 1 + have h := congrArg (Polynomial.map (Int.castRingHom ℚ)) (eq_C_content_mul_primPart Q₀) + rw [Polynomial.map_mul, map_C, hQ₀, eq_intCast] at h + calc + P = C (b : ℚ)⁻¹ * (C (b : ℚ) * P) := by + rw [← mul_assoc, ← C_mul, inv_mul_cancel₀ hb0, C_1, one_mul] + _ = C ((Q₀.content : ℚ) / b) * Q₁.map (Int.castRingHom ℚ) := by + rw [h, ← mul_assoc, ← C_mul, div_eq_inv_mul] + +variable (p) in +/-- **The `p`-adic valuation of `ℚ[X] / (f)`**, for `f` monic and irreducible modulo `p`: the +largest `p`-adic valuation of a coordinate in the basis `1, X, …, X ^ (deg f - 1)`. It extends +`Rat.padicValuation p` (`AdjoinRoot.padicValuation_algebraMap`). -/ +noncomputable def padicValuation (hf : f.Monic) + (hirr : Irreducible (f.map (Int.castRingHom (ZMod p)))) : + Valuation (AdjoinRoot (f.map (Int.castRingHom ℚ))) ℤᵐ⁰ where + toFun := coordVal p hf + map_zero' := by + simp only [coordVal, map_zero, coeff_zero] + exact Finset.sup_bot _ + map_one' := by + have := (coordVal_toRat_eq_one_iff (p := p) hf 1).2.mpr (by + have := Fact.mk hirr + rw [map_one]; exact one_ne_zero) + rwa [map_one] at this + map_mul' x y := by + have := Fact.mk hirr + obtain ⟨r, o, ho, rfl⟩ := exists_eq_smul_toRat hf hirr x + obtain ⟨r', o', ho', rfl⟩ := exists_eq_smul_toRat hf hirr y + rw [smul_mul_smul_comm, ← map_mul, coordVal_smul, coordVal_smul, coordVal_smul, map_mul, + (coordVal_toRat_eq_one_iff hf _).2.mpr (by rw [map_mul]; exact mul_ne_zero ho ho'), + (coordVal_toRat_eq_one_iff hf _).2.mpr ho, (coordVal_toRat_eq_one_iff hf _).2.mpr ho', + mul_one, mul_one, mul_one] + map_add_le_max' x y := by + refine Finset.sup_le fun i hi => ?_ + rw [map_add, coeff_add] + refine ((Rat.padicValuation p).map_add _ _).trans (max_le_max ?_ ?_) <;> + exact Finset.le_sup (f := fun i => Rat.padicValuation p _) hi + +variable (hf : f.Monic) (hirr : Irreducible (f.map (Int.castRingHom (ZMod p)))) + +/-- The valuation is the largest `p`-adic valuation of a coordinate. -/ +theorem padicValuation_apply (x : AdjoinRoot (f.map (Int.castRingHom ℚ))) : + padicValuation p hf hirr x = (Finset.range f.natDegree).sup fun i => + Rat.padicValuation p ((modByMonicHom (hf.map (Int.castRingHom ℚ)) x).coeff i) := by + simp only [padicValuation] + rfl + +/-- **The valuation extends the `p`-adic valuation of `ℚ`.** -/ +theorem padicValuation_algebraMap (r : ℚ) : + padicValuation p hf hirr (algebraMap ℚ _ r) = Rat.padicValuation p r := by + rw [Algebra.algebraMap_eq_smul_one, ← mul_one (Rat.padicValuation p r), + ← (padicValuation p hf hirr).map_one] + exact coordVal_smul hf r 1 + +/-- **An element of `ℤ[X] / (f)` has valuation one exactly when it is nonzero modulo `p`.** -/ +theorem padicValuation_map_eq_one_iff (o : AdjoinRoot f) : + padicValuation p hf hirr (map (Int.castRingHom ℚ) f _ dvd_rfl o) = 1 ↔ + map (Int.castRingHom (ZMod p)) f _ dvd_rfl o ≠ 0 := + (coordVal_toRat_eq_one_iff hf o).2 + +/-- Elements of `ℤ[X] / (f)` have valuation at most one. -/ +theorem padicValuation_map_le_one (o : AdjoinRoot f) : + padicValuation p hf hirr (map (Int.castRingHom ℚ) f _ dvd_rfl o) ≤ 1 := + (coordVal_toRat_eq_one_iff hf o).1 + +/-- **The valuation ring is `ℤ_(p)[X] / (f)`**: the elements whose coordinates have no `p` in their +denominators. -/ +theorem mem_integer_padicValuation_iff (x : AdjoinRoot (f.map (Int.castRingHom ℚ))) : + x ∈ (padicValuation p hf hirr).integer ↔ + ∀ i, Rat.padicValuation p ((modByMonicHom (hf.map (Int.castRingHom ℚ)) x).coeff i) ≤ 1 := by + rw [Valuation.mem_integer_iff, padicValuation_apply, Finset.sup_le_iff] + refine ⟨fun h i => ?_, fun h i _ => h i⟩ + rcases lt_or_ge i f.natDegree with hi | hi + · exact h i (Finset.mem_range.mpr hi) + · rw [coeff_eq_zero_of_degree_lt, map_zero] + · exact zero_le + refine (degree_modByMonicHom_lt (hf.map _) x).trans_le ?_ + rw [hf.degree_map] + exact (degree_le_natDegree).trans (by exact_mod_cast hi) + +/-- **Elements of the valuation ring that are nonzero modulo `p` are units of it**: an element of +valuation one has an inverse of valuation one. -/ +theorem isUnit_of_padicValuation_eq_one {x : AdjoinRoot (f.map (Int.castRingHom ℚ))} + (hx : x ∈ (padicValuation p hf hirr).integer) (h1 : padicValuation p hf hirr x = 1) : + IsUnit (⟨x, hx⟩ : (padicValuation p hf hirr).integer) := by + have := Fact.mk (irreducible_map_rat p hf hirr) + exact (Valuation.integer.integers _).isUnit_iff_valuation_eq_one.mpr h1 + +end AdjoinRoot diff --git a/Complexity/Foundations/RingTheory/GaloisRing.lean b/Complexity/Foundations/RingTheory/GaloisRing.lean new file mode 100644 index 000000000..da9bc2de1 --- /dev/null +++ b/Complexity/Foundations/RingTheory/GaloisRing.lean @@ -0,0 +1,351 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate (Mathlib, Galois rings) + +public import Complexity.Init +public import Complexity.Foundations.Data.Polynomial.RingLagrange +public import Mathlib.FieldTheory.Finite.GaloisField +public import Mathlib.RingTheory.AdjoinRoot +public import Mathlib.RingTheory.LocalRing.ResidueField.Defs +import Mathlib.RingTheory.LocalRing.ResidueField.Basic +import Mathlib.RingTheory.Polynomial.Nilpotent + +/-! +# Galois rings + +For a prime `p`, an exponent `n ≠ 0` and an integer polynomial `f` that is monic and irreducible +modulo `p`, the *Galois ring* `GaloisRing p n f = (ℤ / p ^ n)[X] / (f)` is a local ring. Its maximal +ideal is `(p)`, and reduction modulo `p` identifies its residue field with `𝔽_p[X] / (f)`, the +finite field with `p ^ deg f` elements. In particular an element is a unit exactly when it is +nonzero modulo `p`. + +The *digit lifts* `∑ i, c i * X ^ i` with digits `c i ∈ {0, …, p - 1}` reduce to the `p ^ deg f` +distinct residue-field elements, so any two of them differ by a unit, and Lagrange interpolation +over the ring holds at any set of them (`GaloisRing.eq_ringInterpolate_digitLift`). + +This is the coefficient ring of the Boolean tensor contraction of [OpenAI2026ETH] (§D.4.1, +pp. 57–58), which takes `p = 2`, a degree `e = 4 ⌈log₂ s⌉` and the precision `n`; the manuscript's +binary-coordinate lifts are the digit lifts for `p = 2`. + +The argument is that of a surjection onto a field with nilpotent kernel +(`RingHom.isUnit_iff_ne_zero_of_isNilpotent`): reduction modulo `p` has kernel `(p)`, and +`p ^ n = 0`. The manuscript states the unit criterion for `ℤ_(2)[U] / (f)` and proves it with the +determinant of the multiplication matrix; at a finite precision the nilpotent kernel suffices. The +statement over `ℤ_(p)` is `AdjoinRoot.isUnit_of_padicValuation_eq_one`. + +## Main definitions + +* `GaloisRing`: the ring `(ℤ / p ^ n)[X] / (f)`. +* `GaloisRing.residue`: reduction modulo `p`, onto `𝔽_p[X] / (f)`. +* `GaloisRing.digitLift`: the lift `∑ i, c i * X ^ i` of a digit vector. + +## Main results + +* `RingHom.isLocalHom_of_isNilpotent`: a surjection with nilpotent kernel is a local + homomorphism. +* `AdjoinRoot.map_eq_zero_iff`: an element of `R[X] / (g)` vanishes in `S[X] / (g)` exactly when + the coefficients of its reduced representative do. +* `GaloisRing.ker_residue`: the kernel of reduction modulo `p` is `(p)`. +* `GaloisRing.isUnit_iff`: an element is a unit exactly when it is nonzero modulo `p`. +* `GaloisRing.instIsLocalRing`, `GaloisRing.maximalIdeal_eq`: the ring is local with maximal ideal + `(p)`. +* `GaloisRing.residueFieldEquiv`, `GaloisRing.algEquivGaloisField`: its residue field is + `𝔽_p[X] / (f) ≃ GaloisField p (deg f)`. +* `GaloisRing.isUnit_digitLift_sub`: distinct digit lifts differ by a unit. +* `GaloisRing.eq_ringInterpolate_digitLift`: Lagrange interpolation at digit lifts. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*][OpenAI2026ETH], §D.4.1, pp. 57–58. +-/ + +public section + +open Polynomial IsLocalRing + +/-! ### Surjections with nilpotent kernel -/ + +namespace RingHom + +variable {R S : Type*} [CommRing R] [CommRing S] + +/-- A surjective ring homomorphism whose kernel consists of nilpotent elements is local: if `ψ x` +is a unit then `x y = 1 + n` for some `y` and nilpotent `n`. -/ +theorem isLocalHom_of_isNilpotent (ψ : R →+* S) (hψ : Function.Surjective ψ) + (hnil : ∀ x, ψ x = 0 → IsNilpotent x) : IsLocalHom ψ where + map_nonunit x hx := by + obtain ⟨u, hu⟩ := hx + obtain ⟨y, hy⟩ := hψ ↑u⁻¹ + have hn : IsNilpotent (x * y - 1) := + hnil _ (by rw [map_sub, map_mul, map_one, hy, ← hu, Units.mul_inv, sub_self]) + have h1 : IsUnit (x * y) := by + simpa only [add_sub_cancel] using hn.isUnit_one_add + exact isUnit_of_mul_isUnit_left h1 + +/-- Over a surjection onto a field with nilpotent kernel, an element is a unit exactly when its +image is nonzero. -/ +theorem isUnit_iff_ne_zero_of_isNilpotent {F : Type*} [Field F] (ψ : R →+* F) + (hψ : Function.Surjective ψ) (hnil : ∀ x, ψ x = 0 → IsNilpotent x) {x : R} : + IsUnit x ↔ ψ x ≠ 0 := by + have := ψ.isLocalHom_of_isNilpotent hψ hnil + exact ⟨fun h => (h.map ψ).ne_zero, fun h => isUnit_of_map_unit ψ x (Ne.isUnit h)⟩ + +end RingHom + +/-! ### Reducing the coefficients of `R[X] / (g)` -/ + +namespace AdjoinRoot + +variable {R S : Type*} [CommRing R] [CommRing S] (φ : R →+* S) {g : R[X]} + +/-- Reducing the coefficients maps the class of `P` to the class of `P.map φ`. -/ +theorem map_mk (q : S[X]) (h : q ∣ g.map φ) (P : R[X]) : + map φ g q h (mk g P) = mk q (P.map φ) := by + have : (map φ g q h).comp (mk g) = (mk q).comp (mapRingHom φ) := by + refine Polynomial.ringHom_ext (fun a => ?_) ?_ + · simp only [RingHom.comp_apply, mk_C, map_of, coe_mapRingHom, Polynomial.map_C] + · simp only [RingHom.comp_apply, mk_X, map_root, coe_mapRingHom, Polynomial.map_X] + exact congrArg (fun F : R[X] →+* AdjoinRoot q => F P) this + +/-- Reducing the coefficients is surjective when `φ` is. -/ +theorem map_surjective_of_surjective (q : S[X]) (h : q ∣ g.map φ) + (hφ : Function.Surjective φ) : Function.Surjective (map φ g q h) := by + intro y + obtain ⟨Q, rfl⟩ := mk_surjective y + obtain ⟨P, rfl⟩ := Polynomial.map_surjective φ hφ Q + exact ⟨mk g P, map_mk φ q h P⟩ + +/-- **An element vanishes after reducing the coefficients** of a monic `g` exactly when the +coefficients of its representative of degree below `deg g` do: that representative reduces to a +polynomial of degree below `deg (g.map φ)`, which `g.map φ` divides only when it is zero. -/ +theorem map_eq_zero_iff [Nontrivial S] (hg : g.Monic) {q : S[X]} (h : q ∣ g.map φ) + (hq : q = g.map φ) (x : AdjoinRoot g) : + map φ g q h x = 0 ↔ ∀ i, φ ((modByMonicHom hg x).coeff i) = 0 := by + subst hq + have := φ.domain_nontrivial + obtain ⟨Q, rfl⟩ := mk_surjective x + rw [modByMonicHom_mk] + set P := Q %ₘ g + have hx : mk g P = mk g Q := by + have := mk_leftInverse hg (mk g Q) + rwa [modByMonicHom_mk] at this + have hdeg : (P.map φ).degree < (g.map φ).degree := by + rw [hg.degree_map] + exact degree_map_le.trans_lt (degree_modByMonic_lt _ hg) + rw [← hx, map_mk, mk_eq_zero] + constructor + · intro hdvd i + by_contra hne + have h0 : P.map φ ≠ 0 := fun h0 => hne (by rw [← coeff_map, h0, coeff_zero]) + exact (hg.map φ).not_dvd_of_degree_lt h0 hdeg hdvd + · intro h + have : P.map φ = 0 := Polynomial.ext fun i => by rw [coeff_map, h, coeff_zero] + rw [this] + exact dvd_zero _ + +end AdjoinRoot + +/-! ### Galois rings -/ + +/-- The ring `(ℤ / p ^ n)[X] / (f)` presented by an integer polynomial `f`. For a prime `p`, +`n ≠ 0` and `f` monic and irreducible modulo `p`, it is the *Galois ring* of characteristic +`p ^ n` and rank `deg f`: a local ring with maximal ideal `(p)` and residue field +`𝔽_{p ^ deg f}`. -/ +abbrev GaloisRing (p n : ℕ) (f : ℤ[X]) : Type := + AdjoinRoot (f.map (Int.castRingHom (ZMod (p ^ n)))) + +namespace GaloisRing + +variable (p n : ℕ) (f : ℤ[X]) + +/-- Reducing integer coefficients modulo `m` and then modulo a divisor `d` of `m` is reducing +modulo `d`. -/ +theorem map_castHom_map {d m : ℕ} (h : d ∣ m) : + (f.map (Int.castRingHom (ZMod m))).map (ZMod.castHom h (ZMod d)) = + f.map (Int.castRingHom (ZMod d)) := by + rw [Polynomial.map_map] + congr 1 + exact RingHom.ext_int _ _ + +/-- The *digit lift* `∑ i, c i * X ^ i` of a digit vector `c`, with each digit `c i ∈ ZMod p` read +as an integer in `{0, …, p - 1}`. For `p = 2` these are the binary-coordinate lifts of +[OpenAI2026ETH] (§D.4.1, p. 58). -/ +@[expose] noncomputable def digitLift (c : Fin f.natDegree → ZMod p) : GaloisRing p n f := + ∑ i, ((c i).val : GaloisRing p n f) * AdjoinRoot.root _ ^ (i : ℕ) + +variable [NeZero n] + +/-- Reduction modulo `p`, from `(ℤ / p ^ n)[X] / (f)` onto `𝔽_p[X] / (f)`. -/ +noncomputable def residue : GaloisRing p n f →+* AdjoinRoot (f.map (Int.castRingHom (ZMod p))) := + AdjoinRoot.map (ZMod.castHom (dvd_pow_self p (NeZero.ne n)) (ZMod p)) _ _ + (map_castHom_map f _).symm.dvd + +@[simp] +theorem residue_mk (P : (ZMod (p ^ n))[X]) : + residue p n f (AdjoinRoot.mk _ P) = + AdjoinRoot.mk _ (P.map (ZMod.castHom (dvd_pow_self p (NeZero.ne n)) (ZMod p))) := + AdjoinRoot.map_mk _ _ _ P + +@[simp] +theorem residue_root : residue p n f (AdjoinRoot.root _) = AdjoinRoot.root _ := + AdjoinRoot.map_root _ _ _ _ + +@[simp] +theorem residue_of (a : ZMod (p ^ n)) : + residue p n f (AdjoinRoot.of _ a) = + AdjoinRoot.of _ (ZMod.castHom (dvd_pow_self p (NeZero.ne n)) (ZMod p) a) := + AdjoinRoot.map_of _ _ _ _ _ + +theorem residue_surjective : Function.Surjective (residue p n f) := + AdjoinRoot.map_surjective_of_surjective _ _ _ (ZMod.castHom_surjective _) + +variable {p n f} [Fact p.Prime] + +variable (p n f) in +/-- A digit lift reduces to `∑ i, c i * X ^ i` modulo `p`. -/ +theorem residue_digitLift (c : Fin f.natDegree → ZMod p) : + residue p n f (digitLift p n f c) = AdjoinRoot.mk _ (∑ i, C (c i) * X ^ (i : ℕ)) := by + simp only [digitLift, map_sum, map_mul, map_pow, map_natCast, residue_root, AdjoinRoot.mk_C, + AdjoinRoot.mk_X] + refine Finset.sum_congr rfl fun i _ => ?_ + rw [← map_natCast (AdjoinRoot.of _), ZMod.natCast_zmod_val] + +/-- Digit lifts reduce to distinct elements modulo `p`: the coordinates `1, X, …, X ^ (deg f - 1)` +are independent in `𝔽_p[X] / (f)` for monic `f`. -/ +theorem residue_digitLift_injective (hf : f.Monic) : + Function.Injective fun c : Fin f.natDegree → ZMod p => residue p n f (digitLift p n f c) := by + intro c c' h + simp only [residue_digitLift] at h + rw [AdjoinRoot.mk_eq_mk, ← Finset.sum_sub_distrib] at h + set P : (ZMod p)[X] := ∑ i, (C (c i) * X ^ (i : ℕ) - C (c' i) * X ^ (i : ℕ)) + have hcoeff : ∀ i : Fin f.natDegree, P.coeff i = c i - c' i := fun i => by + simp only [P, finsetSum_coeff, coeff_sub, coeff_C_mul, coeff_X_pow, mul_ite, mul_one, + mul_zero] + rw [Finset.sum_eq_single i (fun j _ hji => ?_) (by simp), ite_eq_left rfl, ite_eq_left rfl] + rw [ite_eq_right fun h => hji (Fin.ext h.symm), ite_eq_right fun h => hji (Fin.ext h.symm), + sub_zero] + have hP : P = 0 := by + by_contra h0 + refine (hf.map (Int.castRingHom (ZMod p))).not_dvd_of_degree_lt h0 ?_ h + rw [hf.degree_map, degree_eq_natDegree hf.ne_zero] + refine (degree_sum_le _ _).trans_lt + ((Finset.sup_lt_iff (WithBot.bot_lt_coe _)).mpr fun i _ => ?_) + refine (degree_sub_le _ _).trans_lt (max_lt ?_ ?_) <;> + exact (degree_C_mul_X_pow_le _ _).trans_lt (by exact_mod_cast i.isLt) + funext i + have := hcoeff i + rw [hP, coeff_zero] at this + exact (sub_eq_zero.mp this.symm) + + +/-- An element of `ℤ / p ^ n` that vanishes modulo `p` is a multiple of `p`. -/ +private theorem dvd_of_castHom_eq_zero {a : ZMod (p ^ n)} + (ha : ZMod.castHom (dvd_pow_self p (NeZero.ne n)) (ZMod p) a = 0) : (p : ZMod (p ^ n)) ∣ a := by + obtain ⟨k, rfl⟩ := ZMod.natCast_zmod_surjective a + rw [map_natCast, ZMod.natCast_eq_zero_iff] at ha + obtain ⟨m, rfl⟩ := ha + exact ⟨m, by push_cast; ring⟩ + +/-- **The kernel of reduction modulo `p` is `(p)`**, when `f` is monic. -/ +theorem ker_residue (hf : f.Monic) : + RingHom.ker (residue p n f) = Ideal.span {(p : GaloisRing p n f)} := by + ext x + rw [RingHom.mem_ker, Ideal.mem_span_singleton] + constructor + · intro hx + rw [residue, AdjoinRoot.map_eq_zero_iff _ (hf.map _) _ + (map_castHom_map f (dvd_pow_self p (NeZero.ne n))).symm] at hx + obtain ⟨Q, hQ⟩ := (C_dvd_iff_dvd_coeff (p : ZMod (p ^ n)) _).mpr fun i => + dvd_of_castHom_eq_zero (hx i) + refine ⟨AdjoinRoot.mk _ Q, ?_⟩ + rw [← AdjoinRoot.mk_leftInverse (hf.map _) x, hQ, map_mul, AdjoinRoot.mk_C, map_natCast] + · rintro ⟨y, rfl⟩ + rw [map_mul, map_natCast, ← map_natCast (AdjoinRoot.of _), ZMod.natCast_self, map_zero, + zero_mul] + +/-- `p ^ n = 0`, so elements that vanish modulo `p` are nilpotent. -/ +theorem isNilpotent_of_residue_eq_zero (hf : f.Monic) {x : GaloisRing p n f} + (hx : residue p n f x = 0) : IsNilpotent x := by + rw [← RingHom.mem_ker, ker_residue hf, Ideal.mem_span_singleton] at hx + obtain ⟨y, rfl⟩ := hx + refine ⟨n, ?_⟩ + rw [mul_pow, ← Nat.cast_pow, ← map_natCast (AdjoinRoot.of _), ZMod.natCast_self, map_zero, + zero_mul] + +variable (hf : f.Monic) (hirr : Irreducible (f.map (Int.castRingHom (ZMod p)))) +include hf hirr + +/-- **Units are the elements that are nonzero modulo `p`.** -/ +theorem isUnit_iff {x : GaloisRing p n f} : IsUnit x ↔ residue p n f x ≠ 0 := + have := Fact.mk hirr + (residue p n f).isUnit_iff_ne_zero_of_isNilpotent (residue_surjective p n f) fun _ => + isNilpotent_of_residue_eq_zero hf + +/-- **Distinct digit lifts differ by a unit.** -/ +theorem isUnit_digitLift_sub {c c' : Fin f.natDegree → ZMod p} (h : c ≠ c') : + IsUnit (digitLift p n f c - digitLift p n f c') := by + rw [isUnit_iff hf hirr, map_sub, sub_ne_zero] + exact fun h' => h (residue_digitLift_injective hf h') + +/-- **Lagrange interpolation at digit lifts.** A polynomial over a Galois ring of degree less than +`#s`, for a set `s` of digit vectors, is the interpolant of its values at their lifts; the lifts +have unit differences. -/ +theorem eq_ringInterpolate_digitLift {s : Finset (Fin f.natDegree → ZMod p)} + {P : (GaloisRing p n f)[X]} (hP : P.degree < s.card) : + P = Lagrange.ringInterpolate s (digitLift p n f) (fun c => P.eval (digitLift p n f c)) := + Lagrange.eq_ringInterpolate (fun _ _ _ _ h => isUnit_digitLift_sub hf hirr h) hP + +/-- **A Galois ring is local.** -/ +theorem isLocalRing : IsLocalRing (GaloisRing p n f) := + have := Fact.mk hirr + have := (residue p n f).isLocalHom_of_isNilpotent (residue_surjective p n f) fun _ => + isNilpotent_of_residue_eq_zero hf + (residue p n f).domain_isLocalRing + +omit hirr in +/-- `𝔽_p[X] / (f)` has `p ^ deg f` elements. -/ +theorem natCard_adjoinRoot : + Nat.card (AdjoinRoot (f.map (Int.castRingHom (ZMod p)))) = p ^ f.natDegree := by + let b := (AdjoinRoot.powerBasis' (hf.map (Int.castRingHom (ZMod p)))).basis + rw [Nat.card_congr b.equivFun.toEquiv, Nat.card_fun, Nat.card_zmod, Nat.card_eq_fintype_card, + Fintype.card_fin, AdjoinRoot.powerBasis'_dim, hf.natDegree_map] + +end GaloisRing + +/-! ### The residue field -/ + +namespace GaloisRing + +variable {p n : ℕ} {f : ℤ[X]} [NeZero n] [Fact p.Prime] [hf : Fact f.Monic] + [hirr : Fact (Irreducible (f.map (Int.castRingHom (ZMod p))))] + +instance instIsLocalRing : IsLocalRing (GaloisRing p n f) := + isLocalRing hf.out hirr.out + +/-- **The maximal ideal of a Galois ring is `(p)`.** -/ +theorem maximalIdeal_eq : maximalIdeal (GaloisRing p n f) = Ideal.span {(p : GaloisRing p n f)} := + by rw [← ker_residue hf.out, IsLocalRing.ker_eq_maximalIdeal _ (residue_surjective p n f)] + +/-- **The residue field of a Galois ring** is `𝔽_p[X] / (f)`, by reduction modulo `p`. -/ +noncomputable def residueFieldEquiv : + ResidueField (GaloisRing p n f) ≃+* AdjoinRoot (f.map (Int.castRingHom (ZMod p))) := + (Ideal.quotEquivOfEq (IsLocalRing.ker_eq_maximalIdeal _ (residue_surjective p n f)).symm).trans + (RingHom.quotientKerEquivOfSurjective (residue_surjective p n f)) + +@[simp] +theorem residueFieldEquiv_residue (x : GaloisRing p n f) : + residueFieldEquiv (IsLocalRing.residue _ x) = residue p n f x := by + simp only [residueFieldEquiv] + rfl + +/-- **The residue field is the Galois field** with `p ^ deg f` elements. -/ +noncomputable def algEquivGaloisField : + AdjoinRoot (f.map (Int.castRingHom (ZMod p))) ≃ₐ[ZMod p] GaloisField p f.natDegree := + GaloisField.algEquivGaloisField p f.natDegree (natCard_adjoinRoot hf.out) + +end GaloisRing diff --git a/ComplexityTests/Foundations/Data/Polynomial/RingLagrange.lean b/ComplexityTests/Foundations/Data/Polynomial/RingLagrange.lean new file mode 100644 index 000000000..94333bd0b --- /dev/null +++ b/ComplexityTests/Foundations/Data/Polynomial/RingLagrange.lean @@ -0,0 +1,54 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Foundations.Data.Polynomial.RingLagrange +import Mathlib.Data.ZMod.Basic +import Mathlib.Tactic.FinCases + +/-! Tests for Lagrange interpolation over a commutative ring. -/ + +namespace ComplexityTests.RingLagrange + +open Polynomial Lagrange + +/-! ### Interpolation over `ZMod 8`, which is not a domain -/ + +/-- The nodes `0` and `1` of `ZMod 8` differ by a unit. -/ +theorem pairwise_isUnit : + ((Finset.univ : Finset (Fin 2)) : Set (Fin 2)).Pairwise + fun i j => IsUnit ((![0, 1] : Fin 2 → ZMod 8) i - ![0, 1] j) := by + intro i _ j _ hij + fin_cases i <;> fin_cases j + · exact absurd rfl hij + · simp + · simp + · exact absurd rfl hij + +/-- The interpolant of the values `3, 5` at `0, 1` takes those values. -/ +example : (ringInterpolate Finset.univ (![0, 1] : Fin 2 → ZMod 8) ![3, 5]).eval 0 = 3 ∧ + (ringInterpolate Finset.univ (![0, 1] : Fin 2 → ZMod 8) ![3, 5]).eval 1 = 5 := + ⟨eval_ringInterpolate_at_node pairwise_isUnit _ (Finset.mem_univ (0 : Fin 2)), + eval_ringInterpolate_at_node pairwise_isUnit _ (Finset.mem_univ (1 : Fin 2))⟩ + +/-- A linear polynomial over `ZMod 8` is the interpolant of its values at `0` and `1`. -/ +example : (C 3 + C 2 * X : (ZMod 8)[X]) = + ringInterpolate Finset.univ (![0, 1] : Fin 2 → ZMod 8) + (fun i => (C 3 + C 2 * X : (ZMod 8)[X]).eval (![0, 1] i)) := + eq_ringInterpolate pairwise_isUnit ((degree_add_le _ _).trans_lt (max_lt + (degree_C_le.trans_lt (by decide)) ((degree_C_mul_X_le _).trans_lt (by decide)))) + +/-! ### Unit differences are needed -/ + +/-- Over `ZMod 4`, the nodes `0` and `2` differ by the non-unit `2`, and the nonzero polynomial +`2 X` of degree below two vanishes at both: uniqueness fails without unit differences. -/ +example : (C 2 * X : (ZMod 4)[X]).eval 0 = 0 ∧ (C 2 * X : (ZMod 4)[X]).eval 2 = 0 ∧ + (C 2 * X : (ZMod 4)[X]) ≠ 0 := by + refine ⟨by simp, by simp only [eval_mul, eval_C, eval_X]; decide, fun h => ?_⟩ + have := congrArg (coeff · 1) h + simp only [coeff_C_mul, coeff_X_one, mul_one, coeff_zero] at this + exact absurd this (by decide) + +end ComplexityTests.RingLagrange diff --git a/ComplexityTests/Foundations/NumberTheory/Padics/AdjoinRootValuation.lean b/ComplexityTests/Foundations/NumberTheory/Padics/AdjoinRootValuation.lean new file mode 100644 index 000000000..1219f44ba --- /dev/null +++ b/ComplexityTests/Foundations/NumberTheory/Padics/AdjoinRootValuation.lean @@ -0,0 +1,98 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Foundations.NumberTheory.Padics.AdjoinRootValuation +import Mathlib.Algebra.Field.ZMod +import Mathlib.Algebra.Polynomial.SpecificDegree +import Mathlib.Tactic.ComputeDegree +import Mathlib.Tactic.FinCases + +/-! Tests for the 2-adic valuation of `K = ℚ[U] / (U ^ 2 + U + 1)`, the case `e = 2` of the +coefficient field of [OpenAI2026ETH], §D.4.1. -/ + +namespace ComplexityTests.AdjoinRootValuation + +open Polynomial +open scoped WithZero + +/-- `U ^ 2 + U + 1`, irreducible modulo 2. -/ +noncomputable def f : ℤ[X] := X ^ 2 + X + 1 + +theorem f_monic : f.Monic := by unfold f; monicity! + +theorem f_irreducible : Irreducible (f.map (Int.castRingHom (ZMod 2))) := by + unfold f + simp only [Polynomial.map_add, Polynomial.map_pow, Polynomial.map_X, Polynomial.map_one] + refine Polynomial.irreducible_of_degree_le_three_of_not_isRoot ?_ ?_ + · have : (X ^ 2 + X + 1 : (ZMod 2)[X]).natDegree = 2 := by compute_degree! + simp [this] + · intro x hx + rw [IsRoot.def, eval_add, eval_add, eval_pow, eval_X, eval_one] at hx + fin_cases x <;> revert hx <;> decide + +/-- The field `K = ℚ[U] / (U ^ 2 + U + 1)`. -/ +abbrev K : Type := AdjoinRoot (f.map (Int.castRingHom ℚ)) + +/-- The 2-adic valuation of `K`. -/ +noncomputable abbrev v : Valuation K ℤᵐ⁰ := AdjoinRoot.padicValuation 2 f_monic f_irreducible + +/-- The map `ℤ[U] / (f) → K`. -/ +noncomputable abbrev ι : AdjoinRoot f →+* K := AdjoinRoot.map (Int.castRingHom ℚ) f _ dvd_rfl + +instance : Fact (Irreducible (f.map (Int.castRingHom (ZMod 2)))) := ⟨f_irreducible⟩ + +/-- `U ^ 2 + U + 1 = 0` modulo `2`. -/ +theorem root_sq_add_root_add_one : + (AdjoinRoot.root (f.map (Int.castRingHom (ZMod 2)))) ^ 2 + AdjoinRoot.root _ + 1 = 0 := by + rw [← AdjoinRoot.mk_X, ← map_pow, ← map_add, ← map_one (AdjoinRoot.mk _), ← map_add, + AdjoinRoot.mk_eq_zero] + exact dvd_of_eq (by simp [f]) + +/-- `U` is nonzero modulo `2`: otherwise `f(0) = 1` would vanish. -/ +theorem root_ne_zero_mod_two : + AdjoinRoot.map (Int.castRingHom (ZMod 2)) f _ dvd_rfl (AdjoinRoot.root f) ≠ 0 := by + rw [AdjoinRoot.map_root] + intro h + have := root_sq_add_root_add_one + rw [h] at this + simp at this + +/-- `1 + U` is nonzero modulo `2`: it is `U²`, the square of a nonzero element of a field. -/ +theorem one_add_root_ne_zero_mod_two : + AdjoinRoot.map (Int.castRingHom (ZMod 2)) f _ dvd_rfl (1 + AdjoinRoot.root f) ≠ 0 := by + have hroot := root_ne_zero_mod_two + rw [AdjoinRoot.map_root] at hroot + rw [map_add, map_one, AdjoinRoot.map_root] + intro h1 + have h := root_sq_add_root_add_one + rw [add_assoc, add_comm (AdjoinRoot.root _), h1, add_zero] at h + exact pow_ne_zero 2 hroot h + +/-! ### The valuation on concrete elements -/ + +theorem padicValRat_two : padicValRat 2 (2 : ℚ) = 1 := by + exact_mod_cast padicValRat.self (p := 2) one_lt_two + +/-- `v (1 / 2) = exp 1`: the valuation extends that of `ℚ`. -/ +example : v (algebraMap ℚ K (1 / 2)) = WithZero.exp 1 := by + rw [AdjoinRoot.padicValuation_algebraMap] + simp [Rat.padicValuation, padicValRat_two] + +/-- `v (2 U) = v 2 * v U = exp (-1)`, by multiplicativity: `U` is nonzero modulo `2`. -/ +example : v (algebraMap ℚ K 2 * ι (AdjoinRoot.root f)) = WithZero.exp (-1) := by + rw [map_mul, AdjoinRoot.padicValuation_algebraMap, + (AdjoinRoot.padicValuation_map_eq_one_iff f_monic f_irreducible _).mpr root_ne_zero_mod_two, + mul_one] + simp [Rat.padicValuation, padicValRat_two] + +/-- `1 + U` is integral and nonzero modulo `2`, hence a unit of the valuation ring. -/ +example : ∃ h : ι (1 + AdjoinRoot.root f) ∈ v.integer, IsUnit (⟨_, h⟩ : v.integer) := + have h := AdjoinRoot.padicValuation_map_le_one f_monic f_irreducible (1 + AdjoinRoot.root f) + ⟨h, AdjoinRoot.isUnit_of_padicValuation_eq_one f_monic f_irreducible h + ((AdjoinRoot.padicValuation_map_eq_one_iff f_monic f_irreducible _).mpr + one_add_root_ne_zero_mod_two)⟩ + +end ComplexityTests.AdjoinRootValuation diff --git a/ComplexityTests/Foundations/RingTheory/GaloisRing.lean b/ComplexityTests/Foundations/RingTheory/GaloisRing.lean new file mode 100644 index 000000000..c11fcc94d --- /dev/null +++ b/ComplexityTests/Foundations/RingTheory/GaloisRing.lean @@ -0,0 +1,111 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Complexity.Foundations.RingTheory.GaloisRing +import Mathlib.Algebra.Polynomial.SpecificDegree +import Mathlib.Tactic.ComputeDegree +import Mathlib.Tactic.FinCases + +/-! Tests for Galois rings, on `(ℤ / 8)[U] / (U ^ 2 + U + 1)`: the case `p = 2`, `e = 2` and +precision `3` of the coefficient ring of [OpenAI2026ETH], §D.4.1. -/ + +namespace ComplexityTests.GaloisRing + +open Polynomial IsLocalRing + +/-- `U ^ 2 + U + 1`, irreducible modulo 2. -/ +noncomputable def f : ℤ[X] := X ^ 2 + X + 1 + +theorem f_monic : f.Monic := by unfold f; monicity! + +theorem f_natDegree : f.natDegree = 2 := by unfold f; compute_degree! + +theorem f_irreducible : Irreducible (f.map (Int.castRingHom (ZMod 2))) := by + unfold f + simp only [Polynomial.map_add, Polynomial.map_pow, Polynomial.map_X, Polynomial.map_one] + refine Polynomial.irreducible_of_degree_le_three_of_not_isRoot ?_ ?_ + · have : (X ^ 2 + X + 1 : (ZMod 2)[X]).natDegree = 2 := by compute_degree! + simp [this] + · intro x hx + rw [IsRoot.def, eval_add, eval_add, eval_pow, eval_X, eval_one] at hx + fin_cases x <;> revert hx <;> decide + +instance : Fact f.Monic := ⟨f_monic⟩ + +instance : Fact (Irreducible (f.map (Int.castRingHom (ZMod 2)))) := ⟨f_irreducible⟩ + +/-- The ring `(ℤ / 8)[U] / (U ^ 2 + U + 1)`. -/ +abbrev A : Type := GaloisRing 2 3 f + +/-- The root `U`. -/ +noncomputable abbrev U : A := AdjoinRoot.root _ + +/-! ### Locality and units -/ + +/-- The residue field has characteristic two. -/ +theorem two_eq_zero : (2 : AdjoinRoot (f.map (Int.castRingHom (ZMod 2)))) = 0 := by + rw [← map_ofNat (AdjoinRoot.of _), show (OfNat.ofNat 2 : ZMod 2) = 0 by decide, map_zero] + +/-- The ring is local. -/ +example : IsLocalRing A := inferInstance + +/-- `2` is not a unit: it vanishes modulo `2`. -/ +example : ¬IsUnit (2 : A) := by + rw [GaloisRing.isUnit_iff f_monic f_irreducible, map_ofNat, not_not] + exact two_eq_zero + +/-- `1 + 2 U` is a unit: it is one modulo `2`. -/ +example : IsUnit (1 + 2 * U) := by + rw [GaloisRing.isUnit_iff f_monic f_irreducible] + simp only [map_add, map_mul, map_one, map_ofNat, two_eq_zero, zero_mul, add_zero] + exact one_ne_zero + +/-- `2` generates the maximal ideal. -/ +example : (2 : A) ∈ maximalIdeal A := by + rw [GaloisRing.maximalIdeal_eq] + exact_mod_cast Ideal.mem_span_singleton_self (2 : A) + +/-- The residue field has `2 ^ 2 = 4` elements. -/ +example : Nat.card (AdjoinRoot (f.map (Int.castRingHom (ZMod 2)))) = 4 := by + rw [GaloisRing.natCard_adjoinRoot f_monic, f_natDegree] + norm_num + +/-! ### Digit lifts and interpolation -/ + +/-- The digit vector `(0, 1)`. -/ +def c₀₁ : Fin f.natDegree → ZMod 2 := fun i => if (i : ℕ) = 1 then 1 else 0 + +/-- The digit vector `(1, 0)`. -/ +def c₁₀ : Fin f.natDegree → ZMod 2 := fun i => if (i : ℕ) = 0 then 1 else 0 + +/-- The lift of `(0, 1)` is `U`, and the lift of `(1, 0)` is `1`. -/ +theorem digitLift_c₀₁ : + GaloisRing.digitLift 2 3 f c₀₁ = U ∧ GaloisRing.digitLift 2 3 f c₁₀ = 1 := by + simp only [GaloisRing.digitLift, Fin.sum_univ_eq_sum_range + (fun i => (((if i = 1 then 1 else 0 : ZMod 2)).val : A) * AdjoinRoot.root _ ^ i), + Fin.sum_univ_eq_sum_range + (fun i => (((if i = 0 then 1 else 0 : ZMod 2)).val : A) * AdjoinRoot.root _ ^ i), + c₀₁, c₁₀, f_natDegree, Finset.sum_range_succ, Finset.sum_range_zero] + exact ⟨by simp [ZMod.val_one]; rfl, by simp [ZMod.val_one]⟩ + +/-- `U - 1` is a unit, as the difference of two distinct digit lifts. -/ +example : IsUnit (U - 1) := by + rw [← digitLift_c₀₁.1, ← digitLift_c₀₁.2] + refine GaloisRing.isUnit_digitLift_sub f_monic f_irreducible fun h => ?_ + have := congrFun h ⟨1, by rw [f_natDegree]; norm_num⟩ + simp [c₀₁, c₁₀] at this + +/-- There are `4` digit vectors, so a cubic over the ring is the interpolant of its values at the +four digit lifts. -/ +example (P : A[X]) (hP : P.natDegree ≤ 3) : + P = Lagrange.ringInterpolate Finset.univ (GaloisRing.digitLift 2 3 f) + (fun c => P.eval (GaloisRing.digitLift 2 3 f c)) := by + refine GaloisRing.eq_ringInterpolate_digitLift f_monic f_irreducible + ((degree_le_natDegree).trans_lt ?_) + rw [Finset.card_univ, Fintype.card_fun, ZMod.card, Fintype.card_fin, f_natDegree] + exact_mod_cast (show P.natDegree < 2 ^ 2 by omega) + +end ComplexityTests.GaloisRing From f9349461854369452a5b74f4698f350ab194f7a5 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 22:11:30 -0400 Subject: [PATCH 2/3] refactor(foundations): move AdjoinRoot coefficient reduction to its own module `AdjoinRoot.map_mk`, `AdjoinRoot.map_surjective_of_surjective` and `AdjoinRoot.map_eq_zero_iff` move unchanged from `GaloisRing.lean` to the new `Complexity/Foundations/RingTheory/AdjoinRoot.lean`. Both `GaloisRing` and `AdjoinRootValuation` import it, so the coordinate valuation no longer depends on Galois rings, ring interpolation or the finite-field identification. Names are unchanged; `GaloisRing` re-exports the module publicly. Addresses the placement finding of reviewer-codex-edemaine on #1859. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity.lean | 1 + .../Padics/AdjoinRootValuation.lean | 3 +- .../Foundations/RingTheory/AdjoinRoot.lean | 85 +++++++++++++++++++ .../Foundations/RingTheory/GaloisRing.lean | 57 +------------ 4 files changed, 89 insertions(+), 57 deletions(-) create mode 100644 Complexity/Foundations/RingTheory/AdjoinRoot.lean diff --git a/Complexity.lean b/Complexity.lean index 7ae579ac4..6e4816571 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2777,6 +2777,7 @@ public import Complexity.Foundations.Probability.TrueSampleMeans public import Complexity.Foundations.Quantum.Measurement public import Complexity.Foundations.Relation.InductiveCounting public import Complexity.Foundations.Relation.RelatesWithinSteps +public import Complexity.Foundations.RingTheory.AdjoinRoot public import Complexity.Foundations.RingTheory.CyclicIntRing public import Complexity.Foundations.RingTheory.CyclicIntRing.Coefficients public import Complexity.Foundations.RingTheory.GaloisRing diff --git a/Complexity/Foundations/NumberTheory/Padics/AdjoinRootValuation.lean b/Complexity/Foundations/NumberTheory/Padics/AdjoinRootValuation.lean index 707dad117..edb4016e1 100644 --- a/Complexity/Foundations/NumberTheory/Padics/AdjoinRootValuation.lean +++ b/Complexity/Foundations/NumberTheory/Padics/AdjoinRootValuation.lean @@ -11,7 +11,8 @@ public import Complexity.Init public import Mathlib.NumberTheory.Padics.PadicNumbers public import Mathlib.RingTheory.AdjoinRoot public import Mathlib.RingTheory.Valuation.Integers -import Complexity.Foundations.RingTheory.GaloisRing +import Complexity.Foundations.RingTheory.AdjoinRoot +import Mathlib.Algebra.Field.ZMod import Mathlib.Algebra.GCDMonoid.IntegrallyClosed import Mathlib.Algebra.Polynomial.Eval.Irreducible import Mathlib.RingTheory.Localization.Integral diff --git a/Complexity/Foundations/RingTheory/AdjoinRoot.lean b/Complexity/Foundations/RingTheory/AdjoinRoot.lean new file mode 100644 index 000000000..39bfed75e --- /dev/null +++ b/Complexity/Foundations/RingTheory/AdjoinRoot.lean @@ -0,0 +1,85 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate (Mathlib, `Mathlib/RingTheory/AdjoinRoot.lean`) + +public import Complexity.Init +public import Mathlib.RingTheory.AdjoinRoot + +/-! +# Reducing the coefficients of `R[X] / (g)` + +For a ring homomorphism `φ : R →+* S` and `q ∣ g.map φ`, Mathlib's `AdjoinRoot.map φ g q` sends +`R[X] / (g)` to `S[X] / (q)`. This file computes it on classes of polynomials, shows that it is +surjective when `φ` is, and characterizes its kernel when `g` is monic and `q = g.map φ`: an element +vanishes exactly when the coefficients of its reduced representative do. + +These facts are used both for Galois rings (`GaloisRing.residue`, reduction modulo `p`) and for the +`p`-adic valuation of `ℚ[X] / (f)` (`AdjoinRoot.padicValuation`). + +## Main results + +* `AdjoinRoot.map_mk`: the class of `P` maps to the class of `P.map φ`. +* `AdjoinRoot.map_surjective_of_surjective`: reducing the coefficients is surjective when `φ` is. +* `AdjoinRoot.map_eq_zero_iff`: an element of `R[X] / (g)` vanishes in `S[X] / (g.map φ)` exactly + when the coefficients of its reduced representative do. +-/ + +public section + +open Polynomial + +namespace AdjoinRoot + +variable {R S : Type*} [CommRing R] [CommRing S] (φ : R →+* S) {g : R[X]} + +/-- Reducing the coefficients maps the class of `P` to the class of `P.map φ`. -/ +theorem map_mk (q : S[X]) (h : q ∣ g.map φ) (P : R[X]) : + map φ g q h (mk g P) = mk q (P.map φ) := by + have : (map φ g q h).comp (mk g) = (mk q).comp (mapRingHom φ) := by + refine Polynomial.ringHom_ext (fun a => ?_) ?_ + · simp only [RingHom.comp_apply, mk_C, map_of, coe_mapRingHom, Polynomial.map_C] + · simp only [RingHom.comp_apply, mk_X, map_root, coe_mapRingHom, Polynomial.map_X] + exact congrArg (fun F : R[X] →+* AdjoinRoot q => F P) this + +/-- Reducing the coefficients is surjective when `φ` is. -/ +theorem map_surjective_of_surjective (q : S[X]) (h : q ∣ g.map φ) + (hφ : Function.Surjective φ) : Function.Surjective (map φ g q h) := by + intro y + obtain ⟨Q, rfl⟩ := mk_surjective y + obtain ⟨P, rfl⟩ := Polynomial.map_surjective φ hφ Q + exact ⟨mk g P, map_mk φ q h P⟩ + +/-- **An element vanishes after reducing the coefficients** of a monic `g` exactly when the +coefficients of its representative of degree below `deg g` do: that representative reduces to a +polynomial of degree below `deg (g.map φ)`, which `g.map φ` divides only when it is zero. -/ +theorem map_eq_zero_iff [Nontrivial S] (hg : g.Monic) {q : S[X]} (h : q ∣ g.map φ) + (hq : q = g.map φ) (x : AdjoinRoot g) : + map φ g q h x = 0 ↔ ∀ i, φ ((modByMonicHom hg x).coeff i) = 0 := by + subst hq + have := φ.domain_nontrivial + obtain ⟨Q, rfl⟩ := mk_surjective x + rw [modByMonicHom_mk] + set P := Q %ₘ g + have hx : mk g P = mk g Q := by + have := mk_leftInverse hg (mk g Q) + rwa [modByMonicHom_mk] at this + have hdeg : (P.map φ).degree < (g.map φ).degree := by + rw [hg.degree_map] + exact degree_map_le.trans_lt (degree_modByMonic_lt _ hg) + rw [← hx, map_mk, mk_eq_zero] + constructor + · intro hdvd i + by_contra hne + have h0 : P.map φ ≠ 0 := fun h0 => hne (by rw [← coeff_map, h0, coeff_zero]) + exact (hg.map φ).not_dvd_of_degree_lt h0 hdeg hdvd + · intro h + have : P.map φ = 0 := Polynomial.ext fun i => by rw [coeff_map, h, coeff_zero] + rw [this] + exact dvd_zero _ + +end AdjoinRoot diff --git a/Complexity/Foundations/RingTheory/GaloisRing.lean b/Complexity/Foundations/RingTheory/GaloisRing.lean index da9bc2de1..79a1b2965 100644 --- a/Complexity/Foundations/RingTheory/GaloisRing.lean +++ b/Complexity/Foundations/RingTheory/GaloisRing.lean @@ -9,8 +9,8 @@ module public import Complexity.Init public import Complexity.Foundations.Data.Polynomial.RingLagrange +public import Complexity.Foundations.RingTheory.AdjoinRoot public import Mathlib.FieldTheory.Finite.GaloisField -public import Mathlib.RingTheory.AdjoinRoot public import Mathlib.RingTheory.LocalRing.ResidueField.Defs import Mathlib.RingTheory.LocalRing.ResidueField.Basic import Mathlib.RingTheory.Polynomial.Nilpotent @@ -48,8 +48,6 @@ statement over `ℤ_(p)` is `AdjoinRoot.isUnit_of_padicValuation_eq_one`. * `RingHom.isLocalHom_of_isNilpotent`: a surjection with nilpotent kernel is a local homomorphism. -* `AdjoinRoot.map_eq_zero_iff`: an element of `R[X] / (g)` vanishes in `S[X] / (g)` exactly when - the coefficients of its reduced representative do. * `GaloisRing.ker_residue`: the kernel of reduction modulo `p` is `(p)`. * `GaloisRing.isUnit_iff`: an element is a unit exactly when it is nonzero modulo `p`. * `GaloisRing.instIsLocalRing`, `GaloisRing.maximalIdeal_eq`: the ring is local with maximal ideal @@ -97,59 +95,6 @@ theorem isUnit_iff_ne_zero_of_isNilpotent {F : Type*} [Field F] (ψ : R →+* F) end RingHom -/-! ### Reducing the coefficients of `R[X] / (g)` -/ - -namespace AdjoinRoot - -variable {R S : Type*} [CommRing R] [CommRing S] (φ : R →+* S) {g : R[X]} - -/-- Reducing the coefficients maps the class of `P` to the class of `P.map φ`. -/ -theorem map_mk (q : S[X]) (h : q ∣ g.map φ) (P : R[X]) : - map φ g q h (mk g P) = mk q (P.map φ) := by - have : (map φ g q h).comp (mk g) = (mk q).comp (mapRingHom φ) := by - refine Polynomial.ringHom_ext (fun a => ?_) ?_ - · simp only [RingHom.comp_apply, mk_C, map_of, coe_mapRingHom, Polynomial.map_C] - · simp only [RingHom.comp_apply, mk_X, map_root, coe_mapRingHom, Polynomial.map_X] - exact congrArg (fun F : R[X] →+* AdjoinRoot q => F P) this - -/-- Reducing the coefficients is surjective when `φ` is. -/ -theorem map_surjective_of_surjective (q : S[X]) (h : q ∣ g.map φ) - (hφ : Function.Surjective φ) : Function.Surjective (map φ g q h) := by - intro y - obtain ⟨Q, rfl⟩ := mk_surjective y - obtain ⟨P, rfl⟩ := Polynomial.map_surjective φ hφ Q - exact ⟨mk g P, map_mk φ q h P⟩ - -/-- **An element vanishes after reducing the coefficients** of a monic `g` exactly when the -coefficients of its representative of degree below `deg g` do: that representative reduces to a -polynomial of degree below `deg (g.map φ)`, which `g.map φ` divides only when it is zero. -/ -theorem map_eq_zero_iff [Nontrivial S] (hg : g.Monic) {q : S[X]} (h : q ∣ g.map φ) - (hq : q = g.map φ) (x : AdjoinRoot g) : - map φ g q h x = 0 ↔ ∀ i, φ ((modByMonicHom hg x).coeff i) = 0 := by - subst hq - have := φ.domain_nontrivial - obtain ⟨Q, rfl⟩ := mk_surjective x - rw [modByMonicHom_mk] - set P := Q %ₘ g - have hx : mk g P = mk g Q := by - have := mk_leftInverse hg (mk g Q) - rwa [modByMonicHom_mk] at this - have hdeg : (P.map φ).degree < (g.map φ).degree := by - rw [hg.degree_map] - exact degree_map_le.trans_lt (degree_modByMonic_lt _ hg) - rw [← hx, map_mk, mk_eq_zero] - constructor - · intro hdvd i - by_contra hne - have h0 : P.map φ ≠ 0 := fun h0 => hne (by rw [← coeff_map, h0, coeff_zero]) - exact (hg.map φ).not_dvd_of_degree_lt h0 hdeg hdvd - · intro h - have : P.map φ = 0 := Polynomial.ext fun i => by rw [coeff_map, h, coeff_zero] - rw [this] - exact dvd_zero _ - -end AdjoinRoot - /-! ### Galois rings -/ /-- The ring `(ℤ / p ^ n)[X] / (f)` presented by an integer polynomial `f`. For a prime `p`, From 5189108242a32270693556cd43044d989591fe1d Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 30 Oct 2026 22:11:30 -0400 Subject: [PATCH 3/3] doc(foundations): scope GaloisRing to the manuscript's base ring O/(2^n) On p. 57 of the pinned manuscript, O = Z_(2)[U]/(f), A = O[V]/(V^l) and A_p = A/(2^p). `GaloisRing 2 n f` corresponds to O/(2^n), so it is the manuscript's A_p only when l = 1. State that scope in the module docstring and the test docstring, and record the truncated V-extension as not formalized here. Addresses the source-scope finding of reviewer-codex-edemaine on #1859. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015DLg8kwPs8yi7ePPdtoNvG --- Complexity/Foundations/RingTheory/GaloisRing.lean | 10 +++++++--- ComplexityTests/Foundations/RingTheory/GaloisRing.lean | 3 ++- 2 files changed, 9 insertions(+), 4 deletions(-) diff --git a/Complexity/Foundations/RingTheory/GaloisRing.lean b/Complexity/Foundations/RingTheory/GaloisRing.lean index 79a1b2965..b9f21502c 100644 --- a/Complexity/Foundations/RingTheory/GaloisRing.lean +++ b/Complexity/Foundations/RingTheory/GaloisRing.lean @@ -28,9 +28,13 @@ The *digit lifts* `∑ i, c i * X ^ i` with digits `c i ∈ {0, …, p - 1}` red distinct residue-field elements, so any two of them differ by a unit, and Lagrange interpolation over the ring holds at any set of them (`GaloisRing.eq_ringInterpolate_digitLift`). -This is the coefficient ring of the Boolean tensor contraction of [OpenAI2026ETH] (§D.4.1, -pp. 57–58), which takes `p = 2`, a degree `e = 4 ⌈log₂ s⌉` and the precision `n`; the manuscript's -binary-coordinate lifts are the digit lifts for `p = 2`. +This is the base coefficient ring of the Boolean tensor contraction of [OpenAI2026ETH] (§D.4.1, +pp. 57–58), with `p = 2`, a degree `e = 4 ⌈log₂ s⌉` and the precision `n`. The manuscript puts +`O = ℤ_(2)[U] / (f)` and `A = O[V] / (V ^ ℓ)`, and computes in `A / (2 ^ n)` (written `A_p` there, +with `p` the precision). `GaloisRing 2 n f` corresponds to `O / (2 ^ n)`, since +`ℤ_(2) / (2 ^ n) ≅ ℤ / 2 ^ n` (that identification is not formalized here). It is therefore the +manuscript's `A / (2 ^ n)` only when `ℓ = 1`; the truncated `V`-extension for general `ℓ` is not +formalized here. The manuscript's binary-coordinate lifts are the digit lifts for `p = 2`. The argument is that of a surjection onto a field with nilpotent kernel (`RingHom.isUnit_iff_ne_zero_of_isNilpotent`): reduction modulo `p` has kernel `(p)`, and diff --git a/ComplexityTests/Foundations/RingTheory/GaloisRing.lean b/ComplexityTests/Foundations/RingTheory/GaloisRing.lean index c11fcc94d..9a4438a77 100644 --- a/ComplexityTests/Foundations/RingTheory/GaloisRing.lean +++ b/ComplexityTests/Foundations/RingTheory/GaloisRing.lean @@ -10,7 +10,8 @@ import Mathlib.Tactic.ComputeDegree import Mathlib.Tactic.FinCases /-! Tests for Galois rings, on `(ℤ / 8)[U] / (U ^ 2 + U + 1)`: the case `p = 2`, `e = 2` and -precision `3` of the coefficient ring of [OpenAI2026ETH], §D.4.1. -/ +precision `3` of the base coefficient ring `O / (2 ^ 3)` of [OpenAI2026ETH], §D.4.1, which is the +manuscript's `A_3` when `ℓ = 1`. -/ namespace ComplexityTests.GaloisRing