move lemmas

Author: ROTARTSI82

Mathlib/FieldTheory/Minpoly/Basic.lean

@@ -6,6 +6,9 @@ Authors: Chris Hughes, Johan Commelin
 module
 
 public import Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
+public import Mathlib.LinearAlgebra.Dimension.Finrank
+import Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
+import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
 
 /-!
 # Minimal polynomials
@@ -236,6 +239,19 @@ theorem two_le_natDegree_subalgebra {B} [CommRing B] [Algebra A B] [Nontrivial B
   rw [two_le_natDegree_iff int, Iff.not]
   apply Set.ext_iff.mp Subtype.range_val_subtype
 
+omit [Nontrivial B] in
+/-- For finite free modules over a nontrivial ring,
+the degree of the minimal polynomials is bounded by the rank of the module -/
+theorem natDegree_le' [Module.Finite A B] [Module.Free A B] [Nontrivial A] :
+    (minpoly A x).natDegree ≤ Module.finrank A B := by
+  have b := Module.Free.chooseBasis A B
+  let M := LinearMap.toMatrixAlgEquiv b (Algebra.lmul A B x)
+  refine (natDegree_le_natDegree (minpoly.min A x M.charpoly_monic ?_)).trans
+    (M.charpoly_natDegree_eq_dim.trans (Module.finrank_eq_card_chooseBasisIndex A B).symm).le
+  let h := Matrix.aeval_self_charpoly M
+  rwa [aeval_algHom_apply, _root_.map_eq_zero_iff _ (LinearMap.toMatrixAlgEquiv b).injective,
+    aeval_algHom_apply, _root_.map_eq_zero_iff _ Algebra.lmul_injective] at h
+
 end
 
 /-- If `B/A` is an injective ring extension, and `a` is an element of `A`,

Mathlib/RingTheory/IsAdjoinRoot.lean

@@ -622,24 +622,55 @@ theorem mkOfAdjoinEqTop_root : (IsAdjoinRoot.mkOfAdjoinEqTop hα hα₂).root =
 
 end mkOfAdjoinEqTop
 
+section Equiv
+
+variable {T : Type*} [CommRing T] [Algebra R T] (h' : IsAdjoinRoot T f) {U : Type*} [CommRing U]
+
+@[simp]
+theorem lift_algEquiv (i : R →+* U) (x hx z) :
+    h'.lift i x hx (h.algEquiv h' z) = h.lift i x hx z := by rw [← h.map_repr z]; simp [-map_repr]
+
+@[simp]
+theorem liftHom_algEquiv [Algebra R U] (x : U) (hx z) :
+    h'.liftHom x hx (h.algEquiv h' z) = h.liftHom x hx z := h.lift_algEquiv h' _ _ hx _
+
+end Equiv
+
+end IsAdjoinRoot
+
+namespace IsAdjoinRootMonic
+
+variable (h : IsAdjoinRootMonic S f)
+
+theorem minpoly_eq [IsDomain R] [IsDomain S] [IsTorsionFree R S] [IsIntegrallyClosed R]
+  (hirr : Irreducible f) : minpoly R h.root = f :=
+  let ⟨q, hq⟩ := minpoly.isIntegrallyClosed_dvd h.isIntegral_root h.aeval_root_self
+  symm <|
+    eq_of_monic_of_associated h.monic (minpoly.monic h.isIntegral_root) <| by
+      convert
+        Associated.mul_left (minpoly R h.root) <|
+          associated_one_iff_isUnit.2 <|
+            (hirr.isUnit_or_isUnit hq).resolve_left <| minpoly.not_isUnit R h.root
+      rw [mul_one]
+
 section mkOfAdjoinEqTop'
 
 variable [Module.Finite R S] [Module.Free R S] [Nontrivial R]
 
-/-- For finite free modules over a nontrivial ring,
-the degree of the minimal polynomials is bounded by the rank of the module -/
-theorem _root_.minpoly.natDegree_le' (α : S) :
-    (minpoly R α).natDegree ≤ Module.finrank R S := by
-  have b := Module.Free.chooseBasis R S
-  let M := LinearMap.toMatrixAlgEquiv b (Algebra.lmul R S α)
-  refine (natDegree_le_natDegree (minpoly.min R α M.charpoly_monic ?_)).trans
-    (M.charpoly_natDegree_eq_dim.trans (Module.finrank_eq_card_chooseBasisIndex R S).symm).le
+-- theorem could be placed here with 0 imports, but
+-- it does not logically make sense.
+theorem alternate_natDegree_le' :
+    (minpoly A x).natDegree ≤ Module.finrank A B := by
+  have b := Module.Free.chooseBasis A B
+  let M := LinearMap.toMatrixAlgEquiv b (Algebra.lmul A B x)
+  refine (natDegree_le_natDegree (minpoly.min A x M.charpoly_monic ?_)).trans
+    (M.charpoly_natDegree_eq_dim.trans (Module.finrank_eq_card_chooseBasisIndex A B).symm).le
   let h := Matrix.aeval_self_charpoly M
   rwa [aeval_algHom_apply, _root_.map_eq_zero_iff _ (LinearMap.toMatrixAlgEquiv b).injective,
     aeval_algHom_apply, _root_.map_eq_zero_iff _ Algebra.lmul_injective] at h
 
 /-- If `α` generates `S` as an algebra, then `S` is given by adjoining a root of `minpoly R α`. -/
-def _root_.IsAdjoinRootMonic.mkOfAdjoinEqTop'
+def mkOfAdjoinEqTop'
     {α : S} (hα : Algebra.adjoin R {α} = ⊤) :
     IsAdjoinRootMonic S (minpoly R α) := by
   set f := minpoly R α
@@ -667,45 +698,14 @@ def _root_.IsAdjoinRootMonic.mkOfAdjoinEqTop'
         (AlgEquiv.ofBijective φ ⟨hφ_inj, hφ_surj⟩) with monic := hf }
 
 @[simp]
-lemma _root_.IsAdjoinRootMonic.mkOfAdjoinEqTop'_map
+lemma mkOfAdjoinEqTop'_map
     {α : S} {hα : Algebra.adjoin R {α} = ⊤} :
     (IsAdjoinRootMonic.mkOfAdjoinEqTop' hα).map = (aeval α) := by
   unfold IsAdjoinRootMonic.mkOfAdjoinEqTop'
   ext; simp
 
 end mkOfAdjoinEqTop'
 
-section Equiv
-
-variable {T : Type*} [CommRing T] [Algebra R T] (h' : IsAdjoinRoot T f) {U : Type*} [CommRing U]
-
-@[simp]
-theorem lift_algEquiv (i : R →+* U) (x hx z) :
-    h'.lift i x hx (h.algEquiv h' z) = h.lift i x hx z := by rw [← h.map_repr z]; simp [-map_repr]
-
-@[simp]
-theorem liftHom_algEquiv [Algebra R U] (x : U) (hx z) :
-    h'.liftHom x hx (h.algEquiv h' z) = h.liftHom x hx z := h.lift_algEquiv h' _ _ hx _
-
-end Equiv
-
-end IsAdjoinRoot
-
-namespace IsAdjoinRootMonic
-
-variable (h : IsAdjoinRootMonic S f)
-
-theorem minpoly_eq [IsDomain R] [IsDomain S] [IsTorsionFree R S] [IsIntegrallyClosed R]
-  (hirr : Irreducible f) : minpoly R h.root = f :=
-  let ⟨q, hq⟩ := minpoly.isIntegrallyClosed_dvd h.isIntegral_root h.aeval_root_self
-  symm <|
-    eq_of_monic_of_associated h.monic (minpoly.monic h.isIntegral_root) <| by
-      convert
-        Associated.mul_left (minpoly R h.root) <|
-          associated_one_iff_isUnit.2 <|
-            (hirr.isUnit_or_isUnit hq).resolve_left <| minpoly.not_isUnit R h.root
-      rw [mul_one]
-
 end IsAdjoinRootMonic
 
 section Algebra