The Chevalley–Warning theorem

This file contains a proof of the Chevalley–Warning theorem. Throughout most of this file, K denotes a finite field and q is notation for the cardinality of K.

Main results

1. Let f be a multivariate polynomial in finitely many variables (X s, s : σ) such that the total degree of f is less than (q-1) times the cardinality of σ. Then the evaluation of f on all points of σ → K (aka K^σ) sums to 0. (sum_eval_eq_zero)
2. The Chevalley–Warning theorem (char_dvd_card_solutions_of_sum_lt). Let f i be a finite family of multivariate polynomials in finitely many variables (X s, s : σ) such 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 the characteristic of K.

Notation

• K is a finite field
• q is notation for the cardinality of K
• σ is the indexing type for the variables of a multivariate polynomial ring over K

theorem MvPolynomial.sum_eval_eq_zero {K : Type u_1} {σ : Type u_2} [Fintype K] [Field K] [Fintype σ] [DecidableEq σ] (f : MvPolynomial σ K) (h : MvPolynomial.totalDegree f < (Fintype.card K - 1) * Fintype.card σ) : (Finset.sum Finset.univ fun (x : σ → K) => (MvPolynomial.eval x) f) = 0

theorem char_dvd_card_solutions_of_sum_lt {K : Type u_1} {σ : Type u_2} {ι : Type u_3} [Fintype K] [Field K] [Fintype σ] [DecidableEq σ] [DecidableEq K] (p : ℕ) [CharP K p] {s : Finset ι} {f : ι → MvPolynomial σ K} (h : (Finset.sum s fun (i : ι) => MvPolynomial.totalDegree (f i)) < Fintype.card σ) : p ∣ Fintype.card { x : σ → K // ∀ i ∈ s, (MvPolynomial.eval x) (f i) = 0 }

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_fintype_sum_lt {K : Type u_1} {σ : Type u_2} {ι : Type u_3} [Fintype K] [Field K] [Fintype σ] [DecidableEq σ] [DecidableEq K] (p : ℕ) [CharP K p] [Fintype ι] {f : ι → MvPolynomial σ K} (h : (Finset.sum Finset.univ fun (i : ι) => MvPolynomial.totalDegree (f i)) < Fintype.card σ) : p ∣ Fintype.card { x : σ → K // ∀ (i : ι), (MvPolynomial.eval x) (f i) = 0 }

The Chevalley–Warning theorem, Fintype 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 {K : Type u_1} {σ : Type u_2} [Fintype K] [Field K] [Fintype σ] [DecidableEq σ] [DecidableEq K] (p : ℕ) [CharP K p] {f : MvPolynomial σ K} (h : MvPolynomial.totalDegree f < Fintype.card σ) : p ∣ Fintype.card { x : σ → K // (MvPolynomial.eval x) f = 0 }

The Chevalley–Warning theorem, unary version. Let f be a multivariate polynomial in finitely many variables (X s, s : σ) over a finite field of characteristic p. Assume that the total degree of f is less than the cardinality of σ. Then the number of solutions of f is divisible by p. See char_dvd_card_solutions_of_sum_lt for a version that takes a family of polynomials f i.

theorem char_dvd_card_solutions_of_add_lt {K : Type u_1} {σ : Type u_2} [Fintype K] [Field K] [Fintype σ] [DecidableEq σ] [DecidableEq K] (p : ℕ) [CharP K p] {f₁ : MvPolynomial σ K} {f₂ : MvPolynomial σ K} (h : MvPolynomial.totalDegree f₁ + MvPolynomial.totalDegree f₂ < Fintype.card σ) : p ∣ Fintype.card { x : σ → K // (MvPolynomial.eval x) f₁ = 0 ∧ (MvPolynomial.eval x) f₂ = 0 }

The Chevalley–Warning theorem, binary version. Let f₁, f₂ be two 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 f₁ and f₂ is less than the cardinality of σ. Then the number of common solutions of the f₁ and f₂ is divisible by p.