homeomorphism of EuclideanSpace on ℝ

Stream: Is there code for X?

[thssliangjz]

Hi all, is there a theorem asserting 2 homeomorphic EuclideanSpace must have same dimensions? Speciffically:

example {m n: ℕ} (h: EuclideanSpace ℝ (Fin n) ≃ₜ EuclideanSpace ℝ (Fin m)) : m = n := by
  sorry

Thanks!

[Aaron Liu]

probably not

[Aaron Liu]

I guess you would need some way to measure the dimension?

[Aaron Liu]

looking through what is in mathlib, I guess if you have a bilipschitz map you can use the hausdorff dimension?

[Yongxi Lin (Aaron)]

#mathlib4 > Invariance of domain

[Yongxi Lin (Aaron)]

Aaron Liu said:

I guess you would need some way to measure the dimension?

The dimension here is just the dimension of vector space. This should be an easy corollary of invariance of domain. The link above says that we do have the invariance of domain but I have trouble finding it in mathlib.

[Yongxi Lin (Aaron)]

Oh maybe I didn't understand the message in the link correctly. I think we don't have both the Jordan curve theorem and the invariance of domain.

[Aaron Liu]

Yongxi Lin said:

Aaron Liu said:

I guess you would need some way to measure the dimension?

The dimension here is just the dimension of vector space. This should be an easy corollary of invariance of domain. The link above says that we do have the invariance of domain but I have trouble finding it in mathlib.

I don't think mathlib would have invariance of domain, since it doesn't have brouwer fixed point or homology of spheres and from a quick search the standard proofs seems to use one of these

[thssliangjz]

Aaron Liu said:

looking through what is in mathlib, I guess if you have a bilipschitz map you can use the hausdorff dimension?

Thanks :slight_smile:, but I know little about hausdorff dimension. A quick search in mathlib does not show relevant theory on topological dimension either :upside_down:I guess there is no short way to prove it?

[Aaron Liu]

thssliangjz said:

Thanks :slight_smile:, but I know little about hausdorff dimension.

The relevant theorems I guess would be docs#LipschitzWith.dimH_image_le and docs#Real.dimH_of_nonempty_interior

[thssliangjz]

aha I see this one https://github.com/leanprover-community/mathlib4/blob/50803f90cd60ddf3d8dad58cbd2bc41b1bd7b4c1/Mathlib/Topology/MetricSpace/HausdorffDimension.lean#L435-L445 is probably what I need as ball is homeomorphic to R^n, thanks!

[Violeta Hernández]

thssliangjz said:

I guess there is no short way to prove it?

Not really, no! This is surprisingly quite a deep result.

[Michael Rothgang]

Indeed, mathlib doesn't know about the homology f spheres (and neither about Brouwer nor invariance of domain).

[Michael Rothgang]

For C1 maps (not mere homeomorphisms), there is a shorter proof using the inverse function theorem on manifolds. I have the latter oa branch (it's a WIP PR, as I want to make the code mathlib generality before merging).

[Michael Rothgang]

There was a proof of Brouwer and the homology of spheres in Lean 3. Since then, singular homology has bee refactored significantly (and is in mathlib now). The Lean 3 proof would have to be completely redone.

[Michael Rothgang]

(That would be very welcome, and a large project.)

[Michael Rothgang]

Search for Brouwer fixed point theorem or singular homology to find the details.

[Yaël Dillies]

Apparently, Brouwer was recently reproved in Lean 4. This too should be findable on Zulip.

[Michael Rothgang]

Indeed, the zulip thread for Brouwer is #general > Formalization of Brouwer's Fixed point Theorem

[Michael Rothgang]

But the proof given is purely combinatorial, i.e. does not use homology at all.

[Lyu Yuwei]

Michael Rothgang 发言道：

But the proof given is purely combinatorial, i.e. does not use homology at all.

I'm interested in exploring a homology-based formalization of Brouwer's fixed-point theorem. If you've already started work in this direction or would like assistance, I'd be happy to help contribute to the project.

[Snir Broshi]

I noticed that "invariance of domain" is not on the 100 or 1000 lists, weird.
Is there somewhere else the TODO to implement it could live?

[Ruben Van de Velde]

An issue on the mathlib repository? (I think we should use that more)

[Snir Broshi]

Ruben Van de Velde said:

An issue on the mathlib repository? (I think we should use that more)

Good idea, opened #33018

[Junyan Xu]

The 1000+ list is extracted from this page, and I just added invariance of domain to it (under Algebraic Topology).