Documentation

TauCeti.Analysis.Complex.UpperHalfPlane.PSL.ConjJ

Conjugation by J on PSL(2, ℝ) #

Mathlib's UpperHalfPlane.J : GL (Fin 2) ℝ acts on ℍ by the orientation-reversing involution z ↦ -conj z, and on the ideal boundary ∂ℍ = ℝ ∪ {∞} by x ↦ -x. Conjugation by J is the automorphism pslConjJ of PSL(2, ℝ), sending the class of !![a, b; c, d] to that of !![a, -b; -c, d], and J intertwines the action of each g with that of pslConjJ g.

Main declarations #

source
def TauCeti.UpperHalfPlane.pslConjJ :
Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ ≃* Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ

Conjugation by the orientation-reversing involution UpperHalfPlane.J : z ↦ -conj z on PSL(2, ℝ): the class of !![a, b; c, d] goes to the class of !![a, -b; -c, d] (pslConjJ_mk). It is characterised by J_smul_smul and J_smul_smul_onePoint.

Instances For
    source
    theorem TauCeti.UpperHalfPlane.pslConjJ_mk (A : Matrix.SpecialLinearGroup (Fin 2) ℝ) :
    pslConjJ ↑A = ↑A.conjJ

    Conjugation by J sends the class of !![a, b; c, d] to the class of !![a, -b; -c, d].

    source
    @[simp]
    theorem TauCeti.UpperHalfPlane.pslConjJ_pslConjJ (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) :
    pslConjJ (pslConjJ g) = g

    Conjugation by J is an involution.

    source
    @[simp]
    theorem TauCeti.UpperHalfPlane.pslConjJ_symm :
    pslConjJ.symm = pslConjJ

    Conjugation by J is its own inverse.

    source
    theorem TauCeti.UpperHalfPlane.J_smul_smul (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (z : UpperHalfPlane) :
    UpperHalfPlane.J • g • z = pslConjJ g • UpperHalfPlane.J • z

    J intertwines the action of g on ℍ with that of its conjugate pslConjJ g.

    source
    theorem TauCeti.UpperHalfPlane.J_smul_smul_onePoint (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) (ξ : OnePoint ℝ) :
    UpperHalfPlane.J • g • ξ = pslConjJ g • UpperHalfPlane.J • ξ

    J intertwines the action of g on the ideal boundary with that of pslConjJ g.

    source
    @[simp]
    theorem TauCeti.UpperHalfPlane.pslConjJ_pslS :
    pslConjJ pslS = pslS

    Conjugation by J fixes the involution pslS : z ↦ -1/z.

    source
    @[simp]
    theorem TauCeti.UpperHalfPlane.pslConjJ_dilation (s : ℝ) :
    pslConjJ ↑(Matrix.SpecialLinearGroup.dilation s) = ↑(Matrix.SpecialLinearGroup.dilation s)

    Conjugation by J fixes the dilations z ↦ exp s * z.

    source
    @[simp]
    theorem TauCeti.UpperHalfPlane.pslConjJ_upperRightHom (x : ℝ) :
    pslConjJ (Matrix.ProjectiveSpecialLinearGroup.upperRightHom x) = Matrix.ProjectiveSpecialLinearGroup.upperRightHom (-x)

    Conjugation by J inverts the translations z ↦ z + x.

    source
    @[simp]
    theorem TauCeti.UpperHalfPlane.J_smul_coe (x : ℝ) :
    UpperHalfPlane.J • ↑x = ↑(-x)

    J negates real ideal points.

    source
    @[simp]
    theorem TauCeti.UpperHalfPlane.J_smul_infty :
    UpperHalfPlane.J • OnePoint.infty = OnePoint.infty

    J fixes the ideal point ∞.

    source
    @[simp]
    theorem TauCeti.UpperHalfPlane.J_smul_J_smul_onePoint (ξ : OnePoint ℝ) :
    UpperHalfPlane.J • UpperHalfPlane.J • ξ = ξ

    J is an involution of the ideal boundary.