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
@[implicit_reducible]
instance
instSMulCommClassMatrixFinOfNatNatProd
{R : Type u_1}
[Semiring R]
{S : Type u_3}
[DistribSMul S R]
[SMulCommClass R S R]
:
SMulCommClass (Matrix (Fin 2) (Fin 2) R) S (R × R)
@[simp]
theorem
Matrix.fin_two_smul_prod
{R : Type u_1}
[Semiring R]
(g : Matrix (Fin 2) (Fin 2) R)
(v : R × R)
:
g • v = (g 0 0 * v.1 + g 0 1 * v.2, g 1 0 * v.1 + g 1 1 * v.2)
@[simp]
theorem
Matrix.GeneralLinearGroup.fin_two_smul_prod
{R : Type u_3}
[CommRing R]
(g : GL (Fin 2) R)
(v : R × R)
:
g • v = (↑g 0 0 * v.1 + ↑g 0 1 * v.2, ↑g 1 0 * v.1 + ↑g 1 1 * v.2)
The one-point compactification of a division ring K is equivalent to
the projectivization ℙ K (K × K).
Instances For
@[simp]
theorem
OnePoint.equivProjectivization_apply_infinity
(K : Type u_1)
[DivisionRing K]
[DecidableEq K]
:
(equivProjectivization K) infty = Projectivization.mk K (1, 0) ⋯
@[simp]
theorem
OnePoint.equivProjectivization_apply_coe
(K : Type u_1)
[DivisionRing K]
[DecidableEq K]
(t : K)
:
(equivProjectivization K) ↑t = Projectivization.mk K (t, 1) ⋯
@[simp]
theorem
OnePoint.equivProjectivization_symm_apply_mk
(K : Type u_1)
[DivisionRing K]
[DecidableEq K]
(x y : K)
(h : (x, y) ≠ 0)
:
(equivProjectivization K).symm (Projectivization.mk K (x, y) h) = if y = 0 then infty else ↑(y⁻¹ * x)
@[implicit_reducible]
For a field K, the group GL(2, K) acts on OnePoint K, via the canonical identification
with the ℙ¹(K) (which is given explicitly by Möbius transformations).
theorem
OnePoint.smul_infty_def
{K : Type u_1}
[Field K]
[DecidableEq K]
{g : GL (Fin 2) K}
:
g • infty = (equivProjectivization K).symm (Projectivization.mk K (↑g 0 0, ↑g 1 0) ⋯)
theorem
OnePoint.smul_some_eq_ite
{K : Type u_1}
[Field K]
[DecidableEq K]
{g : GL (Fin 2) K}
{k : K}
:
g • ↑k = if ↑g 1 0 * k + ↑g 1 1 = 0 then infty else ↑((↑g 0 0 * k + ↑g 0 1) / (↑g 1 0 * k + ↑g 1 1))
theorem
OnePoint.map_smul
{K : Type u_1}
[Field K]
[DecidableEq K]
{L : Type u_2}
[Field L]
[DecidableEq L]
(f : K →+* L)
(g : GL (Fin 2) K)
(c : OnePoint K)
:
OnePoint.map (⇑f) (g • c) = (Matrix.GeneralLinearGroup.map f) g • OnePoint.map (⇑f) c
theorem
Matrix.GeneralLinearGroup.fixpointPolynomial_aeval_eq_zero_iff
{K : Type u_1}
[Field K]
[DecidableEq K]
{c : K}
{g : GL (Fin 2) K}
:
(Polynomial.aeval c) g.fixpointPolynomial = 0 ↔ g • ↑c = ↑c
The roots of g.fixpointPolynomial are the fixed points of g ∈ GL(2, K) acting on the finite
part of OnePoint K.
theorem
Matrix.GeneralLinearGroup.IsParabolic.smul_eq_self_iff
{K : Type u_1}
[Field K]
[DecidableEq K]
{g : GL (Fin 2) K}
(hg : g.IsParabolic)
[NeZero 2]
{c : OnePoint K}
:
g • c = c ↔ c = g.parabolicFixedPoint
theorem
Matrix.GeneralLinearGroup.IsParabolic.parabolicFixedPoint_pow
{K : Type u_1}
[Field K]
[DecidableEq K]
{g : GL (Fin 2) K}
(hg : g.IsParabolic)
[CharZero K]
{n : ℕ}
(hn : n ≠ 0)
:
(g ^ n).parabolicFixedPoint = g.parabolicFixedPoint
theorem
Matrix.GeneralLinearGroup.IsElliptic.smul_ne_self
{K : Type u_1}
[Field K]
[DecidableEq K]
[LinearOrder K]
[IsStrictOrderedRing K]
{g : GL (Fin 2) K}
(hg : g.IsElliptic)
(c : OnePoint K)
:
g • c ≠ c
Elliptic elements have no fixed points in OnePoint K.