Adapted from Charlie Dorsey’s Apache-2.0 Weil Bounds Toolkit for Lean Pool’s module system, Mathlib version, quality requirements and compilation performance.

Trace fibers for the Kloosterman curve

Proves that the map x ↦ x^p-x has the prime field as kernel and the trace-zero hyperplane as image. Each trace-zero fiber has exactly p points. Compare Harcos (2015), equation (3).

noncomputable def KloostermanWeil.Stepanov.artinSchreierLinear (p n : ℕ) [Fact (Nat.Prime p)] : GaloisField p n →ₗ[ZMod p] GaloisField p n

The linear map x ↦ x^p - x on the degree-n finite field.

Equations

• KloostermanWeil.Stepanov.artinSchreierLinear p n = (FiniteField.frobeniusAlgHom (ZMod p) (GaloisField p n)).toLinearMap - LinearMap.id

theorem KloostermanWeil.Stepanov.artinSchreierLinear_apply (p n : ℕ) [Fact (Nat.Prime p)] (x : GaloisField p n) : (artinSchreierLinear p n) x = x ^ p - x

theorem KloostermanWeil.Stepanov.artin_trace_zero (p n : ℕ) [Fact (Nat.Prime p)] (hn : n ≠ 0) (x : GaloisField p n) : (Algebra.trace (ZMod p) (GaloisField p n)) (x ^ p - x) = 0

noncomputable def KloostermanWeil.Stepanov.artinKernelMap (p n : ℕ) [Fact (Nat.Prime p)] : ZMod p →ₗ[ZMod p] ↥(artinSchreierLinear p n).ker

The inclusion of the prime field into the kernel of x ↦ x^p - x.

Equations

• KloostermanWeil.Stepanov.artinKernelMap p n = LinearMap.codRestrict (KloostermanWeil.Stepanov.artinSchreierLinear p n).ker (Algebra.linearMap (ZMod p) (GaloisField p n)) ⋯

theorem KloostermanWeil.Stepanov.artinKernelMap_bijective (p n : ℕ) [Fact (Nat.Prime p)] : Function.Bijective ⇑(artinKernelMap p n)

noncomputable def KloostermanWeil.Stepanov.artinKernelEquiv (p n : ℕ) [Fact (Nat.Prime p)] : ZMod p ≃ₗ[ZMod p] ↥(artinSchreierLinear p n).ker

The prime field is linearly equivalent to the Artin–Schreier kernel.

Equations

• KloostermanWeil.Stepanov.artinKernelEquiv p n = LinearEquiv.ofBijective (KloostermanWeil.Stepanov.artinKernelMap p n) ⋯

theorem KloostermanWeil.Stepanov.finrank_artin_ker (p n : ℕ) [Fact (Nat.Prime p)] : Module.finrank (ZMod p) ↥(artinSchreierLinear p n).ker = 1

theorem KloostermanWeil.Stepanov.artin_range_eq_trace_ker (p n : ℕ) [Fact (Nat.Prime p)] (hn : n ≠ 0) : (artinSchreierLinear p n).range = (Algebra.trace (ZMod p) (GaloisField p n)).ker

@[reducible, inline]

abbrev KloostermanWeil.Stepanov.ArtinSchreierFiber (p n : ℕ) [Fact (Nat.Prime p)] (b : GaloisField p n) : Type

The fiber of the Artin–Schreier linear map over b.

Equations

• KloostermanWeil.Stepanov.ArtinSchreierFiber p n b = { x : GaloisField p n // (KloostermanWeil.Stepanov.artinSchreierLinear p n) x = b }

noncomputable def KloostermanWeil.Stepanov.artinFiberEquivKernel (p n : ℕ) [Fact (Nat.Prime p)] (b x₀ : GaloisField p n) (hx₀ : (artinSchreierLinear p n) x₀ = b) : ↥(artinSchreierLinear p n).ker ≃ ArtinSchreierFiber p n b

Translation by a chosen preimage identifies a fiber with the kernel.

Equations

• One or more equations did not get rendered due to their size.

theorem KloostermanWeil.Stepanov.card_artinSchreierFiber_of_trace_eq_zero (p n : ℕ) [Fact (Nat.Prime p)] (hn : n ≠ 0) (b : GaloisField p n) (hb : (Algebra.trace (ZMod p) (GaloisField p n)) b = 0) : Nat.card (ArtinSchreierFiber p n b) = p