English
A single multivariate polynomial with total degree less than the number of variables has a number of zeros divisible by p in a finite field of characteristic p.
Русский
Один многочлен при характеристике p имеет число нулей делимое на p.
LaTeX
$$$p \\mid \\left|\\{x : \\sigma \\to K \\mid f(x)=0\\}\\right|$ under the degree bound.$$
Lean4
/-- The **Chevalley–Warning theorem**, finitary version.
Let `(f i)` be a finite family of multivariate polynomials
in finitely many variables (`X s`, `s : σ`) over a finite field of characteristic `p`.
Assume that the sum of the total degrees of the `f i` is less than the cardinality of `σ`.
Then the number of common solutions of the `f i` is divisible by `p`. -/
theorem char_dvd_card_solutions_of_sum_lt {s : Finset ι} {f : ι → MvPolynomial σ K}
(h : (∑ i ∈ s, (f i).totalDegree) < Fintype.card σ) : p ∣ Fintype.card { x : σ → K // ∀ i ∈ s, eval x (f i) = 0 } :=
by
have hq : 0 < q - 1 := by rw [← Fintype.card_units, Fintype.card_pos_iff]; exact ⟨1⟩
let S : Finset (σ → K) := {x | ∀ i ∈ s, eval x (f i) = 0}
have hS (x : σ → K) : x ∈ S ↔ ∀ i ∈ s, eval x (f i) = 0 := by
simp [S]
/- The polynomial `F = ∏ i ∈ s, (1 - (f i)^(q - 1))` has the nice property
that it takes the value `1` on elements of `{x : σ → K // ∀ i ∈ s, (f i).eval x = 0}`
while it is `0` outside that locus.
Hence the sum of its values is equal to the cardinality of
`{x : σ → K // ∀ i ∈ s, (f i).eval x = 0}` modulo `p`. -/
let F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))
have hF : ∀ x, eval x F = if x ∈ S then 1 else 0 := by
intro x
calc
eval x F = ∏ i ∈ s, eval x (1 - f i ^ (q - 1)) := eval_prod s _ x
_ = if x ∈ S then 1 else 0 := ?_
simp only [(eval x).map_sub, (eval x).map_pow, (eval x).map_one]
split_ifs with hx
· apply Finset.prod_eq_one
intro i hi
rw [hS] at hx
rw [hx i hi, zero_pow hq.ne', sub_zero]
· obtain ⟨i, hi, hx⟩ : ∃ i ∈ s, eval x (f i) ≠ 0 := by simpa [hS, not_forall, Classical.not_imp] using hx
apply Finset.prod_eq_zero hi
rw [pow_card_sub_one_eq_one (eval x (f i)) hx, sub_self]
-- In particular, we can now show:
have key : ∑ x, eval x F = Fintype.card { x : σ → K // ∀ i ∈ s, eval x (f i) = 0 } := by
rw [Fintype.card_of_subtype S hS, card_eq_sum_ones, Nat.cast_sum, Nat.cast_one, ← Fintype.sum_extend_by_zero S,
sum_congr rfl fun x _ => hF x]
-- With these preparations under our belt, we will approach the main goal.
change p ∣ Fintype.card { x // ∀ i : ι, i ∈ s → eval x (f i) = 0 }
rw [← CharP.cast_eq_zero_iff K, ← key]
change
(∑ x, eval x F) =
0
-- We are now ready to apply the main machine, proven before.
apply F.sum_eval_eq_zero
show F.totalDegree < (q - 1) * Fintype.card σ
calc
F.totalDegree ≤ ∑ i ∈ s, (1 - f i ^ (q - 1)).totalDegree := totalDegree_finset_prod s _
_ ≤ ∑ i ∈ s, (q - 1) * (f i).totalDegree := (sum_le_sum fun i _ => ?_)
_ = (q - 1) * ∑ i ∈ s, (f i).totalDegree := (mul_sum ..).symm
_ < (q - 1) * Fintype.card σ := by
gcongr
-- Now we prove the remaining step from the preceding calculation
change (1 - f i ^ (q - 1)).totalDegree ≤ (q - 1) * (f i).totalDegree
calc
(1 - f i ^ (q - 1)).totalDegree ≤ max (1 : MvPolynomial σ K).totalDegree (f i ^ (q - 1)).totalDegree :=
totalDegree_sub _ _
_ ≤ (f i ^ (q - 1)).totalDegree := by simp
_ ≤ (q - 1) * (f i).totalDegree := totalDegree_pow _ _
