Documentation

Mathlib.Topology.Compactification.OnePointEquiv

One-point compactification and projectivization #

We construct a set-theoretic equivalence between OnePoint K and the projectivization ℙ K (K × K) for an arbitrary division ring K.

TODO: Add the extension of this equivalence to a homeomorphism in the case K = ℝ, where OnePoint ℝ gets the topology of one-point compactification.

Main definitions and results #

Tags #

one-point extension, projectivization

source
def OnePoint.equivProjectivization (K : Type u_1) [DivisionRing K] [DecidableEq K] :
OnePoint K ≃ Projectivization K (K × K)

The one-point compactification of a division ring K is equivalent to the projectivivization ℙ K (K × K).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem OnePoint.equivProjectivization_apply_infinity (K : Type u_1) [DivisionRing K] [DecidableEq K] :
    (OnePoint.equivProjectivization K) OnePoint.infty = Projectivization.mk K (1, 0) ⋯
    source
    @[simp]
    theorem OnePoint.equivProjectivization_apply_coe (K : Type u_1) [DivisionRing K] [DecidableEq K] (t : K) :
    (OnePoint.equivProjectivization K) ↑t = Projectivization.mk K (t, 1) ⋯
    source
    @[simp]
    theorem OnePoint.equivProjectivization_symm_apply_mk (K : Type u_1) [DivisionRing K] [DecidableEq K] (x y : K) (h : (x, y) ≠ 0) :
    (OnePoint.equivProjectivization K).symm (Projectivization.mk K (x, y) h) = if y = 0 then OnePoint.infty else ↑(y⁻¹ * x)