Documentation

Mathlib.Topology.Algebra.UniformField

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 CompletableTopField which packages the assumptions as a Prop-valued type class and the main results are the instances UniformSpace.Completion.Field and UniformSpace.Completion.TopologicalDivisionRing.

class CompletableTopField (K : Type u_1) [Field K] [UniformSpace K] extends T0Space :

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
    theorem CompletableTopField.nice {K : Type u_1} :
    ∀ {inst : Field K} {inst_1 : UniformSpace K} [self : CompletableTopField K] (F : Filter K), Cauchy Fnhds 0 F = Cauchy (Filter.map (fun (x : K) => x⁻¹) F)

    extension of inversion to the completion of a field.

    Equations
    • UniformSpace.Completion.hatInv = .extend fun (x : K) => K x⁻¹
    Instances For
      theorem UniformSpace.Completion.continuous_hatInv {K : Type u_1} [Field K] [UniformSpace K] [CompletableTopField K] {x : UniformSpace.Completion K} (h : x 0) :
      ContinuousAt UniformSpace.Completion.hatInv x
      Equations
      theorem UniformSpace.Completion.hatInv_extends {K : Type u_1} [Field K] [UniformSpace K] [TopologicalDivisionRing K] {x : K} (h : x 0) :
      (K x).hatInv = K x⁻¹
      Equations
      Equations
      • =
      @[instance 100]
      Equations
      • =
      theorem IsUniformInducing.completableTopField {α : Type u_3} {β : Type u_4} [Field β] [b : UniformSpace β] [CompletableTopField β] [Field α] [UniformSpace α] [T0Space α] {f : α →+* β} (hf : IsUniformInducing f) :

      The pullback of a completable topological field along a uniform inducing ring homomorphism is a completable topological field.