Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
wants to merge 21 commits into
base: master
Choose a base branch
from

Conversation

bjoernkjoshanssen
Copy link
Collaborator

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


Open in Gitpod

Copy link

github-actions bot commented Oct 27, 2024

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.

@github-actions github-actions bot added the t-topology Topological spaces, uniform spaces, metric spaces, filters label Oct 27, 2024
@bjoernkjoshanssen
Copy link
Collaborator Author

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

@ocfnash
Copy link
Contributor

ocfnash commented Oct 29, 2024

Hopefully #18411 will help here.

@bjoernkjoshanssen
Copy link
Collaborator Author

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
Copy link
Collaborator Author

bjoernkjoshanssen commented Oct 30, 2024

@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
Copy link
Contributor

ocfnash commented Oct 31, 2024

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.

@ocfnash ocfnash added the awaiting-author A reviewer has asked the author a question or requested changes label Oct 31, 2024
@bjoernkjoshanssen
Copy link
Collaborator Author

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
awaiting-author A reviewer has asked the author a question or requested changes t-topology Topological spaces, uniform spaces, metric spaces, filters
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants