mathlib3 documentation

field_theory.krull_topology

Krull topology #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 group_filter_basis on L ≃ₐ[K] L, whose sets are E.fixing_subgroup for all intermediate fields E with E/K finite dimensional.

Main Definitions #

finite_exts K L. Given a field extension L/K, this is the set of intermediate fields that are finite-dimensional over K.
fixed_by_finite K L. Given a field extension L/K, fixed_by_finite K L is the set of subsets Gal(L/E) of Gal(L/K), where E/K is finite
gal_basis 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.
gal_group_basis K L. This is the same as gal_basis K L, but with the added structure that it is a group filter basis on L ≃ₐ[K] L, rather than just a filter basis.
krull_topology K L. Given a field extension L/K, this is the topology on L ≃ₐ[K] L, induced by the group filter basis gal_group_basis K L.

Main Results #

krull_topology_t2 K L. For an integral field extension L/K, the topology krull_topology K L is Hausdorff.
krull_topology_totally_disconnected K L. For an integral field extension L/K, the topology krull_topology 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 #

krull_topology K L is defined as an instance for type class inference.

theorem intermediate_field.map_mono {K : Type u_1} {L : Type u_2} {M : Type u_3} [field K] [field L] [field M] [algebra K L] [algebra K M] {E1 E2 : intermediate_field K L} (e : L ≃ₐ[K] M) (h12 : E1 ≤ E2) :

intermediate_field.map e.to_alg_hom E1 ≤ intermediate_field.map e.to_alg_hom E2

Mapping intermediate fields along algebra equivalences preserves the partial order

theorem intermediate_field.map_id {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (E : intermediate_field K L) :

intermediate_field.map (alg_hom.id K L) E = E

Mapping intermediate fields along the identity does not change them

@[protected, instance]

def im_finite_dimensional {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] {E : intermediate_field K L} (σ : L ≃ₐ[K] L) [finite_dimensional K ↥E] :

finite_dimensional K ↥(intermediate_field.map σ.to_alg_hom E)

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

def finite_exts (K : Type u_1) [field K] (L : Type u_2) [field L] [algebra K L] :

set (intermediate_field K L)

Given a field extension L/K, finite_exts K L is the set of intermediate field extensions L/E/K such that E/K is finite

Equations

finite_exts K L = {E : intermediate_field K L | finite_dimensional K ↥E}

def fixed_by_finite (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, fixed_by_finite K L is the set of subsets Gal(L/E) of L ≃ₐ[K] L, where E/K is finite

Equations

fixed_by_finite K L = intermediate_field.fixing_subgroup '' finite_exts K L

theorem intermediate_field.finite_dimensional_bot (K : Type u_1) (L : Type u_2) [field K] [field L] [algebra K L] :

finite_dimensional K ↥⊥

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

theorem intermediate_field.fixing_subgroup.bot {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] :

⊥.fixing_subgroup = ⊤

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

theorem top_fixed_by_finite {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] :

⊤ ∈ fixed_by_finite K L

If L/K is a field extension, then we have Gal(L/K) ∈ fixed_by_finite K L

theorem finite_dimensional_sup {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (E1 E2 : intermediate_field K L) (h1 : finite_dimensional K ↥E1) (h2 : finite_dimensional K ↥E2) :

finite_dimensional 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 intermediate_field.mem_fixing_subgroup_iff {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (E : intermediate_field K L) (σ : L ≃ₐ[K] L) :

σ ∈ E.fixing_subgroup ↔ ∀ (x : L), 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 intermediate_field.fixing_subgroup.antimono {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] {E1 E2 : intermediate_field K L} (h12 : E1 ≤ E2) :

E2.fixing_subgroup ≤ E1.fixing_subgroup

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

def gal_basis (K : Type u_1) (L : Type u_2) [field K] [field L] [algebra K L] :

filter_basis (L ≃ₐ[K] L)

Given a field extension L/K, gal_basis 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

gal_basis K L = {sets := subgroup.carrier '' fixed_by_finite K L, nonempty := _, inter_sets := _}

theorem mem_gal_basis_iff (K : Type u_1) (L : Type u_2) [field K] [field L] [algebra K L] (U : set (L ≃ₐ[K] L)) :

U ∈ gal_basis K L ↔ U ∈ subgroup.carrier '' fixed_by_finite K L

A subset of L ≃ₐ[K] L is a member of gal_basis K L if and only if it is the underlying set of Gal(L/E) for some finite subextension E/K

def gal_group_basis (K : Type u_1) (L : Type u_2) [field K] [field L] [algebra K L] :

group_filter_basis (L ≃ₐ[K] L)

For a field extension L/K, gal_group_basis K L is the group filter basis on L ≃ₐ[K] L whose sets are Gal(L/E) for finite subextensions E/K

Equations

gal_group_basis K L = {to_filter_basis := gal_basis K L _inst_3, one' := _, mul' := _, inv' := _, conj' := _}

@[protected, instance]

def krull_topology (K : Type u_1) (L : Type u_2) [field K] [field L] [algebra K L] :

topological_space (L ≃ₐ[K] L)

For a field extension L/K, krull_topology K L is the topological space structure on L ≃ₐ[K] L induced by the group filter basis gal_group_basis K L

Equations

krull_topology K L = (gal_group_basis K L).topology

@[protected, instance]

def alg_equiv.topological_group (K : Type u_1) (L : Type u_2) [field K] [field L] [algebra K L] :

topological_group (L ≃ₐ[K] L)

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

theorem intermediate_field.fixing_subgroup_is_open {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (E : intermediate_field K L) [finite_dimensional K ↥E] :

is_open ↑(E.fixing_subgroup)

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 intermediate_field.fixing_subgroup_is_closed {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (E : intermediate_field K L) [finite_dimensional K ↥E] :

is_closed ↑(E.fixing_subgroup)

Given a tower of fields L/E/K, with E/K finite, the subgroup Gal(L/E) ≤ L ≃ₐ[K] L is closed.

theorem krull_topology_t2 {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (h_int : algebra.is_integral K L) :

t2_space (L ≃ₐ[K] L)

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

theorem krull_topology_totally_disconnected {K : Type u_1} {L : Type u_2} [field K] [field L] [algebra K L] (h_int : algebra.is_integral K L) :

is_totally_disconnected set.univ

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