The Möbius-action conjugation at a positive determinant

Mathlib's UpperHalfPlane.σ sends a matrix g : GL(2, ℝ) to the automorphism of ℂ which is the identity when det g is positive and complex conjugation otherwise. It is the twist that makes the Möbius action of a negative-determinant matrix antiholomorphic, and it is carried through the weight-k slash action of a general real matrix.

Positive determinant is the case everything in this project works in — congruence subgroups, the semigroups Δ₀(N) of the Hecke theory, and the scaling matrices diag(d, 1) all consist of matrices of positive determinant — so the conjugation is invariably trivial and every computation begins by discharging it. This file names that branch, so σ need never be unfolded by hand.

Main results

• UpperHalfPlane.σ_eq_refl_of_det_pos: σ g = ContinuousAlgEquiv.refl ℝ ℂ for 0 < det g.
• UpperHalfPlane.ofReal_mul_add_eq_zero_iff: m z + n = 0 for real m, n and z ∈ ℍ only when m = n = 0, the iff form of Mathlib's UpperHalfPlane.linear_ne_zero.
• UpperHalfPlane.num_sub_smul_mul_denom: the difference formula g • z - g • τ = det g · (z - τ) / ((cz + d)(cτ + d)) for det g > 0, with the denominator of g • z cleared.
• ModularGroup.sl_smul_set: the SL(2, ℤ)-action on subsets of ℍ is the GL(2, ℝ)-action along the coercion, the pointwise-image counterpart of Mathlib's ModularGroup.sl_moeb.
• ModularGroup.smul_eq_smul_of_eq_or_eq_neg: elements of SL(2, ℤ) that agree up to sign act alike on ℍ.
• Matrix.SpecialLinearGroup.toGL_smul: the SL(2, ℝ)-action on ℍ is the GL(2, ℝ)-action of the underlying matrix, the SL(2, ℝ) counterpart of Mathlib's ModularGroup.sl_moeb.
• ModularGroup.re_S_smul, ModularGroup.S_smul_S_smul: the inversion S negates the real part up to a normSq factor, and is an involution of ℍ.

Provenance

The statement and its role follow AINTLIB's sigma_eq_id_of_pos_det in the LeanModularForms project (LeanModularForms/HeckeRIngs/GL2/HeckeAction.lean, commit 2baa76f742bdb4fb8ee323fabba41203bd390e08, Apache-2.0, Chris Birkbeck), where it discharges the σ branch for the Hecke slash action. The proof is written against the current pin — if_pos is deprecated here in favour of ite_eq_left.

@[simp]

theorem UpperHalfPlane.σ_eq_refl_of_det_pos {g : GL (Fin 2) ℝ} (hg : 0 < (↑g).det) : σ g = ContinuousAlgEquiv.refl ℝ ℂ

The Möbius-action conjugation σ is the identity on matrices of positive determinant: that is the branch its definition picks. On the other branch σ is complex conjugation, which is where the antiholomorphic behaviour of a negative-determinant Möbius transformation comes from.

The hypothesis is stated with Matrix.det of the underlying matrix rather than with the ℝˣ-valued GeneralLinearGroup.det: the two agree by Matrix.GeneralLinearGroup.val_det_apply, which is simp, so only this form is in simp-normal form and only this form makes the lemma usable as a conditional simp rule.

@[simp]

theorem Matrix.SpecialLinearGroup.toGL_smul (g : SpecialLinearGroup (Fin 2) ℝ) (τ : UpperHalfPlane) : toGL g • τ = g • τ

The SL(2, ℝ)-action on ℍ is the GL(2, ℝ)-action of the underlying matrix.

theorem UpperHalfPlane.ofReal_mul_add_eq_zero_iff (z : UpperHalfPlane) {m n : ℝ} : ↑m * ↑z + ↑n = 0 ↔ m = 0 ∧ n = 0

A real linear combination m z + n of a point z of the upper half-plane and 1 vanishes only when both coefficients do, as z is not real: the iff form of UpperHalfPlane.linear_ne_zero.

theorem UpperHalfPlane.num_sub_smul_mul_denom {g : GL (Fin 2) ℝ} (hg : 0 < (↑g).det) (τ z : UpperHalfPlane) : num g ↑z - ↑(g • τ) * denom g ↑z = ↑(↑g).det * (↑z - ↑τ) / denom g ↑τ

For g = !![a, b; c, d] of positive determinant, (az + b) - (g • τ)(cz + d) = det g · (z - τ) / (cτ + d): dividing by cz + d gives the difference formula g • z - g • τ = det g · (z - τ) / ((cz + d)(cτ + d)), in the form that clears the denominator of g • z.

@[simp]

theorem ModularGroup.sl_smul_set (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (S : Set UpperHalfPlane) : γ • S = Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ) • S

The SL(2, ℤ)-action on subsets of ℍ is the GL(2, ℝ)-action along the coercion, the pointwise-image counterpart of ModularGroup.sl_moeb. This is useful as a rewrite even though the two actions are definitionally equal.

theorem ModularGroup.smul_eq_smul_of_eq_or_eq_neg {g k : Matrix.SpecialLinearGroup (Fin 2) ℤ} {z : UpperHalfPlane} (hg : g = k ∨ g = -k) : g • z = k • z

Elements of SL(2, ℤ) that agree up to sign act alike on ℍ, since -1 acts trivially (ModularGroup.SL_neg_smul). This absorbs the sign ambiguity g = k ∨ g = -k in the cases of Mathlib's classification ModularGroup.cases_of_mem_fd_smul_mem_fd.

theorem ModularGroup.re_S_smul (p : UpperHalfPlane) : (S • p).re = -p.re / Complex.normSq ↑p

The inversion S negates the real part of every point and divides by its norm-square.

theorem ModularGroup.S_smul_S_smul (p : UpperHalfPlane) : S • S • p = p

The inversion S is an involution of ℍ.