# 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 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`L ≃ₐ[K] L`

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`L ≃ₐ[K] L`

, rather than just a filter basis.`krullTopology K L`

. Given a field extension`L/K`

, this is the topology on`L ≃ₐ[K] L`

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

## Notations #

- 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`L ≃ₐ[K] L`

consisting of automorphisms that fix every element of`E`

. In particular, we distinguish between`L ≃ₐ[E] L`

and`Gal(L/E)`

, since the former is defined to be a subgroup of`L ≃ₐ[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 finite-dimensional intermediate field.

## Equations

- ⋯ = ⋯

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

Given a field extension `L/K`

, `fixedByFinite K L`

is the set of
subsets `Gal(L/E)`

of `L ≃ₐ[K] L`

, where `E/K`

is finite

## Equations

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

## Instances For

If `L/K`

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

If `E1`

and `E2`

are finite-dimensional intermediate fields, then so is their compositum.
This rephrases a result already in mathlib so that it is compatible with our type classes

The map `E ↦ Gal(L/E)`

is inclusion-reversing

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`

## Equations

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

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

## Equations

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

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.

## Equations

- ⋯ = ⋯