feat(RingTheory/IsAdjoinRoot): add mkOfAdjoinEqTop' (#36421)

Alternative hypothesis to existing theorem: prove the result from a `Module.Free `hypothesis instead of `IsIntegrallyClosed`. If `α` generates `S` as an algebra, then `S` is given by adjoining a root of `minpoly R α`.

Author: ROTARTSI82

Mathlib/Analysis/Complex/Polynomial/Basic.lean

@@ -10,6 +10,7 @@ public import Mathlib.Analysis.Complex.Liouville
 public import Mathlib.FieldTheory.PolynomialGaloisGroup
 public import Mathlib.LinearAlgebra.Complex.FiniteDimensional
 public import Mathlib.Topology.Algebra.Polynomial
+public import Mathlib.LinearAlgebra.Charpoly.Basic
 
 /-!
 # The fundamental theorem of algebra
@@ -198,10 +199,9 @@ lemma Irreducible.natDegree_le_two {p : ℝ[X]} (hp : Irreducible p) : natDegree
   obtain ⟨z, hz⟩ : ∃ z : ℂ, aeval z p = 0 :=
     IsAlgClosed.exists_aeval_eq_zero _ p (degree_pos_of_irreducible hp).ne'
   rw [← finrank_real_complex]
-  convert minpoly.natDegree_le z using 1
-  · rw [← minpoly.eq_of_irreducible hp hz, natDegree_mul hp.ne_zero (by simpa using hp.ne_zero),
-      natDegree_C, add_zero]
-  infer_instance
+  suffices p.natDegree = (minpoly ℝ z).natDegree from this ▸ minpoly.natDegree_le (R := ℝ) z
+  rw [← minpoly.eq_of_irreducible hp hz, natDegree_mul hp.ne_zero (by simpa using hp.ne_zero),
+    natDegree_C, add_zero]
 
 /-- An irreducible real polynomial has degree at most two. -/
 lemma Irreducible.degree_le_two {p : ℝ[X]} (hp : Irreducible p) : degree p ≤ 2 :=

Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean

@@ -531,15 +531,6 @@ theorem exists_lt_finrank_of_infinite_dimensional
     have h2 : F⟮x⟯ ≤ L' := le_sup_right
     exact hx <| (h1.symm ▸ h2) <| mem_adjoin_simple_self F x
 
-theorem _root_.minpoly.natDegree_le (x : L) [FiniteDimensional K L] :
-    (minpoly K x).natDegree ≤ finrank K L :=
-  le_of_eq_of_le (IntermediateField.adjoin.finrank (.of_finite _ _)).symm
-    K⟮x⟯.toSubmodule.finrank_le
-
-theorem _root_.minpoly.degree_le (x : L) [FiniteDimensional K L] :
-    (minpoly K x).degree ≤ finrank K L :=
-  degree_le_of_natDegree_le (minpoly.natDegree_le x)
-
 /-- If `x : L` is an integral element in a field extension `L` over `K`, then the degree of the
   minimal polynomial of `x` over `K` divides `[L : K]`. -/
 theorem _root_.minpoly.degree_dvd {x : L} (hx : IsIntegral K x) :

Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean

@@ -8,6 +8,7 @@ module
 public import Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
 public import Mathlib.FieldTheory.PrimitiveElement
 public import Mathlib.FieldTheory.IsAlgClosed.Basic
+public import Mathlib.LinearAlgebra.Charpoly.Basic
 
 /-!
 # Results about `minpoly R x / (X - C x)`

Mathlib/FieldTheory/Normal/Basic.lean

@@ -9,6 +9,7 @@ public import Mathlib.FieldTheory.Extension
 public import Mathlib.FieldTheory.Normal.Defs
 public import Mathlib.GroupTheory.Solvable
 public import Mathlib.FieldTheory.SplittingField.Construction
+public import Mathlib.LinearAlgebra.Charpoly.Basic
 
 /-!
 # Normal field extensions

Mathlib/FieldTheory/PurelyInseparable/Exponent.lean

@@ -6,6 +6,7 @@ Authors: Michal Staromiejski
 module
 
 public import Mathlib.FieldTheory.PurelyInseparable.Basic
+public import Mathlib.LinearAlgebra.Charpoly.Basic
 
 /-!
 

Mathlib/LinearAlgebra/Charpoly/Basic.lean

@@ -29,9 +29,6 @@ in any basis is in `LinearAlgebra/Charpoly/ToMatrix`.
 
 universe u v w
 
-variable {R : Type u} {M : Type v} [CommRing R]
-variable [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] (f : M →ₗ[R] M)
-
 open Matrix Polynomial
 
 noncomputable section
@@ -40,6 +37,9 @@ open Module.Free Polynomial Matrix
 
 namespace LinearMap
 
+variable {R : Type u} {M : Type v} [CommRing R]
+variable [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] (f : M →ₗ[R] M)
+
 section Basic
 
 /-- The characteristic polynomial of `f : M →ₗ[R] M`. -/
@@ -75,8 +75,9 @@ theorem charpoly_monic : f.charpoly.Monic :=
   Matrix.charpoly_monic _
 
 open Module in
-lemma charpoly_natDegree [Nontrivial R] [StrongRankCondition R] :
+lemma charpoly_natDegree [StrongRankCondition R] :
     natDegree (charpoly f) = finrank R M := by
+  haveI := nontrivial_of_invariantBasisNumber
   rw [charpoly, Matrix.charpoly_natDegree_eq_dim, finrank_eq_card_chooseBasisIndex]
 
 end Coeff
@@ -133,3 +134,26 @@ theorem minpoly_coeff_zero_of_injective [Nontrivial R] (hf : Function.Injective
 end CayleyHamilton
 
 end LinearMap
+
+section Algebra
+variable {R M} [CommRing R] [Ring M] [Algebra R M]
+  [Module.Finite R M] [Module.Free R M]
+
+theorem Algebra.aeval_self_charpoly_lmul (α : M) :
+    aeval α (Algebra.lmul R M α).charpoly = 0 :=
+  Algebra.lmul_injective (R := R) <| by
+    simpa [← aeval_algHom_apply] using LinearMap.aeval_self_charpoly <| Algebra.lmul _ _ α
+
+theorem minpoly.natDegree_le (α : M) :
+    (minpoly R α).natDegree ≤ Module.finrank R M := by
+  nontriviality R
+  let f := Algebra.lmul R _ α
+  have : (minpoly R α).natDegree ≤ f.charpoly.natDegree := natDegree_le_natDegree <|
+    minpoly.min _ _ f.charpoly_monic (Algebra.aeval_self_charpoly_lmul α)
+  simpa [← (Algebra.lmul _ _ α).charpoly_natDegree]
+
+theorem minpoly.degree_le (α : M) :
+    (minpoly R α).degree ≤ Module.finrank R M :=
+  degree_le_of_natDegree_le (minpoly.natDegree_le α)
+
+end Algebra

Mathlib/LinearAlgebra/Dimension/Constructions.lean

@@ -104,6 +104,12 @@ theorem Submodule.finrank_quotient_le [StrongRankCondition R] [Module.Finite R M
   toNat_le_toNat ((Submodule.mkQ s).rank_le_of_surjective Quot.mk_surjective)
     (rank_lt_aleph0 _ _)
 
+theorem LinearMap.finrank_le_finrank_of_surjective
+    [Module R M'] [StrongRankCondition R] [Module.Finite R M]
+    {f : M →ₗ[R] M'} (h : Function.Surjective f) : Module.finrank R M' ≤ Module.finrank R M := by
+  rw [← f.quotKerEquivOfSurjective h |>.finrank_eq]
+  exact Submodule.finrank_quotient_le _
+
 end Quotient
 
 variable [Semiring R] [CommSemiring S] [AddCommMonoid M] [AddCommMonoid M'] [AddCommMonoid M₁]

Mathlib/NumberTheory/NumberField/InfinitePlace/Embeddings.lean

@@ -8,6 +8,7 @@ module
 public import Mathlib.Algebra.Algebra.Hom.Rat
 public import Mathlib.Analysis.Complex.Polynomial.Basic
 public import Mathlib.NumberTheory.NumberField.Basic
+public import Mathlib.LinearAlgebra.Charpoly.Basic
 
 /-!
 # Embeddings of number fields

Mathlib/RingTheory/IsAdjoinRoot.lean

@@ -8,6 +8,7 @@ module
 public import Mathlib.Algebra.Polynomial.AlgebraMap
 public import Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
 public import Mathlib.RingTheory.PowerBasis
+public import Mathlib.LinearAlgebra.Charpoly.Basic
 
 /-!
 # A predicate on adjoining roots of polynomial
@@ -591,10 +592,10 @@ end lift
 section mkOfAdjoinEqTop
 
 variable [IsDomain R] [IsDomain S] [IsTorsionFree R S] [IsIntegrallyClosed R]
-    {α : S} {hα : IsIntegral R α} {hα₂ : Algebra.adjoin R {α} = ⊤}
+    {α : S} (hα : IsIntegral R α) (hα₂ : Algebra.adjoin R {α} = ⊤)
 
-variable (hα hα₂) in
 /-- If `α` generates `S` as an algebra, then `S` is given by adjoining a root of `minpoly R α`. -/
+@[simps]
 def mkOfAdjoinEqTop : IsAdjoinRoot S (minpoly R α) where
   map := aeval α
   map_surjective := by
@@ -604,15 +605,14 @@ def mkOfAdjoinEqTop : IsAdjoinRoot S (minpoly R α) where
     ext
     simpa [Ideal.mem_span_singleton] using minpoly.isIntegrallyClosed_dvd_iff hα _
 
-variable (hα hα₂) in
 /-- If `α` generates `S` as an algebra, then `S` is given by adjoining a root of `minpoly R α`. -/
 abbrev _root_.IsAdjoinRootMonic.mkOfAdjoinEqTop : IsAdjoinRootMonic S (minpoly R α) where
   __ := IsAdjoinRoot.mkOfAdjoinEqTop hα hα₂
   monic := minpoly.monic hα
 
 @[simp]
 theorem mkOfAdjoinEqTop_root : (IsAdjoinRoot.mkOfAdjoinEqTop hα hα₂).root = α := by
-  simp [IsAdjoinRoot.mkOfAdjoinEqTop, IsAdjoinRoot.root]
+  simp [IsAdjoinRoot.root]
 
 end mkOfAdjoinEqTop
 
@@ -647,6 +647,44 @@ theorem minpoly_eq [IsDomain R] [IsDomain S] [IsTorsionFree R S] [IsIntegrallyCl
             (hirr.isUnit_or_isUnit hq).resolve_left <| minpoly.not_isUnit R h.root
       rw [mul_one]
 
+/-- If `α` generates `S` as an algebra and `S` is free and finite,
+then `S` is given by adjoining a root of `minpoly R α`.
+Does not require that `R` is an integral domain, unlike `mkOfAdjoinEqTop`. -/
+@[simps]
+def mkOfAdjoinEqTop'
+    [Module.Finite R S] [Module.Free R S]
+    {α : S} (hα : Algebra.adjoin R {α} = ⊤) :
+    IsAdjoinRootMonic S (minpoly R α) where
+  __ : IsAdjoinRoot S (minpoly R α) :=
+    let f := minpoly R α
+    have hf := minpoly.monic (Algebra.IsIntegral.isIntegral (R := R) α)
+    let φ : AdjoinRoot f →ₐ[R] S :=
+      AdjoinRoot.liftAlgHom f (Algebra.ofId R S) α (minpoly.aeval R α)
+    IsAdjoinRoot.ofAdjoinRootEquiv <| AlgEquiv.ofBijective φ <| by
+      have hφ : Function.Surjective φ := by
+        rw [Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at hα
+        intro s; obtain ⟨p, hp⟩ := hα s
+        exact ⟨AdjoinRoot.mk f p, by simp [φ, ← aeval_def, hp]⟩
+      haveI := hf.free_adjoinRoot; haveI := hf.finite_adjoinRoot
+      by_cases h : Nontrivial R
+      · letI e := LinearEquiv.ofFinrankEq (R := R) (AdjoinRoot f) S <|
+          le_antisymm (finrank_quotient_span_eq_natDegree' hf ▸ minpoly.natDegree_le α)
+          (LinearMap.finrank_le_finrank_of_surjective (f := φ.toLinearMap) hφ)
+        exact OrzechProperty.bijective_of_surjective_of_injective
+          e.toLinearMap φ e.injective hφ
+      · apply not_nontrivial_iff_subsingleton.mp at h
+        haveI := Module.subsingleton R (AdjoinRoot f)
+        exact ⟨Function.injective_of_subsingleton φ, hφ⟩
+  map := aeval α
+  monic := minpoly.monic (Algebra.IsIntegral.isIntegral α)
+
+@[simp]
+theorem mkOfAdjoinEqTop'_root
+    [Module.Finite R S] [Module.Free R S]
+    {α : S} (hα : Algebra.adjoin R {α} = ⊤) :
+      (mkOfAdjoinEqTop' hα).root = α := by
+  simp [IsAdjoinRoot.root]
+
 end IsAdjoinRootMonic
 
 section Algebra

Mathlib/RingTheory/OrzechProperty.lean

@@ -91,6 +91,12 @@ theorem injective_of_surjective_of_injective
   replace hf : Surjective f' := by simpa [f'] using hf
   simpa [f'] using injective_of_surjective_of_submodule' f' hf
 
+theorem bijective_of_surjective_of_injective
+    {N : Type w} [AddCommMonoid N] [Module R N]
+    (i f : N →ₗ[R] M) (hi : Function.Injective i)
+    (hf : Function.Surjective f) : Function.Bijective f :=
+  ⟨OrzechProperty.injective_of_surjective_of_injective _ _ hi hf, hf⟩
+
 theorem injective_of_surjective_of_submodule
     {N : Submodule R M} (f : N →ₗ[R] M) (hf : Surjective f) : Injective f :=
   injective_of_surjective_of_injective N.subtype f N.injective_subtype hf