feat(FieldTheory/KrullTopology): define uniform group structure on galois group

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

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
 

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⟩

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 ϕ]⟩

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

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 :=

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 :=

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