The Fricke matrix

The Fricke matrix W = !![0, -1; N, 0], as an element of GL (Fin 2) K for a field K in which N is invertible. Its determinant is N, which is nonzero exactly under the standing [NeZero (N : K)] hypothesis, so W is a unit.

The base field is a parameter rather than ℚ: the two consumers sit over different fields. The weight-k slash is an action of GL (Fin 2) ℝ, while the GL (Fin 2) ℚ Hecke-ring stack of TauCeti/NumberTheory/HeckeRing/GL2/Delta0.lean wants the rational form; both are frickeGL _ N, with no transport lemmas between them. Over ℚ and ℝ a caller holding [NeZero N] on the natural number gets the standing [NeZero (N : K)] by instance search, through NeZero.charZero; the instance runs only in that direction.

This file is only the matrix. TauCeti/NumberTheory/ModularForms/Fricke/Operator.lean builds the Fricke slash operator on M_k(Γ₁(N)) on top of it: the raw f ↦ f ∣[k] W, carrying no normalizing scalar and so not an involution. The normalized 𝒲_N = (√N) ^ (2 - k) • (· ∣[k] W), which rescales that map and is an involution in even weight, is a later rung.

Main definitions

• TauCeti.frickeGL: the Fricke matrix as an element of GL (Fin 2) K.

Main results

• TauCeti.coe_frickeGL: the underlying matrix is !![0, -1; N, 0].
• TauCeti.val_det_frickeGL: the determinant is N.
• TauCeti.val_det_frickeGL_pos: over an ordered ring, that determinant is positive. This is about the single matrix W, deliberately not a general statement about SL-type elements.
• TauCeti.coe_inv_frickeGL: W⁻¹ = !![0, N⁻¹; -1, 0].
• TauCeti.coe_frickeGL_sq: W² = (-N) • 1 as matrices.

Relation to the Atkin–Lehner anti-involution

Both this matrix and the conjugating matrix of TauCeti/NumberTheory/HeckeRing/GL2/Gamma0/AtkinLehner.lean are called "Atkin–Lehner" in the literature, and they are different matrices. That file conjugates by natDiagGL 2 ![1, N], the diagonal rescaling repairing the transpose's failure to preserve Γ₀(N); its docstring already records that it is not !![0, -1; N, 0]. This file is the latter.

At N = 1 the Fricke matrix coincides numerically with the level-one S = !![0, -1; 1, 0] of TauCeti/NumberTheory/ModularForms/STransform.lean and with TauCeti.SU2.weylMatrix. Those are different objects in different settings — neither carries a determinant-N normalization — so frickeGL is not a restatement of either.

Ported from the AINTLIB LeanModularForms project (projects/LeanModularForms/LeanModularForms/HeckeRIngs/GL2/Fricke.lean, Chris Birkbeck, Apache-2.0, https://github.com/CBirkbeck/AINTLIB), realizing part of Layer 6 of the ModularForms roadmap.

noncomputable def TauCeti.frickeGL (K : Type u_2) [Field K] (N : ℕ) [NeZero ↑N] : GL (Fin 2) K

The Fricke matrix W = !![0, -1; N, 0] as an element of GL (Fin 2) K, of determinant N.

Equations

• TauCeti.frickeGL K N = Matrix.GeneralLinearGroup.mkOfDetNeZero !![0, -1; ↑N, 0] ⋯

@[simp]

theorem TauCeti.coe_frickeGL {K : Type u_1} [Field K] {N : ℕ} [NeZero ↑N] : ↑(frickeGL K N) = !![0, -1; ↑N, 0]

The underlying matrix of frickeGL K N.

theorem TauCeti.val_det_frickeGL {K : Type u_1} [Field K] {N : ℕ} [NeZero ↑N] : ↑(Matrix.GeneralLinearGroup.det (frickeGL K N)) = ↑N

The determinant of frickeGL K N is N.

theorem TauCeti.val_det_frickeGL_pos {K : Type u_1} [Field K] {N : ℕ} [NeZero ↑N] [PartialOrder K] [IsOrderedRing K] : 0 < ↑(Matrix.GeneralLinearGroup.det (frickeGL K N))

Over an ordered ring the determinant of frickeGL K N is positive. This is about the single matrix W; it is deliberately not a general statement about determinants of SL-type elements.

theorem TauCeti.coe_inv_frickeGL {K : Type u_1} [Field K] {N : ℕ} [NeZero ↑N] : ↑(frickeGL K N)⁻¹ = !![0, (↑N)⁻¹; -1, 0]

W⁻¹ = !![0, N⁻¹; -1, 0].

Deliberately not @[simp]: Matrix.coe_units_inv is itself simp, so simp rewrites this left-hand side to (!![0, -1; N, 0])⁻¹ and it is not in simp-normal form.

theorem TauCeti.coe_frickeGL_sq {K : Type u_1} [Field K] {N : ℕ} [NeZero ↑N] : ↑(frickeGL K N ^ 2) = -↑N • 1

W² = (-N) • 1 as matrices. This is the entrywise identity behind the centrality of W² — its consumer is frickeGL_sq_mul_comm of TauCeti/NumberTheory/ModularForms/Fricke/Conjugation.lean — and, later, behind the scalar the normalized Fricke operator divides out. It is not itself a statement that W² is central.

Deliberately not @[simp]: the left-hand side ↑(W ^ 2) is not in simp-normal form, since Units.val_pow_eq_pow_val and the in-file simp lemma coe_frickeGL already rewrite its head to (!![0, -1; N, 0]) ^ 2. Tagging it would put a non-normal left-hand side in the simp set.