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

    source
    def Matrix.GeneralLinearGroup.parabolicFixedPoint {K : Type u_1} [Field K] [DecidableEq K] (g : GL (Fin 2) K) :
    OnePoint K

    If g is parabolic, this is the unique fixed point of g in OnePoint K.

    Equations
    Instances For
      source
      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
      source
      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
      source
      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.