[Merged by Bors] - feat(RingTheory/IsAdjoinRoot): add mkOfAdjoinEqTop'

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`. -/
@@ -133,3 +133,19 @@ 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' [Nontrivial R] {α : M} :
+    (minpoly R α).natDegree ≤ Module.finrank R M := by
+  simpa [← (Algebra.lmul _ _ α).charpoly_natDegree] using natDegree_le_natDegree <| minpoly.min _ _
+        (Algebra.lmul R _ α).charpoly_monic Algebra.aeval_self_charpoly_lmul
+
+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/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
+import Mathlib.LinearAlgebra.Charpoly.Basic
 
 /-!
 # A predicate on adjoining roots of polynomial
@@ -647,6 +648,34 @@ 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, then `S` is given by adjoining a root of `minpoly R α`. -/
+def mkOfAdjoinEqTop'
+    [Module.Finite R S] [Module.Free R S] [Nontrivial R]
+    {α : S} (hα : Algebra.adjoin R {α} = ⊤) :
+    IsAdjoinRootMonic S (minpoly R α) where
+  map := aeval α
+  ker_map := by
+    set 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 α)
+    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]⟩
+    refine IsAdjoinRoot.ofAdjoinRootEquiv (AlgEquiv.ofBijective φ ⟨?_, hφ⟩) |>.ker_map
+    haveI := hf.free_adjoinRoot; haveI := hf.finite_adjoinRoot
+    letI : Module R (AdjoinRoot f) := Algebra.toModule
+    have 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 fun x y h => OrzechProperty.injective_of_surjective_endomorphism
+      (e.symm.toLinearMap.comp φ.toLinearMap)
+      (e.symm.surjective.comp hφ) (congr_arg e.symm h)
+  map_surjective := by
+    rwa [Algebra.adjoin_singleton_eq_range_aeval, AlgHom.range_eq_top] at *
+  monic := minpoly.monic (Algebra.IsIntegral.isIntegral α)
+
 end IsAdjoinRootMonic
 
 section Algebra