mathlib documentation

topology.algebra.uniform_field

Completion of topological fields #

The goal of this file is to prove the main part of Proposition 7 of Bourbaki GT III 6.8 :

The completion hat K of a Hausdorff topological field is a field if the image under the mapping x ↦ x⁻¹ of every Cauchy filter (with respect to the additive uniform structure) which does not have a cluster point at 0 is a Cauchy filter (with respect to the additive uniform structure).

Bourbaki does not give any detail here, he refers to the general discussion of extending functions defined on a dense subset with values in a complete Hausdorff space. In particular the subtlety about clustering at zero is totally left to readers.

Note that the separated completion of a non-separated topological field is the zero ring, hence the separation assumption is needed. Indeed the kernel of the completion map is the closure of zero which is an ideal. Hence it's either zero (and the field is separated) or the full field, which implies one is sent to zero and the completion ring is trivial.

The main definition is completable_top_field which packages the assumptions as a Prop-valued type class and the main results are the instances field_completion and topological_division_ring_completion.

source
@[protected, instance]
def uniform_space.completion.nontrivial (K : Type u_1) [field K] [uniform_space K] [separated_space K] :
nontrivial (uniform_space.completion K)
source
@[class]
structure completable_top_field (K : Type u_1) [field K] [uniform_space K] :
Prop

A topological field is completable if it is separated and the image under the mapping x ↦ x⁻¹ of every Cauchy filter (with respect to the additive uniform structure) which does not have a cluster point at 0 is a Cauchy filter (with respect to the additive uniform structure). This ensures the completion is a field.

Instances
source
noncomputable def hat_inv {K : Type u_1} [field K] [uniform_space K] :
uniform_space.completion K → uniform_space.completion K

extension of inversion to the completion of a field.

Equations
source
theorem continuous_hat_inv {K : Type u_1} [field K] [uniform_space K] [completable_top_field K] {x : uniform_space.completion K} (h : x ≠ 0) :
continuous_at hat_inv x
source
@[protected, instance]
noncomputable def completion.has_inv {K : Type u_1} [field K] [uniform_space K] :
has_inv (uniform_space.completion K)
Equations
source
theorem hat_inv_extends {K : Type u_1} [field K] [uniform_space K] [topological_division_ring K] {x : K} (h : x ≠ 0) :
hat_inv ↑x = ↑x⁻¹
source
@[norm_cast]
theorem coe_inv {K : Type u_1} [field K] [uniform_space K] [topological_division_ring K] [completable_top_field K] (x : K) :
(↑x)⁻¹ = ↑x⁻¹
source
theorem mul_hat_inv_cancel {K : Type u_1} [field K] [uniform_space K] [topological_division_ring K] [completable_top_field K] [uniform_add_group K] {x : uniform_space.completion K} (x_ne : x ≠ 0) :
x * hat_inv x = 1
source
@[protected, instance]
noncomputable def field_completion {K : Type u_1} [field K] [uniform_space K] [topological_division_ring K] [completable_top_field K] [uniform_add_group K] :
field (uniform_space.completion K)
Equations
source
@[protected, instance]
def topological_division_ring_completion {K : Type u_1} [field K] [uniform_space K] [topological_division_ring K] [completable_top_field K] [uniform_add_group K] :
topological_division_ring (uniform_space.completion K)