The Atkin-Lehner anti-involution of the Γ₀(N) Hecke pair

Conjugating the transpose by w = diag(1, N),

ι(g) = w · gᵀ · w⁻¹,

is an anti-automorphism of GL₂(ℚ) preserving both the image of Γ₀(N) and the submonoid Δ₀(N), so it restricts to a HeckeAntiInvolution of the Γ₀(N) Hecke datum.

At level one the transpose alone already does this — that is HeckeRing.GLn.transposeAntiInvolution, and it is why the GL_n Hecke ring is commutative. It does not survive the congruence condition: transposition carries Γ₀(N) to Γ⁰(N), swapping which off-diagonal entry is divisible by N. Conjugating by w swaps it back, which is exactly what the Atkin-Lehner twist buys.

On entries the map is (a, b; N c, e) ↦ (a, c; N b, e): the lower-left entry stays divisible by N, the determinant is unchanged, and — the point of the construction — the upper-left entry is untouched, so the coprimality condition cutting out Δ₀(N) transfers with no work. Integrality of the new upper-right entry is precisely the hypothesis N ∣ A 1 0.

Beyond the anti-involution itself, this file proves that ι preserves determinants and fixes the double coset of any x ∈ Δ₀(N) whose determinant is coprime to the level, or divides a power of it. These are the good-prime and bad-prime extremes of the hypothesis HeckeCosetModule.mul_comm_of_antiInvolution takes for commutativity of R(Γ₀(N), Δ₀(N)) (Shimura, Proposition 3.8); a mixed determinant needs both arguments at once.

A second criterion asks nothing of the determinant as a whole, only that the upper-left entry of an integral witness be coprime to it. That one is entrywise; the bad-prime criterion is recovered from it, since inside Δ₀(N) the upper-left entry is already a unit mod N.

An arbitrary determinant is then settled here, by a single argument that needs no case analysis: a primitive witness of determinant m and its entry swap, which is primitive of the same determinant, both lie in the double coset of diag(1, m) (mem_doubleCoset_natDiagGL_of_primitive). Passing from a primitive witness to a general one only costs a central scalar, which the bar fixes. Running those two steps on an arbitrary x ∈ Δ₀(N) — divide an integral witness by the gcd of its entries, then put the scalar back — leaves no double coset unfixed, so Shimura's Proposition 3.8 applies: for nonzero level N, R(Γ₀(N), Δ₀(N)) is commutative over any commutative semiring.

Main definitions

• HeckeRing.GL2.atkinLehnerAntiInvolution: the anti-involution of the Γ₀(N) Hecke pair.
• HeckeRing.GL2.atkinLehnerAutomorphism: the automorphism g ↦ ι(g⁻¹) of the ambient group.
• HeckeRing.GL2.commSemiringHeckeRingGamma0: for nonzero level N, the resulting commutative-semiring structure on the Hecke ring R(Γ₀(N), Δ₀(N)).

Main results

• HeckeRing.GL2.atkinLehnerAntiInvolution_bar: how it acts, g ↦ w · gᵀ · w⁻¹. The bundle itself is opaque, so this is the elimination rule a consumer works with.
• HeckeRing.GL2.atkinLehnerAntiInvolution_bar_val: its entrywise action on a Δ₀(N) witness.
• HeckeRing.GL2.atkinLehnerAntiInvolution_bar_det: it preserves the determinant.
• HeckeRing.GL2.atkinLehnerAntiInvolution_bar_mem_doubleCoset_of_coprimeDet: it fixes the double coset when the determinant is coprime to the level.
• HeckeRing.GL2.atkinLehnerAntiInvolution_bar_mem_doubleCoset_of_coprime_upperLeft: it fixes the double coset when the upper-left entry of an integral witness is coprime to the determinant.
• HeckeRing.GL2.atkinLehnerAntiInvolution_bar_mem_doubleCoset_of_dvd_pow: it fixes the double coset when the determinant divides a power of the level, the witness-free specialisation of the previous one.
• HeckeRing.GL2.atkinLehnerAntiInvolution_bar_mem_doubleCoset_of_smul: the criterion survives scaling, the scalar's positivity and coprimality to the level being automatic.
• HeckeRing.GL2.atkinLehnerAntiInvolution_bar_mem_doubleCoset_of_primitive: it fixes the double coset of a witness no prime divides entrywise, with no hypothesis on the determinant.
• HeckeRing.GL2.atkinLehnerAntiInvolution_bar_mem_doubleCoset: for nonzero level N, it fixes the double coset of every x ∈ Δ₀(N), with no further hypothesis on x.
• HeckeRing.GL2.atkinLehnerAntiInvolution_onHeckeCoset_eq_self: equivalently, for nonzero level N, it acts as the identity on Γ₀(N) \ Δ₀(N) / Γ₀(N).

References

• G. Shimura, Introduction to the arithmetic theory of automorphic functions, Proposition 3.8.
• Ported from the AINTLIB LeanModularForms project (Chris Birkbeck), HeckeRIngs/GLn/CongruenceHecke/AtkinLehner.lean, declarations wN, Gamma0_AL_hom, Gamma0_AL_involutive, Gamma0_AL_map_H, Gamma0_AL_map_Δ and Gamma0_antiInvolution, and — for the results added here — Gamma0_AL_bar_det, bar_eq_SL2_conj, Gamma0_AL_in_DC_coprime, Gamma0_AL_in_DC_bad, Gamma0_AL_in_DC_of_gcd_a00_m_coprime, Gamma0_AL_in_DC_of_smul, Gamma0_AL_in_DC_primitive, Gamma0_AL_in_doubleCoset, Gamma0_onHeckeCoset_eq and instCommRing_Gamma0, all Apache-2.0 at commit 2baa76f742bdb4fb8ee323fabba41203bd390e08. The source states its own transpose equivalence and diagonal-matrix API; here those come from GLn/TransposeAntiInvolution.lean and GLn/DiagonalCosets.lean instead, and the four-field bundle is assembled by HeckeAntiInvolution.ofAmbient. The source proves its own Gamma0_AL_preserves_00 to see that the bar fixes the upper-left entry; here that is already visible in atkinLehnerAntiInvolution_bar_val, so the lemma is not reproduced. The source builds its central scalar by hand and proves centrality entrywise; here it is natDiagGL at a constant family, and centrality is read off natDiagGL_const_comm. The source's two reductions Gamma0_AL_scalar_reduce and bar_mem_DC_of_bar_conj_mem are used in the general form HeckeRing.Commutativity gives them, not re-proved for Γ₀(N). The source builds the content quotient of a witness inline; here that is exists_primitive_content_quotient. Its instCommRing_Gamma0 is a CommRing on the integral Hecke ring; the structure available here is the CommSemiring of HeckeCosetModule.commSemiringOfAntiInvolution over an arbitrary commutative semiring, exactly as at level one. The source's Gamma0_pair_HeckeAlgebra_mul_comm restates that instance's mul_comm, which HeckeCosetModule.mul_comm_of_antiInvolution already provides directly, so it is not reproduced.

noncomputable def HeckeRing.GL2.atkinLehnerAntiInvolution (N : ℕ) [NeZero N] : HeckeAntiInvolution (Delta0 N) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N))

The Atkin-Lehner anti-involution g ↦ w · gᵀ · w⁻¹ of the Γ₀(N) Hecke pair, where w = diag(1, N).

w is the diagonal rescaling that repairs the transpose's failure to preserve Γ₀(N). It is not the Atkin-Lehner matrix of the operator 𝒲_Q, which is !![0, -1; N, 0].

Stated at the unfolded (Gamma0 N).map (mapGL ℚ), which is where Gamma0/Basic.lean puts the IsHeckeTriple instance. That matters and is not cosmetic: HeckeCosetModule.mul_comm_of_antiInvolution asks for a HeckeAntiInvolution Δ H together with [IsHeckeTriple Δ H H] at the same H, and instance search does not see through the sealed Gamma0Image definition. Stated at Gamma0Image N the two do not compose at all — the Hecke ring 𝕋 (Delta0 N) (Gamma0Image N) ℤ does not even have a multiplication, since that too comes from the instance. Measured both ways.

Equations

• HeckeRing.GL2.atkinLehnerAntiInvolution N = HeckeAntiInvolution.ofAmbient (HeckeRing.GL2.atkinLehnerHom✝ N) ⋯ ⋯ ⋯

noncomputable def HeckeRing.GL2.atkinLehnerAutomorphism (N : ℕ) : GL (Fin 2) ℚ ≃* GL (Fin 2) ℚ

The automorphism of the ambient group sending g to the Atkin–Lehner bar of g⁻¹.

Composing two order reversals makes this multiplicative. It is the form of the Atkin–Lehner operation used to transport left-coset multiplicities arising from right slash actions.

Equations

• HeckeRing.GL2.atkinLehnerAutomorphism N = (MulEquiv.inv' (GL (Fin 2) ℚ)).trans (HeckeRing.GL2.atkinLehnerEquiv✝ N).symm

theorem HeckeRing.GL2.atkinLehnerAutomorphism_apply (N : ℕ) (x : GL (Fin 2) ℚ) : (atkinLehnerAutomorphism N) x = GLn.natDiagGL 2 ![1, N] * MulOpposite.unop ((GLn.transposeGLEquiv 2) x⁻¹) * (GLn.natDiagGL 2 ![1, N])⁻¹

The ambient automorphism is the Atkin–Lehner bar applied after inversion.

@[simp]

theorem HeckeRing.GL2.atkinLehnerAutomorphism_involutive (N : ℕ) (x : GL (Fin 2) ℚ) : (atkinLehnerAutomorphism N) ((atkinLehnerAutomorphism N) x) = x

The ambient Atkin–Lehner automorphism is involutive.

@[simp]

theorem HeckeRing.GL2.atkinLehnerAutomorphism_symm (N : ℕ) : (atkinLehnerAutomorphism N).symm = atkinLehnerAutomorphism N

The ambient Atkin–Lehner automorphism is its own inverse.

@[simp]

theorem HeckeRing.GL2.atkinLehnerAutomorphism_map_Gamma0 (N : ℕ) [NeZero N] : Subgroup.map (↑(atkinLehnerAutomorphism N)) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) = Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)

The ambient Atkin–Lehner automorphism preserves the image of Γ₀(N).

@[simp]

theorem HeckeRing.GL2.atkinLehnerAntiInvolution_bar (N : ℕ) [NeZero N] {x : GL (Fin 2) ℚ} (hx : x ∈ Delta0 N) : (atkinLehnerAntiInvolution N).bar x hx = GLn.natDiagGL 2 ![1, N] * MulOpposite.unop ((GLn.transposeGLEquiv 2) x) * (GLn.natDiagGL 2 ![1, N])⁻¹

The anti-involution acts by conjugating the transpose by w, unfolding the sealed definition.

theorem HeckeRing.GL2.atkinLehnerAutomorphism_inv_apply (N : ℕ) [NeZero N] {x : GL (Fin 2) ℚ} (hx : x ∈ Delta0 N) : (atkinLehnerAutomorphism N) x⁻¹ = (atkinLehnerAntiInvolution N).bar x hx

On an inverse from Δ₀(N), the ambient automorphism is the restricted Atkin–Lehner bar.

theorem HeckeRing.GL2.atkinLehnerAntiInvolution_bar_val (N : ℕ) [NeZero N] {x : GL (Fin 2) ℚ} (hx : x ∈ Delta0 N) (A : Matrix (Fin 2) (Fin 2) ℤ) (hA : ↑x = A.map Int.cast) (c : ℤ) (hc : A 1 0 = ↑N * c) : ↑((atkinLehnerAntiInvolution N).bar x hx) = !![A 0 0, c; ↑N * A 0 1, A 1 1].map Int.cast

The entrywise action, on the bundle: (a, b; N c, e) ↦ (a, c; N b, e). This is the form a consumer of Δ₀(N) elements needs; without it the entries can only be recovered by redoing the diagonal-conjugation computation.

theorem HeckeRing.GL2.atkinLehnerAntiInvolution_bar_det (N : ℕ) [NeZero N] {x : GL (Fin 2) ℚ} (hx : x ∈ Delta0 N) : (↑((atkinLehnerAntiInvolution N).bar x hx)).det = (↑x).det

The bar preserves the determinant, so a determinant hypothesis on x transfers to bar x unchanged.

theorem HeckeRing.GL2.atkinLehnerAntiInvolution_bar_mem_doubleCoset_of_coprimeDet (N : ℕ) [NeZero N] (x : GL (Fin 2) ℚ) (hx : x ∈ Delta0 N) (hcop : CoprimeDet N ⟨x, hx⟩) : (atkinLehnerAntiInvolution N).bar x hx ∈ DoubleCoset.doubleCoset x ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N))

The Atkin–Lehner involution fixes a coprime-determinant double coset. If x ∈ Δ₀(N) has determinant coprime to N, then its bar lies in the Γ₀(N)-double coset of x.

theorem HeckeRing.GL2.atkinLehnerAntiInvolution_bar_mem_doubleCoset_of_coprime_upperLeft (N : ℕ) [NeZero N] (m : ℕ) (x : GL (Fin 2) ℚ) (hx : x ∈ Delta0 N) (A : Matrix (Fin 2) (Fin 2) ℤ) (hA : ↑x = A.map Int.cast) (hdet : (↑x).det = ↑m) (ham : (A 0 0).gcd ↑m = 1) : (atkinLehnerAntiInvolution N).bar x hx ∈ DoubleCoset.doubleCoset x ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N))

The Atkin–Lehner involution fixes a double coset whose upper-left entry is coprime to the determinant. If x ∈ Δ₀(N) has integral witness A and determinant m, and A 0 0 is coprime to m, then bar x lies in the Γ₀(N)-double coset of x itself.

Where the other two criteria read the determinant as a whole, this one reads a single entry. Membership of Δ₀(N) already forces A 0 0 to be a unit mod N; this asks the same at m.

The bad-prime criterion below is its witness-free specialisation.

theorem HeckeRing.GL2.atkinLehnerAntiInvolution_bar_mem_doubleCoset_of_dvd_pow (N : ℕ) [NeZero N] (m k : ℕ) (hm_dvd : m ∣ N ^ k) (x : GL (Fin 2) ℚ) (hx : x ∈ Delta0 N) (hdet : (↑x).det = ↑m) : (atkinLehnerAntiInvolution N).bar x hx ∈ DoubleCoset.doubleCoset x ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N))

The Atkin–Lehner involution fixes a bad-prime double coset. If x ∈ Δ₀(N) has determinant m with m ∣ N ^ k, then bar x lies in the Γ₀(N)-double coset of x itself.

This is the bad case, where m shares its primes with the level; the coprime case is separate. It supplies the bad-prime half of the fixing hypothesis that HeckeCosetModule.mul_comm_of_antiInvolution requires, and is the statement to quote when no integral witness is in hand.

theorem HeckeRing.GL2.atkinLehnerAntiInvolution_bar_mem_doubleCoset_of_smul (N : ℕ) [NeZero N] (d : ℕ) (x x₀ : GL (Fin 2) ℚ) (hx : x ∈ Delta0 N) (hx₀ : x₀ ∈ Delta0 N) (hsmul : ↑x = ↑d • ↑x₀) (hfix : (atkinLehnerAntiInvolution N).bar x₀ hx₀ ∈ DoubleCoset.doubleCoset x₀ ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N))) : (atkinLehnerAntiInvolution N).bar x hx ∈ DoubleCoset.doubleCoset x ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N))

The criterion survives scaling. If x is the multiple d • x₀ of an element of Δ₀(N) whose double coset the bar fixes, then the bar fixes the double coset of x as well. Neither positivity of d nor coprimality of d to N is assumed: both are consequences of x lying in Δ₀(N).

theorem HeckeRing.GL2.atkinLehnerAntiInvolution_bar_mem_doubleCoset_of_primitive (N : ℕ) [NeZero N] (x : GL (Fin 2) ℚ) (hx : x ∈ Delta0 N) (A : Matrix (Fin 2) (Fin 2) ℤ) (hA : ↑x = A.map Int.cast) (hprim : ∀ (p : ℕ), Nat.Prime p → ¬(↑p ∣ A 0 0 ∧ ↑p ∣ A 0 1 ∧ ↑p ∣ A 1 0 ∧ ↑p ∣ A 1 1)) : (atkinLehnerAntiInvolution N).bar x hx ∈ DoubleCoset.doubleCoset x ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N))

The Atkin-Lehner involution fixes the double coset of a primitive witness. If x ∈ Δ₀(N) has an integral witness A no prime divides entrywise, then bar x lies in the Γ₀(N)-double coset of x. No hypothesis is placed on the determinant.

theorem HeckeRing.GL2.atkinLehnerAntiInvolution_bar_mem_doubleCoset (N : ℕ) [NeZero N] (x : GL (Fin 2) ℚ) (hx : x ∈ Delta0 N) : (atkinLehnerAntiInvolution N).bar x hx ∈ DoubleCoset.doubleCoset x ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N))

The Atkin-Lehner bar fixes every Γ₀(N)-double coset in Δ₀(N), for nonzero level N and with no further hypothesis on x. This is exactly the hypothesis Shimura's commutativity criterion takes, in the pointwise form HeckeAntiInvolution.bar_mem_doubleCoset_self reads it.

Dividing an integral witness by the gcd d of its four entries leaves a primitive one, which atkinLehnerAntiInvolution_bar_mem_doubleCoset_of_primitive settles with no hypothesis on the determinant. Putting the scalar back is atkinLehnerAntiInvolution_bar_mem_doubleCoset_of_smul, which asks nothing further of d: the positivity and the coprimality to the level it needs are read off x ∈ Δ₀(N) inside it.

@[simp]

theorem HeckeRing.GL2.atkinLehnerAntiInvolution_onHeckeCoset_eq_self (N : ℕ) [NeZero N] (D : HeckeCoset (Delta0 N) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N))) : (atkinLehnerAntiInvolution N).onHeckeCoset D = D

The Atkin-Lehner bar acts trivially on Γ₀(N) \ Δ₀(N) / Γ₀(N), for nonzero level N. Each double coset is fixed, by atkinLehnerAntiInvolution_bar_mem_doubleCoset at any representative.

@[instance_reducible]

noncomputable def HeckeRing.GL2.commSemiringHeckeRingGamma0 (N : ℕ) [NeZero N] (R : Type u_1) [CommSemiring R] : CommSemiring (HeckeRing (Delta0 N) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) R)

Shimura's Proposition 3.8 for Γ₀(N): for nonzero level N, the Hecke ring R(Γ₀(N), Δ₀(N)) over any commutative semiring is commutative, the Atkin-Lehner bar being an anti-involution that fixes every double coset.

This is the level-N counterpart of HeckeRing.GLn.commSemiringHeckeRing, where transposition alone does the same job. Not an instance, for the reason given there: the anti-involution is data. The @[instance_reducible] attribute is required by Lean's class-definition reducibility linter for any def of class type; it governs unfolding during instance search and registers nothing on its own.

Equations

• HeckeRing.GL2.commSemiringHeckeRingGamma0 N R = HeckeCosetModule.commSemiringOfAntiInvolution R (HeckeRing.GL2.atkinLehnerAntiInvolution N) ⋯