Point stabilizers of subgroups of PSL(2, ℝ) #
The transformations fixing a point z of the upper half-plane are recorded by their derivative
there. By the chain rule that derivative is multiplicative on the stabilizer, so it is a
character stabilizer Γ z →* ℂ for any subgroup Γ ≤ PSL(2, ℝ), and it is injective: a Möbius
transformation fixing z with derivative 1 there is the identity. Hence a point stabilizer is
commutative, and cyclic as soon as it is finite — a finite subgroup of the multiplicative monoid
of a field is cyclic.
The injectivity of the character turns the order of a generator into the order of its
derivative, so the derivative of a generator of a finite point stabilizer is a primitive root of
unity whose order is the order of the stabilizer. Consequently the character identifies a finite
point stabilizer of order m with the group of m-th roots of unity, and in the disc coordinate
centred at the fixed point the stabilizer acts by exactly those rotations. Finally, every
nontrivial element of a point stabilizer is an elliptic matrix.
The specialization to discrete subgroups, whose point stabilizers are finite, is
TauCeti.Analysis.Complex.Fuchsian.Stabilizer.
Main declarations #
Subgroup.stabilizerDeriv: the derivative character of a point stabilizer, andSubgroup.stabilizerDeriv_injective.Subgroup.isCyclic_stabilizer: a finite point stabilizer is cyclic.Subgroup.exists_isPrimitiveRoot_stabilizerDeriv: a generator of a finite point stabilizer has a primitive root of unity of the stabilizer's order as its derivative.Subgroup.stabilizerRotationandSubgroup.stabilizerRotationEquiv: the derivative character of a point stabilizer, and, for a finite stabilizer of orderm, the isomorphism it gives onto them-th roots of unity.Subgroup.discCoordinate_stabilizer_smulandSubgroup.discCoordinate_smul_eq_rotation_smul: in the disc coordinate centred at the fixed point, an element of the stabilizer acts by multiplication by its derivative, that is, by its rotation.Subgroup.exists_discCoordinate_generator_transition: replacing a stabilizer generator raises its rotation factor to a power coprime to the stabilizer order.Subgroup.mem_orbit_stabilizer_iff_discCoordinate_pow_eq_pow: two points lie in the same orbit of a finite stabilizer of ordermexactly when their disc coordinates have the samem-th power.Matrix.SpecialLinearGroup.isElliptic_of_smul_eq_self_of_ne_one: a matrix fixing a point ofℍand nontrivial inPSL(2, ℝ)is elliptic.Matrix.ProjectiveSpecialLinearGroup.eq_one_of_smul_eq_self_of_smul_eq_self: a nontrivial element ofPSL(2, ℝ)fixes at most one point ofℍ.Matrix.ProjectiveSpecialLinearGroup.exists_rotation_eq_of_smul_I_eq_I: the stabilizer ofIinPSL(2, ℝ)consists of the classes of the rotationsMatrix.SpecialLinearGroup.rotation θ.
References #
- Alan Beardon, The Geometry of Discrete Groups, Graduate Texts in Mathematics 91, Springer, 1983, Chapters 7–8.
- Hershel Farkas and Irwin Kra, Riemann Surfaces, Chapter I §§4–5.
- Svetlana Katok, Fuchsian Groups, Chicago Lectures in Mathematics, University of Chicago Press, 1992, §§2.1–2.4.
An element of SL(2, ℝ) that fixes z : ℍ and whose automorphy factor at z is a real
number e is the scalar matrix e.
An element of SL(2, ℝ) fixing z : ℍ whose automorphy factor at z squares to one is
central, that is, ±1.
The derivative of the action detects the identity: a Möbius transformation of ℍ fixing
z whose derivative at z is 1 is the identity of PSL(2, ℝ).
A nontrivial Möbius transformation fixes at most one point of ℍ: an element of
PSL(2, ℝ) fixing two distinct points of the upper half-plane is the identity.
The stabilizer of I is the rotation group: every element of PSL(2, ℝ) fixing I is the
class of a rotation Matrix.SpecialLinearGroup.rotation θ.
Source: Katok, Fuchsian groups, geodesic flows… (Clay Math. Proc. 10), §1 p. 6:
K = SO(2) is the stabiliser of i in SL(2, ℝ).
The derivative character of the stabilizer of z : ℍ in a subgroup Γ ≤ PSL(2, ℝ): it
sends an element fixing z to its derivative
Matrix.ProjectiveSpecialLinearGroup.smulDeriv at z.
Equations
- Γ.stabilizerDeriv z = { toFun := fun (q : ↥(MulAction.stabilizer (↥Γ) z)) => (↑↑q).smulDeriv z, map_one' := ⋯, map_mul' := ⋯ }
Instances For
The derivative character evaluated on an element of the stabilizer.
The derivative character of a point stabilizer is injective: a transformation fixing z
is determined by its derivative at z.
A point stabilizer in a subgroup of PSL(2, ℝ) is commutative.
A finite point stabilizer is cyclic. For a discrete subgroup of PSL(2, ℝ), where the
finiteness hypothesis is automatic, see Subgroup.instIsCyclicStabilizer.
The disc coordinate linearizes a point stabilizer: an element of the stabilizer of z
acts, in the disc coordinate centred at z, by multiplication by its derivative at z.
The order of an element of a point stabilizer is the order of its derivative at that point.
Replacing a primitive stabilizer generator by another raises its rotation factor to a power coprime to the stabilizer order. This also gives the exact change in the action on every disc coordinate.
A finite point stabilizer is generated by a transformation whose derivative at the point is a primitive root of unity of order the stabilizer's order — the elliptic order of the point.
The rotation character of a point stabilizer: its derivative character at the fixed point,
which lands in the group of m-th roots of unity for m = Nat.card (stabilizer Γ z). For a
finite stabilizer — the case of interest, and the only one in which m is the order of the
stabilizer — that is Lagrange's theorem, and the character is moreover an isomorphism, by
Subgroup.stabilizerRotationEquiv. For an infinite stabilizer m = 0, so the codomain is the
whole unit group and the roots-of-unity condition is vacuous.
Equations
- Γ.stabilizerRotation z = (Γ.stabilizerDeriv z).toHomUnits.codRestrict (rootsOfUnity (Nat.card ↥(MulAction.stabilizer (↥Γ) z)) ℂ) ⋯
Instances For
A finite point stabilizer of order m is the group of m-th roots of unity, identified
by the derivative character at the fixed point. Together with
Subgroup.discCoordinate_stabilizer_smul this conjugates the stabilizer action on the upper
half-plane to the rotation action of the m-th roots of unity on the unit disc.
Equations
Instances For
The disc coordinate conjugates a point stabilizer into the roots of unity: an element of
the stabilizer of z acts, in the disc coordinate centred at z, by its rotation.
Two points of ℍ lie in the same orbit of a finite stabilizer of z of order m exactly
when their disc coordinates centred at z have the same m-th power.
A nonidentity element fixing a point of ℍ is elliptic.