From 970a1ab2bfb8a7921fd05c872c630a0a83632bb8 Mon Sep 17 00:00:00 2001 From: Oliver Nash Date: Fri, 26 Jan 2024 04:28:56 +0000 Subject: [PATCH] feat: the minimal polynomial is a generator of the annihilator ideal (#10008) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit More precisely, the goal of these changes is to make the following work: ```lean import Mathlib.FieldTheory.Minpoly.Field open Module Polynomial example {K V : Type*} [Field K] [AddCommGroup V] [Module K V] (f : End K V) : (⊤ : Submodule K[X] <| AEval K V f).annihilator = K[X] ∙ minpoly K f := by simp ``` Co-authored-by: Johan Commelin --- Mathlib/Data/Polynomial/Module.lean | 8 ++++++++ Mathlib/FieldTheory/Minpoly/Field.lean | 13 +++++++++++++ 2 files changed, 21 insertions(+) diff --git a/Mathlib/Data/Polynomial/Module.lean b/Mathlib/Data/Polynomial/Module.lean index 70b9cb49c768b..4be728e268ff8 100644 --- a/Mathlib/Data/Polynomial/Module.lean +++ b/Mathlib/Data/Polynomial/Module.lean @@ -88,6 +88,14 @@ instance instIsScalarTowerOrigPolynomial : IsScalarTower R R[X] <| AEval R M a w instance instFinitePolynomial [Finite R M] : Finite R[X] <| AEval R M a := Finite.of_restrictScalars_finite R _ _ +@[simp] +lemma annihilator_top_eq_ker_aeval [FaithfulSMul A M] : + (⊤ : Submodule R[X] <| AEval R M a).annihilator = RingHom.ker (aeval a) := by + ext p + simp only [Submodule.mem_annihilator, Submodule.mem_top, forall_true_left, RingHom.mem_ker] + change (∀ m : M, aeval a p • m = 0) ↔ _ + exact ⟨fun h ↦ eq_of_smul_eq_smul (α := M) <| by simp [h], fun h ↦ by simp [h]⟩ + section Submodule variable {p : Submodule R M} (hp : p ≤ p.comap (Algebra.lsmul R R M a)) diff --git a/Mathlib/FieldTheory/Minpoly/Field.lean b/Mathlib/FieldTheory/Minpoly/Field.lean index 72be5d603622e..4c5c57881e373 100644 --- a/Mathlib/FieldTheory/Minpoly/Field.lean +++ b/Mathlib/FieldTheory/Minpoly/Field.lean @@ -78,6 +78,10 @@ theorem dvd {p : A[X]} (hp : Polynomial.aeval x p = 0) : minpoly A x ∣ p := by exact degree_modByMonic_lt _ (monic hx) #align minpoly.dvd minpoly.dvd +variable {A x} in +lemma dvd_iff {p : A[X]} : minpoly A x ∣ p ↔ Polynomial.aeval x p = 0 := + ⟨fun ⟨q, hq⟩ ↦ by rw [hq, map_mul, aeval, zero_mul], minpoly.dvd A x⟩ + theorem dvd_map_of_isScalarTower (A K : Type*) {R : Type*} [CommRing A] [Field K] [CommRing R] [Algebra A K] [Algebra A R] [Algebra K R] [IsScalarTower A K R] (x : R) : minpoly K x ∣ (minpoly A x).map (algebraMap A K) := by @@ -104,6 +108,15 @@ theorem aeval_of_isScalarTower (R : Type*) {K T U : Type*} [CommRing R] [Field K (minpoly.dvd_map_of_isScalarTower R K x) hy #align minpoly.aeval_of_is_scalar_tower minpoly.aeval_of_isScalarTower +/-- See also `minpoly.ker_eval` which relaxes the assumptions on `A` in exchange for +stronger assumptions on `B`. -/ +@[simp] +lemma ker_aeval_eq_span_minpoly : + RingHom.ker (Polynomial.aeval x) = A[X] ∙ minpoly A x := by + ext p + simp_rw [RingHom.mem_ker, ← minpoly.dvd_iff, Submodule.mem_span_singleton, + dvd_iff_exists_eq_mul_left, smul_eq_mul, eq_comm (a := p)] + variable {A x} theorem eq_of_irreducible_of_monic [Nontrivial B] {p : A[X]} (hp1 : Irreducible p)