Harcos's trace-zero count

The last six counting lines of Corollary 3 on Harcos, page 8 (pages/harcos-stepanov-08.png), use the actual field trace and the change of variables y = 2at - (x^p - x).

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosArtinSchreier (K : Type u_1) (L : Type u_2) [Field K] [Fintype K] [Field L] [Algebra K L] : L →ₗ[K] L

The relative Artin--Schreier linear map for finite fields.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosArtinSchreier K L = (FiniteField.frobeniusAlgHom K L).toLinearMap - LinearMap.id

@[simp]

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosArtinSchreier_apply (K : Type u_1) (L : Type u_2) [Field K] [Fintype K] [Field L] [Algebra K L] (x : L) : (harcosArtinSchreier K L) x = x ^ Fintype.card K - x

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcos_trace_pow_card (K : Type u_1) (L : Type u_2) [Field K] [Fintype K] [Field L] [Fintype L] [Algebra K L] (x : L) : (Algebra.trace K L) (x ^ Fintype.card K) = (Algebra.trace K L) x

Frobenius invariance of the actual algebra trace.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcos_trace_artinSchreier (K : Type u_1) (L : Type u_2) [Field K] [Fintype K] [Field L] [Fintype L] [Algebra K L] (x : L) : (Algebra.trace K L) ((harcosArtinSchreier K L) x) = 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcos_pow_card_eq_self_iff (K : Type u_1) (L : Type u_2) [Field K] [Fintype K] [Field L] [Algebra K L] (x : L) : x ^ Fintype.card K = x ↔ ∃ (c : K), (algebraMap K L) c = x

The fixed points of the relative Frobenius are exactly the embedded base field.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcos_artinSchreier_ker (K : Type u_1) (L : Type u_2) [Field K] [Fintype K] [Field L] [Algebra K L] : (harcosArtinSchreier K L).ker = (Algebra.linearMap K L).range

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcos_artinSchreier_ker_finrank (K : Type u_1) (L : Type u_2) [Field K] [Fintype K] [Field L] [Algebra K L] : Module.finrank K ↥(harcosArtinSchreier K L).ker = 1

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcos_artinSchreier_range (K : Type u_1) (L : Type u_2) [Field K] [Fintype K] [Field L] [Fintype L] [Algebra K L] : (harcosArtinSchreier K L).range = (Algebra.trace K L).ker

Rank-nullity and nondegeneracy of the trace give additive Hilbert 90 here, without assuming any trace-zero solvability statement.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcos_artinSchreier_exists_iff (K : Type u_1) (L : Type u_2) [Field K] [Fintype K] [Field L] [Fintype L] [Algebra K L] (c : L) : (∃ (x : L), x ^ Fintype.card K - x = c) ↔ (Algebra.trace K L) c = 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcos_artinSchreier_fiber_card (K : Type u_1) (L : Type u_2) [Field K] [Fintype K] [Field L] [Fintype L] [Algebra K L] [DecidableEq L] [DecidableEq K] (c : L) : {x : L | x ^ Fintype.card K - x = c}.card = if (Algebra.trace K L) c = 0 then Fintype.card K else 0

Every nonempty Artin--Schreier fiber has exactly #K elements; the empty fibers are exactly those with nonzero field trace.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcos_artinSchreier_eq_iff_quadratic {F : Type u_1} [Field F] (s a b t : F) (ht : t ≠ 0) : s = a * t + b / t ↔ a * t ^ 2 - s * t + b = 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcos_square_iff_quadratic {F : Type u_1} [Field F] (htwo : 2 ≠ 0) (s a b t : F) (ha : a ≠ 0) : (2 * a * t - s) ^ 2 = s ^ 2 - 4 * a * b ↔ a * t ^ 2 - s * t + b = 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcos_quadratic_parameter_nonzero {F : Type u_1} [Field F] (s a b t : F) (hb : b ≠ 0) (h : a * t ^ 2 - s * t + b = 0) : t ≠ 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcos_curve_parameter_inverse {F : Type u_1} [Field F] (htwo : 2 ≠ 0) (s a y : F) (ha : a ≠ 0) : 2 * a * ((y + s) / (2 * a)) - s = y

The explicit inverse substitution t = (y+s)/(2a).

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosCurveArtinSchreierEquiv {F : Type u_1} [Field F] (p : ℕ) (htwo : 2 ≠ 0) (a b : F) (ha : a ≠ 0) (hb : b ≠ 0) : { xt : F × Fˣ // xt.1 ^ p - xt.1 = a * ↑xt.2 + b / ↑xt.2 } ≃ { xy : F × F // xy.2 ^ 2 = (xy.1 ^ p - xy.1) ^ 2 - 4 * a * b }

Harcos's change of variables, with nonzero t represented by a unit. Its forward map is exactly (x,t) ↦ (x,2at-(x^p-x)); the surjectivity proof constructs the inverse parameter (y+(x^p-x))/(2a).

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosCurveArtinSchreierEquiv p htwo a b ha hb = Equiv.ofBijective (fun (xt : { xt : F × Fˣ // xt.1 ^ p - xt.1 = a * ↑xt.2 + b / ↑xt.2 }) => ⟨((↑xt).1, 2 * a * ↑(↑xt).2 - ((↑xt).1 ^ p - (↑xt).1)), ⋯⟩) ⋯

@[simp]

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosCurveArtinSchreierEquiv_apply {F : Type u_1} [Field F] (p : ℕ) (htwo : 2 ≠ 0) (a b : F) (ha : a ≠ 0) (hb : b ≠ 0) (xt : { xt : F × Fˣ // xt.1 ^ p - xt.1 = a * ↑xt.2 + b / ↑xt.2 }) : ↑((harcosCurveArtinSchreierEquiv p htwo a b ha hb) xt) = ((↑xt).1, 2 * a * ↑(↑xt).2 - ((↑xt).1 ^ p - (↑xt).1))

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosCurveArtinSchreierEquiv_symm_apply {F : Type u_1} [Field F] (p : ℕ) (htwo : 2 ≠ 0) (a b : F) (ha : a ≠ 0) (hb : b ≠ 0) (xy : { xy : F × F // xy.2 ^ 2 = (xy.1 ^ p - xy.1) ^ 2 - 4 * a * b }) : (↑((harcosCurveArtinSchreierEquiv p htwo a b ha hb).symm xy)).1 = (↑xy).1 ∧ ↑(↑((harcosCurveArtinSchreierEquiv p htwo a b ha hb).symm xy)).2 = ((↑xy).2 + ((↑xy).1 ^ p - (↑xy).1)) / (2 * a)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosCurvePointCount_eq_artinSchreier_pairCount {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (p : ℕ) (htwo : 2 ≠ 0) (a b : F) (ha : a ≠ 0) (hb : b ≠ 0) : harcosCurvePointCount p a b = {xt : F × Fˣ | xt.1 ^ p - xt.1 = a * ↑xt.2 + b / ↑xt.2}.card

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosCurvePointCount_eq_card_mul_traceZero {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (K : Type u_2) [Field K] [Fintype K] [DecidableEq K] [Algebra K F] (htwo : 2 ≠ 0) (a b : F) (ha : a ≠ 0) (hb : b ≠ 0) : harcosCurvePointCount (Fintype.card K) a b = Fintype.card K * {t : Fˣ | (Algebra.trace K F) (a * ↑t + b / ↑t) = 0}.card

The relative finite-field version of Harcos's trace-zero counting identity.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcos_artinSchreier_prime_fiber_card {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (p : ℕ) [Fact (Nat.Prime p)] [Algebra (ZMod p) F] (c : F) : {x : F | x ^ p - x = c}.card = if (Algebra.trace (ZMod p) F) c = 0 then p else 0

Artin--Schreier fibers over the prime field have size p precisely at trace-zero elements. This uses Algebra.trace, not a fiber-count surrogate.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.harcosCurvePointCount_eq_prime_mul_traceZero {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (p : ℕ) [Fact (Nat.Prime p)] [CharP F p] [Algebra (ZMod p) F] (hp2 : p ≠ 2) (a b : F) (ha : a ≠ 0) (hb : b ≠ 0) : harcosCurvePointCount p a b = p * {t : Fˣ | (Algebra.trace (ZMod p) F) (a * ↑t + b * (↑t)⁻¹) = 0}.card

The last six counting lines of Harcos, Corollary 3, page 8.