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
L ≃ₐ[K] L, whose sets are
all intermediate fields
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
galBasis K L. Given a field extension
L/K, this is the filter basis on
L ≃ₐ[K] Lwhose sets are
Gal(L/E)for intermediate fields
Main Results #
- 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] Lconsisting of automorphisms that fix every element of
E. In particular, we distinguish between
L ≃ₐ[E] Land
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 Lis defined as an instance for type class inference.
Mapping a finite dimensional intermediate field along an algebra equivalence gives a finite-dimensional intermediate field.
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
An element of
L ≃ₐ[K] L is in
Gal(L/E) if and only if it fixes every element of
E ↦ Gal(L/E) is inclusion-reversing
A subset of
L ≃ₐ[K] L is a member of
galBasis K L if and only if it is the underlying set
Gal(L/E) for some finite subextension
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
E/K finite, the subgroup
Gal(L/E) ≤ L ≃ₐ[K] L is