feat: Dual basis of power basis wrt trace form (#8835)

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

Mathlib.lean

@@ -2059,6 +2059,7 @@ import Mathlib.FieldTheory.Laurent
 import Mathlib.FieldTheory.Minpoly.Basic
 import Mathlib.FieldTheory.Minpoly.Field
 import Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
+import Mathlib.FieldTheory.Minpoly.MinpolyDiv
 import Mathlib.FieldTheory.MvPolynomial
 import Mathlib.FieldTheory.Normal
 import Mathlib.FieldTheory.NormalClosure

Mathlib/Data/Polynomial/RingDivision.lean

@@ -1263,6 +1263,31 @@ theorem eq_of_monic_of_dvd_of_natDegree_le {R} [CommRing R] {p q : R[X]} (hp : p
   rw [hq.leadingCoeff, C_1, one_mul]
 #align polynomial.eq_of_monic_of_dvd_of_nat_degree_le Polynomial.eq_of_monic_of_dvd_of_natDegree_le
 
+lemma eq_zero_of_natDegree_lt_card_of_eval_eq_zero {R} [CommRing R] [IsDomain R]
+    (p : R[X]) {ι} [Fintype ι] {f : ι → R} (hf : Function.Injective f)
+    (heval : ∀ i, p.eval (f i) = 0) (hcard : natDegree p < Fintype.card ι) : p = 0 := by
+  classical
+  by_contra hp
+  apply not_lt_of_le (le_refl (Finset.card p.roots.toFinset))
+  calc
+    Finset.card p.roots.toFinset ≤ Multiset.card p.roots := Multiset.toFinset_card_le _
+    _ ≤ natDegree p := Polynomial.card_roots' p
+    _ < Fintype.card ι := hcard
+    _ = Fintype.card (Set.range f) := (Set.card_range_of_injective hf).symm
+    _ = Finset.card (Finset.univ.image f) := by rw [← Set.toFinset_card, Set.toFinset_range]
+    _ ≤ Finset.card p.roots.toFinset := Finset.card_mono ?_
+  intro _
+  simp only [Finset.mem_image, Finset.mem_univ, true_and, Multiset.mem_toFinset, mem_roots', ne_eq,
+    IsRoot.def, forall_exists_index, hp, not_false_eq_true]
+  rintro x rfl
+  exact heval _
+
+lemma eq_zero_of_natDegree_lt_card_of_eval_eq_zero' {R} [CommRing R] [IsDomain R]
+    (p : R[X]) (s : Finset R) (heval : ∀ i ∈ s, p.eval i = 0) (hcard : natDegree p < s.card) :
+    p = 0 :=
+  eq_zero_of_natDegree_lt_card_of_eval_eq_zero p Subtype.val_injective
+    (fun i : s ↦ heval i i.prop) (hcard.trans_eq (Fintype.card_coe s).symm)
+
 theorem isCoprime_X_sub_C_of_isUnit_sub {R} [CommRing R] {a b : R} (h : IsUnit (a - b)) :
     IsCoprime (X - C a) (X - C b) :=
   ⟨-C h.unit⁻¹.val, C h.unit⁻¹.val, by

Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean

@@ -0,0 +1,214 @@
+/-
+Copyright (c) 2023 Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+-/
+import Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
+import Mathlib.FieldTheory.PrimitiveElement
+import Mathlib.FieldTheory.IsAlgClosed.Basic
+
+/-!
+# Results about `minpoly R x / (X - C x)`
+
+## Main definition
+- `minpolyDiv`: The polynomial `minpoly R x / (X - C x)`.
+
+We used the contents of this file to describe the dual basis of a powerbasis under the trace form.
+See `traceForm_dualBasis_powerBasis_eq`.
+
+## Main results
+- `span_coeff_minpolyDiv`: The coefficients of `minpolyDiv` spans `R<x>`.
+-/
+
+open Polynomial BigOperators FiniteDimensional
+
+variable (R K) {L S} [CommRing R] [Field K] [Field L] [CommRing S] [Algebra R S] [Algebra K L]
+variable (x : S)
+
+/-- `minpolyDiv R x : S[X]` for `x : S` is the polynomial `minpoly R x / (X - C x)`. -/
+noncomputable def minpolyDiv : S[X] := (minpoly R x).map (algebraMap R S) /ₘ (X - C x)
+
+lemma minpolyDiv_spec :
+    minpolyDiv R x * (X - C x) = (minpoly R x).map (algebraMap R S) := by
+  delta minpolyDiv
+  rw [mul_comm, mul_divByMonic_eq_iff_isRoot, IsRoot, eval_map, ← aeval_def, minpoly.aeval]
+
+lemma coeff_minpolyDiv (i) : coeff (minpolyDiv R x) i =
+    algebraMap R S (coeff (minpoly R x) (i + 1)) + coeff (minpolyDiv R x) (i + 1) * x := by
+  rw [← coeff_map, ← minpolyDiv_spec R x]; simp [mul_sub]
+
+variable (hx : IsIntegral R x) {R x}
+
+lemma minpolyDiv_ne_zero [Nontrivial S] : minpolyDiv R x ≠ 0 := by
+  intro e
+  have := minpolyDiv_spec R x
+  rw [e, zero_mul] at this
+  exact ((minpoly.monic hx).map (algebraMap R S)).ne_zero this.symm
+
+lemma minpolyDiv_eq_zero (hx : ¬IsIntegral R x) : minpolyDiv R x = 0 := by
+  delta minpolyDiv minpoly
+  rw [dif_neg hx, Polynomial.map_zero, zero_divByMonic]
+
+lemma minpolyDiv_monic : Monic (minpolyDiv R x) := by
+  nontriviality S
+  have := congr_arg leadingCoeff (minpolyDiv_spec R x)
+  rw [leadingCoeff_mul', ((minpoly.monic hx).map (algebraMap R S)).leadingCoeff] at this
+  · simpa using this
+  · simpa using minpolyDiv_ne_zero hx
+
+lemma eval_minpolyDiv_self : (minpolyDiv R x).eval x = aeval x (derivative <| minpoly R x) := by
+  rw [aeval_def, ← eval_map, ← derivative_map, ← minpolyDiv_spec R x]; simp
+
+lemma minpolyDiv_eval_eq_zero_of_ne_of_aeval_eq_zero [IsDomain S]
+    {y} (hxy : y ≠ x) (hy : aeval y (minpoly R x) = 0) : (minpolyDiv R x).eval y = 0 := by
+  rw [aeval_def, ← eval_map, ← minpolyDiv_spec R x] at hy
+  simp only [eval_mul, eval_sub, eval_X, eval_C, mul_eq_zero] at hy
+  exact hy.resolve_right (by rwa [sub_eq_zero])
+
+lemma eval₂_minpolyDiv_of_eval₂_eq_zero {T} [CommRing T]
+    [IsDomain T] [DecidableEq T] {x y}
+    (σ : S →+* T) (hy : eval₂ (σ.comp (algebraMap R S)) y (minpoly R x) = 0) :
+    eval₂ σ y (minpolyDiv R x) =
+      if σ x = y then σ (aeval x (derivative <| minpoly R x)) else 0 := by
+  split_ifs with h
+  · rw [← h, eval₂_hom, eval_minpolyDiv_self]
+  · rw [← eval₂_map, ← minpolyDiv_spec] at hy
+    simpa [sub_eq_zero, Ne.symm h] using hy
+
+lemma eval₂_minpolyDiv_self {T} [CommRing T] [Algebra R T] [IsDomain T] [DecidableEq T] (x : S)
+    (σ₁ σ₂ : S →ₐ[R] T) :
+    eval₂ σ₁ (σ₂ x) (minpolyDiv R x) =
+      if σ₁ x = σ₂ x then σ₁ (aeval x (derivative <| minpoly R x)) else 0 := by
+  apply eval₂_minpolyDiv_of_eval₂_eq_zero
+  rw [AlgHom.comp_algebraMap, ← σ₂.comp_algebraMap, ← eval₂_map, ← RingHom.coe_coe, eval₂_hom,
+    eval_map, ← aeval_def, minpoly.aeval, map_zero]
+
+lemma eval_minpolyDiv_of_aeval_eq_zero [IsDomain S] [DecidableEq S]
+    {y} (hy : aeval y (minpoly R x) = 0) :
+    (minpolyDiv R x).eval y = if x = y then aeval x (derivative <| minpoly R x) else 0 := by
+  rw [eval, eval₂_minpolyDiv_of_eval₂_eq_zero]; rfl
+  exact hy
+
+lemma natDegree_minpolyDiv_succ [Nontrivial S] :
+    natDegree (minpolyDiv R x) + 1 = natDegree (minpoly R x) := by
+  rw [← (minpoly.monic hx).natDegree_map (algebraMap R S), ← minpolyDiv_spec, natDegree_mul']
+  · simp
+  · simpa using minpolyDiv_ne_zero hx
+
+lemma natDegree_minpolyDiv :
+    natDegree (minpolyDiv R x) = natDegree (minpoly R x) - 1 := by
+  nontriviality S
+  by_cases hx : IsIntegral R x
+  · rw [← natDegree_minpolyDiv_succ hx]; rfl
+  · rw [minpolyDiv_eq_zero hx, minpoly.eq_zero hx]; rfl
+
+lemma natDegree_minpolyDiv_lt [Nontrivial S] :
+    natDegree (minpolyDiv R x) < natDegree (minpoly R x) := by
+  rw [← natDegree_minpolyDiv_succ hx]
+  exact Nat.lt.base _
+
+lemma coeff_minpolyDiv_mem_adjoin (x : S) (i) :
+    coeff (minpolyDiv R x) i ∈ Algebra.adjoin R {x} := by
+  by_contra H
+  have : ∀ j, coeff (minpolyDiv R x) (i + j) ∉ Algebra.adjoin R {x}
+  · intro j; induction j with
+    | zero => exact H
+    | succ j IH =>
+      intro H; apply IH
+      rw [coeff_minpolyDiv]
+      refine add_mem ?_ (mul_mem H (Algebra.self_mem_adjoin_singleton R x))
+      exact Subalgebra.algebraMap_mem _ _
+  apply this (natDegree (minpolyDiv R x) + 1)
+  rw [coeff_eq_zero_of_natDegree_lt]
+  · exact zero_mem _
+  · refine (Nat.le_add_left _ i).trans_lt ?_
+    rw [← add_assoc]
+    exact Nat.lt.base _
+
+lemma minpolyDiv_eq_of_isIntegrallyClosed [IsDomain R] [IsIntegrallyClosed R] [IsDomain S]
+    [Algebra R K] [Algebra K S] [IsScalarTower R K S] [IsFractionRing R K] :
+    minpolyDiv R x = minpolyDiv K x := by
+  delta minpolyDiv
+  rw [IsScalarTower.algebraMap_eq R K S, ← map_map,
+    ← minpoly.isIntegrallyClosed_eq_field_fractions' _ hx]
+
+lemma coeff_minpolyDiv_sub_pow_mem_span {i} (hi : i ≤ natDegree (minpolyDiv R x)) :
+    coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - i) - x ^ i ∈
+      Submodule.span R ((x ^ ·) '' Set.Iio i) := by
+  induction i with
+  | zero => simp [(minpolyDiv_monic hx).leadingCoeff]
+  | succ i IH =>
+    rw [coeff_minpolyDiv, add_sub_assoc, pow_succ', ← sub_mul, Algebra.algebraMap_eq_smul_one]
+    refine add_mem ?_ ?_
+    · apply Submodule.smul_mem
+      apply Submodule.subset_span
+      exact ⟨0, Nat.zero_lt_succ _, pow_zero _⟩
+    · rw [Nat.succ_eq_add_one, ← tsub_tsub, tsub_add_cancel_of_le
+        (le_tsub_of_add_le_left (b := 1) hi)]
+      apply SetLike.le_def.mp ?_
+        (Submodule.mul_mem_mul (IH ((Nat.le_succ _).trans hi))
+          (Submodule.mem_span_singleton_self x))
+      rw [Submodule.span_mul_span, Set.mul_singleton, Set.image_image]
+      apply Submodule.span_mono
+      rintro _ ⟨j, hj : j < i, rfl⟩
+      exact ⟨j + 1, Nat.add_lt_of_lt_sub hj, pow_succ' x j⟩
+
+lemma span_coeff_minpolyDiv :
+    Submodule.span R (Set.range (coeff (minpolyDiv R x))) =
+      Subalgebra.toSubmodule (Algebra.adjoin R {x}) := by
+  nontriviality S
+  classical
+  apply le_antisymm
+  · rw [Submodule.span_le]
+    rintro _ ⟨i, rfl⟩
+    apply coeff_minpolyDiv_mem_adjoin
+  · rw [← Submodule.span_range_natDegree_eq_adjoin (minpoly.monic hx) (minpoly.aeval _ _),
+      Submodule.span_le]
+    simp only [Finset.coe_image, Finset.coe_range, Set.image_subset_iff]
+    intro i
+    apply Nat.strongInductionOn i
+    intro i hi hi'
+    have : coeff (minpolyDiv R x) (natDegree (minpolyDiv R x) - i) ∈
+        Submodule.span R (Set.range (coeff (minpolyDiv R x))) :=
+      Submodule.subset_span (Set.mem_range_self _)
+    rw [Set.mem_preimage, SetLike.mem_coe, ← Submodule.sub_mem_iff_right _ this]
+    refine SetLike.le_def.mp ?_ (coeff_minpolyDiv_sub_pow_mem_span hx ?_)
+    · rw [Submodule.span_le, Set.image_subset_iff]
+      intro j (hj : j < i)
+      exact hi j hj (lt_trans hj hi')
+    · rwa [← natDegree_minpolyDiv_succ hx, Set.mem_Iio, Nat.lt_succ_iff] at hi'
+
+section PowerBasis
+
+variable {K}
+
+lemma sum_smul_minpolyDiv_eq_X_pow (E) [Field E] [Algebra K E] [IsAlgClosed E]
+    [FiniteDimensional K L] [IsSeparable K L]
+    {x : L} (hxL : Algebra.adjoin K {x} = ⊤) {r : ℕ} (hr : r < finrank K L) :
+    ∑ σ : L →ₐ[K] E, ((x ^ r / aeval x (derivative <| minpoly K x)) •
+      minpolyDiv K x).map σ = (X ^ r : E[X]) := by
+  classical
+  rw [← sub_eq_zero]
+  have : Function.Injective (fun σ : L →ₐ[K] E ↦ σ x) := fun _ _ h =>
+    AlgHom.ext_of_adjoin_eq_top hxL (fun _ hx ↦ hx ▸ h)
+  apply Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zero _ this
+  · intro σ
+    simp only [Polynomial.map_smul, map_div₀, map_pow, RingHom.coe_coe, eval_sub, eval_finset_sum,
+      eval_smul, eval_map, eval₂_minpolyDiv_self, this.eq_iff, smul_eq_mul, mul_ite, mul_zero,
+      Finset.sum_ite_eq', Finset.mem_univ, ite_true, eval_pow, eval_X]
+    rw [sub_eq_zero, div_mul_cancel]
+    rw [ne_eq, map_eq_zero_iff σ σ.toRingHom.injective]
+    exact (IsSeparable.separable _ _).aeval_derivative_ne_zero (minpoly.aeval _ _)
+  · refine (Polynomial.natDegree_sub_le _ _).trans_lt
+      (max_lt ((Polynomial.natDegree_sum_le _ _).trans_lt ?_) ?_)
+    · simp only [AlgEquiv.toAlgHom_eq_coe, Polynomial.map_smul,
+        map_div₀, map_pow, RingHom.coe_coe, AlgHom.coe_coe, Function.comp_apply,
+        Finset.mem_univ, forall_true_left, true_and, Finset.fold_max_lt, AlgHom.card]
+      refine ⟨finrank_pos, ?_⟩
+      intro σ
+      exact ((Polynomial.natDegree_smul_le _ _).trans (natDegree_map_le _ _)).trans_lt
+        ((natDegree_minpolyDiv_lt (Algebra.IsIntegral.of_finite _ _ x)).trans_le
+          (minpoly.natDegree_le _))
+    · rwa [natDegree_pow, natDegree_X, mul_one, AlgHom.card]
+
+end PowerBasis

Mathlib/FieldTheory/Separable.lean

@@ -130,6 +130,19 @@ theorem Separable.map {p : R[X]} (h : p.Separable) {f : R →+* S} : (p.map f).S
       Polynomial.map_one]⟩
 #align polynomial.separable.map Polynomial.Separable.map
 
+theorem Separable.eval₂_derivative_ne_zero [Nontrivial S] (f : R →+* S) {p : R[X]}
+    (h : p.Separable) {x : S} (hx : p.eval₂ f x = 0) :
+    (derivative p).eval₂ f x ≠ 0 := by
+  intro hx'
+  obtain ⟨a, b, e⟩ := h
+  apply_fun Polynomial.eval₂ f x at e
+  simp only [eval₂_add, eval₂_mul, hx, mul_zero, hx', add_zero, eval₂_one, zero_ne_one] at e
+
+theorem Separable.aeval_derivative_ne_zero [Nontrivial S] [Algebra R S] {p : R[X]}
+    (h : p.Separable) {x : S} (hx : aeval x p = 0) :
+    aeval x (derivative p) ≠ 0 :=
+  h.eval₂_derivative_ne_zero (algebraMap R S) hx
+
 variable (p q : ℕ)
 
 theorem isUnit_of_self_mul_dvd_separable {p q : R[X]} (hp : p.Separable) (hq : q * q ∣ p) :

Mathlib/RingTheory/IntegralClosure.lean

@@ -170,22 +170,29 @@ theorem isIntegral_iff_isIntegral_closure_finite {r : B} :
   exact hsr.of_subring _
 #align is_integral_iff_is_integral_closure_finite isIntegral_iff_isIntegral_closure_finite
 
-theorem IsIntegral.fg_adjoin_singleton {x : B} (hx : IsIntegral R x) :
-    (Algebra.adjoin R {x}).toSubmodule.FG := by
-  rcases hx with ⟨f, hfm, hfx⟩
-  use (Finset.range <| f.natDegree + 1).image (x ^ ·)
+theorem Submodule.span_range_natDegree_eq_adjoin {R A} [CommRing R] [Semiring A] [Algebra R A]
+    {x : A} {f : R[X]} (hf : f.Monic) (hfx : aeval x f = 0) :
+    span R (Finset.image (x ^ ·) (Finset.range (natDegree f))) =
+      Subalgebra.toSubmodule (Algebra.adjoin R {x}) := by
+  nontriviality A
+  have hf1 : f ≠ 1 := by rintro rfl; simp [one_ne_zero' A] at hfx
   refine (span_le.mpr fun s hs ↦ ?_).antisymm fun r hr ↦ ?_
   · rcases Finset.mem_image.1 hs with ⟨k, -, rfl⟩
     exact (Algebra.adjoin R {x}).pow_mem (Algebra.subset_adjoin rfl) k
   rw [Subalgebra.mem_toSubmodule, Algebra.adjoin_singleton_eq_range_aeval] at hr
   rcases (aeval x).mem_range.mp hr with ⟨p, rfl⟩
-  rw [← modByMonic_add_div p hfm, map_add, map_mul, aeval_def x f, hfx,
+  rw [← modByMonic_add_div p hf, map_add, map_mul, hfx,
       zero_mul, add_zero, ← sum_C_mul_X_pow_eq (p %ₘ f), aeval_def, eval₂_sum, sum_def]
   refine sum_mem fun k hkq ↦ ?_
   rw [C_mul_X_pow_eq_monomial, eval₂_monomial, ← Algebra.smul_def]
-  exact smul_mem _ _ (subset_span <| Finset.mem_image_of_mem _ <| Finset.mem_range_succ_iff.mpr <|
-    (le_natDegree_of_mem_supp _ hkq).trans <| natDegree_modByMonic_le p hfm)
-#align fg_adjoin_singleton_of_integral IsIntegral.fg_adjoin_singleton
+  exact smul_mem _ _ (subset_span <| Finset.mem_image_of_mem _ <| Finset.mem_range.mpr <|
+    (le_natDegree_of_mem_supp _ hkq).trans_lt <| natDegree_modByMonic_lt p hf hf1)
+
+theorem IsIntegral.fg_adjoin_singleton {x : B} (hx : IsIntegral R x) :
+    (Algebra.adjoin R {x}).toSubmodule.FG := by
+  rcases hx with ⟨f, hfm, hfx⟩
+  use (Finset.range <| f.natDegree).image (x ^ ·)
+  exact span_range_natDegree_eq_adjoin hfm (by rwa [aeval_def])
 
 theorem fg_adjoin_of_finite {s : Set A} (hfs : s.Finite) (his : ∀ x ∈ s, IsIntegral R x) :
     (Algebra.adjoin R s).toSubmodule.FG :=

Mathlib/RingTheory/Trace.lean

@@ -13,6 +13,7 @@ import Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
 import Mathlib.FieldTheory.PrimitiveElement
 import Mathlib.FieldTheory.Galois
 import Mathlib.RingTheory.PowerBasis
+import Mathlib.FieldTheory.Minpoly.MinpolyDiv
 
 #align_import ring_theory.trace from "leanprover-community/mathlib"@"3e068ece210655b7b9a9477c3aff38a492400aa1"
 
@@ -43,6 +44,8 @@ the roots of the minimal polynomial of `s` over `R`.
    algebraically closed field
  * `traceForm_nondegenerate`: the trace form over a separable extension is a nondegenerate
    bilinear form
+* `traceForm_dualBasis_powerBasis_eq`: The dual basis of a powerbasis `{1, x, x²...}` under the
+   trace form is `aᵢ / f'(x)`, with `f` being the minpoly of `x` and `f / (X - x) = ∑ aᵢxⁱ`.
 
 ## Implementation notes
 
@@ -660,4 +663,32 @@ theorem Algebra.trace_surjective [FiniteDimensional K L] [IsSeparable K L] :
   rw [LinearMap.range_eq_bot]
   exact Algebra.trace_ne_zero K L
 
+variable {K L}
+
+/--
+The dual basis of a powerbasis `{1, x, x²...}` under the trace form is `aᵢ / f'(x)`,
+with `f` being the minimal polynomial of `x` and `f / (X - x) = ∑ aᵢxⁱ`.
+-/
+lemma traceForm_dualBasis_powerBasis_eq [FiniteDimensional K L] [IsSeparable K L]
+    (pb : PowerBasis K L) (i) :
+    (Algebra.traceForm K L).dualBasis (traceForm_nondegenerate K L) pb.basis i =
+      (minpolyDiv K pb.gen).coeff i / aeval pb.gen (derivative <| minpoly K pb.gen) := by
+  classical
+  apply ((Algebra.traceForm K L).toDual (traceForm_nondegenerate K L)).injective
+  apply pb.basis.ext
+  intro j
+  simp only [BilinForm.toDual_def, BilinForm.apply_dualBasis_left]
+  apply (algebraMap K (AlgebraicClosure K)).injective
+  have := congr_arg (coeff · i) (sum_smul_minpolyDiv_eq_X_pow (AlgebraicClosure K)
+    pb.adjoin_gen_eq_top (r := j) (pb.finrank.symm ▸ j.prop))
+  simp only [AlgEquiv.toAlgHom_eq_coe, Polynomial.map_smul, map_div₀,
+    map_pow, RingHom.coe_coe, AlgHom.coe_coe, finset_sum_coeff, coeff_smul, coeff_map, smul_eq_mul,
+    coeff_X_pow, ← Fin.ext_iff, @eq_comm _ i] at this
+  rw [PowerBasis.coe_basis, Algebra.traceForm_apply, RingHom.map_ite_one_zero,
+  ← this, trace_eq_sum_embeddings (E := AlgebraicClosure K)]
+  apply Finset.sum_congr rfl
+  intro σ _
+  simp only [_root_.map_mul, map_div₀, map_pow]
+  ring
+
 end DetNeZero