Documentation

TauCeti.LinearAlgebra.Matrix.SpecialLinearGroup.Dilation

The dilations in SL(2, ℝ) #

The diagonal matrices dilation s = !![exp (s / 2), 0; 0, exp (-(s / 2))] form a one-parameter subgroup of SL(2, ℝ) (dilation_zero, dilation_add, dilation_inv): the positive component of the diagonal subgroup of SL(2, ℝ), parametrised by the logarithm of the eigenvalue ratio. Acting on the upper half-plane by Möbius transformations they are the dilations z ↦ exp s * z, which is why the parameter is s rather than the eigenvalue exp (s / 2): dilation s moves a point of the imaginary axis upward by the signed displacement s, that is, by hyperbolic distance |s|, upward for s > 0 and downward for s < 0.

Main declarations #

source
noncomputable def Matrix.SpecialLinearGroup.dilation (s : ℝ) :
SpecialLinearGroup (Fin 2) ℝ

The dilation !![exp (s / 2), 0; 0, exp (-(s / 2))], an element of SL(2, ℝ) acting on ℍ as z ↦ exp s * z.

Equations
Instances For
    source
    @[simp]
    theorem Matrix.SpecialLinearGroup.coe_dilation (s : ℝ) :
    ↑(dilation s) = !![Real.exp (s / 2), 0; 0, Real.exp (-(s / 2))]

    The entries of dilation s.

    source
    @[simp]
    theorem Matrix.SpecialLinearGroup.dilation_zero :
    dilation 0 = 1

    The dilation by 0 is the identity.

    source
    theorem Matrix.SpecialLinearGroup.dilation_add (s t : ℝ) :
    dilation (s + t) = dilation s * dilation t

    The dilations form a one-parameter subgroup: dilation (s + t) = dilation s * dilation t.

    source
    @[simp]
    theorem Matrix.SpecialLinearGroup.dilation_inv (s : ℝ) :
    (dilation s)⁻¹ = dilation (-s)

    The inverse of dilation s is dilation (-s).

    source
    theorem Matrix.SpecialLinearGroup.eq_dilation_two_mul_log {A : SpecialLinearGroup (Fin 2) ℝ} (h₁₀ : ↑A 1 0 = 0) (h₀₁ : ↑A 0 1 = 0) (hpos : 0 < ↑A 0 0) :
    A = dilation (2 * Real.log (↑A 0 0))

    A diagonal matrix of SL(2, ℝ) with positive entries is a dilation: the one by twice the logarithm of its top-left entry.