chore: split FieldTheory/Tower (#15689)

The results in this file were unrelated (and had disjoint import requirements!) so I've separated them.

The doc-string was badly out of date before I came along, so I've replaced it.

Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

Author: 3 people

Mathlib.lean

@@ -21,6 +21,7 @@ import Mathlib.Algebra.Algebra.RestrictScalars
 import Mathlib.Algebra.Algebra.Spectrum
 import Mathlib.Algebra.Algebra.Subalgebra.Basic
 import Mathlib.Algebra.Algebra.Subalgebra.Directed
+import Mathlib.Algebra.Algebra.Subalgebra.IsSimpleOrder
 import Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
 import Mathlib.Algebra.Algebra.Subalgebra.Operations
 import Mathlib.Algebra.Algebra.Subalgebra.Order

Mathlib/Algebra/Algebra/Subalgebra/IsSimpleOrder.lean

@@ -0,0 +1,33 @@
+/-
+Copyright (c) 2020 Kenny Lau. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kenny Lau
+-/
+import Mathlib.LinearAlgebra.FiniteDimensional.Defs
+import Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
+import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
+
+/-!
+If `A` is a domain, and a finite-dimensional algebra over a field `F`, with prime dimension,
+then there are no non-trivial `F`-subalgebras.
+-/
+
+open FiniteDimensional Submodule
+
+theorem Subalgebra.isSimpleOrder_of_finrank_prime (F A) [Field F] [Ring A] [IsDomain A]
+    [Algebra F A] (hp : (finrank F A).Prime) : IsSimpleOrder (Subalgebra F A) :=
+  { toNontrivial :=
+      ⟨⟨⊥, ⊤, fun he =>
+          Nat.not_prime_one ((Subalgebra.bot_eq_top_iff_finrank_eq_one.1 he).subst hp)⟩⟩
+    eq_bot_or_eq_top := fun K => by
+      haveI : FiniteDimensional _ _ := .of_finrank_pos hp.pos
+      letI := divisionRingOfFiniteDimensional F K
+      refine (hp.eq_one_or_self_of_dvd _ ⟨_, (finrank_mul_finrank F K A).symm⟩).imp ?_ fun h => ?_
+      · exact fun h' => Subalgebra.eq_bot_of_finrank_one h'
+      · exact
+          Algebra.toSubmodule_eq_top.1 (eq_top_of_finrank_eq <| K.finrank_toSubmodule.trans h) }
+-- TODO: `IntermediateField` version
+
+@[deprecated (since := "2024-08-11")]
+alias FiniteDimensional.Subalgebra.is_simple_order_of_finrank_prime :=
+  Subalgebra.isSimpleOrder_of_finrank_prime

Mathlib/Algebra/CharP/IntermediateField.lean

@@ -5,6 +5,7 @@ Authors: Jz Pan
 -/
 import Mathlib.Algebra.CharP.ExpChar
 import Mathlib.FieldTheory.IntermediateField.Basic
+import Mathlib.Algebra.EuclideanDomain.Field
 
 /-!
 

Mathlib/FieldTheory/Adjoin.lean

@@ -8,6 +8,7 @@ import Mathlib.FieldTheory.IntermediateField.Algebraic
 import Mathlib.FieldTheory.Separable
 import Mathlib.FieldTheory.SplittingField.IsSplittingField
 import Mathlib.RingTheory.TensorProduct.Basic
+import Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
 
 /-!
 # Adjoining Elements to Fields

Mathlib/FieldTheory/Fixed.lean

@@ -8,7 +8,7 @@ import Mathlib.Algebra.Ring.Action.Field
 import Mathlib.Algebra.Ring.Action.Invariant
 import Mathlib.FieldTheory.Normal
 import Mathlib.FieldTheory.Separable
-import Mathlib.FieldTheory.Tower
+import Mathlib.LinearAlgebra.FreeModule.Finite.Matrix
 
 /-!
 # Fixed field under a group action.

Mathlib/FieldTheory/IntermediateField/Algebraic.lean

@@ -7,6 +7,7 @@ import Mathlib.FieldTheory.IntermediateField.Basic
 import Mathlib.RingTheory.Algebraic
 import Mathlib.FieldTheory.Tower
 import Mathlib.FieldTheory.Minpoly.Basic
+import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
 
 /-!
 # Results on finite dimensionality and algebraicity of intermediate fields.

Mathlib/FieldTheory/NormalClosure.lean

@@ -6,6 +6,7 @@ Authors: Thomas Browning
 
 import Mathlib.FieldTheory.Normal
 import Mathlib.Order.Closure
+import Mathlib.LinearAlgebra.FreeModule.Finite.Matrix
 /-!
 # Normal closures
 

Mathlib/FieldTheory/Tower.lean

@@ -3,27 +3,19 @@ Copyright (c) 2020 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 -/
-import Mathlib.Data.Nat.Prime.Defs
 import Mathlib.RingTheory.AlgebraTower
-import Mathlib.LinearAlgebra.FiniteDimensional.Defs
-import Mathlib.LinearAlgebra.FreeModule.Finite.Matrix
-import Mathlib.RingTheory.LocalRing.Basic
+import Mathlib.RingTheory.Noetherian
 
 /-!
-# Tower of field extensions
+# Finiteness of `IsScalarTower`
 
-In this file we prove the tower law for arbitrary extensions and finite extensions.
-Suppose `L` is a field extension of `K` and `K` is a field extension of `F`.
-Then `[L:F] = [L:K] [K:F]` where `[E₁:E₂]` means the `E₂`-dimension of `E₁`.
+We prove that given `IsScalarTower F K A`, if `A` is finite as a module over `F` then
+`A` is finite over `K`, and
+(as long as `A` is Noetherian over `F` and we have `NoZeroSMulDivisors K A`) `K` is finite over `F`.
 
-In fact we generalize it to rings and modules, where `L` is not necessarily a field,
-but just a free module over `K`.
+In particular these conditions hold when `A`, `F`, and `K` are fields.
 
-## Implementation notes
-
-We prove two versions, since there are two notions of dimensions: `Module.rank` which gives
-the dimension of an arbitrary vector space as a cardinal, and `FiniteDimensional.finrank` which
-gives the dimension of a finite-dimensional vector space as a natural number.
+The formulas for the dimensions are given elsewhere by `FiniteDimensional.finrank_mul_finrank`.
 
 ## Tags
 
@@ -38,49 +30,31 @@ open Cardinal Submodule
 
 variable (F : Type u) (K : Type v) (A : Type w)
 
-section Field
-
-variable [DivisionRing F] [DivisionRing K] [AddCommGroup A]
-variable [Module F K] [Module K A] [Module F A] [IsScalarTower F K A]
-
-namespace FiniteDimensional
-
-open IsNoetherian
+namespace Module.Finite
 
+variable [Ring F] [Ring K] [Module F K]
+  [AddCommGroup A] [Module K A] [NoZeroSMulDivisors K A]
+  [Module F A] [IsNoetherian F A] [IsScalarTower F K A] in
 /-- In a tower of field extensions `A / K / F`, if `A / F` is finite, so is `K / F`.
 
 (In fact, it suffices that `A` is a nontrivial ring.)
 
 Note this cannot be an instance as Lean cannot infer `A`.
 -/
-theorem left [Nontrivial A] [FiniteDimensional F A] : FiniteDimensional F K :=
+theorem left [Nontrivial A] : Module.Finite F K :=
   let ⟨x, hx⟩ := exists_ne (0 : A)
-  FiniteDimensional.of_injective
+  Module.Finite.of_injective
     (LinearMap.ringLmapEquivSelf K ℕ A |>.symm x |>.restrictScalars F) (smul_left_injective K hx)
 
-theorem right [hf : FiniteDimensional F A] : FiniteDimensional K A :=
+variable [Semiring F] [Semiring K] [Module F K]
+  [AddCommMonoid A] [Module K A] [Module F A] [IsScalarTower F K A] in
+theorem right [hf : Module.Finite F A] : Module.Finite K A :=
   let ⟨⟨b, hb⟩⟩ := hf
   ⟨⟨b, Submodule.restrictScalars_injective F _ _ <| by
     rw [Submodule.restrictScalars_top, eq_top_iff, ← hb, Submodule.span_le]
     exact Submodule.subset_span⟩⟩
 
-theorem Subalgebra.isSimpleOrder_of_finrank_prime (F A) [Field F] [Ring A] [IsDomain A]
-    [Algebra F A] (hp : (finrank F A).Prime) : IsSimpleOrder (Subalgebra F A) :=
-  { toNontrivial :=
-      ⟨⟨⊥, ⊤, fun he =>
-          Nat.not_prime_one ((Subalgebra.bot_eq_top_iff_finrank_eq_one.1 he).subst hp)⟩⟩
-    eq_bot_or_eq_top := fun K => by
-      haveI : FiniteDimensional _ _ := .of_finrank_pos hp.pos
-      letI := divisionRingOfFiniteDimensional F K
-      refine (hp.eq_one_or_self_of_dvd _ ⟨_, (finrank_mul_finrank F K A).symm⟩).imp ?_ fun h => ?_
-      · exact fun h' => Subalgebra.eq_bot_of_finrank_one h'
-      · exact
-          Algebra.toSubmodule_eq_top.1 (eq_top_of_finrank_eq <| K.finrank_toSubmodule.trans h) }
--- TODO: `IntermediateField` version
-
-@[deprecated (since := "2024-01-12")]
-alias finrank_linear_map' := FiniteDimensional.finrank_linearMap_self
-
-end FiniteDimensional
-
-end Field
+end Module.Finite
+
+alias FiniteDimensional.left := Module.Finite.left
+alias FiniteDimensional.right := Module.Finite.right

Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean

@@ -5,6 +5,7 @@ Authors: Alexander Bentkamp
 -/
 import Mathlib.LinearAlgebra.Eigenspace.Basic
 import Mathlib.FieldTheory.IsAlgClosed.Spectrum
+import Mathlib.LinearAlgebra.FreeModule.Finite.Matrix
 
 /-!
 # Triangularizable linear endomorphisms

Mathlib/LinearAlgebra/FreeModule/Finite/Matrix.lean

@@ -65,6 +65,9 @@ theorem FiniteDimensional.rank_linearMap_self :
 theorem FiniteDimensional.finrank_linearMap_self : finrank S (M →ₗ[R] S) = finrank R M := by
   rw [finrank_linearMap, finrank_self, mul_one]
 
+@[deprecated (since := "2024-01-12")]
+alias FiniteDimensional.finrank_linear_map' := FiniteDimensional.finrank_linearMap_self
+
 end Ring
 
 section AlgHom