The rational projective action on the upper half-plane

GL(2, ℚ)⁺ does not act on ℍ; PSL(2, ℝ) does. This file supplies the homomorphism between them, ratPosToPSL2R, and identifies its kernel on the determinant-one locus.

Hecke operators are indexed by double cosets of matrices with rational entries, so every geometric statement about them has to be pushed along such a homomorphism before Mathlib's ℍ-API applies. The change of scalars GL(2, ℚ) →* GL(2, ℝ) alone will not do: it is injective, so it keeps -1, which acts trivially on ℍ. Anything demanding a faithful action — MeasureTheory.IsFundamentalDomain in particular, whose a.e.-disjointness clause is Pairwise over group elements — is then unsatisfiable. Passing to PSL(2, ℝ) collapses exactly the scalars, and eq_one_or_neg_one_of_mem_ratPosToPSL2R_ker_of_det_eq_one says that on the determinant-one locus nothing else is lost: an element of the kernel with determinant one is ±1. (Only that containment is proved here; the converse, that ±1 do lie in the kernel, is not needed by any consumer and is not claimed.)

Main definitions

• TauCeti.ratPosToRealPos: the change of scalars GL(2, ℚ)⁺ →* GL(2, ℝ)⁺.
• TauCeti.ratPosToPSL2R: the composite GL(2, ℚ)⁺ →* GL(2, ℝ)⁺ →* PSL(2, ℝ).

Main results

• UpperHalfPlane.ratPosToPSL2R_smul: ratPosToPSL2R g acts on ℍ as the real matrix does.
• TauCeti.eq_one_or_neg_one_of_mem_ratPosToPSL2R_ker_of_det_eq_one: an element of ker ratPosToPSL2R with determinant one is ±1 — a containment, not an identification.
• TauCeti.ratPosToPSL2R_ker_inf_le: the consequence consumers apply — ker ratPosToPSL2R ⊓ H ≤ Γ whenever H lies in the determinant-one locus and -1 ∈ Γ, which holds of every Γ₀(N).

References

• [DS] Diamond–Shurman, A First Course in Modular Forms, §5.5

noncomputable def TauCeti.ratPosToRealPos : ↥(Matrix.GLPos (Fin 2) ℚ) →* ↥(Matrix.GLPos (Fin 2) ℝ)

The change of scalars GL(2, ℚ)⁺ →* GL(2, ℝ)⁺, the restriction of Matrix.GeneralLinearGroup.map (algebraMap ℚ ℝ) to the positive-determinant subgroups. Its underlying GL (Fin 2) ℝ matrix is that map applied to g definitionally, so a goal mixing the two spellings closes by rfl.

Equations

• TauCeti.ratPosToRealPos = MonoidHom.restrict TauCeti.ratPosToRealPos._proof_2✝

@[simp]

theorem TauCeti.coe_ratPosToRealPos (g : ↥(Matrix.GLPos (Fin 2) ℚ)) : ↑(ratPosToRealPos g) = (Matrix.GeneralLinearGroup.map (algebraMap ℚ ℝ)) ↑g

The underlying GL (Fin 2) ℝ matrix of ratPosToRealPos g is the entrywise change of scalars ℚ → ℝ applied to g.

noncomputable def TauCeti.ratPosToPSL2R : ↥(Matrix.GLPos (Fin 2) ℚ) →* Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ

The rational projective action. GL(2, ℚ)⁺ acts on ℍ through PSL(2, ℝ): the change of scalars ratPosToRealPos followed by the projectivization glPosToPSL2R. Compute the action with UpperHalfPlane.ratPosToPSL2R_smul; unlike ratPosToRealPos this map is deliberately not injective, as it collapses the scalar matrices, which act trivially on ℍ.

Equations

• TauCeti.ratPosToPSL2R = glPosToPSL2R.comp TauCeti.ratPosToRealPos

@[simp]

theorem UpperHalfPlane.ratPosToPSL2R_smul (g : ↥(Matrix.GLPos (Fin 2) ℚ)) (τ : UpperHalfPlane) : TauCeti.ratPosToPSL2R g • τ = (Matrix.GeneralLinearGroup.map (algebraMap ℚ ℝ)) ↑g • τ

ratPosToPSL2R g acts on ℍ exactly as the real matrix g does. Rewriting with this turns a goal about the PSL(2, ℝ)-action into one about Mathlib's GL(2, ℝ)-action on ℍ; it is the ℚ-coefficient counterpart of UpperHalfPlane.glPosToPSL2R_smul.

theorem TauCeti.map_mem_center_of_mem_ratPosToPSL2R_ker {g : ↥(Matrix.GLPos (Fin 2) ℚ)} (hg : g ∈ ratPosToPSL2R.ker) : (Matrix.GeneralLinearGroup.map (algebraMap ℚ ℝ)) ↑g ∈ Subgroup.center (GL (Fin 2) ℝ)

An element of ker ratPosToPSL2R has central real image.

Central in GL (Fin 2) ℝ means scalar (Matrix.GeneralLinearGroup.center_eq_range_scalar), so this alone pins the image down only up to a scalar; adding determinant one cuts it to ±1 — that stronger form is eq_one_or_neg_one_of_mem_ratPosToPSL2R_ker_of_det_eq_one.

theorem TauCeti.eq_one_or_neg_one_of_mem_ratPosToPSL2R_ker_of_det_eq_one {g : ↥(Matrix.GLPos (Fin 2) ℚ)} (hg : g ∈ ratPosToPSL2R.ker) (hdet : (↑↑g).det = 1) : ↑g = 1 ∨ ↑g = -1

On the determinant-one locus, a kernel element is ±1.

This is one containment only; nothing here says ±1 lie in the kernel, and no consumer needs that. Use it to discharge ratPosToPSL2R.ker ⊓ H ≤ Γ whenever H lies in the determinant-one locus and Γ contains ±1 — every Γ₀(N), in particular. Without hdet only map_mem_center_of_mem_ratPosToPSL2R_ker is available, and that pins the image down to a scalar, no further.

theorem TauCeti.ratPosToPSL2R_ker_inf_le {H Γ : Subgroup ↥(Matrix.GLPos (Fin 2) ℚ)} (hH : ∀ g ∈ H, (↑↑g).det = 1) (hneg : -1 ∈ Γ) : ratPosToPSL2R.ker ⊓ H ≤ Γ

The kernel meets the determinant-one locus inside any Γ containing -1.

This is the consequence of eq_one_or_neg_one_of_mem_ratPosToPSL2R_ker_of_det_eq_one that consumers actually apply: it is the hker hypothesis of the Hecke-coset tiling HeckeRing.GL2.isFundamentalDomain_iUnion_rightCosetRep_smul, and without it every call site repeats the same two-case split.

Only -1 ∈ Γ is asked for; the 1 branch is discharged internally by Γ.one_mem. Every Γ₀(N) contains -1, whose lower-left entry is zero. Γ₁(N) does not, except at N ∣ 2: -1 has diagonal (-1, -1) and Γ₁(N) asks for ≡ (1, 1). A consumer whose Γ is a Γ₁(N) therefore cannot use this lemma at N ≥ 3, and indeed ker ratPosToPSL2R ⊓ H ≤ Γ₁(N) is false there, since -1 lies in the kernel.

The form a consumer actually wants is Γ.withCenter, which adjoins the centre and so contains -1 for every Γ. That is the shape the Petersson layer works in — peterssonInnerCosets sums over SL(2, ℤ) ⧸ Γ.withCenter — so the hypothesis is satisfiable exactly where it is needed.

hH is stated on the underlying matrix because that is the form in which the determinant condition defining the locus arrives.