diff --git a/Mathlib.lean b/Mathlib.lean index 952307f7e36481..da5e424a0da608 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -4518,6 +4518,7 @@ public import Mathlib.FieldTheory.ChevalleyWarning public import Mathlib.FieldTheory.Differential.Basic public import Mathlib.FieldTheory.Differential.Liouville public import Mathlib.FieldTheory.Extension +public import Mathlib.FieldTheory.FinTrdeg public import Mathlib.FieldTheory.Finite.Basic public import Mathlib.FieldTheory.Finite.Extension public import Mathlib.FieldTheory.Finite.GaloisField diff --git a/Mathlib/Analysis/Calculus/FDeriv/Measurable.lean b/Mathlib/Analysis/Calculus/FDeriv/Measurable.lean index ff064c774c6fe5..305bb401e14bca 100644 --- a/Mathlib/Analysis/Calculus/FDeriv/Measurable.lean +++ b/Mathlib/Analysis/Calculus/FDeriv/Measurable.lean @@ -372,7 +372,7 @@ variable [CompleteSpace F] /-- The set of differentiability points of a function taking values in a complete space is Borel-measurable. -/ theorem measurableSet_of_differentiableAt : MeasurableSet { x | DifferentiableAt 𝕜 f x } := by - have : IsComplete (univ : Set (E →L[𝕜] F)) := complete_univ + have : IsComplete (univ : Set (E →L[𝕜] F)) := isComplete_univ convert! measurableSet_of_differentiableAt_of_isComplete 𝕜 f this simp @@ -700,7 +700,7 @@ variable [CompleteSpace F] Borel-measurable. -/ theorem measurableSet_of_differentiableWithinAt_Ici : MeasurableSet { x | DifferentiableWithinAt ℝ f (Ici x) x } := by - have : IsComplete (univ : Set F) := complete_univ + have : IsComplete (univ : Set F) := isComplete_univ convert! measurableSet_of_differentiableWithinAt_Ici_of_isComplete f this simp @@ -893,7 +893,7 @@ variable [CompleteSpace F] values in a complete space is Borel-measurable. -/ theorem measurableSet_of_differentiableAt_with_param (hf : Continuous f.uncurry) : MeasurableSet {p : α × E | DifferentiableAt 𝕜 (f p.1) p.2} := by - have : IsComplete (univ : Set (E →L[𝕜] F)) := complete_univ + have : IsComplete (univ : Set (E →L[𝕜] F)) := isComplete_univ convert! measurableSet_of_differentiableAt_of_isComplete_with_param hf this simp diff --git a/Mathlib/FieldTheory/FinTrdeg.lean b/Mathlib/FieldTheory/FinTrdeg.lean new file mode 100644 index 00000000000000..ee0c7d64506441 --- /dev/null +++ b/Mathlib/FieldTheory/FinTrdeg.lean @@ -0,0 +1,91 @@ +/- +Copyright (c) 2026 Aaron Liu. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Aaron Liu +-/ +module + +public import Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis +public import Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra +public import Mathlib.FieldTheory.IntermediateField.Adjoin.Basic + +/-! +# Extensions with Finite Transcendence Degree + +A field extension L/K has finite transcendence degree if +the transcendence degree of L over K is finite. +Equivalently, if L is an algebraic extension of a finitely generated field extension of K. +-/ + +public section + +open IntermediateField + +/-- A field extension L/K is said to have finite transcendence degree if there is some +intermediate extension L/E/K with E/K finitely generated and L/E algebraic. -/ +class FinTrdeg (K L : Type*) [Field K] [Field L] [Algebra K L] where + exists_fg_isAlgebraic (K L) : ∃ E : IntermediateField K L, E.FG ∧ Algebra.IsAlgebraic E L + +variable {K L : Type*} [Field K] [Field L] [Algebra K L] + +variable (K L) in +instance [Algebra.IsAlgebraic K L] : FinTrdeg K L where + exists_fg_isAlgebraic := ⟨⊥, IntermediateField.fg_bot, inferInstance⟩ + +variable (K L) in +instance [Algebra.EssFiniteType K L] : FinTrdeg K L where + exists_fg_isAlgebraic := ⟨⊤, IntermediateField.fg_top_iff.mpr ‹_›, inferInstance⟩ + +theorem finTrdeg_iff_trdeg : FinTrdeg K L ↔ Algebra.trdeg K L < .aleph0 := by + constructor + · intro ⟨E, fg, alg⟩ + rw [← trdeg_add_eq K E, trdeg_eq_zero_iff.2 alg, add_zero] + rw [← essFiniteType_iff, Algebra.essFiniteType_iff_exists_subalgebra] at fg + obtain ⟨S₀, M, fin, islocal⟩ := fg + rw [← trdeg_add_eq K S₀, trdeg_eq_zero_iff.2 islocal.isAlgebraic, add_zero] + exact trdeg_lt_aleph0_of_finiteType + · intro h + obtain ⟨s, hs⟩ := exists_isTranscendenceBasis K L + have fin : s.Finite := Cardinal.lt_aleph0_iff_set_finite.1 (hs.cardinalMk_eq_trdeg.trans_lt h) + constructor + refine ⟨adjoin K s, fg_adjoin_of_finite fin, ?_⟩ + have alg := hs.isAlgebraic_field + rwa [Subtype.range_coe] at alg + +alias ⟨_, FinTrdeg.of_trdeg⟩ := finTrdeg_iff_trdeg + +variable (K L) in +theorem trdeg_lt_aleph0 [FinTrdeg K L] : Algebra.trdeg K L < .aleph0 := + finTrdeg_iff_trdeg.mp ‹_› + +theorem FinTrdeg.trans (K E L : Type*) [Field K] [Field E] [Field L] + [Algebra K E] [Algebra K L] [Algebra E L] [IsScalarTower K E L] + [FinTrdeg K E] [FinTrdeg E L] : FinTrdeg K L := by + rw [finTrdeg_iff_trdeg, ← Cardinal.lift_lt_aleph0, ← lift_trdeg_add_eq K E L, + Cardinal.add_lt_aleph0_iff, Cardinal.lift_lt_aleph0, Cardinal.lift_lt_aleph0] + exact ⟨trdeg_lt_aleph0 K E, trdeg_lt_aleph0 E L⟩ + +theorem finite_of_isTranscendenceBasis [FinTrdeg K L] {ι : Type*} {x : ι → L} + (hx : IsTranscendenceBasis K x) : Finite ι := by + rw [← Cardinal.mk_lt_aleph0_iff, ← Cardinal.lift_lt_aleph0, + hx.lift_cardinalMk_eq_trdeg, Cardinal.lift_lt_aleph0] + exact trdeg_lt_aleph0 K L + +theorem finite_of_algebraicIndependent [FinTrdeg K L] {ι : Type*} {x : ι → L} + (hx : AlgebraicIndependent K x) : Finite ι := by + rw [← Cardinal.mk_lt_aleph0_iff, ← Cardinal.lift_lt_aleph0] + exact hx.lift_cardinalMk_le_trdeg.trans_lt (Cardinal.lift_lt_aleph0.mpr (trdeg_lt_aleph0 K L)) + +theorem FinTrdeg.of_isTranscendenceBasis {ι : Type*} [Finite ι] {x : ι → L} + (hx : IsTranscendenceBasis K x) : FinTrdeg K L := by + rw [finTrdeg_iff_trdeg, ← Cardinal.lift_lt_aleph0, + ← hx.lift_cardinalMk_eq_trdeg, Cardinal.lift_lt_aleph0] + exact Cardinal.mk_lt_aleph0 + +variable (K L) in +theorem exists_finset_isTranscendenceBasis [FinTrdeg K L] : + ∃ s : Finset L, IsTranscendenceBasis K ((↑) : s → L) := by + obtain ⟨s, hs⟩ := exists_isTranscendenceBasis K L + obtain ⟨s, rfl⟩ := Finset.mem_range_coe_iff.2 + (Set.finite_coe_iff.1 (finite_of_isTranscendenceBasis hs)) + exact ⟨s, hs⟩ diff --git a/Mathlib/FieldTheory/Galois/Basic.lean b/Mathlib/FieldTheory/Galois/Basic.lean index ca7c4c787c1f51..89aa72f61ae6ec 100644 --- a/Mathlib/FieldTheory/Galois/Basic.lean +++ b/Mathlib/FieldTheory/Galois/Basic.lean @@ -270,6 +270,16 @@ def fixingSubgroupEquiv : fixingSubgroup K ≃* Gal(E/K) where invFun ϕ := ⟨ϕ.restrictScalars _, ϕ.commutes⟩ map_mul' _ _ := by ext; rfl +@[simp] +theorem coe_fixingSubgroupEquiv_apply (σ : K.fixingSubgroup) : + ⇑(K.fixingSubgroupEquiv σ) = ⇑σ.1 := + rfl + +@[simp] +theorem coe_fixingSubgroupEquiv_symm_apply (σ : Gal(E/K)) : + ⇑(K.fixingSubgroupEquiv.symm σ).1 = ⇑σ := + rfl + theorem fixingSubgroup_fixedField [FiniteDimensional F E] : fixingSubgroup (fixedField H) = H := by have H_le : H ≤ fixingSubgroup (fixedField H) := (le_iff_le _ _).mp le_rfl suffices Nat.card H = Nat.card (fixingSubgroup (fixedField H)) by @@ -288,6 +298,16 @@ def subgroupEquivAlgEquiv [FiniteDimensional F E] (H : Subgroup Gal(E/F)) : H ≃* Gal(E/IntermediateField.fixedField H) := (MulEquiv.subgroupCongr (fixingSubgroup_fixedField H).symm).trans (fixingSubgroupEquiv _) +@[simp] +theorem coe_subgroupEquivAlgEquiv_apply [FiniteDimensional F E] (σ : H) : + ⇑(subgroupEquivAlgEquiv H σ) = ⇑σ.1 := + rfl + +@[simp] +theorem coe_subgroupEquivAlgEquiv_symm_apply [FiniteDimensional F E] (σ : Gal(E/fixedField H)) : + ⇑((subgroupEquivAlgEquiv H).symm σ).1 = ⇑σ := + rfl + instance fixedField.smul : SMul K (fixedField (fixingSubgroup K)) where smul x y := ⟨x * y, fun ϕ => by rw [smul_mul', show ϕ • (x : E) = ↑x from ϕ.2 x, show ϕ • (y : E) = ↑y from y.2 ϕ]⟩ diff --git a/Mathlib/FieldTheory/Galois/Infinite.lean b/Mathlib/FieldTheory/Galois/Infinite.lean index c8a3b0151ec980..bf011d287174fd 100644 --- a/Mathlib/FieldTheory/Galois/Infinite.lean +++ b/Mathlib/FieldTheory/Galois/Infinite.lean @@ -22,8 +22,6 @@ closed subgroups of the Galois group. In `K/k`, for any intermediate field `L` : -* `fixingSubgroup_isClosed` : the subgroup fixing `L` (`Gal(K/L)`) is closed. - * `fixedField_fixingSubgroup` : the field fixed by the subgroup fixing `L` is equal to `L` itself. @@ -61,26 +59,10 @@ open scoped Pointwise open FiniteGaloisIntermediateField AlgEquiv --Note: The `adjoin`s below are `FiniteGaloisIntermediateField.adjoin` +@[deprecated IntermediateField.isClosed_fixingSubgroup (since := "2026-05-14")] lemma fixingSubgroup_isClosed (L : IntermediateField k K) [IsGalois k K] : - IsClosed (L.fixingSubgroup : Set Gal(K/k)) where - isOpen_compl := isOpen_iff_mem_nhds.mpr fun σ h => by - apply mem_nhds_iff.mpr - rcases Set.not_subset.mp ((mem_fixingSubgroup_iff Gal(K/k)).not.mp h) with ⟨y, yL, ne⟩ - use σ • ((adjoin k {y}).1.fixingSubgroup : Set Gal(K/k)) - constructor - · intro f hf - rcases (Set.mem_smul_set.mp hf) with ⟨g, hg, eq⟩ - simp only [Set.mem_compl_iff, SetLike.mem_coe, ← eq] - apply (mem_fixingSubgroup_iff Gal(K/k)).not.mpr - push Not - use y - simp only [yL, smul_eq_mul, AlgEquiv.smul_def, AlgEquiv.mul_apply, ne_eq, true_and] - have : g y = y := (mem_fixingSubgroup_iff Gal(K/k)).mp hg y <| - adjoin_simple_le_iff.mp le_rfl - simpa only [this, ne_eq, AlgEquiv.smul_def] using! ne - · simp only [(IntermediateField.fixingSubgroup_isOpen (adjoin k {y}).1).smul σ, true_and] - use 1 - simp only [SetLike.mem_coe, smul_eq_mul, mul_one, and_true, Subgroup.one_mem] + IsClosed (L.fixingSubgroup : Set Gal(K/k)) := + IntermediateField.isClosed_fixingSubgroup L lemma fixedField_fixingSubgroup (L : IntermediateField k K) [IsGalois k K] : IntermediateField.fixedField L.fixingSubgroup = L := by @@ -150,21 +132,17 @@ lemma fixingSubgroup_fixedField (H : ClosedSubgroup Gal(K/k)) [IsGalois k K] : intro σ hσ by_contra h have nhds : H.carrierᶜ ∈ nhds σ := H.isClosed'.isOpen_compl.mem_nhds h - rw [GroupFilterBasis.nhds_eq (x₀ := σ) (galGroupBasis k K)] at nhds - rcases nhds with ⟨b, ⟨gp, ⟨L, hL, eq'⟩, eq⟩, sub⟩ - rw [← eq'] at eq - have := hL.out + rw [← map_mul_left_nhds_one, Filter.mem_map, krullTopology_mem_nhds_one_iff] at nhds + rcases nhds with ⟨L, hL, sub⟩ let L' : FiniteGaloisIntermediateField k K := { normalClosure k L K with finiteDimensional := normalClosure.is_finiteDimensional k L K isGalois := IsGalois.normalClosure k L K } - have compl : σ • L'.1.fixingSubgroup.carrier ⊆ H.carrierᶜ := by - rintro φ ⟨τ, hτ, muleq⟩ - have sub' : σ • b ⊆ H.carrierᶜ := Set.smul_set_subset_iff.mpr sub - apply sub' - simp only [← muleq, ← eq] - apply Set.smul_mem_smul_set - exact (L.fixingSubgroup_le (IntermediateField.le_normalClosure L) hτ) + have compl : σ • L'.1.fixingSubgroup.carrier ⊆ H.carrierᶜ := + calc σ • (SetLike.coe L'.1.fixingSubgroup) + _ ⊆ σ • (SetLike.coe L.fixingSubgroup) := + Set.smul_set_mono (fixingSubgroup_antitone (L.le_normalClosure)) + _ ⊆ H.carrierᶜ := Set.smul_set_subset_iff.mpr sub have fix : ∀ x ∈ IntermediateField.fixedField H.toSubgroup ⊓ ↑L', σ x = x := fun x hx ↦ ((mem_fixingSubgroup_iff Gal(K/k)).mp hσ) x hx.1 rw [restrict_fixedField H.1 L'.1] at fix @@ -195,7 +173,7 @@ lemma fixingSubgroup_fixedField (H : ClosedSubgroup Gal(K/k)) [IsGalois k K] : /-- The Galois correspondence from intermediate fields to closed subgroups. -/ def IntermediateFieldEquivClosedSubgroup [IsGalois k K] : IntermediateField k K ≃o (ClosedSubgroup Gal(K/k))ᵒᵈ where - toFun L := ⟨L.fixingSubgroup, fixingSubgroup_isClosed L⟩ + toFun L := ⟨L.fixingSubgroup, L.isClosed_fixingSubgroup⟩ invFun H := IntermediateField.fixedField H.1 left_inv L := fixedField_fixingSubgroup L right_inv H := by @@ -208,7 +186,7 @@ def IntermediateFieldEquivClosedSubgroup [IsGalois k K] : /-- The Galois correspondence as a `GaloisInsertion` -/ def GaloisInsertionIntermediateFieldClosedSubgroup [IsGalois k K] : GaloisInsertion (OrderDual.toDual ∘ fun (E : IntermediateField k K) ↦ - (⟨E.fixingSubgroup, fixingSubgroup_isClosed E⟩ : ClosedSubgroup Gal(K/k))) + (⟨E.fixingSubgroup, E.isClosed_fixingSubgroup⟩ : ClosedSubgroup Gal(K/k))) ((fun (H : ClosedSubgroup Gal(K/k)) ↦ IntermediateField.fixedField H) ∘ OrderDual.toDual) := OrderIso.toGaloisInsertion IntermediateFieldEquivClosedSubgroup @@ -240,13 +218,11 @@ set_option backward.isDefEq.respectTransparency false in open IntermediateField in theorem isOpen_iff_finite (L : IntermediateField k K) [IsGalois k K] : IsOpen L.fixingSubgroup.carrier ↔ FiniteDimensional k L := by - refine ⟨fun h ↦ ?_, fun h ↦ IntermediateField.fixingSubgroup_isOpen L⟩ + refine ⟨fun h ↦ ?_, fun h ↦ IntermediateField.isOpen_fixingSubgroup L⟩ have : (IntermediateFieldEquivClosedSubgroup.toFun L).carrier ∈ nhds 1 := IsOpen.mem_nhds h (congrFun rfl) - rw [GroupFilterBasis.nhds_one_eq] at this - rcases this with ⟨S, ⟨gp, ⟨M, hM, eq'⟩, eq⟩, sub⟩ - rw [← eq, ← eq'] at sub - have := hM.out + rw [krullTopology_mem_nhds_one_iff] at this + rcases this with ⟨M, hM, sub⟩ let L' : FiniteGaloisIntermediateField k K := { normalClosure k M K with finiteDimensional := normalClosure.is_finiteDimensional k M K diff --git a/Mathlib/FieldTheory/Galois/Profinite.lean b/Mathlib/FieldTheory/Galois/Profinite.lean index 1fa9e055db3ca3..a575fe88f8cd2d 100644 --- a/Mathlib/FieldTheory/Galois/Profinite.lean +++ b/Mathlib/FieldTheory/Galois/Profinite.lean @@ -163,7 +163,7 @@ theorem restrictNormalHom_continuous (L : IntermediateField k K) [Normal k L] : dsimp at this rw [hx y.1 ((IntermediateField.mem_lift y).mpr hy)] at this exact SetLike.coe_eq_coe.mp this - · exact ⟨IntermediateField.fixingSubgroup_isOpen (IntermediateField.lift L'), congrFun rfl⟩ + · exact ⟨IntermediateField.isOpen_fixingSubgroup (IntermediateField.lift L'), one_mem _⟩ set_option backward.isDefEq.respectTransparency false in lemma algEquivToLimit_continuous : Continuous (algEquivToLimit k K) := by @@ -326,9 +326,6 @@ noncomputable def continuousMulEquivToLimit [IsGalois k K] : continuous_toFun := algEquivToLimit_continuous continuous_invFun := mulEquivToLimit_symm_continuous -instance [IsGalois k K] : CompactSpace Gal(K/k) := - (continuousMulEquivToLimit k K).symm.compactSpace - /-- `Gal(K/k)` as a profinite group as there is a `ContinuousMulEquiv` to a `ProfiniteGrp` given above -/ noncomputable def profiniteGalGrp [IsGalois k K] : ProfiniteGrp := diff --git a/Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean b/Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean index 4356fb001bd12b..d9e76329ff3dda 100644 --- a/Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean +++ b/Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean @@ -93,7 +93,6 @@ lemma fg_top_iff : (⊤ : IntermediateField F E).FG ↔ Algebra.EssFiniteType F E := by constructor · intro ⟨s, hs⟩ - have : Algebra.FiniteType F (Algebra.adjoin F (s : Set E)) := .adjoin_of_finite s.finite_toSet have : Algebra.EssFiniteType (Algebra.adjoin F (s : Set E)) (adjoin F (s : Set E)) := .of_isLocalization _ (nonZeroDivisors _) have : Algebra.EssFiniteType F (adjoin F (s : Set E)) := @@ -124,6 +123,9 @@ lemma essFiniteType_iff {K : IntermediateField F E} : adjoin_map, ← Set.range_comp, Function.comp_def, ← AlgHom.fieldRange_eq_map] using! this exact ⟨fun ⟨s, _, hs⟩ ↦ ⟨s, hs⟩, fun ⟨s, hs⟩ ↦ ⟨s, hs ▸ subset_adjoin _ _, hs⟩⟩ +instance [Finite S] : Algebra.EssFiniteType F (adjoin F S) := + essFiniteType_iff.mpr (fg_adjoin_of_finite S.toFinite) + /-- A field is finitely generated if and only if it is essentially of finite type over its prime subfield. -/ theorem _root_.Field.fg_iff_essFiniteType : Field.FG F ↔ Algebra.EssFiniteType (⊥ : Subfield F) F := diff --git a/Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean b/Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean index e29255c21b390a..1925ce835c7ed8 100644 --- a/Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean +++ b/Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean @@ -554,6 +554,18 @@ theorem _root_.Polynomial.Irreducible.natDegree_dvd_finrank {f : K[X]} (hi : Irr contrapose hi rwa [hi, mul_zero] at key +instance : Algebra.IsAlgebraic K (⊥ : IntermediateField K L) where + isAlgebraic := by + intro ⟨x, hx⟩ + obtain ⟨c, rfl⟩ := hx + exact isAlgebraic_algebraMap c + +instance : Algebra.IsAlgebraic (⊤ : IntermediateField K L) L where + isAlgebraic := by + intro x + let xt : (⊤ : IntermediateField K L) := ⟨x, mem_top⟩ + exact isAlgebraic_algebraMap xt + -- TODO: generalize to `Sort` /-- A compositum of algebraic extensions is algebraic -/ theorem isAlgebraic_iSup {ι : Type*} {t : ι → IntermediateField K L} @@ -581,6 +593,10 @@ theorem finiteDimensional_adjoin {S : Set L} [Finite S] (hS : ∀ x ∈ S, IsInt have (x : S) := adjoin.finiteDimensional (hS x.1 x.2) exact finiteDimensional_iSup_of_finite +instance {S : Set L} [Finite S] [Algebra.IsIntegral K L] : + FiniteDimensional K (adjoin K S) := + finiteDimensional_adjoin fun _ _ => Algebra.IsIntegral.isIntegral _ + end PowerBasis /-- Algebra homomorphism `F⟮α⟯ →ₐ[F] K` are in bijection with the set of roots diff --git a/Mathlib/FieldTheory/KrullTopology.lean b/Mathlib/FieldTheory/KrullTopology.lean index f76f89179d1b37..17367d26a15e79 100644 --- a/Mathlib/FieldTheory/KrullTopology.lean +++ b/Mathlib/FieldTheory/KrullTopology.lean @@ -1,37 +1,31 @@ /- Copyright (c) 2022 Sebastian Monnet. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Sebastian Monnet +Authors: Sebastian Monnet, Aaron Liu -/ module +public import Mathlib.FieldTheory.FinTrdeg public import Mathlib.FieldTheory.Galois.Basic +public import Mathlib.Topology.Algebra.IsUniformGroup.Basic +-- this `import` is only used in the deprecated material at the bottom of the file +-- it should be removed when the deprecated material is removed public import Mathlib.Topology.Algebra.FilterBasis -public import Mathlib.Topology.Algebra.OpenSubgroup + +import Mathlib.Topology.Algebra.OpenSubgroup +import Mathlib.Topology.Connected.Separation +import Mathlib.Topology.UniformSpace.Separation /-! # Krull topology -We define the Krull topology on `Gal(L/K)` for an arbitrary field extension `L/K`. In order to do -this, we first define a `GroupFilterBasis` on `Gal(L/K)`, whose sets are `E.fixingSubgroup` for -all intermediate fields `E` with `E/K` finite dimensional. +We define the Krull topology on `Gal(L/K)` for an arbitrary field extension `L/K`, whose basic +open neighborhoods of `1` are given by `E.fixingSubgroup`, where `E` ranges over intermediate +field between `L` and `K` such that `E/K` is finitely generated. ## Main Definitions -- `finiteExts K L`. Given a field extension `L/K`, this is the set of intermediate fields that are - finite-dimensional over `K`. - -- `fixedByFinite K L`. Given a field extension `L/K`, `fixedByFinite K L` is the set of - subsets `Gal(L/E)` of `Gal(L/K)`, where `E/K` is finite - -- `galBasis K L`. Given a field extension `L/K`, this is the filter basis on `Gal(L/K)` whose - sets are `Gal(L/E)` for intermediate fields `E` with `E/K` finite. - -- `galGroupBasis K L`. This is the same as `galBasis K L`, but with the added structure - that it is a group filter basis on `Gal(L/K)`, rather than just a filter basis. - -- `krullTopology K L`. Given a field extension `L/K`, this is the topology on `Gal(L/K)`, induced - by the group filter basis `galGroupBasis K L`. +- `krullTopology K L`. Given a field extension `L/K`, this is the topology on `Gal(L/K)`. ## Main Results @@ -53,31 +47,404 @@ all intermediate fields `E` with `E/K` finite dimensional. ## Implementation Notes -- `krullTopology K L` is defined as an instance for type class inference. +We first define a `UniformGroup` structure on `Gal(L/K)`, +and use this to construct the Krull topology. +This lets us use the uniform structure to easily prove compactness of the Krull topology, +by showing it is complete and totally bounded. -/ -@[expose] public section +public section + +open Filter +open scoped Pointwise Uniformity + +variable {K L : Type*} [Field K] [Field L] [Algebra K L] + +variable (K L) in +/-- For a field extension `L/K`, we equiv `Gal(L/K)` with the left uniform structure. -/ +@[no_expose] +instance : UniformSpace Gal(L/K) := .ofCore + { uniformity := ⨅ x : L, 𝓟 {p | p.1 x = p.2 x} + refl := le_iInf fun _ => principal_mono.2 (SetRel.id_subset_iff.2 ⟨fun _ => rfl⟩) + symm := tendsto_iInf_iInf fun _ => Set.MapsTo.tendsto fun _ => Eq.symm + comp := le_iInf fun x => lift'_le (mem_iInf_of_mem x (mem_principal_self _)) + (principal_mono.2 (SetRel.isTrans_iff_comp_subset_self.1 ⟨fun _ _ _ => Eq.trans⟩)) } + +theorem krullTopology_uniformity_def : 𝓤 Gal(L/K) = ⨅ x : L, 𝓟 {p | p.1 x = p.2 x} := (rfl) + +open SetRel in +theorem krullTopology_mem_uniformity_iff {s : SetRel Gal(L/K) Gal(L/K)} : + s ∈ 𝓤 Gal(L/K) ↔ ∃ u : Finset L, ∀ σ τ : Gal(L/K), Set.EqOn σ τ u → σ ~[s] τ := by + rw [krullTopology_uniformity_def, Filter.mem_iInf_finite] + refine exists_congr fun u => ?_ + rw [Filter.iInf_principal_finset, Filter.mem_principal, Set.subset_def, Prod.forall] + refine forall_congr' fun σ => forall_congr' fun τ => imp_congr_left ?_ + rw [Set.mem_iInter₂] + rfl + +open SetRel IntermediateField in +theorem krullTopology_mem_uniformity_iff_fg {s : SetRel Gal(L/K) Gal(L/K)} : + s ∈ 𝓤 Gal(L/K) ↔ ∃ F : IntermediateField K L, + F.FG ∧ ∀ σ τ : Gal(L/K), Set.EqOn σ τ F → σ ~[s] τ := by + rw [krullTopology_mem_uniformity_iff] + simp_rw [FG, existsAndEq, true_and] + refine exists_congr fun u => forall_congr' fun σ => forall_congr' fun τ => imp_congr_left ?_ + unfold Set.EqOn + simp_rw [← AlgEquiv.symm_apply_eq, ← AlgEquiv.coe_inv, ← AlgEquiv.mul_apply] + have hst (σ : Gal(L/K)) (x : L) : σ x = x ↔ x ∈ fixedField (Subgroup.zpowers σ) := by + rw [← SetLike.mem_coe, ← Set.singleton_subset_iff, ← adjoin_le_iff, le_iff_le, + Subgroup.zpowers_le, ← AlgEquiv.smul_def, ← MulAction.mem_stabilizer_iff] + revert σ + rw [← SetLike.ext_iff, le_antisymm_iff, ← le_iff_le, adjoin_simple_le_iff] + constructor + · simp + · intro σ hσ + simpa using hσ ⟨x, mem_adjoin_simple_self K x⟩ + simp_rw [hst, ← Set.ofPred_subset_ofPred, SetLike.setOfPred_mem_eq, + Set.ofPred_mem_eq, SetLike.coe_subset_coe, adjoin_le_iff] + +variable (K L) in +/-- For a field extension `L/K`, `krullTopology K L` is the topological space structure on +`Gal(L/K)` induced by the uniform structure. -/ +instance krullTopology : TopologicalSpace Gal(L/K) := inferInstance + +variable (K L) in +/-- For a field extension `L/K`, the Krull topology on `Gal(L/K)` makes it a topological group. -/ +@[stacks 0BMJ "We define the Krull topology directly without proving the universal property"] +instance : IsLeftUniformGroup Gal(L/K) where + continuous_mul := by + rw [Uniform.continuous_iff'_left] + intro p + rw [nhds_eq_comap_uniformity', uniformity_prod, comap_inf, comap_comap, comap_comap, + krullTopology_uniformity_def, comap_iInf, comap_iInf, tendsto_iInf] + intro x + rw [tendsto_principal, eventually_inf] + refine ⟨{στ | στ.1 (p.2 x) = p.1 (p.2 x)}, ?_, {στ | στ.2 x = p.2 x}, ?_, ?_⟩ + · exact mem_iInf_of_mem (p.2 x) (by simp) + · exact mem_iInf_of_mem x (by simp) + · simp +contextual + continuous_inv := by + rw [Uniform.continuous_iff'_right] + intro p + rw [nhds_eq_comap_uniformity', krullTopology_uniformity_def, comap_iInf, tendsto_iInf] + intro x + apply tendsto_iInf' (p.symm x) + rw [comap_principal, tendsto_principal_principal] + intro σ hp + apply σ.eq_symm_apply.mpr + simpa using hp + uniformity_eq := by + rw [nhds_eq_comap_uniformity, comap_comap, krullTopology_uniformity_def, comap_iInf] + refine iInf_congr fun x => ?_ + simp [AlgEquiv.eq_symm_apply] + +open IntermediateField in +open scoped Topology in +lemma krullTopology_mem_nhds_one_iff' {s : Set Gal(L/K)} : + s ∈ 𝓝 1 ↔ ∃ E : IntermediateField K L, E.FG ∧ (E.fixingSubgroup : Set Gal(L/K)) ⊆ s := by + rw [nhds_eq_comap_uniformity', ← le_principal_iff, comap_le_iff_le_kernMap, + kernMap_principal, le_principal_iff, krullTopology_mem_uniformity_iff] + simp_rw [← Prod.forall', ← Set.ofPred_subset_ofPred, Prod.eta, Set.ofPred_mem_eq, + Set.subset_kernImage_iff, Set.preimage_ofPred_eq, Set.ofPred_subset, + FG, existsAndEq, true_and, Set.subset_def, SetLike.mem_coe, + IntermediateField.mem_fixingSubgroup_iff, Set.EqOn, AlgEquiv.one_apply] + refine exists_congr fun u => forall_congr' fun σ => imp_congr_left ?_ + revert σ + have hst (σ : Gal(L/K)) (x : L) : σ x = x ↔ x ∈ fixedField (Subgroup.zpowers σ) := by + rw [← SetLike.mem_coe, ← Set.singleton_subset_iff, ← adjoin_le_iff, le_iff_le, + Subgroup.zpowers_le, ← AlgEquiv.smul_def, ← MulAction.mem_stabilizer_iff] + revert σ + rw [← SetLike.ext_iff, le_antisymm_iff, ← le_iff_le, adjoin_simple_le_iff] + constructor + · simp + · intro σ hσ + simpa using hσ ⟨x, mem_adjoin_simple_self K x⟩ + simp_rw [hst, ← Set.ofPred_subset_ofPred, SetLike.setOfPred_mem_eq, + Set.ofPred_mem_eq, SetLike.coe_subset_coe, adjoin_le_iff, forall_true_iff] + +open IntermediateField in +open scoped Topology in +lemma krullTopology_mem_nhds_one_iff [Algebra.IsAlgebraic K L] {s : Set Gal(L/K)} : + s ∈ 𝓝 1 ↔ ∃ E : IntermediateField K L, + FiniteDimensional K E ∧ (E.fixingSubgroup : Set Gal(L/K)) ⊆ s := by + rw [krullTopology_mem_nhds_one_iff'] + refine exists_congr fun E => and_congr_left' ?_ + rw [← IntermediateField.essFiniteType_iff] + exact ⟨fun _ => Algebra.finite_of_essFiniteType_of_isAlgebraic, fun _ => inferInstance⟩ + +open scoped Topology in +lemma krullTopology_mem_nhds_one_iff_of_normal [Normal K L] {s : Set Gal(L/K)} : + s ∈ 𝓝 1 ↔ ∃ E : IntermediateField K L, + FiniteDimensional K E ∧ Normal K E ∧ (E.fixingSubgroup : Set Gal(L/K)) ⊆ s := by + rw [krullTopology_mem_nhds_one_iff] + refine ⟨fun ⟨E, _, hE⟩ ↦ ?_, fun ⟨E, hE⟩ ↦ ⟨E, hE.1, hE.2.2⟩⟩ + use (IntermediateField.normalClosure K E L) + simp only [normalClosure.is_finiteDimensional K E L, normalClosure.normal K E L, true_and] + exact le_trans (E.fixingSubgroup_antitone E.le_normalClosure) hE + +section KrullT2 + +open scoped Topology Filter + +/-- Let `L/E/K` be a tower of fields with `E/K` finitely generated. +Then `Gal(L/E)` is an open subgroup of `Gal(L/K)`. -/ +theorem IntermediateField.isOpen_fixingSubgroup (E : IntermediateField K L) + [Algebra.EssFiniteType K E] : IsOpen (E.fixingSubgroup : Set Gal(L/K)) := + Subgroup.isOpen_of_mem_nhds _ (krullTopology_mem_nhds_one_iff'.2 + ⟨E, essFiniteType_iff.1 ‹_›, subset_rfl⟩) + +@[deprecated (since := "2026-03-05")] +alias IntermediateField.fixingSubgroup_isOpen := IntermediateField.isOpen_fixingSubgroup + +/-- Given a tower of fields `L/E/K`, the subgroup `Gal(L/E) ≤ Gal(L/K)` is closed. -/ +theorem IntermediateField.isClosed_fixingSubgroup (E : IntermediateField K L) : + IsClosed (E.fixingSubgroup : Set Gal(L/K)) := by + have hx (x : E) : IsClosed ((adjoin K {(x : L)}).fixingSubgroup : Set Gal(L/K)) := + have : Algebra.EssFiniteType K (adjoin K {(x : L)}) := + essFiniteType_iff.2 (fg_adjoin_of_finite (Set.finite_singleton _)) + Subgroup.isClosed_of_isOpen _ (isOpen_fixingSubgroup _) + convert isClosed_iInter hx + ext g + simp only [SetLike.mem_coe, mem_fixingSubgroup_iff, Set.mem_iInter, Subtype.forall] + exact ⟨fun h a ha x hx => h x (adjoin_simple_le_iff.2 ha hx), + fun h x hx => h x hx x (mem_adjoin_simple_self K x)⟩ + +@[deprecated (since := "2026-03-05")] +alias IntermediateField.fixingSubgroup_isClosed := IntermediateField.isClosed_fixingSubgroup + +end KrullT2 + +section TotallySeparated + +instance : TotallySeparatedSpace Gal(L/K) := by + rw [totallySeparatedSpace_iff_exists_isClopen] + intro σ τ h_diff + have hστ : σ⁻¹ * τ ≠ 1 := by rwa [Ne, inv_mul_eq_one] + rcases DFunLike.exists_ne hστ with ⟨x, hx : (σ⁻¹ * τ) x ≠ x⟩ + let E := IntermediateField.adjoin K ({x} : Set L) + have fg : Algebra.EssFiniteType K E := + IntermediateField.essFiniteType_iff.2 + (IntermediateField.fg_adjoin_of_finite (Set.finite_singleton _)) + refine ⟨σ • E.fixingSubgroup, + ⟨E.isClosed_fixingSubgroup.leftCoset σ, E.isOpen_fixingSubgroup.leftCoset σ⟩, + ⟨1, E.fixingSubgroup.one_mem', mul_one σ⟩, ?_⟩ + simp only [Set.mem_compl_iff, mem_leftCoset_iff, SetLike.mem_coe, + IntermediateField.mem_fixingSubgroup_iff, not_forall] + exact ⟨x, IntermediateField.mem_adjoin_simple_self K x, hx⟩ + +/-- The Krull topology on `Gal(L/K)` is Hausdorff. -/ +instance krullTopology_t2 : T2Space Gal(L/K) := TotallySeparatedSpace.t2Space + +/-- The Krull topology on `Gal(L/K)` is totally separated. -/ +@[deprecated TotallySeparatedSpace.isTotallySeparated_univ (since := "2026-03-05")] +theorem krullTopology_isTotallySeparated : + IsTotallySeparated (Set.univ : Set Gal(L/K)) := + (totallySeparatedSpace_iff _).mp inferInstance + +end TotallySeparated + +variable (K L) in +instance krullTopology_discreteUniformity_of_essFiniteType + [Algebra.EssFiniteType K L] : DiscreteUniformity Gal(L/K) := by + rw [discreteUniformity_iff_eq_principal_setRelId, le_antisymm_iff, + and_iff_left refl_le_uniformity, krullTopology_uniformity_def] + obtain ⟨s, hs⟩ := IntermediateField.fg_top K L + rw [Filter.le_principal_iff, Filter.mem_iInf_finite] + refine ⟨s, ?_⟩ + rw [Filter.iInf_principal_finset, Filter.mem_principal] + intro p hp + rw [Set.mem_iInter₂] at hp + have hpe (x : L) : p.1 x = p.2 x ↔ + x ∈ IntermediateField.fixedField (Subgroup.zpowers (p.1⁻¹ * p.2)) := by + rw [← SetLike.mem_coe, ← Set.singleton_subset_iff, ← IntermediateField.adjoin_le_iff, + IntermediateField.le_iff_le, Subgroup.zpowers_le, ← p.1.eq_symm_apply, + ← AlgEquiv.coe_inv, ← AlgEquiv.mul_apply, ← AlgEquiv.smul_def, eq_comm, + ← MulAction.mem_stabilizer_iff] + generalize p.1⁻¹ * p.2 = σ + revert σ + rw [← SetLike.ext_iff, le_antisymm_iff, ← IntermediateField.le_iff_le, + IntermediateField.adjoin_simple_le_iff] + constructor + · simp + · intro σ hσ + simpa using hσ ⟨x, IntermediateField.mem_adjoin_simple_self K x⟩ + ext x + have hx : x ∈ (⊤ : IntermediateField K L) := IntermediateField.mem_top + rw [hpe] + revert x hx + rw [← SetLike.le_def, ← hs, IntermediateField.adjoin_le_iff] + intro x hx + rw [SetLike.mem_coe, ← hpe] + exact hp x hx + +open IntermediateField in +theorem AlgEquiv.isComplete_fixingSubgroup (E : IntermediateField K L) [FinTrdeg E L] : + IsComplete (E.fixingSubgroup : Set Gal(L/K)) := by + intro f hf hfE + rw [cauchy_iff] at hf + obtain ⟨_, hf⟩ := hf + obtain ⟨_, ⟨u, rfl⟩, alg⟩ := FinTrdeg.exists_fg_isAlgebraic E L + replace hf (F : IntermediateField K L) (_ : F.FG) : + ∃ σ : Gal(L/K), ∀ᶠ τ : Gal(L/K) in f, Set.EqOn σ τ F := by + obtain ⟨t, hf, ht⟩ := hf {p | Set.EqOn p.1 p.2 F} + (krullTopology_mem_uniformity_iff_fg.2 ⟨F, ‹_›, fun _ _ h => h⟩) + obtain ⟨σ, hσ⟩ := Filter.nonempty_of_mem hf + exact ⟨σ, Filter.eventually_of_mem hf fun τ hτ => @ht (σ, τ) ⟨hσ, hτ⟩⟩ + have h (x : L) : ∃ y, ∀ᶠ τ in f, y = τ x := + (hf (adjoin K {x}) (fg_adjoin_of_finite (Set.finite_singleton _))).elim + fun σ hσ => ⟨σ x, hσ.mono fun τ hτ => hτ (mem_adjoin_simple_self K x)⟩ + choose s hs using h + let σh : L →ₐ[E] L := + { toFun := s + map_zero' := (hs 0).exists.elim fun _ h => by simp [h] + map_one' := (hs 1).exists.elim fun _ h => by simp [h] + commutes' x := + ((hs x.1).and ((Filter.eventually_mem_principal _).filter_mono hfE)).exists.elim fun _ h => + by simp [h.1, (mem_fixingSubgroup_iff _ _).1 h.2] + map_add' x y := by + obtain ⟨τ, hτ⟩ := ((hs x).and ((hs y).and (hs (x + y)))).exists + simp [hτ.1, hτ.2.1, hτ.2.2] + map_mul' x y := by + obtain ⟨τ, hτ⟩ := ((hs x).and ((hs y).and (hs (x * y)))).exists + simp [hτ.1, hτ.2.1, hτ.2.2] } + let σ : Gal(L/E) := .ofBijective σh <| by + refine ⟨σh.injective, fun x => ?_⟩ + obtain ⟨su, hsu, hsuE⟩ := + (((Filter.eventually_all_finite u.finite_toSet).2 fun y hy => hs y).and + ((Filter.eventually_mem_principal _).filter_mono hfE)).exists + let Eu : IntermediateField E L := adjoin E (u : Set L) + let suE : Gal(L/E) := E.fixingSubgroupEquiv ⟨su, hsuE⟩ + have algm : Algebra.IsIntegral (Eu.map (suE : L →ₐ[E] L)) L := sorry + let mp : Polynomial (Eu.map (suE : L →ₐ[E] L)) := minpoly _ x + let p : Polynomial Eu := mp.map + ((IntermediateField.equivMap Eu (suE : L →ₐ[E] L)).symm : Eu.map (suE : L →ₐ[E] L) →+* Eu) + have hp0 : p ≠ 0 := by + unfold p + refine (Polynomial.map_ne_zero_iff ?_).mpr ?_ + · apply AlgEquiv.injective + unfold mp + apply minpoly.ne_zero + apply Algebra.IsIntegral.isIntegral + let S : Set L := p.rootSet L + have hS : S.Finite := Polynomial.rootSet_finite _ _ + obtain ⟨τ, hτ, hτE⟩ := + (((Filter.eventually_all_finite (u.finite_toSet.union hS)).2 + fun y hy => hs y).and ((Filter.eventually_mem_principal _).filter_mono hfE)).exists + suffices h : τ.symm x ∈ S from ⟨τ.symm x, by simp [hτ (τ.symm x) (Set.mem_union_right u h), σh]⟩ + let τE : Gal(L/E) := E.fixingSubgroupEquiv ⟨τ, hτE⟩ + have hττE : ⇑τ.symm = τE.symm := rfl + unfold S + rw [Polynomial.mem_rootSet_of_ne hp0] + unfold p + apply (τE : L →+* L).injective + rw [hττE, map_zero, Polynomial.aeval_def, Polynomial.hom_eval₂, + RingHom.coe_coe, τE.apply_symm_apply, Polynomial.eval₂_eq_eval_map, Polynomial.map_map] + stop + conv => + enter [1, 2, 1] + equals τE.symm.toRingHom.comp (algebraMap _ _) => ext; simp [AlgEquiv.] + stop + sorry + refine ⟨E.fixingSubgroupEquiv.symm σ, (E.fixingSubgroupEquiv.symm σ).2, fun U hU => ?_⟩ + rw [← map_mul_left_nhds_one, Filter.mem_map, krullTopology_mem_nhds_one_iff'] at hU + obtain ⟨F, fg, hF⟩ := hU + rw [← Set.image_subset_iff] at hF + refine Filter.mem_of_superset ?_ hF + obtain ⟨σ', hσ'⟩ := hf F fg + have eq : Set.EqOn σ σ' F := fun x hx => + ((hs x).and hσ').exists.elim fun _ h => h.1.trans (h.2 hx).symm + filter_upwards [hσ'] with τ hτ + refine ⟨_ * τ, (F.mem_fixingSubgroup_iff _).2 fun x hx => ?_, mul_inv_cancel_left _ τ⟩ + simp [AlgEquiv.symm_apply_eq, eq hx, hτ hx] + +theorem AlgEquiv.totallyBounded_fixingSubgroup + (E : IntermediateField K L) [Algebra.IsAlgebraic E L] : + TotallyBounded (E.fixingSubgroup : Set Gal(L/K)) := by + intro U hU + rw [krullTopology_mem_uniformity_iff] at hU + obtain ⟨s, hs⟩ := hU + let F := IntermediateField.adjoin E (s : Set L) + have : IsScalarTower K F L := ⟨fun a b c => smul_assoc a b.1 c⟩ + have : FiniteDimensional E F := + IntermediateField.finiteDimensional_adjoin fun _ _ => Algebra.IsIntegral.isIntegral _ + let f (σ : Gal(L/E)) : F →ₐ[E] L := σ.toAlgHom.comp (IsScalarTower.toAlgHom E F L) + refine ⟨Set.range (AlgEquiv.restrictScalars K ∘ Function.invFun f), + Set.finite_range _, fun σ hσ => ?_⟩ + let σE := E.fixingSubgroupEquiv ⟨σ, hσ⟩ + rw [Set.biUnion_range] + refine Set.mem_iUnion_of_mem (f σE) (hs σ _ fun x hx => ?_) + let xE : F := ⟨x, IntermediateField.mem_adjoin_of_mem E hx⟩ + have hf : f (Function.invFun f (f σE)) xE = f σE xE := + DFunLike.congr_fun (Function.invFun_eq ⟨σE, rfl⟩) xE + simpa [f, σE, xE] using hf.symm + +variable (K L) in +theorem AlgEquiv.totallyBounded_univ [Algebra.IsAlgebraic K L] : + TotallyBounded (Set.univ : Set Gal(L/K)) := by + rw [← Subgroup.coe_top, ← IntermediateField.fixingSubgroup_bot] + exact AlgEquiv.totallyBounded_fixingSubgroup ⊥ + +variable (K L) in +instance [FinTrdeg K L] : LocallyCompactSpace Gal(L/K) := sorry + +variable (K L) in +instance [FinTrdeg K L] : CompleteSpace Gal(L/K) := + IsLeftUniformGroup.completeSpace_of_weaklyLocallyCompactSpace + +variable (K L) in +open IntermediateField in +instance [Algebra.IsIntegral K L] : CompactSpace Gal(L/K) where + isCompact_univ := (AlgEquiv.totallyBounded_univ K L).isCompact_of_isComplete isComplete_univ + +section MulAction + +/-- The stabilizer in `Gal(L/K)` of any element in `L` is open for the Krull topology. -/ +theorem stabilizer_isOpen_of_isIntegral (x : L) : + IsOpen (MulAction.stabilizer Gal(L/K) x : Set Gal(L/K)) := by + open IntermediateField in + let E := adjoin K {x} + have hL : Algebra.EssFiniteType K E := IntermediateField.essFiniteType_iff.2 + (IntermediateField.fg_adjoin_of_finite (Set.finite_singleton _)) + convert! isOpen_fixingSubgroup E + ext g + simpa using (forall_mem_adjoin_smul_eq_self_iff K (S := {x}) g).symm + +end MulAction + +section deprecated -open scoped Pointwise +/-! +The definitions and theorems in this section were formerly implementation details +used in the definition of the Krull topology. Since the Krull topology is now defined in +terms of the uniform group structure on `Gal(L/K)`, they are now unused, +and have been deprecated without replacement. + +When this section is removed then the `public import Mathlib.Topology.Algebra.FilterBasis` at +the top of this file should be removed too. +-/ /-- Given a field extension `L/K`, `finiteExts K L` is the set of intermediate field extensions `L/E/K` such that `E/K` is finite. -/ +@[deprecated "deprecated without replacement" (since := "2026-03-05")] def finiteExts (K : Type*) [Field K] (L : Type*) [Field L] [Algebra K L] : Set (IntermediateField K L) := {E | FiniteDimensional K E} /-- Given a field extension `L/K`, `fixedByFinite K L` is the set of subsets `Gal(L/E)` of `Gal(L/K)`, where `E/K` is finite. -/ +@[deprecated "deprecated without replacement" (since := "2026-03-05")] def fixedByFinite (K L : Type*) [Field K] [Field L] [Algebra K L] : Set (Subgroup Gal(L/K)) := IntermediateField.fixingSubgroup '' finiteExts K L /-- If `L/K` is a field extension, then we have `Gal(L/K) ∈ fixedByFinite K L`. -/ +@[deprecated "deprecated without replacement" (since := "2026-03-05")] theorem top_fixedByFinite {K L : Type*} [Field K] [Field L] [Algebra K L] : ⊤ ∈ fixedByFinite K L := ⟨⊥, IntermediateField.instFiniteSubtypeMemBot K, IntermediateField.fixingSubgroup_bot⟩ /-- Given a field extension `L/K`, `galBasis K L` is the filter basis on `Gal(L/K)` whose sets are `Gal(L/E)` for intermediate fields `E` with `E/K` finite dimensional. -/ +@[deprecated "deprecated without replacement" (since := "2026-03-05")] def galBasis (K L : Type*) [Field K] [Field L] [Algebra K L] : FilterBasis Gal(L/K) where sets := (fun g => g.carrier) '' fixedByFinite K L nonempty := ⟨⊤, ⊤, top_fixedByFinite, rfl⟩ @@ -90,13 +457,14 @@ def galBasis (K L : Type*) [Field K] [Field L] [Algebra K L] : FilterBasis Gal(L /-- A subset of `Gal(L/K)` is a member of `galBasis K L` if and only if it is the underlying set of `Gal(L/E)` for some finite subextension `E/K`. -/ +@[deprecated "deprecated without replacement" (since := "2026-03-05")] theorem mem_galBasis_iff (K L : Type*) [Field K] [Field L] [Algebra K L] (U : Set Gal(L/K)) : U ∈ galBasis K L ↔ U ∈ (fun g => g.carrier) '' fixedByFinite K L := Iff.rfl /-- For a field extension `L/K`, `galGroupBasis K L` is the group filter basis on `Gal(L/K)` whose sets are `Gal(L/E)` for finite subextensions `E/K`. -/ -@[instance_reducible] +@[instance_reducible, deprecated "deprecated without replacement" (since := "2026-03-05")] def galGroupBasis (K L : Type*) [Field K] [Field L] [Algebra K L] : GroupFilterBasis Gal(L/K) where toFilterBasis := galBasis K L @@ -128,142 +496,4 @@ def galGroupBasis (K L : Type*) [Field K] [Field L] [Algebra K L] : change σ (σ⁻¹ x) = x exact AlgEquiv.apply_symm_apply σ x -/-- For a field extension `L/K`, `krullTopology K L` is the topological space structure on -`Gal(L/K)` induced by the group filter basis `galGroupBasis K L`. -/ -instance krullTopology (K L : Type*) [Field K] [Field L] [Algebra K L] : - TopologicalSpace Gal(L/K) := - GroupFilterBasis.topology (galGroupBasis K L) - -/-- For a field extension `L/K`, the Krull topology on `Gal(L/K)` makes it a topological group. -/ -@[stacks 0BMJ "We define Krull topology directly without proving the universal property"] -instance (K L : Type*) [Field K] [Field L] [Algebra K L] : IsTopologicalGroup Gal(L/K) := - GroupFilterBasis.isTopologicalGroup (galGroupBasis K L) - -open scoped Topology in -lemma krullTopology_mem_nhds_one_iff (K L : Type*) [Field K] [Field L] [Algebra K L] - (s : Set Gal(L/K)) : s ∈ 𝓝 1 ↔ ∃ E : IntermediateField K L, - FiniteDimensional K E ∧ (E.fixingSubgroup : Set Gal(L/K)) ⊆ s := by - rw [GroupFilterBasis.nhds_one_eq] - constructor - · rintro ⟨-, ⟨-, ⟨E, fin, rfl⟩, rfl⟩, hE⟩ - exact ⟨E, fin, hE⟩ - · rintro ⟨E, fin, hE⟩ - exact ⟨E.fixingSubgroup, ⟨E.fixingSubgroup, ⟨E, fin, rfl⟩, rfl⟩, hE⟩ - -open scoped Topology in -lemma krullTopology_mem_nhds_one_iff_of_normal (K L : Type*) [Field K] [Field L] [Algebra K L] - [Normal K L] (s : Set Gal(L/K)) : s ∈ 𝓝 1 ↔ ∃ E : IntermediateField K L, - FiniteDimensional K E ∧ Normal K E ∧ (E.fixingSubgroup : Set Gal(L/K)) ⊆ s := by - rw [krullTopology_mem_nhds_one_iff] - refine ⟨fun ⟨E, _, hE⟩ ↦ ?_, fun ⟨E, hE⟩ ↦ ⟨E, hE.1, hE.2.2⟩⟩ - use (IntermediateField.normalClosure K E L) - simp only [normalClosure.is_finiteDimensional K E L, normalClosure.normal K E L, true_and] - exact le_trans (E.fixingSubgroup_antitone E.le_normalClosure) hE - -section KrullT2 - -open scoped Topology Filter - -/-- Let `L/E/K` be a tower of fields with `E/K` finite. Then `Gal(L/E)` is an open subgroup of - `Gal(L/K)`. -/ -theorem IntermediateField.fixingSubgroup_isOpen {K L : Type*} [Field K] [Field L] [Algebra K L] - (E : IntermediateField K L) [FiniteDimensional K E] : - IsOpen (E.fixingSubgroup : Set Gal(L/K)) := by - have h_basis : E.fixingSubgroup.carrier ∈ galGroupBasis K L := - ⟨E.fixingSubgroup, ⟨E, ‹_›, rfl⟩, rfl⟩ - have h_nhds := GroupFilterBasis.mem_nhds_one (galGroupBasis K L) h_basis - exact Subgroup.isOpen_of_mem_nhds _ h_nhds - -/-- Given a tower of fields `L/E/K`, with `E/K` finite, the subgroup `Gal(L/E) ≤ Gal(L/K)` is - closed. -/ -theorem IntermediateField.fixingSubgroup_isClosed {K L : Type*} [Field K] [Field L] [Algebra K L] - (E : IntermediateField K L) [FiniteDimensional K E] : - IsClosed (E.fixingSubgroup : Set Gal(L/K)) := - OpenSubgroup.isClosed ⟨E.fixingSubgroup, E.fixingSubgroup_isOpen⟩ - -/-- If `L/K` is an algebraic extension, then the Krull topology on `Gal(L/K)` is Hausdorff. -/ -theorem krullTopology_t2 {K L : Type*} [Field K] [Field L] [Algebra K L] - [Algebra.IsIntegral K L] : T2Space Gal(L/K) := - { t2 := fun f g hfg => by - let φ := f⁻¹ * g - obtain ⟨x, hx⟩ := DFunLike.exists_ne hfg - have hφx : φ x ≠ x := by - apply ne_of_apply_ne f - change f (f.symm (g x)) ≠ f x - rw [AlgEquiv.apply_symm_apply f (g x), ne_comm] - exact hx - let E : IntermediateField K L := IntermediateField.adjoin K {x} - let h_findim : FiniteDimensional K E := IntermediateField.adjoin.finiteDimensional - (Algebra.IsIntegral.isIntegral x) - let H := E.fixingSubgroup - have h_basis : (H : Set Gal(L/K)) ∈ galGroupBasis K L := ⟨H, ⟨E, ⟨h_findim, rfl⟩⟩, rfl⟩ - have h_nhds := GroupFilterBasis.mem_nhds_one (galGroupBasis K L) h_basis - rw [mem_nhds_iff] at h_nhds - rcases h_nhds with ⟨W, hWH, hW_open, hW_1⟩ - refine ⟨f • W, g • W, - ⟨hW_open.leftCoset f, hW_open.leftCoset g, ⟨1, hW_1, mul_one _⟩, ⟨1, hW_1, mul_one _⟩, ?_⟩⟩ - rw [Set.disjoint_left] - rintro σ ⟨w1, hw1, h⟩ ⟨w2, hw2, rfl⟩ - dsimp at h - rw [eq_inv_mul_iff_mul_eq.symm, ← mul_assoc, mul_inv_eq_iff_eq_mul.symm] at h - have h_in_H : w1 * w2⁻¹ ∈ H := H.mul_mem (hWH hw1) (H.inv_mem (hWH hw2)) - rw [h] at h_in_H - change φ ∈ E.fixingSubgroup at h_in_H - rw [IntermediateField.mem_fixingSubgroup_iff] at h_in_H - specialize h_in_H x - have hxE : x ∈ E := by - apply IntermediateField.subset_adjoin - apply Set.mem_singleton - exact hφx (h_in_H hxE) } - -end KrullT2 - -section TotallySeparated - -instance {K L : Type*} [Field K] [Field L] [Algebra K L] [Algebra.IsIntegral K L] : - TotallySeparatedSpace Gal(L/K) := by - rw [totallySeparatedSpace_iff_exists_isClopen] - intro σ τ h_diff - have hστ : σ⁻¹ * τ ≠ 1 := by rwa [Ne, inv_mul_eq_one] - rcases DFunLike.exists_ne hστ with ⟨x, hx : (σ⁻¹ * τ) x ≠ x⟩ - let E := IntermediateField.adjoin K ({x} : Set L) - have := IntermediateField.adjoin.finiteDimensional - (Algebra.IsIntegral.isIntegral (R := K) x) - refine ⟨σ • E.fixingSubgroup, - ⟨E.fixingSubgroup_isClosed.leftCoset σ, E.fixingSubgroup_isOpen.leftCoset σ⟩, - ⟨1, E.fixingSubgroup.one_mem', mul_one σ⟩, ?_⟩ - simp only [Set.mem_compl_iff, mem_leftCoset_iff, SetLike.mem_coe, - IntermediateField.mem_fixingSubgroup_iff, not_forall] - exact ⟨x, IntermediateField.mem_adjoin_simple_self K x, hx⟩ - -/-- If `L/K` is an algebraic field extension, then the Krull topology on `Gal(L/K)` is - totally separated. -/ -theorem krullTopology_isTotallySeparated {K L : Type*} [Field K] [Field L] [Algebra K L] - [Algebra.IsIntegral K L] : IsTotallySeparated (Set.univ : Set Gal(L/K)) := - (totallySeparatedSpace_iff _).mp inferInstance - -end TotallySeparated - -instance krullTopology_discreteTopology_of_finiteDimensional (K L : Type*) [Field K] [Field L] - [Algebra K L] [FiniteDimensional K L] : DiscreteTopology Gal(L/K) := by - rw [discreteTopology_iff_isOpen_singleton_one] - change IsOpen ((⊥ : Subgroup Gal(L/K)) : Set Gal(L/K)) - rw [← IntermediateField.fixingSubgroup_top] - exact IntermediateField.fixingSubgroup_isOpen ⊤ - -section MulAction - -variable {K L : Type*} [Field K] [Field L] [Algebra K L] - -/-- If `L/K` is an algebraic field extension, then the stabilizer -in `Gal(L/K)` of any element in `L` is open for the Krull topology. -/ -theorem stabilizer_isOpen_of_isIntegral [Algebra.IsIntegral K L] (x : L) : - IsOpen (MulAction.stabilizer Gal(L/K) x : Set Gal(L/K)) := by - open IntermediateField in - let E := adjoin K {x} - have hL : FiniteDimensional K E := adjoin.finiteDimensional (Algebra.IsIntegral.isIntegral x) - convert! fixingSubgroup_isOpen E - ext g - simpa using (forall_mem_adjoin_smul_eq_self_iff K (S := {x}) g).symm - -end MulAction +end deprecated diff --git a/Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean b/Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean index 0f40c346fad4e0..1efe095719591e 100644 --- a/Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean +++ b/Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean @@ -343,23 +343,22 @@ lemma cyclotomicCharacter.continuous (p : ℕ) [Fact p.Prime] choose ζ hζ using H refine Continuous.of_coeHom_comp ?_ apply continuous_of_continuousAt_one - rw [ContinuousAt, map_one, (galGroupBasis K L).nhds_one_hasBasis.tendsto_iff - (Metric.nhds_basis_ball (α := ℤ_[p]) (x := 1))] + rw [Metric.continuousAt_iff'] intro ε hε + rw [Filter.eventually_iff, krullTopology_mem_nhds_one_iff] obtain ⟨k, hk', hk⟩ : ∃ k : ℕ, k ≠ 0 ∧ p ^ (-k : ℤ) < ε := by obtain ⟨k, hk⟩ := PadicInt.exists_pow_neg_lt p hε exact ⟨k + 1, by simp, lt_of_le_of_lt (by gcongr <;> simp [‹Fact p.Prime›.1.one_le]) hk⟩ - refine ⟨_, ⟨_, ⟨(K⟮ζ k⟯), adjoin.finiteDimensional ?_, rfl⟩, rfl⟩, ?_⟩ + refine ⟨(K⟮ζ k⟯), adjoin.finiteDimensional ?_, ?_⟩ · exact ((hζ k).isIntegral (Nat.pos_of_neZero _)).tower_top · intro σ hσ refine lt_of_le_of_lt ?_ hk dsimp rw [dist_eq_norm, PadicInt.norm_le_pow_iff_mem_span_pow, ← PadicInt.ker_toZModPow, - RingHom.mem_ker, map_sub, map_one, cyclotomicCharacter.toZModPow, - sub_eq_zero, eq_comm] + RingHom.mem_ker, map_one, map_one, Units.val_one, map_sub, map_one, + cyclotomicCharacter.toZModPow, sub_eq_zero, eq_comm] apply modularCyclotomicCharacter.unique intro t ht obtain ⟨i, hi, rfl⟩ := ((hζ k).isUnit_unit NeZero.out).eq_pow_of_mem_rootsOfUnity ht - rw [ZMod.val_one'', pow_one] - · exact hσ ⟨ζ k ^ i, pow_mem (mem_adjoin_simple_self K (ζ k)) _⟩ - · exact (one_lt_pow₀ ‹Fact p.Prime›.1.one_lt hk').ne' + rw [ZMod.val_one'' (one_lt_pow₀ (Nat.Prime.one_lt Fact.out) hk').ne', pow_one] + exact hσ ⟨ζ k ^ i, pow_mem (mem_adjoin_simple_self K (ζ k)) _⟩ diff --git a/Mathlib/NumberTheory/Padics/ProperSpace.lean b/Mathlib/NumberTheory/Padics/ProperSpace.lean index db68867d9bb6f2..2fe8af00160a22 100644 --- a/Mathlib/NumberTheory/Padics/ProperSpace.lean +++ b/Mathlib/NumberTheory/Padics/ProperSpace.lean @@ -54,7 +54,7 @@ theorem totallyBounded_univ : TotallyBounded (Set.univ : Set ℤ_[p]) := by /-- The set of p-adic integers `ℤ_[p]` is a compact topological space. -/ instance compactSpace : CompactSpace ℤ_[p] := by rw [← isCompact_univ_iff, isCompact_iff_totallyBounded_isComplete] - exact ⟨totallyBounded_univ p, complete_univ⟩ + exact ⟨totallyBounded_univ p, isComplete_univ⟩ end PadicInt diff --git a/Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean b/Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean index 3fc6d888aef1fc..4fbff1f01e5b53 100644 --- a/Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean +++ b/Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean @@ -451,7 +451,7 @@ theorem Polynomial.trdeg_of_isDomain [IsDomain R] : trdeg R (Polynomial R) = 1 : simpa using (IsTranscendenceBasis.polynomial Unit R).lift_cardinalMk_eq_trdeg.symm -- TODO: generalize to Nontrivial S -theorem trdeg_lt_aleph0 [IsDomain R] [fin : FiniteType R S] : trdeg R S < ℵ₀ := +theorem trdeg_lt_aleph0_of_finiteType [IsDomain R] [fin : FiniteType R S] : trdeg R S < ℵ₀ := have ⟨n, f, surj⟩ := FiniteType.iff_quotient_mvPolynomial''.mp fin lift_lt.mp <| (lift_trdeg_le_of_surjective f surj).trans_lt <| by simp diff --git a/Mathlib/RingTheory/FiniteType.lean b/Mathlib/RingTheory/FiniteType.lean index 1ba1ee31b36601..202202f7ca2440 100644 --- a/Mathlib/RingTheory/FiniteType.lean +++ b/Mathlib/RingTheory/FiniteType.lean @@ -202,6 +202,9 @@ lemma adjoin_of_finite {A : Type*} [CommSemiring A] [Algebra R A] {t : Set A} (h rw [← Subalgebra.fg_iff_finiteType] exact ⟨h.toFinset, by simp⟩ +instance {A : Type*} [CommSemiring A] [Algebra R A] {t : Set A} [Finite t] : + FiniteType R (Algebra.adjoin R t) := adjoin_of_finite t.toFinite + end FiniteType end Algebra diff --git a/Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean b/Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean index 4d82e9594a1417..8c749507e60e32 100644 --- a/Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean +++ b/Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean @@ -142,6 +142,12 @@ theorem Algebra.IsIntegral.adjoin {S : Set A} (hS : ∀ x ∈ S, IsIntegral R x) Algebra.IsIntegral R (adjoin R S) := le_integralClosure_iff_isIntegral.mp <| adjoin_le hS +instance [Algebra.IsIntegral R A] (S : Set A) : Algebra.IsIntegral R (Algebra.adjoin R S) := + Algebra.IsIntegral.adjoin fun _ _ => Algebra.IsIntegral.isIntegral _ + +instance [Algebra.IsIntegral R A] (S : Set A) [Finite S] : Module.Finite R (Algebra.adjoin R S) := + Algebra.IsIntegral.finite + theorem integralClosure_eq_top_iff : integralClosure R A = ⊤ ↔ Algebra.IsIntegral R A := by rw [← top_le_iff, le_integralClosure_iff_isIntegral, (Subalgebra.topEquiv (R := R) (A := A)).isIntegral_iff] -- explicit arguments for speedup diff --git a/Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean b/Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean index 8f8d8abf600ab1..e01cc473283d70 100644 --- a/Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean +++ b/Mathlib/Topology/Algebra/IsUniformGroup/Basic.lean @@ -86,23 +86,47 @@ variable {G : Type*} [Group G] [UniformSpace G] [IsRightUniformGroup G] /-- A locally compact right-uniform group is complete. -/ @[to_additive /-- A locally compact right-uniform additive group is complete. -/] +-- not an instance for performance reasons, see benchmark on PR #42117 theorem completeSpace_of_weaklyLocallyCompactSpace [WeaklyLocallyCompactSpace G] : CompleteSpace G where complete {f} hf := by open scoped RightActions in have : f.NeBot := hf.1 obtain ⟨K, K_compact, K_mem⟩ := WeaklyLocallyCompactSpace.exists_compact_mem_nhds (1 : G) - obtain ⟨x, hx⟩ : ∃ x, ∀ᶠ y in f, y / x ∈ K := by - rw [cauchy_iff_le, uniformity_eq_comap_nhds_one, ← tendsto_iff_comap] at hf + obtain ⟨x, hx⟩ : ∃ x, ∀ᶠ y in f, y * x⁻¹ ∈ K := by + rw [cauchy_iff_le, uniformity_eq_comap_mul_inv_nhds_one, ← tendsto_iff_comap] at hf exact hf.eventually_mem K_mem |>.curry.exists - simp_rw [div_eq_mul_inv, ← op_smul_eq_mul, MulOpposite.op_inv, - ← mem_smul_set_iff_inv_smul_mem] at hx + simp_rw [← op_smul_eq_mul, MulOpposite.op_inv, ← mem_smul_set_iff_inv_smul_mem] at hx have Kx_complete : IsComplete (K <• x) := K_compact.smul _ |>.isComplete obtain ⟨l, -, hl⟩ := Kx_complete f hf (by simpa using hx) exact ⟨l, hl⟩ end IsRightUniformGroup +namespace IsLeftUniformGroup + +variable {G : Type*} [Group G] [UniformSpace G] [IsLeftUniformGroup G] + +/-- A locally compact left-uniform group is complete. -/ +@[to_additive +/-- A locally compact left-uniform additive group is complete. -/] +-- not an instance for performance reasons, see benchmark on PR #42117 +theorem completeSpace_of_weaklyLocallyCompactSpace + [WeaklyLocallyCompactSpace G] : CompleteSpace G where + complete {f} hf := by + open scoped RightActions in + have : f.NeBot := hf.1 + obtain ⟨K, K_compact, K_mem⟩ := WeaklyLocallyCompactSpace.exists_compact_mem_nhds (1 : G) + obtain ⟨x, hx⟩ : ∃ x, ∀ᶠ y in f, x⁻¹ * y ∈ K := by + rw [cauchy_iff_le, uniformity_eq_comap_inv_mul_nhds_one, ← tendsto_iff_comap] at hf + exact hf.eventually_mem K_mem |>.curry.exists + simp_rw [← smul_eq_mul, ← mem_smul_set_iff_inv_smul_mem] at hx + have Kx_complete : IsComplete (x •> K) := K_compact.smul _ |>.isComplete + obtain ⟨l, -, hl⟩ := Kx_complete f hf (by simpa using hx) + exact ⟨l, hl⟩ + +end IsLeftUniformGroup + namespace Subgroup @[to_additive] diff --git a/Mathlib/Topology/UniformSpace/Cauchy.lean b/Mathlib/Topology/UniformSpace/Cauchy.lean index e32c38af6b5a53..146088998669cd 100644 --- a/Mathlib/Topology/UniformSpace/Cauchy.lean +++ b/Mathlib/Topology/UniformSpace/Cauchy.lean @@ -371,11 +371,13 @@ class CompleteSpace (α : Type u) [UniformSpace α] : Prop where /-- In a complete uniform space, every Cauchy filter converges. -/ complete : ∀ {f : Filter α}, Cauchy f → ∃ x, f ≤ 𝓝 x -theorem complete_univ {α : Type u} [UniformSpace α] [CompleteSpace α] : +theorem isComplete_univ {α : Type u} [UniformSpace α] [CompleteSpace α] : IsComplete (univ : Set α) := fun f hf _ => by rcases CompleteSpace.complete hf with ⟨x, hx⟩ exact ⟨x, mem_univ x, hx⟩ +@[deprecated (since := "2026-07-27")] alias complete_univ := isComplete_univ + instance CompleteSpace.prod [UniformSpace β] [CompleteSpace α] [CompleteSpace β] : CompleteSpace (α × β) where complete hf := @@ -413,7 +415,7 @@ theorem completeSpace_of_isComplete_univ (h : IsComplete (univ : Set α)) : Comp ⟨fun hf => let ⟨x, _, hx⟩ := h _ hf ((@principal_univ α).symm ▸ le_top); ⟨x, hx⟩⟩ theorem completeSpace_iff_isComplete_univ : CompleteSpace α ↔ IsComplete (univ : Set α) := - ⟨@complete_univ α _, completeSpace_of_isComplete_univ⟩ + ⟨@isComplete_univ α _, completeSpace_of_isComplete_univ⟩ theorem completeSpace_iff_ultrafilter : CompleteSpace α ↔ ∀ l : Ultrafilter α, Cauchy (l : Filter α) → ∃ x : α, ↑l ≤ 𝓝 x := by