mathlib3documentation

topology.algebra.uniform_field

Completion of topological fields #

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

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 uniform_space.completion.field and uniform_space.completion.topological_division_ring.

@[class]
structure completable_top_field (K : Type u_1) [field 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 of this typeclass
@[protected, instance]
noncomputable def uniform_space.completion.hat_inv {K : Type u_1} [field K]  :

extension of inversion to the completion of a field.

Equations
@[protected, instance]
noncomputable def uniform_space.completion.has_inv {K : Type u_1} [field K]  :
Equations
theorem uniform_space.completion.hat_inv_extends {K : Type u_1} [field K] {x : K} (h : x 0) :
@[norm_cast]
theorem uniform_space.completion.coe_inv {K : Type u_1} [field K] (x : K) :
@[protected, instance]
noncomputable def uniform_space.completion.field {K : Type u_1} [field K]  :
Equations
@[protected, instance]
@[protected, instance]
def subfield.completable_top_field (L : Type u_2) [field L] (K : subfield L) :
@[protected, instance]