Finite Field Basic

In this file we introduce some generally helpful lemmas for the finite field F with q fulfilling IsPrimePow/Prime, Fintype.card F = q and q % 4 = 3.

The assumption IsPrimePow q of [bernstein2013a] never has to be stated: by card_isPrimePow it is a consequence of Fintype.card F = q, so q ranges over exactly the prime powers congruent to 3 modulo 4. Conversely, prime_of_natCast_surjective shows that representing field elements by the naturals 0, 1, …, q - 1, as the string encoding of Section 3.4 does, is possible only when q is prime.

References

See [bernstein2013a] for the original account on this specifc finite field.

theorem Elligator.FiniteFieldBasic.card_isPrimePow {F : Type u_1} [Field F] [Fintype F] {q : ℕ} (hq_card : Fintype.card F = q) : IsPrimePow q

The cardinality of a finite field is always a prime power.

This is why no statement of this development has to assume IsPrimePow q: the hypothesis Fintype.card F = q already forces q to be a prime power, so all results proved for a finite field F with Fintype.card F = q and q % 4 = 3 are exactly the results of [bernstein2013a] for an arbitrary prime power q ≡ 3 (mod 4).

theorem Elligator.FiniteFieldBasic.q_odd {q : ℕ} (hq_mod : q % 4 = 3) : Odd q

theorem Elligator.FiniteFieldBasic.q_sub_one_div_two_odd {q : ℕ} (hq_mod : q % 4 = 3) : Odd ((q - 1) / 2)

theorem Elligator.FiniteFieldBasic.q_sub_one_even {q : ℕ} (hq_mod : q % 4 = 3) : Even (q - 1)

theorem Elligator.FiniteFieldBasic.one_ne_zero {F : Type u_1} [Field F] : 1 ≠ 0

theorem Elligator.FiniteFieldBasic.q_add_one_div_four_ne_zero {q : ℕ} (hq_mod : q % 4 = 3) : (1 + q) / 4 ≠ 0

theorem Elligator.FiniteFieldBasic.q_add_one_div_two_ne_zero {q : ℕ} (hq_mod : q % 4 = 3) : (1 + q) / 2 ≠ 0

theorem Elligator.FiniteFieldBasic.two_ne_zero {F : Type u_1} [Field F] [Fintype F] {q : ℕ} (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) : 2 ≠ 0

theorem Elligator.FiniteFieldBasic.four_ne_zero {F : Type u_1} [Field F] [Fintype F] {q : ℕ} (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) : 4 ≠ 0

theorem Elligator.FiniteFieldBasic.ringChar_ne_two {F : Type u_1} [Field F] [Fintype F] {q : ℕ} (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) : ringChar F ≠ 2

theorem Elligator.FiniteFieldBasic.neg_one_ne_zero {F : Type u_1} [Field F] : -1 ≠ 0

theorem Elligator.FiniteFieldBasic.neg_one_non_square {F : Type u_1} [Field F] [Fintype F] {q : ℕ} (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) : ¬IsSquare (-1)

theorem Elligator.FiniteFieldBasic.false_of_isSquare_neg_one {F : Type u_1} [Field F] [Fintype F] {q : ℕ} (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) (h : IsSquare (-1)) : False

If some algebraic identity would force -1 to be a square, contradiction - -1 is never a square when q % 4 = 3. A common closing step for the r/d nonvanishing proofs.

theorem Elligator.FiniteFieldBasic.one_sub_t_ne_zero {F : Type u_1} [Field F] (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : 1 - ↑t ≠ 0

theorem Elligator.FiniteFieldBasic.one_add_t_ne_zero {F : Type u_1} [Field F] (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : 1 + ↑t ≠ 0

theorem Elligator.FiniteFieldBasic.neg_t_ne_one_and_neg_t_ne_neg_one {F : Type u_1} [Field F] (t : { t : F // t ≠ 1 ∧ t ≠ -1 }) : -↑t ≠ 1 ∧ -↑t ≠ -1

theorem Elligator.FiniteFieldBasic.not_t_ne_one_and_t_ne_neg_one {F : Type u_1} [Field F] (t : { t : F // t = 1 ∨ t = -1 }) : ¬(↑t ≠ 1 ∧ ↑t ≠ -1)

theorem Elligator.FiniteFieldBasic.one_add_q_div_four_mul_two_eq_one_add_q_div_two {q : ℕ} (hq_mod : q % 4 = 3) : (1 + q) / 4 * 2 = (1 + q) / 2

theorem Elligator.FiniteFieldBasic.ringChar_of_F_eq_q {F : Type u_1} [Field F] [Fintype F] {q : ℕ} (hq_card : Fintype.card F = q) (q_prime : Prime q) : ringChar F = q

If F has q elements and q is prime, q is literally the characteristic of F.

theorem Elligator.FiniteFieldBasic.fin_to_finfield_injective {F : Type u_1} [Field F] [Fintype F] {q : ℕ} (hq_card : Fintype.card F = q) (q_prime : Prime q) : Function.Injective fun (n : Fin q) => ↑↑n

The cast Fin q → F is injective

theorem Elligator.FiniteFieldBasic.fin_to_finfield_bijective {F : Type u_1} [Field F] [Fintype F] {q : ℕ} (hq_card : Fintype.card F = q) (q_prime : Prime q) : Function.Bijective fun (n : Fin q) => ↑↑n

theorem Elligator.FiniteFieldBasic.exists_fin_cast_eq {F : Type u_1} [Field F] [Fintype F] {q : ℕ} (hq_card : Fintype.card F = q) (q_prime : Prime q) (t : F) : ∃ (n : Fin q), ↑↑n = t

Every element of F is the cast of some n : Fin q: this cast is injective and Fin q and F have the same cardinality, so it is bijective.

theorem Elligator.FiniteFieldBasic.exists_nat_cast_eq {F : Type u_1} [Field F] [Fintype F] {q : ℕ} (hq_card : Fintype.card F = q) (q_prime : Prime q) (t : F) : ∃ n < q, ↑n = t

theorem Elligator.FiniteFieldBasic.exists_field_card_eq_iff_isPrimePow (q : ℕ) : (∃ (F : Type) (x : Field F) (x : Fintype F), Fintype.card F = q) ↔ IsPrimePow q

A natural number q is the cardinality of some finite field iff it is a prime power.

Together with Elligator.FiniteFieldBasic.card_isPrimePow this says that the standing hypotheses Fintype.card F = q, q % 4 = 3 of this development describe exactly the setting of [bernstein2013a], Section 3.1: an arbitrary prime power q ≡ 3 (mod 4).

theorem Elligator.FiniteFieldBasic.prime_of_natCast_surjective {F : Type u_1} [Field F] [Fintype F] {q : ℕ} (hq_card : Fintype.card F = q) (hsurj : Function.Surjective Nat.cast) : Nat.Prime q

If every element of F is the image of a natural number under the canonical cast, then the cardinality of F is prime, not merely a prime power.

This is the precise reason why the string encoding ι of [bernstein2013a], Section 3.4, is formalized for prime q only: it represents field elements by the naturals 0, 1, ..., q - 1, which requires the natural casts to exhaust F. The ϕ part of the development makes no such assumption and therefore covers all prime powers.