Completion of a complete space

Stream: Is there code for X?

[Xavier Roblot]

I was not able to find the following in mathlib. Is it missing? It's true that the proof is quite straightforward but I think it could be useful to have.

import topology.uniform_space.abstract_completion

noncomputable def abstract_completion.complete_equiv_self {α : Type*} [uniform_space α]
[separated_space α] [complete_space α] (pkg : abstract_completion α) :
pkg.space ≃ α :=
abstract_completion.compare_equiv pkg (abstract_completion.mk α id
  (by apply_instance) (by apply_instance) (by apply_instance) uniform_inducing_id
  (function.surjective.dense_range function.surjective_id))

[Riccardo Brasca]

Are you sure you want to use docs#abstract_completion instead of docs#uniform_space.completion?

[Riccardo Brasca]

Hmm, I don't see the theorem even for "the" completion

[Junyan Xu]

Why is docs#abstract_completion.compare_equiv not a docs#uniform_equiv?

[Riccardo Brasca]

Probably because we forgot to do so

[Riccardo Brasca]

Indeed what we want is, for a complete space α, an element of abstract_completion α, given by α itself.

[Xavier Roblot]

Riccardo Brasca said:

Are you sure you want to use docs#abstract_completion instead of docs#uniform_space.completion?

I thought that if the result holds for abstract_completion then we can deduce the same for any completion, so the equivalent statement for uniform_completion should follow.

[Riccardo Brasca]

Sure, I just thought maybe the result was already there for uniform_completion, but I don't see it.

[Anatole Dedecker]

Junyan Xu said:

Why is docs#abstract_completion.compare_equiv not a docs#uniform_equiv?

Because it docs#uniform_equiv didn't exist until a few months ago

[Xavier Roblot]

import topology.uniform_space.completion

noncomputable def abstract_completion.complete_equiv_self {α : Type*} [uniform_space α]
[separated_space α] [complete_space α] (pkg : abstract_completion α) :
pkg.space ≃ α :=
abstract_completion.compare_equiv pkg (abstract_completion.mk α id
  (by apply_instance) (by apply_instance) (by apply_instance) uniform_inducing_id
  (function.surjective.dense_range function.surjective_id))

noncomputable def uniform_completion.complete_equiv_self {α : Type*} [uniform_space α]
[complete_space α] [separated_space α]:
uniform_space.completion α ≃ α :=
abstract_completion.complete_equiv_self uniform_space.completion.cpkg

[Xavier Roblot]

Should I just PR those results?
Oh, I see maybe I should prove those with uniform_equiv first, I guess.

[Anatole Dedecker]

I'd say what should be in mathlib is:

• docs#abstract_completion.compare_equiv upgraded to a docs#uniform_equiv
• a complete space is a docs#abstract_completion of itself

[Riccardo Brasca]

Maybe we want inhabitated (abstract_completion α), but I am not sure

[Anatole Dedecker]

Riccardo Brasca said:

Maybe we want inhabitated (abstract_completion α), but I am not sure

No because we want the one with pkg.space = \alpha I think

[Riccardo Brasca]

This is why I said inhabitated and not nonempty, but I don't really care

[Riccardo Brasca]

In any case we want to say that α is an abstract completion of α

[Xavier Roblot]

Upgrading docs#abstract_completion.compare_equiv upgraded to a docs#uniform_equiv is fairly easy:

import topology.uniform_space.equiv
import topology.uniform_space.completion


open abstract_completion

noncomputable theory

variables {α : Type*} [uniform_space α] (pkg : abstract_completion α)
variables (pkg' : abstract_completion α)

instance : uniform_space pkg.space := pkg.uniform_struct

/-- The bijection between two completions of the same uniform space. -/
def abstract_completion.compare_equiv0 : pkg.space  ≃ᵤ pkg'.space :=
{ to_fun := pkg.compare pkg',
  inv_fun := pkg'.compare pkg,
  left_inv := congr_fun (pkg'.inverse_compare pkg),
  right_inv := congr_fun (pkg.inverse_compare pkg'),
  uniform_continuous_to_fun := uniform_continuous_compare _ _,
  uniform_continuous_inv_fun := uniform_continuous_compare _ _ }

[Xavier Roblot]

Although I needed to make an instance to say that pkg.space is a uniform_space to be able to state the result. I don't know if there is another way to do that without using an instance...

[Xavier Roblot]

I do not know enough about inhabited to answer to that...

Riccardo Brasca said:

Maybe we want inhabitated (abstract_completion α), but I am not sure

[Riccardo Brasca]

inhabited X just means that there is an element of X, in some sense "canonical". In practice you can obtain this fixed element via p.default if p : inhabited X

[Riccardo Brasca]

but really, this is not really important, once you have the element it's more or less the same

[Junyan Xu]

The instance was already registered locally via

local attribute [instance]
abstract_completion.uniform_struct

So if you add abstract_completion.compare_equiv0 to the same file (same section, actually) it would just work. (Notice that it's also impossible to state uniform_continuous_compare without the instance.)

[Xavier Roblot]

I opened a PR with the results #16612