# 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.IsTopologicalDivisionRing`.

source
class CompletableTopField (K : Type u_1) [Field K] [UniformSpace K] extends T0Space 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.

- t0 ⦃x y : K⦄ : Inseparable x y → x = y
- nice (F : Filter K) : Cauchy F → nhds 0 ⊓ F = ⊥ → Cauchy (Filter.map (fun (x : K) => x⁻¹) F)

Instances

source
@[instance 100]
instance UniformSpace.Completion.instNontrivialOfT0Space (K : Type u_1) [Field K] [UniformSpace K] [T0Space K] :
Nontrivial (Completion K)
source
def UniformSpace.Completion.hatInv {K : Type u_1} [Field K] [UniformSpace K] :
Completion K → Completion K

extension of inversion to the completion of a field.

Equations

- UniformSpace.Completion.hatInv = ⋯.extend fun (x : K) => ↑x⁻¹

Instances For

source
theorem UniformSpace.Completion.continuous_hatInv {K : Type u_1} [Field K] [UniformSpace K] [CompletableTopField K] {x : Completion K} (h : x ≠ 0) :
ContinuousAt hatInv x
source
instance UniformSpace.Completion.instInvCompletion {K : Type u_1} [Field K] [UniformSpace K] :
Inv (Completion K)

The value of `hat_inv` at zero is not really specified, although it's probably zero. Here we explicitly enforce the `inv_zero` axiom.

Equations

- UniformSpace.Completion.instInvCompletion = { inv := fun (x : UniformSpace.Completion K) => if x = 0 then 0 else x.hatInv }

source
theorem UniformSpace.Completion.hatInv_extends {K : Type u_1} [Field K] [UniformSpace K] [IsTopologicalDivisionRing K] {x : K} (h : x ≠ 0) :
(↑x).hatInv = ↑x⁻¹
source
theorem UniformSpace.Completion.coe_inv {K : Type u_1} [Field K] [UniformSpace K] [IsTopologicalDivisionRing K] [CompletableTopField K] (x : K) :
(↑x)⁻¹ = ↑x⁻¹
source
theorem UniformSpace.Completion.mul_hatInv_cancel {K : Type u_1} [Field K] [UniformSpace K] [IsTopologicalDivisionRing K] [CompletableTopField K] [IsUniformAddGroup K] {x : Completion K} (x_ne : x ≠ 0) :
x * x.hatInv = 1
source
instance UniformSpace.Completion.instField {K : Type u_1} [Field K] [UniformSpace K] [IsTopologicalDivisionRing K] [CompletableTopField K] [IsUniformAddGroup K] :
Field (Completion K)
Equations

- One or more equations did not get rendered due to their size.

source
instance UniformSpace.Completion.instIsTopologicalDivisionRing {K : Type u_1} [Field K] [UniformSpace K] [IsTopologicalDivisionRing K] [CompletableTopField K] [IsUniformAddGroup K] :
IsTopologicalDivisionRing (Completion K)
source
instance Subfield.completableTopField (L : Type u_2) [Field L] [UniformSpace L] [CompletableTopField L] (K : Subfield L) :
CompletableTopField ↥K
source
@[instance 100]
instance completableTopField_of_complete (L : Type u_3) [Field L] [UniformSpace L] [IsTopologicalDivisionRing L] [T0Space L] [CompleteSpace L] :
CompletableTopField L
source
theorem IsUniformInducing.completableTopField {α : Type u_3} {β : Type u_4} [Field β] [b : UniformSpace β] [CompletableTopField β] [Field α] [UniformSpace α] [T0Space α] {f : α →+* β} (hf : IsUniformInducing ⇑f) :
CompletableTopField α

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