From ed125a4216d18273cb1b96d4c846d32b85d74faf Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 21 Aug 2024 07:40:16 +0000 Subject: [PATCH] chore: split FieldTheory/IntermediateField (#15692) --- Mathlib.lean | 3 +- Mathlib/Algebra/CharP/IntermediateField.lean | 2 +- Mathlib/FieldTheory/Adjoin.lean | 2 +- .../IntermediateField/Algebraic.lean | 118 ++++++++++++++++++ .../Basic.lean} | 105 +--------------- Mathlib/FieldTheory/NormalClosure.lean | 4 +- .../SplittingField/IsSplittingField.lean | 2 +- Mathlib/LinearAlgebra/JordanChevalley.lean | 1 + Mathlib/RingTheory/LittleWedderburn.lean | 1 + Mathlib/Topology/Instances/Complex.lean | 2 +- 10 files changed, 133 insertions(+), 107 deletions(-) create mode 100644 Mathlib/FieldTheory/IntermediateField/Algebraic.lean rename Mathlib/FieldTheory/{IntermediateField.lean => IntermediateField/Basic.lean} (86%) diff --git a/Mathlib.lean b/Mathlib.lean index 64a5a6d864010..fae3bab6b1d3c 100644 --- a/Mathlib.lean +++ b/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 diff --git a/Mathlib/Algebra/CharP/IntermediateField.lean b/Mathlib/Algebra/CharP/IntermediateField.lean index 9854b6a841e48..4424731754203 100644 --- a/Mathlib/Algebra/CharP/IntermediateField.lean +++ b/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 /-! diff --git a/Mathlib/FieldTheory/Adjoin.lean b/Mathlib/FieldTheory/Adjoin.lean index bb6ec619c92ea..ba316a0f73367 100644 --- a/Mathlib/FieldTheory/Adjoin.lean +++ b/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 diff --git a/Mathlib/FieldTheory/IntermediateField/Algebraic.lean b/Mathlib/FieldTheory/IntermediateField/Algebraic.lean new file mode 100644 index 0000000000000..c546c92eb2c36 --- /dev/null +++ b/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 diff --git a/Mathlib/FieldTheory/IntermediateField.lean b/Mathlib/FieldTheory/IntermediateField/Basic.lean similarity index 86% rename from Mathlib/FieldTheory/IntermediateField.lean rename to Mathlib/FieldTheory/IntermediateField/Basic.lean index 1f54cb6acfb38..580f2d03ea7f6 100644 --- a/Mathlib/FieldTheory/IntermediateField.lean +++ b/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 diff --git a/Mathlib/FieldTheory/NormalClosure.lean b/Mathlib/FieldTheory/NormalClosure.lean index a1d7bf881f7dd..128ea47d5bfd0 100644 --- a/Mathlib/FieldTheory/NormalClosure.lean +++ b/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] diff --git a/Mathlib/FieldTheory/SplittingField/IsSplittingField.lean b/Mathlib/FieldTheory/SplittingField/IsSplittingField.lean index 4ca9cadac0e55..6409f11b3f95e 100644 --- a/Mathlib/FieldTheory/SplittingField/IsSplittingField.lean +++ b/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 diff --git a/Mathlib/LinearAlgebra/JordanChevalley.lean b/Mathlib/LinearAlgebra/JordanChevalley.lean index 76d5f6488464f..b526d14e3ebcd 100644 --- a/Mathlib/LinearAlgebra/JordanChevalley.lean +++ b/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 diff --git a/Mathlib/RingTheory/LittleWedderburn.lean b/Mathlib/RingTheory/LittleWedderburn.lean index 0c6818c3c622f..bb054fb0dc9a4 100644 --- a/Mathlib/RingTheory/LittleWedderburn.lean +++ b/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 diff --git a/Mathlib/Topology/Instances/Complex.lean b/Mathlib/Topology/Instances/Complex.lean index d3dad6f31c97f..1bd41163d0387 100644 --- a/Mathlib/Topology/Instances/Complex.lean +++ b/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 ℂ