Documentation

TauCeti.LinearAlgebra.Matrix.ProjectiveSpecialLinearGroup.FinTwo

Parabolic elements of PSL(2, R) #

Mathlib classifies 2 × 2 matrices as parabolic, elliptic or hyperbolic (Matrix.IsParabolic, with the dot-notation synonym Matrix.GeneralLinearGroup.IsParabolic). Being parabolic is invariant under negation (Matrix.isParabolic_neg_iff), so over a ring without zero divisors, where the center of SL(2, R) is {±1}, it descends to the projective special linear group PSL(2, R) = SL(2, R) ⧸ {±1}. This is the notion of a parabolic Möbius transformation which does not depend on a choice of matrix representative.

The model parabolic elements are the translations upperRightHom x, the classes of the transvections !![1, x; 0, 1], which act on the projective line by z ↦ z + x. Over a field of characteristic other than two every parabolic element of PSL(2, K) is conjugate to one of them; that classification, which runs through the action on the projective line, is in TauCeti.Topology.Compactification.OnePoint.ProjectiveLine.

Main declarations #

References #

source
def Matrix.ProjectiveSpecialLinearGroup.IsParabolic {R : Type u_1} [CommRing R] (g : ProjectiveSpecialLinearGroup (Fin 2) R) :
Prop

An element of PSL(2, R) is parabolic when it is the class of a parabolic matrix of SL(2, R). When R has no zero divisors every representative is then parabolic (Matrix.ProjectiveSpecialLinearGroup.isParabolic_mk_iff).

Equations
Instances For
    source
    @[simp]
    theorem Matrix.ProjectiveSpecialLinearGroup.isParabolic_mk_iff {R : Type u_1} [CommRing R] [NoZeroDivisors R] (a : SpecialLinearGroup (Fin 2) R) :
    IsParabolic ↑a ↔ (SpecialLinearGroup.toGL a).IsParabolic

    The class of a matrix of SL(2, R) is parabolic exactly when the matrix is: the only other representative is its negative, which is parabolic along with it.

    source
    @[simp]
    theorem Matrix.ProjectiveSpecialLinearGroup.isParabolic_conj_iff {R : Type u_1} [CommRing R] [NoZeroDivisors R] (g h : ProjectiveSpecialLinearGroup (Fin 2) R) :
    (g * h * g⁻¹).IsParabolic ↔ h.IsParabolic

    Parabolicity is invariant under conjugation in PSL(2, R).

    source
    @[simp]
    theorem Matrix.ProjectiveSpecialLinearGroup.isParabolic_conj_iff' {R : Type u_1} [CommRing R] [NoZeroDivisors R] (g h : ProjectiveSpecialLinearGroup (Fin 2) R) :
    (g⁻¹ * h * g).IsParabolic ↔ h.IsParabolic

    Parabolicity is invariant under conjugation in PSL(2, R), with the inverse on the left.

    source
    @[simp]
    theorem Matrix.ProjectiveSpecialLinearGroup.not_isParabolic_one {R : Type u_1} [CommRing R] [NoZeroDivisors R] :
    ¬IsParabolic 1

    The identity of PSL(2, R) is not parabolic: a parabolic matrix is not scalar.

    source
    theorem Matrix.ProjectiveSpecialLinearGroup.IsParabolic.ne_one {R : Type u_1} [CommRing R] [NoZeroDivisors R] {g : ProjectiveSpecialLinearGroup (Fin 2) R} (hg : g.IsParabolic) :
    g ≠ 1
    source
    @[simp]
    theorem Matrix.ProjectiveSpecialLinearGroup.isParabolic_inv_iff {R : Type u_1} [CommRing R] [NoZeroDivisors R] {g : ProjectiveSpecialLinearGroup (Fin 2) R} :
    g⁻¹.IsParabolic ↔ g.IsParabolic

    Parabolicity is invariant under inversion in PSL(2, R): the inverse of a matrix of SL(2, R) is its adjugate, which has the same trace and is scalar exactly when the matrix is.

    source
    theorem Matrix.ProjectiveSpecialLinearGroup.IsParabolic.inv {R : Type u_1} [CommRing R] [NoZeroDivisors R] {g : ProjectiveSpecialLinearGroup (Fin 2) R} :
    g.IsParabolic → g⁻¹.IsParabolic

    Alias of the reverse direction of Matrix.ProjectiveSpecialLinearGroup.isParabolic_inv_iff.

    Parabolicity is invariant under inversion in PSL(2, R): the inverse of a matrix of SL(2, R) is its adjugate, which has the same trace and is scalar exactly when the matrix is.

    source
    theorem Matrix.ProjectiveSpecialLinearGroup.IsParabolic.pow {K : Type u_2} [Field K] [CharZero K] {g : ProjectiveSpecialLinearGroup (Fin 2) K} (hg : g.IsParabolic) {n : ℕ} (hn : n ≠ 0) :
    (g ^ n).IsParabolic

    A nonzero power of a parabolic element of PSL(2, K) is parabolic.

    source
    theorem Matrix.ProjectiveSpecialLinearGroup.IsParabolic.zpow {K : Type u_2} [Field K] [CharZero K] {g : ProjectiveSpecialLinearGroup (Fin 2) K} (hg : g.IsParabolic) {n : ℤ} (hn : n ≠ 0) :
    (g ^ n).IsParabolic

    A nonzero integer power of a parabolic element of PSL(2, K) is parabolic.

    source
    def Matrix.ProjectiveSpecialLinearGroup.upperRightHom {R : Type u_1} [CommRing R] :
    AddChar R (ProjectiveSpecialLinearGroup (Fin 2) R)

    The translation upperRightHom x ∈ PSL(2, R), the class of the transvection !![1, x; 0, 1]; it acts on the projective line by z ↦ z + x.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Matrix.ProjectiveSpecialLinearGroup.upperRightHom_apply {R : Type u_1} [CommRing R] (x : R) :
      upperRightHom x = ↑(SpecialLinearGroup.transvection ⋯ x)
      source
      theorem Matrix.ProjectiveSpecialLinearGroup.upperRightHom_injective {R : Type u_1} [CommRing R] :
      Function.Injective ⇑upperRightHom

      Distinct translations are distinct in PSL(2, R): if the classes of two transvections are equal, then the transvections differ by a central factor, which is the transvection of the difference of their parameters, and a transvection is central only when its parameter is zero.

      source
      theorem Matrix.ProjectiveSpecialLinearGroup.mul_zpow_mul_inv_eq_upperRightHom {R : Type u_1} [CommRing R] {σ γ : ProjectiveSpecialLinearGroup (Fin 2) R} {w : R} (h : σ * γ * σ⁻¹ = upperRightHom w) (n : ℤ) :
      σ * γ ^ n * σ⁻¹ = upperRightHom (↑n * w)

      If σ conjugates γ to the translation by w, it conjugates γ ^ n to the translation by n * w.

      source
      @[simp]
      theorem Matrix.ProjectiveSpecialLinearGroup.isParabolic_upperRightHom_iff {R : Type u_1} [CommRing R] [NoZeroDivisors R] {x : R} :
      (upperRightHom x).IsParabolic ↔ x ≠ 0

      A translation is parabolic exactly when it is nontrivial.