# 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.

source
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}

Instances For

source
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

Instances For

source
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`.

source
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 := ⋯ }

Instances For

source
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`.

source
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' := ⋯ }

Instances For

source
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

source
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.

source
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
source
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
source
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)`.

source
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.

source
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.

source
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)
source
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.

source
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)
source
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`).

source
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`.

source
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`.