Krull topology #
We define the Krull topology on L ≃ₐ[K] L
for an arbitrary field extension L/K
. In order to do
this, we first define a GroupFilterBasis
on L ≃ₐ[K] L
, whose sets are E.fixingSubgroup
for
all intermediate fields E
with E/K
finite dimensional.
Main Definitions #

finiteExts K L
. Given a field extensionL/K
, this is the set of intermediate fields that are finitedimensional overK
. 
fixedByFinite K L
. Given a field extensionL/K
,fixedByFinite K L
is the set of subsetsGal(L/E)
ofGal(L/K)
, whereE/K
is finite 
galBasis K L
. Given a field extensionL/K
, this is the filter basis onL ≃ₐ[K] L
whose sets areGal(L/E)
for intermediate fieldsE
withE/K
finite. 
galGroupBasis K L
. This is the same asgalBasis K L
, but with the added structure that it is a group filter basis onL ≃ₐ[K] L
, rather than just a filter basis. 
krullTopology K L
. Given a field extensionL/K
, this is the topology onL ≃ₐ[K] L
, induced by the group filter basisgalGroupBasis K L
.
Main Results #

krullTopology_t2 K L
. For an integral field extensionL/K
, the topologykrullTopology K L
is Hausdorff. 
krullTopology_totallyDisconnected K L
. For an integral field extensionL/K
, the topologykrullTopology K L
is totally disconnected.
Notations #
 In docstrings, we will write
Gal(L/E)
to denote the fixing subgroup of an intermediate fieldE
. That is,Gal(L/E)
is the subgroup ofL ≃ₐ[K] L
consisting of automorphisms that fix every element ofE
. In particular, we distinguish betweenL ≃ₐ[E] L
andGal(L/E)
, since the former is defined to be a subgroup ofL ≃ₐ[K] L
, while the latter is a group in its own right.
Implementation Notes #
krullTopology K L
is defined as an instance for type class inference.
Mapping intermediate fields along the identity does not change them
Mapping a finite dimensional intermediate field along an algebra equivalence gives a finitedimensional intermediate field.
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
Instances For
For a field extension L/K
, the intermediate field K
is finitedimensional over K
If L/K
is a field extension, then we have Gal(L/K) ∈ fixedByFinite K L
If E1
and E2
are finitedimensional intermediate fields, then so is their compositum.
This rephrases a result already in mathlib so that it is compatible with our type classes
An element of L ≃ₐ[K] L
is in Gal(L/E)
if and only if it fixes every element of E
The map E ↦ Gal(L/E)
is inclusionreversing
For a field extension L/K
, galGroupBasis K L
is the group filter basis on L ≃ₐ[K] L
whose sets are Gal(L/E)
for finite subextensions E/K
Instances For
For a field extension L/K
, krullTopology K L
is the topological space structure on
L ≃ₐ[K] L
induced by the group filter basis galGroupBasis K L
For a field extension L/K
, the Krull topology on L ≃ₐ[K] L
makes it a topological group.
Let L/E/K
be a tower of fields with E/K
finite. Then Gal(L/E)
is an open subgroup of
L ≃ₐ[K] L
.
Given a tower of fields L/E/K
, with E/K
finite, the subgroup Gal(L/E) ≤ L ≃ₐ[K] L
is
closed.
If L/K
is an algebraic field extension, then the Krull topology on L ≃ₐ[K] L
is
totally disconnected.