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 #
OnePoint.equivProjectivization
: the equivalenceOnePoint K ≃ ℙ K (K × K)
.
Tags #
one-point extension, projectivization
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
@[simp]
theorem
OnePoint.equivProjectivization_apply_infinity
(K : Type u_1)
[DivisionRing K]
[DecidableEq K]
:
@[simp]
theorem
OnePoint.equivProjectivization_apply_coe
(K : Type u_1)
[DivisionRing K]
[DecidableEq K]
(t : K)
:
@[simp]
theorem
OnePoint.equivProjectivization_symm_apply_mk
(K : Type u_1)
[DivisionRing K]
[DecidableEq K]
(x y : K)
(h : (x, y) ≠ 0)
: