Documentation

Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

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
instance instModuleMatrixFinOfNatNatProd {R : Type u_1} [Semiring R] :
Module (Matrix (Fin 2) (Fin 2) R) (R × R)
Equations
source
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)
source
@[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)
source
@[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)
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 projectivization ℙ 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] :
    (equivProjectivization K) infty = Projectivization.mk K (1, 0) ⋯
    source
    @[simp]
    theorem OnePoint.equivProjectivization_apply_coe (K : Type u_1) [DivisionRing K] [DecidableEq K] (t : K) :
    (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) :
    (equivProjectivization K).symm (Projectivization.mk K (x, y) h) = if y = 0 then infty else ↑(y⁻¹ * x)
    source
    instance OnePoint.instGLAction {K : Type u_1} [Field K] [DecidableEq K] :
    MulAction (GL (Fin 2) K) (OnePoint K)

    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).

    Equations
    source
    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) ⋯)
    source
    theorem OnePoint.smul_infty_eq_ite {K : Type u_1} [Field K] [DecidableEq K] (g : GL (Fin 2) K) :
    g • infty = if ↑g 1 0 = 0 then infty else ↑(↑g 0 0 / ↑g 1 0)
    source
    theorem OnePoint.smul_infty_eq_iff {K : Type u_1} [Field K] [DecidableEq K] (g : GL (Fin 2) K) :
    g • infty = infty ↔ ↑g 1 0 = 0
    source
    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))