Möbius transformations of the projective line #
Mathlib's OnePoint.smul_some_eq_ite and OnePoint.smul_infty_eq_ite give the value of the
GL (Fin 2) K action on OnePoint K. This file adds the companion criterion for the
exceptional case — when an affine point is carried to ∞ — which Mathlib does not state.
It then descends the GL (Fin 2) K action to the projective general linear group PGL(2, K),
which is possible because the scalar matrices fix every point
(TauCeti.scalar_smul_onePoint_eq_self), and faithful because they are the whole kernel
(TauCeti.ker_toPermHom_onePoint_eq_center).
It then equips OnePoint K with the action of the projective special linear group
PSL(2, K), transported from Mathlib's action of PSL(2, K) on ℙ K (Fin 2 → K) along
OnePoint.equivProjectivization. The class of a matrix acts as the matrix does
(OnePoint.pslMk_smul); the action is faithful and transitive. For K = ℝ this is the action of
PSL(2, ℝ) on the ideal boundary of the upper half-plane.
When K has characteristic other than two ([NeZero (2 : K)]), a parabolic element g of
PSL(2, K) (Matrix.ProjectiveSpecialLinearGroup.IsParabolic) has exactly one fixed point,
parabolicFixedPoint g, the descent of Mathlib's
Matrix.GeneralLinearGroup.parabolicFixedPoint. A parabolic element fixing ∞ is a nonzero
translation, and so a parabolic element is conjugate to a translation by any σ carrying ∞ to
its fixed point. This normal form is where the cusps of a Fuchsian group are measured from: the
stabilizer of a cusp, moved to ∞, consists of translations.
Main results #
OnePoint.smul_some_eq_infty_iff:g • (k : OnePoint K) = ∞exactly when the denominatorg 1 0 * k + g 1 1vanishes.TauCeti.scalar_smul_onePoint_eq_selfandTauCeti.mem_center_of_forall_smul_onePoint_eq_self: a matrix fixes every point of the projective line exactly when it is scalar, whenceTauCeti.ker_toPermHom_onePoint_eq_center, the kernel of the permutation representation ofGL₂(F)on the projective line.OnePoint.instMulActionPGL: the action ofPGL(2, K)onOnePoint K, withpglMk_smuland its faithfulness.OnePoint.instMulActionPSL: the action ofPSL(2, K)onOnePoint K, withpslMk_smul.Matrix.ProjectiveSpecialLinearGroup.mk_smul_zero_eq_infty_iff,mk_smul_infty_eq_infty_iff,mk_smul_zero_eq_coe_iff,mk_smul_infty_eq_coe_iff: where the class of!![a, b; c, d]sends the points0and∞, in terms of its entries.Matrix.ProjectiveSpecialLinearGroup.IsParabolic.smul_eq_self_iff: a parabolic element fixes a point exactly when it isparabolicFixedPoint g(in characteristic other than two).Matrix.ProjectiveSpecialLinearGroup.isParabolic_iff_exists_eq_upperRightHom: an element fixing∞is parabolic exactly when it is a nonzero translation.Matrix.ProjectiveSpecialLinearGroup.exists_conj_upperRightHom_of_smul_infty: conjugation by an element fixing∞rescales every translation by the same nonzero square, andMatrix.ProjectiveSpecialLinearGroup.exists_eq_upperRightHom_of_commute: such an element commuting with a nonzero translation is itself a translation.Matrix.ProjectiveSpecialLinearGroup.IsParabolic.exists_conj_eq_upperRightHomandMatrix.ProjectiveSpecialLinearGroup.isParabolic_iff_exists_conj_upperRightHom: the parabolic elements are exactly the conjugates of nonzero translations (in characteristic other than two).
References #
- Alan Beardon, The Geometry of Discrete Groups, Graduate Texts in Mathematics 91, Springer, 1983, §4.3.
- Svetlana Katok, Fuchsian Groups, Chicago Lectures in Mathematics, University of Chicago Press, 1992, §§2.1 and 4.2.
When a Möbius image is the point at infinity. Mathlib's smul_some_eq_ite gives the
value of g • (k : OnePoint K); this is the companion criterion for the exceptional case.
[DecidableEq K] is a hypothesis of the statement, not of the proof: Mathlib's instGLAction
is itself declared under [Field K] [DecidableEq K]
(Mathlib/Topology/Compactification/OnePoint/ProjectiveLine.lean), so g • (k : OnePoint K) does
not elaborate without it.
A scalar matrix fixes every point of the projective line: it rescales every vector, hence preserves every line.
A matrix fixing every point of the projective line is central. Fixing ∞ kills the lower
left entry, fixing 0 then kills the upper right one, and fixing 1 makes the two diagonal
entries agree; so the matrix is scalar, and the scalar matrices are the centre.
PGL₂(F) acts faithfully on the projective line: the kernel of the permutation
representation of GL₂(F) on OnePoint F is the centre of GL₂(F).
PGL(2, K) acts on the projective line: the Möbius action of GL (Fin 2) K is trivial on
the scalar matrices (TauCeti.scalar_smul_onePoint_eq_self), so it descends to the quotient.
The class in PGL(2, K) of an invertible matrix acts on OnePoint K as the matrix does.
The action of PGL(2, K) on OnePoint K is faithful: a matrix fixing every point of the
projective line is central (TauCeti.ker_toPermHom_onePoint_eq_center), so it is trivial in
PGL(2, K).
The projective special linear group PSL(2, K) acts on OnePoint K, via the canonical
identification with ℙ¹(K).
The class in PSL(2, K) of a matrix of SL(2, K) acts on OnePoint K as the matrix does.
The action of PSL(2, K) on OnePoint K is faithful.
The action of PSL(2, K) on OnePoint K is transitive.
The translation upperRightHom x fixes ∞.
The translation upperRightHom x acts on K ⊆ OnePoint K by k ↦ k + x.
The class of !![a, b; c, d] sends 0 to ∞ exactly when d = 0.
The class of !![a, b; c, d] fixes ∞ exactly when c = 0.
The class of !![a, b; c, d] sends 0 to the affine point e exactly when d ≠ 0 and
b = e d.
The class of !![a, b; c, d] sends ∞ to the affine point e exactly when c ≠ 0 and
a = e c.
The fixed point of a parabolic element of PSL(2, K), well defined because the formula
Matrix.GeneralLinearGroup.parabolicFixedPoint is unchanged by negating the representative. For a
parabolic g it is the unique fixed point of g (IsParabolic.smul_eq_self_iff); otherwise it
carries no meaning.
Equations
- g.parabolicFixedPoint = Quotient.liftOn' g (fun (a : Matrix.SpecialLinearGroup (Fin 2) K) => (Matrix.SpecialLinearGroup.toGL a).parabolicFixedPoint) ⋯
Instances For
The fixed point of a translation is ∞.
A parabolic element of PSL(2, K) fixes exactly one point of OnePoint K, namely
parabolicFixedPoint g.
The fixed point of a conjugate σ g σ⁻¹ of a parabolic element is the image under σ of the
fixed point of g.
An element of PSL(2, K) fixing ∞ is parabolic exactly when it is a nonzero translation.
Conjugating translations by an element fixing ∞. Conjugation by an element g of
PSL(2, K) fixing ∞ rescales every translation by the same nonzero square.
An element of PSL(2, K) fixing ∞ and commuting with a nonzero translation is itself a
translation.
Normal form of a parabolic element. If σ carries ∞ to the fixed point of a parabolic
g, then σ⁻¹ g σ is a nonzero translation.
The parabolic elements of PSL(2, K) are exactly the conjugates of nonzero translations.