If X and Y are homeomorphic and X is complete, then Y is

Stream: Is there code for X?

[Michael Stoll]

What is the best way of obtaining the following?

import Mathlib

example {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [UniformSpace X] [CompleteSpace X]
    [UniformSpace Y] {f : X → Y} (h : IsHomeomorph f) :
    CompleteSpace Y := by
  sorry

It doesn't look like there are a lot of results in Mathlib that allow to transport topological properties via homeomorphisms...

[Ruben Van de Velde]

How about with a map?

[Michael Stoll]

f is a map ??

[Kalle Kytölä]

Maybe I misunderstand the question, but $\R$ is complete and homeomorphic to, say $(-\pi/2,\pi/2)$, which is not complete.

Completeness is a metric property (or well, a uniformity property, I guess), so just homeomorphisms don't preserve it. (Isometries would of course preserve it.)

[Michael Stoll]

OK; maybe one needs more properties. In my use case, I have two equivalent absolute values on the real numbers (one is the standard one), and I want to show that $\R$ is complete w.r.t. the other one.

[Michael Stoll]

Is it enough if f maps the uniformities to each other?

[Michael Stoll]

How would I write this down?

[Michael Stoll]

Is the following reasonable?

lemma completeSpace_of_comap_uniformity {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
    [UniformSpace X] [CompleteSpace X] [UniformSpace Y] {f : X → Y}
    (h : Filter.comap (Prod.map f f) (uniformity Y) = uniformity X) :
    CompleteSpace Y := by
  sorry

[Kalle Kytölä]

We have docs#IsometryEquiv.completeSpace. It sounds like in your case you don't have an isometry but a bilipschitz map (which also preserves completeness). I don't know how those are called in Mathlib off the top of my head.

[Michael Stoll]

The relation is not linear: one absolute value (= metric) is a power of the other.

[Michael Stoll]

But they certainly induce the same uniformities...

[Michael Stoll]

It seems like I have to use docs#UniformSpace.complete_of_cauchySeq_tendsto and bash through the filters. I'll try that tomorrow (CEST) unless a better idea has emerged by then.

[Kalle Kytölä]

I don't understand your exact situation, but we also have docs#Cauchy.map. So if your homeomorphism is uniformly continuous (maybe in both directions, depending on what you want), using your mentioned docs#UniformSpace.complete_of_cauchySeq_tendsto may not be too bad. (Also I still don't know if Mathlib has something more direct. Are there any results about homeomorphisms which are uniformly continuous in both directions?)

[Junyan Xu]

I think we only have local uniform continuity provided by abs_pow_sub_pow_le.

[Junyan Xu]

More precisely, uniform_continuous_npow_on_bounded which makes it easy to show that a power of a Cauchy sequence is still Cauchy. But Michael is probably interested in real powers, not just natural powers ...

[Junyan Xu]

HolderWith.uniformContinuous is probably useful but the triangle inequality fails one way or the other so not both X and Y can be PseudoEMetricSpace ...

[Aaron Liu]

Michael Stoll said:

Is the following reasonable?

lemma completeSpace_of_comap_uniformity {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
    [UniformSpace X] [CompleteSpace X] [UniformSpace Y] {f : X → Y}
    (h : Filter.comap (Prod.map f f) (uniformity Y) = uniformity X) :
    CompleteSpace Y := by
  sorry

This is docs#IsUniformInducing.isComplete_range

[Matt Diamond]

@Aaron Liu is it? that gets you to IsComplete (Set.range f), not CompleteSpace Y

I think you might need the additional fact that f is surjective so you can use docs#IsUniformInducing.completeSpace_congr

[Matt Diamond]

though if you also have IsHomeomorph f then you've already got surjectivity

[Jireh Loreaux]

Junyan Xu said:

HolderWith.uniformContinuous is probably useful

I think you can use this to build a UniformEquiv quite easily, and then you can apply docs#UniformEquiv.completeSpace_iff

[Anatole Dedecker]

Maybe I’m missing something, but both of your uniformities are (additive) group uniformities right ? If so, showing that they induce the same topology is enough to know that they induce the same uniformity.

[Michael Stoll]

Is there a ready-made result in Mathlib that shows that?

[Notification Bot]

A message was moved from this topic to #Is there code for X? > Uniform structures on ℝ by Junyan Xu.

[Anatole Dedecker]

We have docs#IsUniformAddGroup.toUniformSpace_eq as well as docs#isUniformAddGroup_of_addCommGroup

[Michael Stoll]

Thanks everybody!

I now have the following (equiv₂ v₁ v₂ is the ring isomorphism between WithAbs v₁ and WithAbs v₂ whose underlying map is the identity, and I had already shown that it is continuous when the two absolute values are equivalent).

variable {F : Type*} [Field F] {v₁ v₂ : AbsoluteValue F ℝ} (h : v₁ ≈ v₂)

lemma uniformContinuous_equiv₂_of_isEquiv : UniformContinuous (equiv₂ v₁ v₂) :=
  uniformContinuous_of_continuousAt_zero _ (continuous_equiv₂ h).continuousAt

/-- If `v₁` and `v₂` are equivalent absolute values on `F`, then `WithAbs.equiv₂ v₁ v₂`
is an equivalence of uniformities. This gives the `UniformEquiv`. -/
def uniformEquivOfIsEquiv : WithAbs v₁ ≃ᵤ WithAbs v₂ :=
  UniformEquiv.mk (equiv₂ v₁ v₂) (uniformContinuous_equiv₂_of_isEquiv h)
    (uniformContinuous_equiv₂_of_isEquiv <| Setoid.symm h)

/-- The underlying equivalence of `uniformEquivOfIsEquiv h` is `WithAbs.equiv₂ _ _`. -/
lemma uniformEquiv_eq_equiv₂ :
    (uniformEquivOfIsEquiv h).toEquiv = (equiv₂ v₁ v₂).toEquiv :=
  rfl

/-- If `v₁` and `v₂` are equivalent absolute values on `F` and `F` is complete
with respect to `v₁`, then `F` is also complete with respect to `v₂`. -/
lemma completeSpace_of_isEquiv [CompleteSpace (WithAbs v₁)] :
    CompleteSpace (WithAbs v₂) :=
  (uniformEquivOfIsEquiv h).completeSpace_iff.mp ‹CompleteSpace (WithAbs v₁)›