Projective translations of the upper half-plane

The projective upper unipotent matrix acts by real translation. This identifies conjugated parabolic stabilizers with the translations used in cusp coordinates.

Main results

• TauCeti.UpperHalfPlane.upperRightHom_smul: upperRightHom x acts as z ↦ x + z.
• TauCeti.UpperHalfPlane.smul_zpow_smul: conjugating to a translation turns the action of integer powers into translation by integer multiples.
• TauCeti.UpperHalfPlane.smulDeriv_upperRightHom: a translation has derivative 1.

@[simp]

theorem TauCeti.UpperHalfPlane.upperRightHom_smul (x : ℝ) (z : UpperHalfPlane) : Matrix.ProjectiveSpecialLinearGroup.upperRightHom x • z = x +ᵥ z

The projective upper unipotent matrix acts by real translation.

theorem TauCeti.UpperHalfPlane.smul_zpow_smul {σ γ : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ} {w : ℝ} (h : σ * γ * σ⁻¹ = Matrix.ProjectiveSpecialLinearGroup.upperRightHom w) (n : ℤ) (z : UpperHalfPlane) : σ • γ ^ n • z = ↑n * w +ᵥ σ • z

A transformation conjugating an element to a translation sends its integer-power action to translation by the corresponding integer multiple.

theorem TauCeti.UpperHalfPlane.smulDeriv_upperRightHom (x : ℝ) (z : UpperHalfPlane) : (Matrix.ProjectiveSpecialLinearGroup.upperRightHom x).smulDeriv z = 1

The derivative of a translation is 1.