import field_theory.separable

import ring_theory.integral_domain

import tactic.apply_fun

variables {K : Type*} {R : Type*}

local notation `q` := fintype.card K

open finset function

open_locale big_operators polynomial

namespace finite_field

section polynomial

variables [comm_ring R] [is_domain R]

open polynomial

lemma card_image_polynomial_eval [decidable_eq R] [fintype R] {p : R[X]}

(hp : 0 < p.degree) : fintype.card R ≤ nat_degree p * (univ.image (λ x, eval x p)).card :=

finset.card_le_mul_card_image _ _

(λ a _, calc _ = (p - C a).roots.to_finset.card : congr_arg card

(by simp [finset.ext_iff, mem_roots_sub_C hp])

... ≤ (p - C a).roots.card : multiset.to_finset_card_le _

... ≤ _ : card_roots_sub_C' hp)

lemma exists_root_sum_quadratic [fintype R] {f g : R[X]} (hf2 : degree f = 2)

(hg2 : degree g = 2) (hR : fintype.card R % 2 = 1) : ∃ a b, f.eval a + g.eval b = 0 :=

by letI := classical.dec_eq R; exact

suffices ¬ disjoint (univ.image (λ x : R, eval x f)) (univ.image (λ x : R, eval x (-g))),

simp only [disjoint_left, mem_image] at this,

push_neg at this,

rcases this with ⟨x, ⟨a, _, ha⟩, ⟨b, _, hb⟩⟩,

exact ⟨a, b, by rw [ha, ← hb, eval_neg, neg_add_self]⟩

end,

assume hd : disjoint _ _,

lt_irrefl (2 * ((univ.image (λ x : R, eval x f)) ∪ (univ.image (λ x : R, eval x (-g)))).card) $

calc 2 * ((univ.image (λ x : R, eval x f)) ∪ (univ.image (λ x : R, eval x (-g)))).card

≤ 2 * fintype.card R : nat.mul_le_mul_left _ (finset.card_le_univ _)

... = fintype.card R + fintype.card R : two_mul _

... < nat_degree f * (univ.image (λ x : R, eval x f)).card +

nat_degree (-g) * (univ.image (λ x : R, eval x (-g))).card :

add_lt_add_of_lt_of_le

(lt_of_le_of_ne

(card_image_polynomial_eval (by rw hf2; exact dec_trivial))

(mt (congr_arg (%2)) (by simp [nat_degree_eq_of_degree_eq_some hf2, hR])))

(card_image_polynomial_eval (by rw [degree_neg, hg2]; exact dec_trivial))

... = 2 * (univ.image (λ x : R, eval x f) ∪ univ.image (λ x : R, eval x (-g))).card :

by rw [card_disjoint_union hd]; simp [nat_degree_eq_of_degree_eq_some hf2,

nat_degree_eq_of_degree_eq_some hg2, bit0, mul_add]

end polynomial

lemma prod_univ_units_id_eq_neg_one [comm_ring K] [is_domain K] [fintype Kˣ] :

(∏ x : Kˣ, x) = (-1 : Kˣ) :=

classical,

have : (∏ x in (@univ Kˣ _).erase (-1), x) = 1,

from prod_involution (λ x _, x⁻¹) (by simp)

(λ a, by simp [units.inv_eq_self_iff] {contextual := tt})

(λ a, by simp [@inv_eq_iff_eq_inv _ _ a])

(by simp),

rw [← insert_erase (mem_univ (-1 : Kˣ)), prod_insert (not_mem_erase _ _),

this, mul_one]

variables [group_with_zero K] [fintype K]

lemma pow_card_sub_one_eq_one (a : K) (ha : a ≠ 0) : a ^ (q - 1) = 1 :=

calc a ^ (fintype.card K - 1) = (units.mk0 a ha ^ (fintype.card K - 1) : Kˣ) :

by rw [units.coe_pow, units.coe_mk0]

... = 1 : by { classical, rw [← fintype.card_units, pow_card_eq_one], refl }

lemma pow_card (a : K) : a ^ q = a :=

have hp : 0 < fintype.card K := lt_trans zero_lt_one fintype.one_lt_card,

by_cases h : a = 0, { rw h, apply zero_pow hp },

rw [← nat.succ_pred_eq_of_pos hp, pow_succ, nat.pred_eq_sub_one,

pow_card_sub_one_eq_one a h, mul_one],

lemma pow_card_pow (n : ℕ) (a : K) : a ^ q ^ n = a :=

induction n with n ih,

{ simp, },

{ simp [pow_succ, pow_mul, ih, pow_card], },

variables (K) [field K] [fintype K]

theorem card (p : ℕ) [char_p K p] : ∃ (n : ℕ+), nat.prime p ∧ q = p^(n : ℕ) :=

haveI hp : fact p.prime := ⟨char_p.char_is_prime K p⟩,

letI : module (zmod p) K := { .. (zmod.cast_hom dvd_rfl K : zmod p →+* _).to_module },

obtain ⟨n, h⟩ := vector_space.card_fintype (zmod p) K,

rw zmod.card at h,

refine ⟨⟨n, _⟩, hp.1, h⟩,

apply or.resolve_left (nat.eq_zero_or_pos n),

rintro rfl,

rw pow_zero at h,

have : (0 : K) = 1, { apply fintype.card_le_one_iff.mp (le_of_eq h) },

exact absurd this zero_ne_one,

theorem card' : ∃ (p : ℕ) (n : ℕ+), nat.prime p ∧ fintype.card K = p^(n : ℕ) :=

let ⟨p, hc⟩ := char_p.exists K in ⟨p, @finite_field.card K _ _ p hc⟩

@[simp] lemma cast_card_eq_zero : (q : K) = 0 :=

rcases char_p.exists K with ⟨p, _char_p⟩, resetI,

rcases card K p with ⟨n, hp, hn⟩,

simp only [char_p.cast_eq_zero_iff K p, hn],

conv { congr, rw [← pow_one p] },

exact pow_dvd_pow _ n.2,

lemma forall_pow_eq_one_iff (i : ℕ) :

(∀ x : Kˣ, x ^ i = 1) ↔ q - 1 ∣ i :=

classical,

obtain ⟨x, hx⟩ := is_cyclic.exists_generator Kˣ,

rw [←fintype.card_units, ←order_of_eq_card_of_forall_mem_zpowers hx, order_of_dvd_iff_pow_eq_one],

split,

{ intro h, apply h },

{ intros h y,

simp_rw ← mem_powers_iff_mem_zpowers at hx,

rcases hx y with ⟨j, rfl⟩,

rw [← pow_mul, mul_comm, pow_mul, h, one_pow], }

lemma sum_pow_units [fintype Kˣ] (i : ℕ) :

∑ x : Kˣ, (x ^ i : K) = if (q - 1) ∣ i then -1 else 0 :=

let φ : Kˣ →* K :=

{ to_fun := λ x, x ^ i,

map_one' := by rw [units.coe_one, one_pow],

map_mul' := by { intros, rw [units.coe_mul, mul_pow] } },

haveI : decidable (φ = 1), { classical, apply_instance },

calc ∑ x : Kˣ, φ x = if φ = 1 then fintype.card Kˣ else 0 : sum_hom_units φ

... = if (q - 1) ∣ i then -1 else 0 : _,

suffices : (q - 1) ∣ i ↔ φ = 1,

{ simp only [this],

split_ifs with h h, swap, refl,

rw [fintype.card_units, nat.cast_sub, cast_card_eq_zero, nat.cast_one, zero_sub],

show 1 ≤ q, from fintype.card_pos_iff.mpr ⟨0⟩ },

rw [← forall_pow_eq_one_iff, monoid_hom.ext_iff],

apply forall_congr, intro x,

rw [units.ext_iff, units.coe_pow, units.coe_one, monoid_hom.one_apply],

refl,

lemma sum_pow_lt_card_sub_one (i : ℕ) (h : i < q - 1) :

∑ x : K, x ^ i = 0 :=

by_cases hi : i = 0,

{ simp only [hi, nsmul_one, sum_const, pow_zero, card_univ, cast_card_eq_zero], },

classical,

have hiq : ¬ (q - 1) ∣ i, { contrapose! h, exact nat.le_of_dvd (nat.pos_of_ne_zero hi) h },

let φ : Kˣ ↪ K := ⟨coe, units.ext⟩,

have : univ.map φ = univ \ {0},

{ ext x,

simp only [true_and, embedding.coe_fn_mk, mem_sdiff, units.exists_iff_ne_zero,

mem_univ, mem_map, exists_prop_of_true, mem_singleton] },

calc ∑ x : K, x ^ i = ∑ x in univ \ {(0 : K)}, x ^ i :

by rw [← sum_sdiff ({0} : finset K).subset_univ, sum_singleton,

zero_pow (nat.pos_of_ne_zero hi), add_zero]

... = ∑ x : Kˣ, x ^ i : by { rw [← this, univ.sum_map φ], refl }

... = 0 : by { rw [sum_pow_units K i, if_neg], exact hiq, }

open polynomial

variables (K' : Type*) [field K'] {p n : ℕ}

lemma X_pow_card_sub_X_nat_degree_eq (hp : 1 < p) :

(X ^ p - X : K'[X]).nat_degree = p :=

have h1 : (X : K'[X]).degree < (X ^ p : K'[X]).degree,

{ rw [degree_X_pow, degree_X],

exact_mod_cast hp },

rw [nat_degree_eq_of_degree_eq (degree_sub_eq_left_of_degree_lt h1), nat_degree_X_pow],

lemma X_pow_card_pow_sub_X_nat_degree_eq (hn : n ≠ 0) (hp : 1 < p) :

(X ^ p ^ n - X : K'[X]).nat_degree = p ^ n :=

X_pow_card_sub_X_nat_degree_eq K' $ nat.one_lt_pow _ _ (nat.pos_of_ne_zero hn) hp

lemma X_pow_card_sub_X_ne_zero (hp : 1 < p) : (X ^ p - X : K'[X]) ≠ 0 :=

ne_zero_of_nat_degree_gt $

calc 1 < _ : hp

... = _ : (X_pow_card_sub_X_nat_degree_eq K' hp).symm

lemma X_pow_card_pow_sub_X_ne_zero (hn : n ≠ 0) (hp : 1 < p) :

(X ^ p ^ n - X : K'[X]) ≠ 0 :=

X_pow_card_sub_X_ne_zero K' $ nat.one_lt_pow _ _ (nat.pos_of_ne_zero hn) hp

variables (p : ℕ) [fact p.prime] [algebra (zmod p) K]

lemma roots_X_pow_card_sub_X : roots (X^q - X : K[X]) = finset.univ.val :=

classical,

have aux : (X^q - X : K[X]) ≠ 0 := X_pow_card_sub_X_ne_zero K fintype.one_lt_card,

have : (roots (X^q - X : K[X])).to_finset = finset.univ,

{ rw eq_univ_iff_forall,

intro x,

rw [multiset.mem_to_finset, mem_roots aux, is_root.def, eval_sub, eval_pow, eval_X, sub_eq_zero,

pow_card] },

rw [←this, multiset.to_finset_val, eq_comm, multiset.dedup_eq_self],

apply nodup_roots,

rw separable_def,

convert is_coprime_one_right.neg_right using 1,

{ rw [derivative_sub, derivative_X, derivative_X_pow, char_p.cast_card_eq_zero K, C_0, zero_mul,

zero_sub] },

end

variables {K}

theorem frobenius_pow {p : ℕ} [fact p.prime] [char_p K p] {n : ℕ} (hcard : q = p^n) :

(frobenius K p) ^ n = 1 :=

ext, conv_rhs { rw [ring_hom.one_def, ring_hom.id_apply, ← pow_card x, hcard], }, clear hcard,

induction n, {simp},

rw [pow_succ, pow_succ', pow_mul, ring_hom.mul_def, ring_hom.comp_apply, frobenius_def, n_ih]

open polynomial

lemma expand_card (f : K[X]) :

expand K q f = f ^ q :=

cases char_p.exists K with p hp,

letI := hp,

rcases finite_field.card K p with ⟨⟨n, npos⟩, ⟨hp, hn⟩⟩,

haveI : fact p.prime := ⟨hp⟩,

dsimp at hn,

rw [hn, ← map_expand_pow_char, frobenius_pow hn, ring_hom.one_def, map_id]

end finite_field

namespace zmod

open finite_field polynomial

lemma sq_add_sq (p : ℕ) [hp : fact p.prime] (x : zmod p) :

∃ a b : zmod p, a^2 + b^2 = x :=

cases hp.1.eq_two_or_odd with hp2 hp_odd,

{ substI p, change fin 2 at x, fin_cases x, { use 0, simp }, { use [0, 1], simp } },

let f : (zmod p)[X] := X^2,

let g : (zmod p)[X] := X^2 - C x,

obtain ⟨a, b, hab⟩ : ∃ a b, f.eval a + g.eval b = 0 :=

@exists_root_sum_quadratic _ _ _ _ f g

(degree_X_pow 2) (degree_X_pow_sub_C dec_trivial _) (by rw [zmod.card, hp_odd]),

refine ⟨a, b, _⟩,

rw ← sub_eq_zero,

simpa only [eval_C, eval_X, eval_pow, eval_sub, ← add_sub_assoc] using hab,

end zmod

namespace char_p

lemma sq_add_sq (R : Type*) [comm_ring R] [is_domain R]

(p : ℕ) [ne_zero p] [char_p R p] (x : ℤ) :

∃ a b : ℕ, (a^2 + b^2 : R) = x :=

haveI := char_is_prime_of_pos R p,

obtain ⟨a, b, hab⟩ := zmod.sq_add_sq p x,

refine ⟨a.val, b.val, _⟩,

simpa using congr_arg (zmod.cast_hom dvd_rfl R) hab

end char_p

open_locale nat

open zmod

@[simp] lemma zmod.pow_totient {n : ℕ} (x : (zmod n)ˣ) : x ^ φ n = 1 :=

cases n,

{ rw [nat.totient_zero, pow_zero] },

{ rw [← card_units_eq_totient, pow_card_eq_one] }

lemma nat.modeq.pow_totient {x n : ℕ} (h : nat.coprime x n) : x ^ φ n ≡ 1 [MOD n] :=

rw ← zmod.eq_iff_modeq_nat,

let x' : units (zmod n) := zmod.unit_of_coprime _ h,

have := zmod.pow_totient x',

apply_fun (coe : units (zmod n) → zmod n) at this,

simpa only [-zmod.pow_totient, nat.succ_eq_add_one, nat.cast_pow, units.coe_one,

nat.cast_one, coe_unit_of_coprime, units.coe_pow],

variables {V : Type*} [fintype K] [division_ring K] [add_comm_group V] [module K V]

lemma card_eq_pow_finrank [fintype V] :

fintype.card V = q ^ (finite_dimensional.finrank K V) :=

let b := is_noetherian.finset_basis K V,

rw [module.card_fintype b, ← finite_dimensional.finrank_eq_card_basis b],

open finite_field

namespace zmod

@[simp] lemma pow_card {p : ℕ} [fact p.prime] (x : zmod p) : x ^ p = x :=

by { have h := finite_field.pow_card x, rwa zmod.card p at h }

@[simp] lemma pow_card_pow {n p : ℕ} [fact p.prime] (x : zmod p) : x ^ p ^ n = x :=

induction n with n ih,

{ simp, },

{ simp [pow_succ, pow_mul, ih, pow_card], },

@[simp] lemma frobenius_zmod (p : ℕ) [fact p.prime] :

frobenius (zmod p) p = ring_hom.id _ :=

by { ext a, rw [frobenius_def, zmod.pow_card, ring_hom.id_apply] }

@[simp] lemma card_units (p : ℕ) [fact p.prime] : fintype.card ((zmod p)ˣ) = p - 1 :=

by rw [fintype.card_units, card]

theorem units_pow_card_sub_one_eq_one (p : ℕ) [fact p.prime] (a : (zmod p)ˣ) :

a ^ (p - 1) = 1 :=

by rw [← card_units p, pow_card_eq_one]

theorem pow_card_sub_one_eq_one {p : ℕ} [fact p.prime] {a : zmod p} (ha : a ≠ 0) :

a ^ (p - 1) = 1 :=

by { have h := pow_card_sub_one_eq_one a ha, rwa zmod.card p at h }

theorem order_of_units_dvd_card_sub_one {p : ℕ} [fact p.prime] (u : (zmod p)ˣ) :

order_of u ∣ p - 1 :=

order_of_dvd_of_pow_eq_one $ units_pow_card_sub_one_eq_one _ _

theorem order_of_dvd_card_sub_one {p : ℕ} [fact p.prime] {a : zmod p} (ha : a ≠ 0) :

order_of a ∣ p - 1 :=

order_of_dvd_of_pow_eq_one $ pow_card_sub_one_eq_one ha

open polynomial

lemma expand_card {p : ℕ} [fact p.prime] (f : polynomial (zmod p)) :

expand (zmod p) p f = f ^ p :=

by { have h := finite_field.expand_card f, rwa zmod.card p at h }

end zmod

lemma int.modeq.pow_card_sub_one_eq_one {p : ℕ} (hp : nat.prime p) {n : ℤ} (hpn : is_coprime n p) :

n ^ (p - 1) ≡ 1 [ZMOD p] :=

haveI : fact p.prime := ⟨hp⟩,

have : ¬ (n : zmod p) = 0,

{ rw [char_p.int_cast_eq_zero_iff _ p, ← (nat.prime_iff_prime_int.mp hp).coprime_iff_not_dvd],

{ exact hpn.symm },

exact zmod.char_p p },

simpa [← zmod.int_coe_eq_int_coe_iff] using zmod.pow_card_sub_one_eq_one this

namespace finite_field

variables {F : Type*} [field F]

section finite

variables [finite F]

lemma is_square_of_char_two (hF : ring_char F = 2) (a : F) : is_square a :=

haveI hF' : char_p F 2 := ring_char.of_eq hF,

exact is_square_of_char_two' a,

lemma exists_nonsquare (hF : ring_char F ≠ 2) : ∃ (a : F), ¬ is_square a :=

-- Idea: the squaring map on `F` is not injective, hence not surjective

let sq : F → F := λ x, x ^ 2,

have h : ¬ injective sq,

{ simp only [injective, not_forall, exists_prop],

refine ⟨-1, 1, _, ring.neg_one_ne_one_of_char_ne_two hF⟩,

simp only [sq, one_pow, neg_one_sq] },

rw finite.injective_iff_surjective at h, -- sq not surjective

simp_rw [is_square, ←pow_two, @eq_comm _ _ (_ ^ 2)],

push_neg at ⊢ h,

exact h,

end finite

variables [fintype F]

lemma even_card_iff_char_two : ring_char F = 2 ↔ fintype.card F % 2 = 0 :=

rcases finite_field.card F (ring_char F) with ⟨n, hp, h⟩,

rw [h, nat.pow_mod],

split,

{ intro hF,

rw hF,

simp only [nat.bit0_mod_two, zero_pow', ne.def, pnat.ne_zero, not_false_iff, nat.zero_mod], },

{ rw [← nat.even_iff, nat.even_pow],

rintros ⟨hev, hnz⟩,

rw [nat.even_iff, nat.mod_mod] at hev,

exact (nat.prime.eq_two_or_odd hp).resolve_right (ne_of_eq_of_ne hev zero_ne_one), },

lemma even_card_of_char_two (hF : ring_char F = 2) : fintype.card F % 2 = 0 :=

even_card_iff_char_two.mp hF

lemma odd_card_of_char_ne_two (hF : ring_char F ≠ 2) : fintype.card F % 2 = 1 :=

nat.mod_two_ne_zero.mp (mt even_card_iff_char_two.mpr hF)

lemma pow_dichotomy (hF : ring_char F ≠ 2) {a : F} (ha : a ≠ 0) :

a ^ (fintype.card F / 2) = 1 ∨ a ^ (fintype.card F / 2) = -1 :=

have h₁ := finite_field.pow_card_sub_one_eq_one a ha,

rw [← nat.two_mul_odd_div_two (finite_field.odd_card_of_char_ne_two hF),

mul_comm, pow_mul, pow_two] at h₁,

exact mul_self_eq_one_iff.mp h₁,

lemma unit_is_square_iff (hF : ring_char F ≠ 2) (a : Fˣ) :

is_square a ↔ a ^ (fintype.card F / 2) = 1 :=

classical,

obtain ⟨g, hg⟩ := is_cyclic.exists_generator Fˣ,

obtain ⟨n, hn⟩ : a ∈ submonoid.powers g, { rw mem_powers_iff_mem_zpowers, apply hg },

have hodd := nat.two_mul_odd_div_two (finite_field.odd_card_of_char_ne_two hF),

split,

{ rintro ⟨y, rfl⟩,

rw [← pow_two, ← pow_mul, hodd],

apply_fun (@coe Fˣ F _) using units.ext,

{ push_cast,

exact finite_field.pow_card_sub_one_eq_one (y : F) (units.ne_zero y), }, },

{ subst a, assume h,

have key : 2 * (fintype.card F / 2) ∣ n * (fintype.card F / 2),

{ rw [← pow_mul] at h,

rw [hodd, ← fintype.card_units, ← order_of_eq_card_of_forall_mem_zpowers hg],

apply order_of_dvd_of_pow_eq_one h },

have : 0 < fintype.card F / 2 := nat.div_pos fintype.one_lt_card (by norm_num),

obtain ⟨m, rfl⟩ := nat.dvd_of_mul_dvd_mul_right this key,

refine ⟨g ^ m, _⟩,

rw [mul_comm, pow_mul, pow_two], },

lemma is_square_iff (hF : ring_char F ≠ 2) {a : F} (ha : a ≠ 0) :

is_square a ↔ a ^ (fintype.card F / 2) = 1 :=

apply (iff_congr _ (by simp [units.ext_iff])).mp

(finite_field.unit_is_square_iff hF (units.mk0 a ha)),

simp only [is_square, units.ext_iff, units.coe_mk0, units.coe_mul],

split,

{ rintro ⟨y, hy⟩, exact ⟨y, hy⟩ },

{ rintro ⟨y, rfl⟩,

have hy : y ≠ 0, { rintro rfl, simpa [zero_pow] using ha, },

refine ⟨units.mk0 y hy, _⟩, simp, }

end finite_field