Feat: projective line over ℝ is homeomorphic to the one-point compactification of ℝ

[bjoernkjoshanssen]

ℙ ℝ (Fin 2 → ℝ) and OnePoint ℝ are homeomorphic:
the projective line over ℝ is homeomorphic to the one-point compactification of ℝ.

---

[github-actions]

PR summary d5c1b083b2

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Topology.Compactification.OnePointRealLemmas	1337
Mathlib.Topology.Compactification.OnePointHomeomorph	1456

---

Declarations diff

+ OnePointHomeo
+ OnePointHomeo'
+ OnePoint_div
+ abs_le_inv
+ continuous_lift_unit_circle
+ continuous_slope_nonzero_case
+ continuous_slope_zero_case
+ distConeNegNeg
+ distConeNegPos
+ distConePosNeg
+ distConePosPos
+ dist_cone_neg
+ dist_cone_pos
+ div_slope
+ div_slope_continuous
+ div_slope_continuous_unlifted
+ div_slope_equiv
+ div_slope_well_defined
+ flipPos
+ geometryPos
+ geometry_neg
+ geometry_pos
+ instance : T2Space (ℙ ℝ (Fin 2 → ℝ)) := Homeomorph.t2Space OnePointHomeo.symm
+ instance {n : ℕ}: TopologicalSpace (ℙ ℝ (Fin n → ℝ)) := instTopologicalSpaceQuot
+ instance {n:ℕ} : CompactSpace (ℙ ℝ (Fin n → ℝ)) := by
+ instance {n:ℕ} : CompactSpace {v : Fin n → ℝ // dist v 0 = 1} := Metric.sphere.compactSpace 0 1
+ lift_unit_circle
+ lt_div_two
+ nonzero_of_nonzero
+ open_geometry_neg
+ open_geometry_pos
+ open_nonzero
+ posOrNeg
+ pos_or_neg
+ projFinTup
+ reconcile
+ slopeUniform_of_compact
+ slope_open
+ slope_open_nonzero
+ slope_uniform_of_compact
+ slope_uniform_of_compact_neg
+ slope_uniform_of_compact_pos
+ surjective_lift_unit_circle
+ symmetrize
+ tupFinNonzero

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[bjoernkjoshanssen]

This is just a first draft. Needs dramatic reduction in size, and interfacing with OnePointEquiv.lean.

[ocfnash]

Hopefully #18411 will help here.

[bjoernkjoshanssen]

Hopefully #18411 will help here.

Awesome!
Using this, I guess the map can just be fun x => ⟦ ![x,1] ⟧ which should be relatively easy to reason about, compared to my map.

[bjoernkjoshanssen]

@ocfnash Two things left to prove:

• IsOpenMap fun r ↦ ⟦⟨![r, 1], ⋯⟩⟧.
• The projective line is a T2 space

I was able to prove everything else that's needed in order to apply your uniqueness theorem.

In principle I can prove the two items above, using the fact that IsOpen is by definition just the coinduced topology and the plane has the L^\infty metric, and every wedge containing x contains a rectangle containing x. The way I'm looking at it now it's not going to be shorter than my original version in the end, but maybe there is a shortcut?

[ocfnash]

I think what's happening is that because you are the first to define the topology of projective space, everything is missing. So the total amount of work to get to a situation where you can apply OnePoint.equivOfIsEmbeddingOfRangeEq will indeed be quite a few lines (and possibly more than your original work). However, the key point is that with the approach I am pushing, almost all of the work will be "general theory", and not specific to your end result. This will therefore enrich the library much more than adding one isolated result (and will also be much easier to maintain).

I would advocate splitting out a new PR from this one, which just sets up the topology on projective space and proves a few basic properties. You could create a new file Mathlib.Topology.Instances.Projectivization and add things like:

open scoped LinearAlgebra.Projectivization

-- Let `K` be a topological division ring
-- (for later results, may need `NormedDivisionRing K` instead)
variable {K : Type*}
  [DivisionRing K] [TopologicalSpace K] [TopologicalDivisionRing K]

-- Let `V` be a topological vector space over `K`
variable {V : Type*}
  [AddCommGroup V] [Module K V]
  [TopologicalSpace V] [ContinuousAdd V] [ContinuousSMul K V]

instance : TopologicalSpace (ℙ K V) := instTopologicalSpaceQuot
instance : T2Space (ℙ K V) := sorry
instance [FiniteDimensional K V] : CompactSpace (ℙ K V) := sorry

Once that is done, the next step will be to see what lemmas we have about linear / affine maps (and continuous linear / affine maps) and the induced topology. Ultimately you will be applying this to the map ℝ → ℝ × ℝ that sends x ↦ (x, 1) but we will want to develop (or if we are lucky, locate) the results quite generally.

Once these two components are in place, only then will we bring the pieces together use OnePoint.equivOfIsEmbeddingOfRangeEq and if we have done our job above well, all proofs should be short and easy.

[bjoernkjoshanssen]

Once these two components are in place, only then will we bring the pieces together use OnePoint.equivOfIsEmbeddingOfRangeEq and if we have done our job above well, all proofs should be short and easy.

Yes, this all makes sense. I have no idea how to prove your instance : T2Space (ℙ K V) above though.

I added, just now, a proof that your approach using equivOfIsEmbeddingOfRangeEq does in fact succeed, using my original proofs as a lever.