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.

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.

Main Results

• krullTopology_t2 K L. For an integral field extension L/K, the topology krullTopology K L is Hausdorff.

• krullTopology_totallyDisconnected K L. For an integral field extension L/K, the topology krullTopology K L is totally disconnected.

• IntermediateField.finrank_eq_fixingSubgroup_index: given a Galois extension K/k and an intermediate field L, the [L : k] as a natural number is equal to the index of the fixing subgroup of L.

Notation

• In docstrings, we will write Gal(L/E) to denote the fixing subgroup of an intermediate field E. That is, Gal(L/E) is the subgroup of Gal(L/K) consisting of automorphisms that fix every element of E. In particular, we distinguish between Gal(L/E) and Gal(L/E), since the former is defined to be a subgroup of Gal(L/K), while the latter is a group in its own right.

Implementation Notes

• krullTopology K L is defined as an instance for type class inference.

def finiteExts (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] : Set (IntermediateField K L)

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.

Equations

• finiteExts K L = {E : IntermediateField K L | FiniteDimensional K ↥E}

def fixedByFinite (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] : Set (Subgroup Gal(L/K))

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.

Equations

• fixedByFinite K L = IntermediateField.fixingSubgroup '' finiteExts K L

@[deprecated IntermediateField.instFiniteSubtypeMemBot (since := "2025-03-16")]

theorem IntermediateField.finiteDimensional_bot (F : Type u_1) [Field F] {E : Type u_2} [Field E] [Algebra F E] : Module.Finite F ↥⊥

Alias of IntermediateField.instFiniteSubtypeMemBot.

@[deprecated IntermediateField.fixingSubgroup_bot (since := "2025-03-12")]

theorem IntermediateField.fixingSubgroup.bot {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] : ⊥.fixingSubgroup = ⊤

Alias of IntermediateField.fixingSubgroup_bot.

theorem top_fixedByFinite {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] : ⊤ ∈ fixedByFinite K L

If L/K is a field extension, then we have Gal(L/K) ∈ fixedByFinite K L.

@[deprecated IntermediateField.finiteDimensional_sup (since := "2025-03-16")]

theorem finiteDimensional_sup {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] (E1 E2 : IntermediateField K L) [FiniteDimensional K ↥E1] [FiniteDimensional K ↥E2] : FiniteDimensional K ↥(E1 ⊔ E2)

Alias of IntermediateField.finiteDimensional_sup.

def galBasis (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] : FilterBasis Gal(L/K)

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.

Equations

• galBasis K L = { sets := (fun (g : Subgroup Gal(L/K)) => g.carrier) '' fixedByFinite K L, nonempty := ⋯, inter_sets := ⋯ }

theorem mem_galBasis_iff (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] (U : Set Gal(L/K)) : U ∈ galBasis K L ↔ U ∈ (fun (g : Subgroup Gal(L/K)) => g.carrier) '' fixedByFinite K 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.

def galGroupBasis (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] : GroupFilterBasis Gal(L/K)

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.

Equations

• galGroupBasis K L = { toFilterBasis := galBasis K L, one' := ⋯, mul' := ⋯, inv' := ⋯, conj' := ⋯ }

instance krullTopology (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] : TopologicalSpace Gal(L/K)

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.

Equations

• krullTopology K L = (galGroupBasis K L).topology

instance instIsTopologicalGroupAlgEquiv (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] : IsTopologicalGroup Gal(L/K)

For a field extension L/K, the Krull topology on Gal(L/K) makes it a topological group.

theorem krullTopology_mem_nhds_one_iff (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] (s : Set Gal(L/K)) : s ∈ nhds 1 ↔ ∃ (E : IntermediateField K L), FiniteDimensional K ↥E ∧ ↑E.fixingSubgroup ⊆ s

theorem krullTopology_mem_nhds_one_iff_of_normal (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [Normal K L] (s : Set Gal(L/K)) : s ∈ nhds 1 ↔ ∃ (E : IntermediateField K L), FiniteDimensional K ↥E ∧ Normal K ↥E ∧ ↑E.fixingSubgroup ⊆ s

theorem IntermediateField.fixingSubgroup_isOpen {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (E : IntermediateField K L) [FiniteDimensional K ↥E] : IsOpen ↑E.fixingSubgroup

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_isClosed {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (E : IntermediateField K L) [FiniteDimensional K ↥E] : IsClosed ↑E.fixingSubgroup

Given a tower of fields L/E/K, with E/K finite, the subgroup Gal(L/E) ≤ Gal(L/K) is closed.

theorem krullTopology_t2 {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [Algebra.IsIntegral K L] : T2Space Gal(L/K)

If L/K is an algebraic extension, then the Krull topology on Gal(L/K) is Hausdorff.

instance instTotallySeparatedSpaceAlgEquivOfIsIntegral {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [Algebra.IsIntegral K L] : TotallySeparatedSpace Gal(L/K)

theorem krullTopology_isTotallySeparated {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [Algebra.IsIntegral K L] : IsTotallySeparated Set.univ

If L/K is an algebraic field extension, then the Krull topology on Gal(L/K) is totally disconnected.

@[deprecated krullTopology_isTotallySeparated (since := "2025-04-03")]

theorem krullTopology_totallyDisconnected {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [Algebra.IsIntegral K L] : IsTotallySeparated Set.univ

Alias of krullTopology_isTotallySeparated.

---

If L/K is an algebraic field extension, then the Krull topology on Gal(L/K) is totally disconnected.

instance krullTopology_discreteTopology_of_finiteDimensional (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] : DiscreteTopology Gal(L/K)

theorem IntermediateField.map_fixingSubgroup {k : Type u_1} {E : Type u_2} (K : Type u_3) [Field k] [Field E] [Field K] [Algebra k E] [Algebra k K] [Algebra E K] [IsScalarTower k E K] (L : IntermediateField k E) [Normal k E] : (map (IsScalarTower.toAlgHom k E K) L).fixingSubgroup = Subgroup.comap (AlgEquiv.restrictNormalHom E) L.fixingSubgroup

If K / E / k is a field extension tower with E / k normal, L is an intermediate field of E / k, then the fixing subgroup of L viewed as an intermediate field of K / k is equal to the preimage of the fixing subgroup of L viewed as an intermediate field of E / k under the natural map Aut(K / k) → Aut(E / k) (AlgEquiv.restrictNormalHom).

theorem IntermediateField.map_fixingSubgroup_index {k : Type u_1} {E : Type u_2} (K : Type u_3) [Field k] [Field E] [Field K] [Algebra k E] [Algebra k K] [Algebra E K] [IsScalarTower k E K] (L : IntermediateField k E) [Normal k E] [Normal k K] : (map (IsScalarTower.toAlgHom k E K) L).fixingSubgroup.index = L.fixingSubgroup.index

If K / E / k is a field extension tower with E / k and K / k normal, L is an intermediate field of E / k, then the index of the fixing subgroup of L viewed as an intermediate field of K / k is equal to the index of the fixing subgroup of L viewed as an intermediate field of E / k.

theorem IntermediateField.finrank_eq_fixingSubgroup_index {k : Type u_1} {K : Type u_3} [Field k] [Field K] [Algebra k K] (L : IntermediateField k K) [IsGalois k K] : Module.finrank k ↥L = L.fixingSubgroup.index

If K / k is a Galois extension, L is an intermediate field of K / k, then [L : k] as a natural number is equal to the index of the fixing subgroup of L.