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.

theorem IntermediateField.map_id {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (E : IntermediateField K L) : IntermediateField.map (AlgHom.id K L) E = E

Mapping intermediate fields along the identity does not change them

instance im_finiteDimensional {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {E : IntermediateField K L} (σ : L ≃ₐ[K] L) [FiniteDimensional K ↥E] : FiniteDimensional K ↥(IntermediateField.map (↑σ) E)

Mapping a finite dimensional intermediate field along an algebra equivalence gives a finite-dimensional intermediate field.

Equations

• ⋯ = ⋯

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

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

theorem IntermediateField.finiteDimensional_bot (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] : FiniteDimensional K ↥⊥

For a field extension L/K, the intermediate field K is finite-dimensional over K

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

This lemma says that Gal(L/K) = L ≃ₐ[K] L

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

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

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

theorem IntermediateField.mem_fixingSubgroup_iff {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (E : IntermediateField K L) (σ : L ≃ₐ[K] L) : σ ∈ E.fixingSubgroup ↔ ∀ x ∈ E, σ x = x

An element of L ≃ₐ[K] L is in Gal(L/E) if and only if it fixes every element of E

theorem IntermediateField.fixingSubgroup.antimono {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {E1 : IntermediateField K L} {E2 : IntermediateField K L} (h12 : E1 ≤ E2) : E2.fixingSubgroup ≤ E1.fixingSubgroup

The map E ↦ Gal(L/E) is inclusion-reversing

def galBasis (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] : FilterBasis (L ≃ₐ[K] L)

Given a field extension L/K, galBasis K L is the filter basis on L ≃ₐ[K] L whose sets are Gal(L/E) for intermediate fields E with E/K finite dimensional

Equations

• galBasis K L = { sets := (fun (g : Subgroup (L ≃ₐ[K] L)) => 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 (L ≃ₐ[K] L)) : U ∈ galBasis K L ↔ U ∈ (fun (g : Subgroup (L ≃ₐ[K] L)) => g.carrier) '' fixedByFinite K L

A subset of L ≃ₐ[K] L 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 (L ≃ₐ[K] L)

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

instance krullTopology (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] : TopologicalSpace (L ≃ₐ[K] L)

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

instance instTopologicalGroupAlgEquiv (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] : TopologicalGroup (L ≃ₐ[K] L)

For a field extension L/K, the Krull topology on L ≃ₐ[K] L makes it a topological group.

Equations

• ⋯ = ⋯

theorem krullTopology_mem_nhds_one (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] (s : Set (L ≃ₐ[K] L)) : s ∈ nhds 1 ↔ ∃ (E : IntermediateField K L), FiniteDimensional 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 L ≃ₐ[K] L.

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) ≤ L ≃ₐ[K] L 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 (L ≃ₐ[K] L)

If L/K is an algebraic extension, then the Krull topology on L ≃ₐ[K] L is Hausdorff.

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

If L/K is an algebraic field extension, then the Krull topology on L ≃ₐ[K] L is totally disconnected.

@[simp]

theorem IntermediateField.fixingSubgroup_top (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] : ⊤.fixingSubgroup = ⊥

@[simp]

theorem IntermediateField.fixingSubgroup_bot (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] : ⊥.fixingSubgroup = ⊤

instance krullTopology_discreteTopology_of_finiteDimensional (K : Type) (L : Type) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] : DiscreteTopology (L ≃ₐ[K] L)

Equations

• ⋯ = ⋯