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.

source

@[class]

structure completable_top_field (K : Type u_1) [field K] [uniform_space K] :

Prop

to_separated_space : separated_space K
nice : ∀ (F : filter K), cauchy F → nhds 0 ⊓ F = ⊥ → cauchy (filter.map (λ (x : K), x⁻¹) F)

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

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

noncomputable def uniform_space.completion.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

uniform_space.completion.hat_inv = uniform_space.completion.dense_inducing_coe.extend (λ (x : K), ↑x⁻¹)

source

theorem uniform_space.completion.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 uniform_space.completion.hat_inv x

source

@[protected, instance]

noncomputable def uniform_space.completion.has_inv {K : Type u_1} [field K] [uniform_space K] :

has_inv (uniform_space.completion K)

Equations

uniform_space.completion.has_inv = {inv := λ (x : uniform_space.completion K), ite (x = 0) 0 x.hat_inv}

source

theorem uniform_space.completion.hat_inv_extends {K : Type u_1} [field K] [uniform_space K] [topological_division_ring K] {x : K} (h : x ≠ 0) :

↑x.hat_inv = ↑x⁻¹

source

@[norm_cast]

theorem uniform_space.completion.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 uniform_space.completion.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 * x.hat_inv = 1

source

@[protected, instance]

noncomputable def uniform_space.completion.field {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

uniform_space.completion.field = {add := comm_ring.add (uniform_space.completion.comm_ring K), add_assoc := _, zero := comm_ring.zero (uniform_space.completion.comm_ring K), zero_add := _, add_zero := _, nsmul := comm_ring.nsmul (uniform_space.completion.comm_ring K), nsmul_zero' := _, nsmul_succ' := _, neg := comm_ring.neg (uniform_space.completion.comm_ring K), sub := comm_ring.sub (uniform_space.completion.comm_ring K), sub_eq_add_neg := _, zsmul := comm_ring.zsmul (uniform_space.completion.comm_ring K), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := comm_ring.int_cast (uniform_space.completion.comm_ring K), nat_cast := comm_ring.nat_cast (uniform_space.completion.comm_ring K), one := comm_ring.one (uniform_space.completion.comm_ring K), nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := comm_ring.mul (uniform_space.completion.comm_ring K), mul_assoc := _, one_mul := _, mul_one := _, npow := comm_ring.npow (uniform_space.completion.comm_ring K), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := has_inv.inv uniform_space.completion.has_inv, div := division_ring.div._default comm_ring.mul uniform_space.completion.field._proof_25 comm_ring.one uniform_space.completion.field._proof_26 uniform_space.completion.field._proof_27 comm_ring.npow uniform_space.completion.field._proof_28 uniform_space.completion.field._proof_29 has_inv.inv, div_eq_mul_inv := _, zpow := division_ring.zpow._default comm_ring.mul uniform_space.completion.field._proof_31 comm_ring.one uniform_space.completion.field._proof_32 uniform_space.completion.field._proof_33 comm_ring.npow uniform_space.completion.field._proof_34 uniform_space.completion.field._proof_35 has_inv.inv, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, rat_cast := division_ring.rat_cast._default comm_ring.add uniform_space.completion.field._proof_40 comm_ring.zero uniform_space.completion.field._proof_41 uniform_space.completion.field._proof_42 comm_ring.nsmul uniform_space.completion.field._proof_43 uniform_space.completion.field._proof_44 comm_ring.neg comm_ring.sub uniform_space.completion.field._proof_45 comm_ring.zsmul uniform_space.completion.field._proof_46 uniform_space.completion.field._proof_47 uniform_space.completion.field._proof_48 uniform_space.completion.field._proof_49 uniform_space.completion.field._proof_50 comm_ring.int_cast comm_ring.nat_cast comm_ring.one uniform_space.completion.field._proof_51 uniform_space.completion.field._proof_52 uniform_space.completion.field._proof_53 uniform_space.completion.field._proof_54 comm_ring.mul uniform_space.completion.field._proof_55 uniform_space.completion.field._proof_56 uniform_space.completion.field._proof_57 comm_ring.npow uniform_space.completion.field._proof_58 uniform_space.completion.field._proof_59 uniform_space.completion.field._proof_60 uniform_space.completion.field._proof_61 has_inv.inv (division_ring.div._default comm_ring.mul uniform_space.completion.field._proof_25 comm_ring.one uniform_space.completion.field._proof_26 uniform_space.completion.field._proof_27 comm_ring.npow uniform_space.completion.field._proof_28 uniform_space.completion.field._proof_29 has_inv.inv) uniform_space.completion.field._proof_62 (division_ring.zpow._default comm_ring.mul uniform_space.completion.field._proof_31 comm_ring.one uniform_space.completion.field._proof_32 uniform_space.completion.field._proof_33 comm_ring.npow uniform_space.completion.field._proof_34 uniform_space.completion.field._proof_35 has_inv.inv) uniform_space.completion.field._proof_63 uniform_space.completion.field._proof_64 uniform_space.completion.field._proof_65, mul_inv_cancel := _, inv_zero := _, rat_cast_mk := _, qsmul := division_ring.qsmul._default (… uniform_space.completion.field._proof_46 uniform_space.completion.field._proof_47 uniform_space.completion.field._proof_48 uniform_space.completion.field._proof_49 uniform_space.completion.field._proof_50 comm_ring.int_cast comm_ring.nat_cast comm_ring.one uniform_space.completion.field._proof_51 uniform_space.completion.field._proof_52 uniform_space.completion.field._proof_53 uniform_space.completion.field._proof_54 comm_ring.mul uniform_space.completion.field._proof_55 uniform_space.completion.field._proof_56 uniform_space.completion.field._proof_57 comm_ring.npow uniform_space.completion.field._proof_58 uniform_space.completion.field._proof_59 uniform_space.completion.field._proof_60 uniform_space.completion.field._proof_61 has_inv.inv (division_ring.div._default comm_ring.mul uniform_space.completion.field._proof_25 comm_ring.one uniform_space.completion.field._proof_26 uniform_space.completion.field._proof_27 comm_ring.npow uniform_space.completion.field._proof_28 uniform_space.completion.field._proof_29 has_inv.inv) uniform_space.completion.field._proof_62 (division_ring.zpow._default comm_ring.mul uniform_space.completion.field._proof_31 comm_ring.one uniform_space.completion.field._proof_32 uniform_space.completion.field._proof_33 comm_ring.npow uniform_space.completion.field._proof_34 uniform_space.completion.field._proof_35 has_inv.inv) uniform_space.completion.field._proof_63 uniform_space.completion.field._proof_64 uniform_space.completion.field._proof_65) comm_ring.add uniform_space.completion.field._proof_69 comm_ring.zero uniform_space.completion.field._proof_70 uniform_space.completion.field._proof_71 comm_ring.nsmul uniform_space.completion.field._proof_72 uniform_space.completion.field._proof_73 comm_ring.neg comm_ring.sub uniform_space.completion.field._proof_74 comm_ring.zsmul uniform_space.completion.field._proof_75 uniform_space.completion.field._proof_76 uniform_space.completion.field._proof_77 uniform_space.completion.field._proof_78 uniform_space.completion.field._proof_79 comm_ring.int_cast comm_ring.nat_cast comm_ring.one uniform_space.completion.field._proof_80 uniform_space.completion.field._proof_81 uniform_space.completion.field._proof_82 uniform_space.completion.field._proof_83 comm_ring.mul uniform_space.completion.field._proof_84 uniform_space.completion.field._proof_85 uniform_space.completion.field._proof_86 comm_ring.npow uniform_space.completion.field._proof_87 uniform_space.completion.field._proof_88 uniform_space.completion.field._proof_89 uniform_space.completion.field._proof_90, qsmul_eq_mul' := _}

source

@[protected, instance]

def uniform_space.completion.topological_division_ring {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)

source

@[protected, instance]

def subfield.completable_top_field (L : Type u_2) [field L] [uniform_space L] [completable_top_field L] (K : subfield L) :

completable_top_field ↥K

source

@[protected, instance]

def completable_top_field_of_complete (L : Type u_1) [field L] [uniform_space L] [topological_division_ring L] [separated_space L] [complete_space L] :

completable_top_field L