chore: split FieldTheory/IntermediateField (#15692)

Mathlib.lean

@@ -2595,7 +2595,8 @@ import Mathlib.FieldTheory.Finite.Trace
 import Mathlib.FieldTheory.Finiteness
 import Mathlib.FieldTheory.Fixed
 import Mathlib.FieldTheory.Galois
-import Mathlib.FieldTheory.IntermediateField
+import Mathlib.FieldTheory.IntermediateField.Algebraic
+import Mathlib.FieldTheory.IntermediateField.Basic
 import Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
 import Mathlib.FieldTheory.IsAlgClosed.Basic
 import Mathlib.FieldTheory.IsAlgClosed.Classification

Mathlib/Algebra/CharP/IntermediateField.lean

@@ -3,8 +3,8 @@ Copyright (c) 2024 Jz Pan. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jz Pan
 -/
-import Mathlib.FieldTheory.IntermediateField
 import Mathlib.Algebra.CharP.ExpChar
+import Mathlib.FieldTheory.IntermediateField.Basic
 
 /-!
 

Mathlib/FieldTheory/Adjoin.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Thomas Browning, Patrick Lutz
 -/
 import Mathlib.Algebra.Algebra.Subalgebra.Directed
-import Mathlib.FieldTheory.IntermediateField
+import Mathlib.FieldTheory.IntermediateField.Algebraic
 import Mathlib.FieldTheory.Separable
 import Mathlib.FieldTheory.SplittingField.IsSplittingField
 import Mathlib.RingTheory.TensorProduct.Basic

Mathlib/FieldTheory/IntermediateField/Algebraic.lean

@@ -0,0 +1,118 @@
+/-
+Copyright (c) 2020 Anne Baanen. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anne Baanen
+-/
+import Mathlib.FieldTheory.IntermediateField.Basic
+import Mathlib.RingTheory.Algebraic
+import Mathlib.FieldTheory.Tower
+import Mathlib.FieldTheory.Minpoly.Basic
+
+/-!
+# Results on finite dimensionality and algebraicity of intermediate fields.
+-/
+
+open FiniteDimensional
+
+variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
+  {S : IntermediateField K L}
+
+namespace IntermediateField
+
+section FiniteDimensional
+
+variable (F E : IntermediateField K L)
+
+instance finiteDimensional_left [FiniteDimensional K L] : FiniteDimensional K F :=
+  left K F L
+
+instance finiteDimensional_right [FiniteDimensional K L] : FiniteDimensional F L :=
+  right K F L
+
+@[simp]
+theorem rank_eq_rank_subalgebra : Module.rank K F.toSubalgebra = Module.rank K F :=
+  rfl
+
+@[simp]
+theorem finrank_eq_finrank_subalgebra : finrank K F.toSubalgebra = finrank K F :=
+  rfl
+
+variable {F} {E}
+
+@[simp]
+theorem toSubalgebra_eq_iff : F.toSubalgebra = E.toSubalgebra ↔ F = E := by
+  rw [SetLike.ext_iff, SetLike.ext'_iff, Set.ext_iff]
+  rfl
+
+/-- If `F ≤ E` are two intermediate fields of `L / K` such that `[E : K] ≤ [F : K]` are finite,
+then `F = E`. -/
+theorem eq_of_le_of_finrank_le [hfin : FiniteDimensional K E] (h_le : F ≤ E)
+    (h_finrank : finrank K E ≤ finrank K F) : F = E :=
+  haveI : Module.Finite K E.toSubalgebra := hfin
+  toSubalgebra_injective <| Subalgebra.eq_of_le_of_finrank_le h_le h_finrank
+
+/-- If `F ≤ E` are two intermediate fields of `L / K` such that `[F : K] = [E : K]` are finite,
+then `F = E`. -/
+theorem eq_of_le_of_finrank_eq [FiniteDimensional K E] (h_le : F ≤ E)
+    (h_finrank : finrank K F = finrank K E) : F = E :=
+  eq_of_le_of_finrank_le h_le h_finrank.ge
+
+-- If `F ≤ E` are two intermediate fields of a finite extension `L / K` such that
+-- `[L : F] ≤ [L : E]`, then `F = E`. Marked as private since it's a direct corollary of
+-- `eq_of_le_of_finrank_le'` (the `FiniteDimensional K L` implies `FiniteDimensional F L`
+-- automatically by typeclass resolution).
+private theorem eq_of_le_of_finrank_le'' [FiniteDimensional K L] (h_le : F ≤ E)
+    (h_finrank : finrank F L ≤ finrank E L) : F = E := by
+  apply eq_of_le_of_finrank_le h_le
+  have h1 := finrank_mul_finrank K F L
+  have h2 := finrank_mul_finrank K E L
+  have h3 : 0 < finrank E L := finrank_pos
+  nlinarith
+
+/-- If `F ≤ E` are two intermediate fields of `L / K` such that `[L : F] ≤ [L : E]` are finite,
+then `F = E`. -/
+theorem eq_of_le_of_finrank_le' [FiniteDimensional F L] (h_le : F ≤ E)
+    (h_finrank : finrank F L ≤ finrank E L) : F = E := by
+  refine le_antisymm h_le (fun l hl ↦ ?_)
+  rwa [← mem_extendScalars (le_refl F), eq_of_le_of_finrank_le''
+    ((extendScalars_le_extendScalars_iff (le_refl F) h_le).2 h_le) h_finrank, mem_extendScalars]
+
+/-- If `F ≤ E` are two intermediate fields of `L / K` such that `[L : F] = [L : E]` are finite,
+then `F = E`. -/
+theorem eq_of_le_of_finrank_eq' [FiniteDimensional F L] (h_le : F ≤ E)
+    (h_finrank : finrank F L = finrank E L) : F = E :=
+  eq_of_le_of_finrank_le' h_le h_finrank.le
+
+end FiniteDimensional
+
+theorem isAlgebraic_iff {x : S} : IsAlgebraic K x ↔ IsAlgebraic K (x : L) :=
+  (isAlgebraic_algebraMap_iff (algebraMap S L).injective).symm
+
+theorem isIntegral_iff {x : S} : IsIntegral K x ↔ IsIntegral K (x : L) := by
+  rw [← isAlgebraic_iff_isIntegral, isAlgebraic_iff, isAlgebraic_iff_isIntegral]
+
+theorem minpoly_eq (x : S) : minpoly K x = minpoly K (x : L) :=
+  (minpoly.algebraMap_eq (algebraMap S L).injective x).symm
+
+end IntermediateField
+
+/-- If `L/K` is algebraic, the `K`-subalgebras of `L` are all fields.  -/
+def subalgebraEquivIntermediateField [Algebra.IsAlgebraic K L] :
+    Subalgebra K L ≃o IntermediateField K L where
+  toFun S := S.toIntermediateField fun x hx => S.inv_mem_of_algebraic
+    (Algebra.IsAlgebraic.isAlgebraic ((⟨x, hx⟩ : S) : L))
+  invFun S := S.toSubalgebra
+  left_inv _ := toSubalgebra_toIntermediateField _ _
+  right_inv := toIntermediateField_toSubalgebra
+  map_rel_iff' := Iff.rfl
+
+@[simp]
+theorem mem_subalgebraEquivIntermediateField [Algebra.IsAlgebraic K L] {S : Subalgebra K L}
+    {x : L} : x ∈ subalgebraEquivIntermediateField S ↔ x ∈ S :=
+  Iff.rfl
+
+@[simp]
+theorem mem_subalgebraEquivIntermediateField_symm [Algebra.IsAlgebraic K L]
+    {S : IntermediateField K L} {x : L} :
+    x ∈ subalgebraEquivIntermediateField.symm S ↔ x ∈ S :=
+  Iff.rfl

Mathlib/FieldTheory/IntermediateField.lean → Mathlib/FieldTheory/IntermediateField/Basic.lean

@@ -3,9 +3,10 @@ Copyright (c) 2020 Anne Baanen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen
 -/
-import Mathlib.FieldTheory.Tower
-import Mathlib.RingTheory.Algebraic
-import Mathlib.FieldTheory.Minpoly.Basic
+import Mathlib.Algebra.Field.Subfield
+import Mathlib.Algebra.Polynomial.AlgebraMap
+import Mathlib.RingTheory.LocalRing.Basic
+import Mathlib.RingTheory.IntegralClosure.IsIntegral.Defs
 
 /-!
 # Intermediate fields
@@ -36,7 +37,7 @@ intermediate field, field extension
 -/
 
 
-open FiniteDimensional Polynomial
+open Polynomial
 
 open Polynomial
 
@@ -752,100 +753,4 @@ end Restrict
 
 end Tower
 
-section FiniteDimensional
-
-variable (F E : IntermediateField K L)
-
-instance finiteDimensional_left [FiniteDimensional K L] : FiniteDimensional K F :=
-  left K F L
-
-instance finiteDimensional_right [FiniteDimensional K L] : FiniteDimensional F L :=
-  right K F L
-
-@[simp]
-theorem rank_eq_rank_subalgebra : Module.rank K F.toSubalgebra = Module.rank K F :=
-  rfl
-
-@[simp]
-theorem finrank_eq_finrank_subalgebra : finrank K F.toSubalgebra = finrank K F :=
-  rfl
-
-variable {F} {E}
-
-@[simp]
-theorem toSubalgebra_eq_iff : F.toSubalgebra = E.toSubalgebra ↔ F = E := by
-  rw [SetLike.ext_iff, SetLike.ext'_iff, Set.ext_iff]
-  rfl
-
-/-- If `F ≤ E` are two intermediate fields of `L / K` such that `[E : K] ≤ [F : K]` are finite,
-then `F = E`. -/
-theorem eq_of_le_of_finrank_le [hfin : FiniteDimensional K E] (h_le : F ≤ E)
-    (h_finrank : finrank K E ≤ finrank K F) : F = E :=
-  haveI : Module.Finite K E.toSubalgebra := hfin
-  toSubalgebra_injective <| Subalgebra.eq_of_le_of_finrank_le h_le h_finrank
-
-/-- If `F ≤ E` are two intermediate fields of `L / K` such that `[F : K] = [E : K]` are finite,
-then `F = E`. -/
-theorem eq_of_le_of_finrank_eq [FiniteDimensional K E] (h_le : F ≤ E)
-    (h_finrank : finrank K F = finrank K E) : F = E :=
-  eq_of_le_of_finrank_le h_le h_finrank.ge
-
--- If `F ≤ E` are two intermediate fields of a finite extension `L / K` such that
--- `[L : F] ≤ [L : E]`, then `F = E`. Marked as private since it's a direct corollary of
--- `eq_of_le_of_finrank_le'` (the `FiniteDimensional K L` implies `FiniteDimensional F L`
--- automatically by typeclass resolution).
-private theorem eq_of_le_of_finrank_le'' [FiniteDimensional K L] (h_le : F ≤ E)
-    (h_finrank : finrank F L ≤ finrank E L) : F = E := by
-  apply eq_of_le_of_finrank_le h_le
-  have h1 := finrank_mul_finrank K F L
-  have h2 := finrank_mul_finrank K E L
-  have h3 : 0 < finrank E L := finrank_pos
-  nlinarith
-
-/-- If `F ≤ E` are two intermediate fields of `L / K` such that `[L : F] ≤ [L : E]` are finite,
-then `F = E`. -/
-theorem eq_of_le_of_finrank_le' [FiniteDimensional F L] (h_le : F ≤ E)
-    (h_finrank : finrank F L ≤ finrank E L) : F = E := by
-  refine le_antisymm h_le (fun l hl ↦ ?_)
-  rwa [← mem_extendScalars (le_refl F), eq_of_le_of_finrank_le''
-    ((extendScalars_le_extendScalars_iff (le_refl F) h_le).2 h_le) h_finrank, mem_extendScalars]
-
-/-- If `F ≤ E` are two intermediate fields of `L / K` such that `[L : F] = [L : E]` are finite,
-then `F = E`. -/
-theorem eq_of_le_of_finrank_eq' [FiniteDimensional F L] (h_le : F ≤ E)
-    (h_finrank : finrank F L = finrank E L) : F = E :=
-  eq_of_le_of_finrank_le' h_le h_finrank.le
-
-end FiniteDimensional
-
-theorem isAlgebraic_iff {x : S} : IsAlgebraic K x ↔ IsAlgebraic K (x : L) :=
-  (isAlgebraic_algebraMap_iff (algebraMap S L).injective).symm
-
-theorem isIntegral_iff {x : S} : IsIntegral K x ↔ IsIntegral K (x : L) := by
-  rw [← isAlgebraic_iff_isIntegral, isAlgebraic_iff, isAlgebraic_iff_isIntegral]
-
-theorem minpoly_eq (x : S) : minpoly K x = minpoly K (x : L) :=
-  (minpoly.algebraMap_eq (algebraMap S L).injective x).symm
-
 end IntermediateField
-
-/-- If `L/K` is algebraic, the `K`-subalgebras of `L` are all fields.  -/
-def subalgebraEquivIntermediateField [Algebra.IsAlgebraic K L] :
-    Subalgebra K L ≃o IntermediateField K L where
-  toFun S := S.toIntermediateField fun x hx => S.inv_mem_of_algebraic
-    (Algebra.IsAlgebraic.isAlgebraic ((⟨x, hx⟩ : S) : L))
-  invFun S := S.toSubalgebra
-  left_inv _ := toSubalgebra_toIntermediateField _ _
-  right_inv := toIntermediateField_toSubalgebra
-  map_rel_iff' := Iff.rfl
-
-@[simp]
-theorem mem_subalgebraEquivIntermediateField [Algebra.IsAlgebraic K L] {S : Subalgebra K L}
-    {x : L} : x ∈ subalgebraEquivIntermediateField S ↔ x ∈ S :=
-  Iff.rfl
-
-@[simp]
-theorem mem_subalgebraEquivIntermediateField_symm [Algebra.IsAlgebraic K L]
-    {S : IntermediateField K L} {x : L} :
-    x ∈ subalgebraEquivIntermediateField.symm S ↔ x ∈ S :=
-  Iff.rfl

Mathlib/FieldTheory/NormalClosure.lean

@@ -98,8 +98,8 @@ lemma isNormalClosure_normalClosure : IsNormalClosure F K (normalClosure F K L)
       SetLike.coe_subset_coe.mpr <| by apply le_iSup _ x)
   simp_rw [normalClosure, ← top_le_iff]
   refine fun x _ ↦ (IntermediateField.val _).injective.mem_set_image.mp ?_
-  change x.val ∈ IntermediateField.map (IntermediateField.val _) _
-  rw [IntermediateField.map_iSup]
+  rw [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, coe_val, ← IntermediateField.coe_val,
+    ← IntermediateField.coe_map, IntermediateField.map_iSup]
   refine (iSup_le fun f ↦ ?_ : normalClosure F K L ≤ _) x.2
   refine le_iSup_of_le (f.codRestrict _ fun x ↦ f.fieldRange_le_normalClosure ⟨x, rfl⟩) ?_
   rw [AlgHom.map_fieldRange, val, AlgHom.val_comp_codRestrict]

Mathlib/FieldTheory/SplittingField/IsSplittingField.lean

@@ -3,8 +3,8 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
-import Mathlib.FieldTheory.IntermediateField
 import Mathlib.RingTheory.Adjoin.Field
+import Mathlib.FieldTheory.IntermediateField.Basic
 
 /-!
 # Splitting fields

Mathlib/LinearAlgebra/JordanChevalley.lean

@@ -5,6 +5,7 @@ Authors: Oliver Nash
 -/
 import Mathlib.Dynamics.Newton
 import Mathlib.LinearAlgebra.Semisimple
+import Mathlib.LinearAlgebra.FreeModule.Finite.Matrix
 
 /-!
 # Jordan-Chevalley-Dunford decomposition

Mathlib/RingTheory/LittleWedderburn.lean

@@ -6,6 +6,7 @@ Authors: Johan Commelin, Eric Rodriguez
 import Mathlib.GroupTheory.ClassEquation
 import Mathlib.GroupTheory.GroupAction.ConjAct
 import Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
+import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
 
 /-!
 # Wedderburn's Little Theorem

Mathlib/Topology/Instances/Complex.lean

@@ -5,10 +5,10 @@ Authors: Xavier Roblot
 -/
 import Mathlib.Analysis.Complex.Basic
 import Mathlib.Data.Complex.FiniteDimensional
-import Mathlib.FieldTheory.IntermediateField
 import Mathlib.LinearAlgebra.FiniteDimensional
 import Mathlib.Topology.Algebra.Field
 import Mathlib.Topology.Algebra.UniformRing
+import Mathlib.FieldTheory.IntermediateField.Basic
 
 /-!
 # Some results about the topology of ℂ