Skip to content

Commit ed125a4

Browse files
kim-emkim-em
committed
chore: split FieldTheory/IntermediateField (#15692)
1 parent 40f53e8 commit ed125a4

File tree

10 files changed

+133
-107
lines changed

10 files changed

+133
-107
lines changed

‎Mathlib.lean‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2595,7 +2595,8 @@ import Mathlib.FieldTheory.Finite.Trace
25952595
import Mathlib.FieldTheory.Finiteness
25962596
import Mathlib.FieldTheory.Fixed
25972597
import Mathlib.FieldTheory.Galois
2598-
import Mathlib.FieldTheory.IntermediateField
2598+
import Mathlib.FieldTheory.IntermediateField.Algebraic
2599+
import Mathlib.FieldTheory.IntermediateField.Basic
25992600
import Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
26002601
import Mathlib.FieldTheory.IsAlgClosed.Basic
26012602
import Mathlib.FieldTheory.IsAlgClosed.Classification

‎Mathlib/Algebra/CharP/IntermediateField.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@ Copyright (c) 2024 Jz Pan. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Jz Pan
55
-/
6-
import Mathlib.FieldTheory.IntermediateField
76
import Mathlib.Algebra.CharP.ExpChar
7+
import Mathlib.FieldTheory.IntermediateField.Basic
88

99
/-!
1010

‎Mathlib/FieldTheory/Adjoin.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Thomas Browning, Patrick Lutz
55
-/
66
import Mathlib.Algebra.Algebra.Subalgebra.Directed
7-
import Mathlib.FieldTheory.IntermediateField
7+
import Mathlib.FieldTheory.IntermediateField.Algebraic
88
import Mathlib.FieldTheory.Separable
99
import Mathlib.FieldTheory.SplittingField.IsSplittingField
1010
import Mathlib.RingTheory.TensorProduct.Basic

‎Mathlib/FieldTheory/IntermediateField/Algebraic.lean‎

Lines changed: 118 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,118 @@
1+
/-
2+
Copyright (c) 2020 Anne Baanen. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Anne Baanen
5+
-/
6+
import Mathlib.FieldTheory.IntermediateField.Basic
7+
import Mathlib.RingTheory.Algebraic
8+
import Mathlib.FieldTheory.Tower
9+
import Mathlib.FieldTheory.Minpoly.Basic
10+
11+
/-!
12+
# Results on finite dimensionality and algebraicity of intermediate fields.
13+
-/
14+
15+
open FiniteDimensional
16+
17+
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
18+
{S : IntermediateField K L}
19+
20+
namespace IntermediateField
21+
22+
section FiniteDimensional
23+
24+
variable (F E : IntermediateField K L)
25+
26+
instance finiteDimensional_left [FiniteDimensional K L] : FiniteDimensional K F :=
27+
left K F L
28+
29+
instance finiteDimensional_right [FiniteDimensional K L] : FiniteDimensional F L :=
30+
right K F L
31+
32+
@[simp]
33+
theorem rank_eq_rank_subalgebra : Module.rank K F.toSubalgebra = Module.rank K F :=
34+
rfl
35+
36+
@[simp]
37+
theorem finrank_eq_finrank_subalgebra : finrank K F.toSubalgebra = finrank K F :=
38+
rfl
39+
40+
variable {F} {E}
41+
42+
@[simp]
43+
theorem toSubalgebra_eq_iff : F.toSubalgebra = E.toSubalgebra ↔ F = E := by
44+
rw [SetLike.ext_iff, SetLike.ext'_iff, Set.ext_iff]
45+
rfl
46+
47+
/-- If `F ≤ E` are two intermediate fields of `L / K` such that `[E : K] ≤ [F : K]` are finite,
48+
then `F = E`. -/
49+
theorem eq_of_le_of_finrank_le [hfin : FiniteDimensional K E] (h_le : F ≤ E)
50+
(h_finrank : finrank K E ≤ finrank K F) : F = E :=
51+
haveI : Module.Finite K E.toSubalgebra := hfin
52+
toSubalgebra_injective <| Subalgebra.eq_of_le_of_finrank_le h_le h_finrank
53+
54+
/-- If `F ≤ E` are two intermediate fields of `L / K` such that `[F : K] = [E : K]` are finite,
55+
then `F = E`. -/
56+
theorem eq_of_le_of_finrank_eq [FiniteDimensional K E] (h_le : F ≤ E)
57+
(h_finrank : finrank K F = finrank K E) : F = E :=
58+
eq_of_le_of_finrank_le h_le h_finrank.ge
59+
60+
-- If `F ≤ E` are two intermediate fields of a finite extension `L / K` such that
61+
-- `[L : F] ≤ [L : E]`, then `F = E`. Marked as private since it's a direct corollary of
62+
-- `eq_of_le_of_finrank_le'` (the `FiniteDimensional K L` implies `FiniteDimensional F L`
63+
-- automatically by typeclass resolution).
64+
private theorem eq_of_le_of_finrank_le'' [FiniteDimensional K L] (h_le : F ≤ E)
65+
(h_finrank : finrank F L ≤ finrank E L) : F = E := by
66+
apply eq_of_le_of_finrank_le h_le
67+
have h1 := finrank_mul_finrank K F L
68+
have h2 := finrank_mul_finrank K E L
69+
have h3 : 0 < finrank E L := finrank_pos
70+
nlinarith
71+
72+
/-- If `F ≤ E` are two intermediate fields of `L / K` such that `[L : F] ≤ [L : E]` are finite,
73+
then `F = E`. -/
74+
theorem eq_of_le_of_finrank_le' [FiniteDimensional F L] (h_le : F ≤ E)
75+
(h_finrank : finrank F L ≤ finrank E L) : F = E := by
76+
refine le_antisymm h_le (fun l hl ↦ ?_)
77+
rwa [← mem_extendScalars (le_refl F), eq_of_le_of_finrank_le''
78+
((extendScalars_le_extendScalars_iff (le_refl F) h_le).2 h_le) h_finrank, mem_extendScalars]
79+
80+
/-- If `F ≤ E` are two intermediate fields of `L / K` such that `[L : F] = [L : E]` are finite,
81+
then `F = E`. -/
82+
theorem eq_of_le_of_finrank_eq' [FiniteDimensional F L] (h_le : F ≤ E)
83+
(h_finrank : finrank F L = finrank E L) : F = E :=
84+
eq_of_le_of_finrank_le' h_le h_finrank.le
85+
86+
end FiniteDimensional
87+
88+
theorem isAlgebraic_iff {x : S} : IsAlgebraic K x ↔ IsAlgebraic K (x : L) :=
89+
(isAlgebraic_algebraMap_iff (algebraMap S L).injective).symm
90+
91+
theorem isIntegral_iff {x : S} : IsIntegral K x ↔ IsIntegral K (x : L) := by
92+
rw [← isAlgebraic_iff_isIntegral, isAlgebraic_iff, isAlgebraic_iff_isIntegral]
93+
94+
theorem minpoly_eq (x : S) : minpoly K x = minpoly K (x : L) :=
95+
(minpoly.algebraMap_eq (algebraMap S L).injective x).symm
96+
97+
end IntermediateField
98+
99+
/-- If `L/K` is algebraic, the `K`-subalgebras of `L` are all fields. -/
100+
def subalgebraEquivIntermediateField [Algebra.IsAlgebraic K L] :
101+
Subalgebra K L ≃o IntermediateField K L where
102+
toFun S := S.toIntermediateField fun x hx => S.inv_mem_of_algebraic
103+
(Algebra.IsAlgebraic.isAlgebraic ((⟨x, hx⟩ : S) : L))
104+
invFun S := S.toSubalgebra
105+
left_inv _ := toSubalgebra_toIntermediateField _ _
106+
right_inv := toIntermediateField_toSubalgebra
107+
map_rel_iff' := Iff.rfl
108+
109+
@[simp]
110+
theorem mem_subalgebraEquivIntermediateField [Algebra.IsAlgebraic K L] {S : Subalgebra K L}
111+
{x : L} : x ∈ subalgebraEquivIntermediateField S ↔ x ∈ S :=
112+
Iff.rfl
113+
114+
@[simp]
115+
theorem mem_subalgebraEquivIntermediateField_symm [Algebra.IsAlgebraic K L]
116+
{S : IntermediateField K L} {x : L} :
117+
x ∈ subalgebraEquivIntermediateField.symm S ↔ x ∈ S :=
118+
Iff.rfl

‎Mathlib/FieldTheory/IntermediateField.lean‎ renamed to ‎Mathlib/FieldTheory/IntermediateField/Basic.lean‎

Lines changed: 5 additions & 100 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,10 @@ Copyright (c) 2020 Anne Baanen. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Anne Baanen
55
-/
6-
import Mathlib.FieldTheory.Tower
7-
import Mathlib.RingTheory.Algebraic
8-
import Mathlib.FieldTheory.Minpoly.Basic
6+
import Mathlib.Algebra.Field.Subfield
7+
import Mathlib.Algebra.Polynomial.AlgebraMap
8+
import Mathlib.RingTheory.LocalRing.Basic
9+
import Mathlib.RingTheory.IntegralClosure.IsIntegral.Defs
910

1011
/-!
1112
# Intermediate fields
@@ -36,7 +37,7 @@ intermediate field, field extension
3637
-/
3738

3839

39-
open FiniteDimensional Polynomial
40+
open Polynomial
4041

4142
open Polynomial
4243

@@ -752,100 +753,4 @@ end Restrict
752753

753754
end Tower
754755

755-
section FiniteDimensional
756-
757-
variable (F E : IntermediateField K L)
758-
759-
instance finiteDimensional_left [FiniteDimensional K L] : FiniteDimensional K F :=
760-
left K F L
761-
762-
instance finiteDimensional_right [FiniteDimensional K L] : FiniteDimensional F L :=
763-
right K F L
764-
765-
@[simp]
766-
theorem rank_eq_rank_subalgebra : Module.rank K F.toSubalgebra = Module.rank K F :=
767-
rfl
768-
769-
@[simp]
770-
theorem finrank_eq_finrank_subalgebra : finrank K F.toSubalgebra = finrank K F :=
771-
rfl
772-
773-
variable {F} {E}
774-
775-
@[simp]
776-
theorem toSubalgebra_eq_iff : F.toSubalgebra = E.toSubalgebra ↔ F = E := by
777-
rw [SetLike.ext_iff, SetLike.ext'_iff, Set.ext_iff]
778-
rfl
779-
780-
/-- If `F ≤ E` are two intermediate fields of `L / K` such that `[E : K] ≤ [F : K]` are finite,
781-
then `F = E`. -/
782-
theorem eq_of_le_of_finrank_le [hfin : FiniteDimensional K E] (h_le : F ≤ E)
783-
(h_finrank : finrank K E ≤ finrank K F) : F = E :=
784-
haveI : Module.Finite K E.toSubalgebra := hfin
785-
toSubalgebra_injective <| Subalgebra.eq_of_le_of_finrank_le h_le h_finrank
786-
787-
/-- If `F ≤ E` are two intermediate fields of `L / K` such that `[F : K] = [E : K]` are finite,
788-
then `F = E`. -/
789-
theorem eq_of_le_of_finrank_eq [FiniteDimensional K E] (h_le : F ≤ E)
790-
(h_finrank : finrank K F = finrank K E) : F = E :=
791-
eq_of_le_of_finrank_le h_le h_finrank.ge
792-
793-
-- If `F ≤ E` are two intermediate fields of a finite extension `L / K` such that
794-
-- `[L : F] ≤ [L : E]`, then `F = E`. Marked as private since it's a direct corollary of
795-
-- `eq_of_le_of_finrank_le'` (the `FiniteDimensional K L` implies `FiniteDimensional F L`
796-
-- automatically by typeclass resolution).
797-
private theorem eq_of_le_of_finrank_le'' [FiniteDimensional K L] (h_le : F ≤ E)
798-
(h_finrank : finrank F L ≤ finrank E L) : F = E := by
799-
apply eq_of_le_of_finrank_le h_le
800-
have h1 := finrank_mul_finrank K F L
801-
have h2 := finrank_mul_finrank K E L
802-
have h3 : 0 < finrank E L := finrank_pos
803-
nlinarith
804-
805-
/-- If `F ≤ E` are two intermediate fields of `L / K` such that `[L : F] ≤ [L : E]` are finite,
806-
then `F = E`. -/
807-
theorem eq_of_le_of_finrank_le' [FiniteDimensional F L] (h_le : F ≤ E)
808-
(h_finrank : finrank F L ≤ finrank E L) : F = E := by
809-
refine le_antisymm h_le (fun l hl ↦ ?_)
810-
rwa [← mem_extendScalars (le_refl F), eq_of_le_of_finrank_le''
811-
((extendScalars_le_extendScalars_iff (le_refl F) h_le).2 h_le) h_finrank, mem_extendScalars]
812-
813-
/-- If `F ≤ E` are two intermediate fields of `L / K` such that `[L : F] = [L : E]` are finite,
814-
then `F = E`. -/
815-
theorem eq_of_le_of_finrank_eq' [FiniteDimensional F L] (h_le : F ≤ E)
816-
(h_finrank : finrank F L = finrank E L) : F = E :=
817-
eq_of_le_of_finrank_le' h_le h_finrank.le
818-
819-
end FiniteDimensional
820-
821-
theorem isAlgebraic_iff {x : S} : IsAlgebraic K x ↔ IsAlgebraic K (x : L) :=
822-
(isAlgebraic_algebraMap_iff (algebraMap S L).injective).symm
823-
824-
theorem isIntegral_iff {x : S} : IsIntegral K x ↔ IsIntegral K (x : L) := by
825-
rw [← isAlgebraic_iff_isIntegral, isAlgebraic_iff, isAlgebraic_iff_isIntegral]
826-
827-
theorem minpoly_eq (x : S) : minpoly K x = minpoly K (x : L) :=
828-
(minpoly.algebraMap_eq (algebraMap S L).injective x).symm
829-
830756
end IntermediateField
831-
832-
/-- If `L/K` is algebraic, the `K`-subalgebras of `L` are all fields. -/
833-
def subalgebraEquivIntermediateField [Algebra.IsAlgebraic K L] :
834-
Subalgebra K L ≃o IntermediateField K L where
835-
toFun S := S.toIntermediateField fun x hx => S.inv_mem_of_algebraic
836-
(Algebra.IsAlgebraic.isAlgebraic ((⟨x, hx⟩ : S) : L))
837-
invFun S := S.toSubalgebra
838-
left_inv _ := toSubalgebra_toIntermediateField _ _
839-
right_inv := toIntermediateField_toSubalgebra
840-
map_rel_iff' := Iff.rfl
841-
842-
@[simp]
843-
theorem mem_subalgebraEquivIntermediateField [Algebra.IsAlgebraic K L] {S : Subalgebra K L}
844-
{x : L} : x ∈ subalgebraEquivIntermediateField S ↔ x ∈ S :=
845-
Iff.rfl
846-
847-
@[simp]
848-
theorem mem_subalgebraEquivIntermediateField_symm [Algebra.IsAlgebraic K L]
849-
{S : IntermediateField K L} {x : L} :
850-
x ∈ subalgebraEquivIntermediateField.symm S ↔ x ∈ S :=
851-
Iff.rfl

‎Mathlib/FieldTheory/NormalClosure.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -98,8 +98,8 @@ lemma isNormalClosure_normalClosure : IsNormalClosure F K (normalClosure F K L)
9898
SetLike.coe_subset_coe.mpr <| by apply le_iSup _ x)
9999
simp_rw [normalClosure, ← top_le_iff]
100100
refine fun x _ ↦ (IntermediateField.val _).injective.mem_set_image.mp ?_
101-
change x.val ∈ IntermediateField.map (IntermediateField.val _) _
102-
rw [IntermediateField.map_iSup]
101+
rw [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, coe_val, ← IntermediateField.coe_val,
102+
← IntermediateField.coe_map, IntermediateField.map_iSup]
103103
refine (iSup_le fun f ↦ ?_ : normalClosure F K L ≤ _) x.2
104104
refine le_iSup_of_le (f.codRestrict _ fun x ↦ f.fieldRange_le_normalClosure ⟨x, rfl⟩) ?_
105105
rw [AlgHom.map_fieldRange, val, AlgHom.val_comp_codRestrict]

‎Mathlib/FieldTheory/SplittingField/IsSplittingField.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@ Copyright (c) 2018 Chris Hughes. All rights reserved.
33
Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Chris Hughes
55
-/
6-
import Mathlib.FieldTheory.IntermediateField
76
import Mathlib.RingTheory.Adjoin.Field
7+
import Mathlib.FieldTheory.IntermediateField.Basic
88

99
/-!
1010
# Splitting fields

‎Mathlib/LinearAlgebra/JordanChevalley.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ Authors: Oliver Nash
55
-/
66
import Mathlib.Dynamics.Newton
77
import Mathlib.LinearAlgebra.Semisimple
8+
import Mathlib.LinearAlgebra.FreeModule.Finite.Matrix
89

910
/-!
1011
# Jordan-Chevalley-Dunford decomposition

‎Mathlib/RingTheory/LittleWedderburn.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ Authors: Johan Commelin, Eric Rodriguez
66
import Mathlib.GroupTheory.ClassEquation
77
import Mathlib.GroupTheory.GroupAction.ConjAct
88
import Mathlib.RingTheory.Polynomial.Cyclotomic.Eval
9+
import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
910

1011
/-!
1112
# Wedderburn's Little Theorem

‎Mathlib/Topology/Instances/Complex.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,10 +5,10 @@ Authors: Xavier Roblot
55
-/
66
import Mathlib.Analysis.Complex.Basic
77
import Mathlib.Data.Complex.FiniteDimensional
8-
import Mathlib.FieldTheory.IntermediateField
98
import Mathlib.LinearAlgebra.FiniteDimensional
109
import Mathlib.Topology.Algebra.Field
1110
import Mathlib.Topology.Algebra.UniformRing
11+
import Mathlib.FieldTheory.IntermediateField.Basic
1212

1313
/-!
1414
# Some results about the topology of ℂ

0 commit comments

Comments
 (0)