Projective extended real line

Stream: mathlib4

[Bjørn Kjos-Hanssen]

I started making a file PReal.lean by removing negative infinity from the extended reals in EReal.lean.
I believe

$$\mathbb R \cup \{\top\}$$

is sometimes called the projective extended real line: https://en.wikipedia.org/wiki/Projectively_extended_real_line
whereas EReal would be the affine extended real line.
Just wanted to check (a) that this hasn't been done already and (b) whether there are comments on the sensibility of such a definition. My use case is a family of curves

$$y = \frac{1+ce^t}{1-ce^t}$$

alternatively,

$$y = \frac{1/c+e^t}{1/c-e^t}$$

which are the solutions to

$$y'=\frac12(y^2-1)$$

as c varies over PReal. In particular the equation 1/0=⊤ could be handy for proving that.

[Yury G. Kudryashov]

Should we reuse the type docs#OnePoint ?

[Edward van de Meent]

i think there is/should be a more general construction possible with quotients...

[Edward van de Meent]

i see we already have Projectivization

[Edward van de Meent]

which would allow you to get the appropriate type using ℙ ℝ (Fin 2 -> ℝ)

[Oliver Nash]

Maybe someone might like to add results along these lines:

import Mathlib.LinearAlgebra.Projectivization.Basic
import Mathlib.Topology.Compactification.OnePoint
import Mathlib.Topology.Instances.Real

open scoped LinearAlgebra.Projectivization OnePoint
open Projectivization

variable (K : Type*) [Field K]

-- A homeo when topology present etc.
def foo : OnePoint K ≃ ℙ K (Fin 2 → K) where
  toFun p := Option.elim p (mk' K ⟨![1, 0], by simp⟩) (fun t ↦ mk' K ⟨![t, 1], by simp⟩)
  invFun := sorry
  left_inv := sorry
  right_inv := sorry

[Oliver Nash]

(or even a similar result for a point and a line (disjoint) in an affine plane)

[Bjørn Kjos-Hanssen]

Edward van de Meent said:

i think there is/should be a more general construction possible with quotients...

Nice, this seems to cover my use case, because mapping a point in ℙ K (Fin 2 → K) to its image under

$$[(u, v)] \mapsto \left(x \mapsto \frac{u+ve^x}{u - ve^x}\right)$$

constitutes a parametrization of the solution space of the ODE. Full proof here.

[Notification Bot]

Bjørn Kjos-Hanssen has marked this topic as resolved.

[Bjørn Kjos-Hanssen]

Oliver Nash said:

Maybe someone might like to add results along these lines:

-- A homeo when topology present etc.
def foo : OnePoint K ≃ ℙ K (Fin 2 → K) where
  toFun p := Option.elim p (mk' K ⟨![1, 0], by simp⟩) (fun t ↦ mk' K ⟨![t, 1], by simp⟩)
  invFun := sorry
  left_inv := sorry
  right_inv := sorry

Done, I have proved that it's a homeomorphism. Worked mostly with a map in the other direction,

Quotient.lift
    (λ u : { v : Fin 2 → ℝ // v ≠ 0} ↦
      F_ (u.1 0) (u.1 1))

where `F_ a r = ite (r ≠ 0) (a / r) ∞. Could try to PR it although the proof is a bit cumbersome...

[Bjørn Kjos-Hanssen]

I made a pull request, https://github.com/leanprover-community/mathlib4/pull/16128 for just the equivalence portion. Can PR the homeomorphism part as well.

[Bjørn Kjos-Hanssen]

Update --- the equivalence is on Mathlib now (thanks to @Oliver Nash and @Riccardo Brasca for help) and #18306 is a preliminary PR for the homeomorphism. (It's not yet ready for line-by-line review.)

[Notification Bot]

Oliver Nash has marked this topic as unresolved.

[Oliver Nash]

Looking now, I see that we do not have the uniqueness of one-point compactification. I think if you first added this, then it should help golf #18306.

[Oliver Nash]

To be precise, I think the following is true and would be worth having:

import Mathlib.Topology.Compactification.OnePoint

namespace OnePoint

open Filter Set Topology

variable {X Y : Type*}
  [TopologicalSpace X]
  [TopologicalSpace Y] [T2Space Y] [CompactSpace Y]
  (y : Y) (f : X → Y) (hy : range f = {y}ᶜ)

-- May need other assumptions on `X`. E.g., `[LocallyCompactSpace X]`. At least by
-- `IsEmbedding.t2Space`, do not need `[T2Space X]`.
def lift (hf : IsDenseEmbedding f) :
    OnePoint X ≃ₜ Y := by
  sorry

@[simp]
lemma lift_apply_coe (hf : IsDenseEmbedding f) (x : X) :
    lift f hf x = f x :=
  sorry

-- Convenience variant of `lift`
def lift' [NeBot (𝓝[≠] y)] (hf : IsEmbedding f) :
    OnePoint X ≃ₜ Y :=
  lift f
    { induced := hf.induced
      inj := have : T2Space X := hf.t2Space; hf.injective
      dense := by
        suffices y ∈ closure (range f) by
          intro z
          rcases eq_or_ne z y with rfl | hz
          · exact this
          · replace hz : z ∈ range f := by simpa [hy]
            exact subset_closure hz
        simp [hy, closure_compl_singleton] }

end OnePoint

[Bjørn Kjos-Hanssen]

Thanks @Oliver Nash If someone claims and proves lift I'd be glad to try to use it (and if nobody does maybe I'll eventually try).
In the meantime I'll tinker with my original approach a bit...

[Oliver Nash]

I thought it might be helpful if I filled in the sorrys I sketched above so I created #18411

[Bjørn Kjos-Hanssen]

Great, I hope #18411 has a good outcome.