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 : 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)

theorem CompletableTopField.nice {K : Type u_1} : ∀ {inst : Field K} {inst_1 : UniformSpace K} [self : CompletableTopField K] (F : Filter K), Cauchy F → nhds 0 ⊓ F = ⊥ → Cauchy (Filter.map (fun (x : K) => x⁻¹) F)

@[instance 100]

instance UniformSpace.Completion.instNontrivialOfT0Space (K : Type u_1) [Field K] [UniformSpace K] [T0Space K] : Nontrivial (UniformSpace.Completion K)

Equations

• ⋯ = ⋯

def UniformSpace.Completion.hatInv {K : Type u_1} [Field K] [UniformSpace K] : UniformSpace.Completion K → UniformSpace.Completion K

extension of inversion to the completion of a field.

Equations

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

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

instance UniformSpace.Completion.instInvCompletion {K : Type u_1} [Field K] [UniformSpace K] : Inv (UniformSpace.Completion K)

Equations

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

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⁻¹

theorem UniformSpace.Completion.coe_inv {K : Type u_1} [Field K] [UniformSpace K] [TopologicalDivisionRing K] [CompletableTopField K] (x : K) : (↑K x)⁻¹ = ↑K x⁻¹

theorem UniformSpace.Completion.mul_hatInv_cancel {K : Type u_1} [Field K] [UniformSpace K] [TopologicalDivisionRing K] [CompletableTopField K] [UniformAddGroup K] {x : UniformSpace.Completion K} (x_ne : x ≠ 0) : x * x.hatInv = 1

instance UniformSpace.Completion.instField {K : Type u_1} [Field K] [UniformSpace K] [TopologicalDivisionRing K] [CompletableTopField K] [UniformAddGroup K] : Field (UniformSpace.Completion K)

Equations

• UniformSpace.Completion.instField = Field.mk ⋯ zpowRec ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ (fun (x : ℚ≥0) => HMul.hMul ↑x) ⋯ ⋯ (fun (x : ℚ) => HMul.hMul ↑x) ⋯

instance UniformSpace.Completion.instTopologicalDivisionRing {K : Type u_1} [Field K] [UniformSpace K] [TopologicalDivisionRing K] [CompletableTopField K] [UniformAddGroup K] : TopologicalDivisionRing (UniformSpace.Completion K)

Equations

• ⋯ = ⋯

instance Subfield.completableTopField (L : Type u_2) [Field L] [UniformSpace L] [CompletableTopField L] (K : Subfield L) : CompletableTopField ↥K

Equations

• ⋯ = ⋯

@[instance 100]

instance completableTopField_of_complete (L : Type u_3) [Field L] [UniformSpace L] [TopologicalDivisionRing L] [T0Space L] [CompleteSpace L] : CompletableTopField L

Equations

• ⋯ = ⋯

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.