Conjugating Γ₀(N) and Γ₁(N) by the Fricke matrix

Over a field in which N is invertible, and for σ = !![a, b; c, d] ∈ Γ₀(N), so N ∣ c, conjugating by the Fricke matrix W = !![0, -1; N, 0] of TauCeti/NumberTheory/ModularForms/Fricke/Matrix.lean gives

W · σ · W⁻¹ = !![d, -c/N; -N·b, a],

which is again integral, again of determinant one, and again in Γ₀(N). This file builds the right-hand side as an honest SL(2, ℤ) matrix — frickeConjSL — reading it off the entries of σ, so that it is defined at every level; records that a Γ₀(N) input stays inside Γ₀(N) and that a Γ₁(N) input stays inside Γ₁(N), again at every level; and proves, over a field in which N is invertible, the two matrix identities that move W past σ and are what make frickeConjSL σ the conjugate W · σ · W⁻¹.

frickeConjSL is defined directly by its entries rather than as a product W * σ * W⁻¹: the latter lives in GL (Fin 2) K and is only incidentally integral, so reading an SL(2, ℤ) element back out of it would need the divisibility argument anyway. Defining it by entries and proving the product identities afterwards keeps the divisibility in one place.

Level

(N : K) ≠ 0 is what makes W invertible, and so what makes conjugation by W mean anything. Over the arbitrary field K of the identities below that is strictly stronger than N ≠ 0: a nonzero level casts to zero whenever the characteristic of K divides it. It is needed for the conjugation, not for the entry formula that computes it, so it is stated where W itself appears: as [NeZero (N : K)] on the two normalization identities over K, which are the statements that exhibit frickeConjSL σ as a conjugate.

The formula itself needs no level hypothesis: !![d, -c'; -N·b, a] has determinant 1, lies in Γ₀(N) for every N, lies in Γ₁(N) whenever σ does, and is multiplicative in σ, c = N · (c / N) holding at N = 0 as well, both sides being zero. At N = 0 the value is junk rather than a conjugation: Γ₀(0) is the upper-triangular subgroup, the quotient c / N is 0, the formula collapses to !![a, b; 0, d] ↦ !![d, 0; 0, a], which forgets b, and frickeGL K 0 does not exist for it to be a conjugation by.

The names follow the intended meaning rather than that degenerate value, as mathlib's do for Matrix.inv at a singular matrix, for Int.ediv by 0, and for Gamma0 0 itself: frickeConjSL, frickeConjGamma0 and frickeConjGamma1 are named for the Fricke conjugation they compute. The level hypothesis then appears only on the declarations that need it — [NeZero N] on the two MulEquivs and the involution lemmas, [NeZero (N : K)] on the identities over K — and not on the all-level declarations, where unusedArguments would reject it as an argument the definition never uses.

[NeZero N] is a hypothesis on the natural number N, not on its image in a field: what fails at level zero is the integer division c / N. The entry map is a homomorphism at every level but an isomorphism only at nonzero level, so [NeZero N] is what the two involution lemmas and the two automorphisms take.

Base field

The conjugation identities are stated over an arbitrary field K in which N is invertible, matching the parameterization of frickeGL. The weight-k slash action needs them over ℝ while the GL (Fin 2) ℚ Hecke-ring stack needs them over ℚ; stating them over K serves both directly, with no transport lemma between the two, since Matrix.SpecialLinearGroup.mapGL is itself defined at an arbitrary algebra.

Main definitions

• TauCeti.frickeConjSL: the matrix !![d, -c/N; -N·b, a] as an element of SL(2, ℤ), read off the entries of σ at every level; over a field in which N is invertible it is the conjugate W · σ · W⁻¹.
• TauCeti.frickeConjGamma0, TauCeti.frickeConjGamma1: that map bundled as a group endomorphism Γ₀(N) →* Γ₀(N), and its restriction Γ₁(N) →* Γ₁(N). Like the map itself these exist at every level, so what they record is that the entry formula preserves the subgroup — not, on its own, that W normalizes it.
• TauCeti.frickeConjGamma0MulEquiv, TauCeti.frickeConjGamma1MulEquiv: for [NeZero N], the same maps as automorphisms Γ₀(N) ≃* Γ₀(N) and Γ₁(N) ≃* Γ₁(N), each its own inverse. These are the declarations that say W normalizes the subgroup.

Main results

• TauCeti.coe_frickeConjSL: the entries of frickeConjSL σ, namely !![d, -c/N; -N·b, a].
• TauCeti.frickeConjSL_mem_Gamma0: a Γ₀(N) input has frickeConjSL σ ∈ Γ₀(N), at every level.
• TauCeti.frickeConjSL_mem_Gamma1: a Γ₁(N) input has frickeConjSL σ ∈ Γ₁(N), at every level. This is a second hypothesis on σ, not a consequence of the previous line.
• TauCeti.frickeConjSL_mul, TauCeti.frickeConjSL_one: the entry map is multiplicative and unital, at every level. These are what the bundled endomorphisms above are built from.
• TauCeti.frickeConjGamma0_frickeConjGamma0, TauCeti.frickeConjGamma1_frickeConjGamma1: for [NeZero N], applying the entry map twice is the identity.
• TauCeti.gamma0Map_frickeConjGamma0_mul: the Gamma0Map images of frickeConjGamma0 σ and of σ are inverse in ZMod N, at every level. This is the ZMod-level content of AINTLIB's diamond-character companion; see the Provenance section.
• TauCeti.frickeConjGamma0MulEquiv_apply, TauCeti.frickeConjGamma0MulEquiv_symm, and their Γ₁ twins: the automorphisms act as the endomorphisms and are their own inverses. These, with coe_frickeConjGamma0 and coe_frickeConjGamma1, are the intended interface for the bundled declarations: a consumer works through these simp lemmas rather than through the bodies.
• TauCeti.frickeGL_mul_mapGL, TauCeti.mapGL_mul_frickeGL: for (N : K) ≠ 0, the two normalization identities W · σ = (W σ W⁻¹) · W and σ · W = W · (W σ W⁻¹) in GL (Fin 2) K. These are the statements that exhibit frickeConjSL σ as the conjugate W σ W⁻¹; that W normalizes the subgroup is the two MulEquivs.

Relation to the Atkin–Lehner anti-involution

TauCeti/NumberTheory/HeckeRing/GL2/Gamma0/AtkinLehner.lean also carries Γ₀(N) into itself, so the two results look superficially alike. They are different maps. That one is g ↦ w · gᵀ · w⁻¹ for the diagonal w = natDiagGL 2 ![1, N]: it transposes, and it is an anti-homomorphism, bundled as HeckeRing.GL2.atkinLehnerAntiInvolution_bar on the Hecke ring Δ₀(N). frickeConjSL is the entry formula for plain conjugation by !![0, -1; N, 0], with no transpose, and lives on Γ₀(N) itself. The two matrices are already distinguished in Fricke/Matrix.lean; this is the corresponding note for the two conjugation maps.

Provenance

Ported from the AINTLIB LeanModularForms project (LeanModularForms/HeckeRIngs/GL2/Fricke.lean, commit 340875adfb2, Apache-2.0, Chris Birkbeck), realizing part of Layer 6 of the ModularForms roadmap.

Ported from there: the divisibility witness and its spec (botLeftDiv, botLeftDiv_spec upstream, natCast_mul_lowerLeft_ediv here), frickeConjSL with its coercion lemma, frickeConjSL_mem_Gamma0 and frickeConjSL_mem_Gamma1, and the two normalization identities frickeGL_mul_mapGL and mapGL_mul_frickeGL. Added here, with no counterpart upstream: frickeConjSL_one, frickeConjSL_mul, lowerLeft_ediv_mul, mapGL_frickeConjSL, the bundled frickeConjGamma0 and frickeConjGamma1 with their involution lemmas, and the two MulEquivs frickeConjGamma0MulEquiv and frickeConjGamma1MulEquiv with their apply/symm lemmas.

AINTLIB names the divisibility witness botLeftDiv and keeps it private. Here its spec is public, as natCast_mul_lowerLeft_ediv, and it is @[simp]: coe_frickeConjSL writes the quotient c / N out as an Int.ediv, so a consumer of that simp lemma needs the spec to make progress, and keeping it private would force every use site to re-derive (N : ℤ) ∣ c from Gamma0_mem. The public API is therefore the matrix formula together with that one normalization rule.

AINTLIB obtains the witness as the Exists.choose of the Γ₀(N) divisibility, which makes it and frickeConjSL noncomputable and their entries opaque; here it is the honest quotient c / N, exact because N ∣ c, so both definitions are computable and reduce entrywise. AINTLIB states the two normalization identities over ℚ and then transports each along ℚ → ℝ by hand, in glMap_frickeGL_mul_mapGL and mapGL_mul_glMap_frickeGL; stating them over K as below makes both transports the corresponding instance, so those two lemmas have no counterpart here.

The diamond-character companion Gamma0MapUnits_frickeConjSL is ported in both of its halves. Its ZMod-level content is gamma0Map_frickeConjGamma0_mul below, and its unit-valued content is toHomUnits_gamma0Map_frickeConjGamma0_eq_inv. The two differ from upstream in how they reach the units: AINTLIB states the refinement in terms of its own Gamma0MapUnits, a unit-valued refinement of mathlib's CongruenceSubgroup.Gamma0Map, whereas here the same content is obtained from the ZMod identity through mathlib's MonoidHom.toHomUnits. What is not ported is that Gamma0MapUnits definition itself: TauCeti does not have it, and it belongs with the Gamma0Map API rather than with the Fricke conjugation.

References

• F. Diamond and J. Shurman, A First Course in Modular Forms, §5.

@[simp]

theorem TauCeti.natCast_mul_lowerLeft_ediv {N : ℕ} (σ : ↥(CongruenceSubgroup.Gamma0 N)) : ↑N * (↑↑σ 1 0 / ↑N) = ↑↑σ 1 0

The Γ₀(N) divisibility, in the exact form the entry formula needs: the lower-left entry c of σ is N times the quotient c / N, that quotient being exact because N ∣ c.

Public because coe_frickeConjSL displays c / N, an Int.ediv: without this a consumer of that simp lemma is left with an opaque quotient and has to re-derive (N : ℤ) ∣ c from Gamma0_mem at every use site. This is the only place the Γ₀(N) divisibility is used.

def TauCeti.frickeConjSL {N : ℕ} (σ : ↥(CongruenceSubgroup.Gamma0 N)) : Matrix.SpecialLinearGroup (Fin 2) ℤ

The Fricke conjugate of σ = !![a, b; N·c', d] ∈ Γ₀(N), as an element of SL(2, ℤ): the matrix !![d, -c'; -N·b, a].

It is defined by its entries rather than as a product, so it exists at every level; the conjugation it computes exists only at nonzero level, and at N = 0 the value is junk — see the Level section of the module docstring.

Over a field K with (N : K) ≠ 0 this is W · σ · W⁻¹, and equally W⁻¹ · σ · W since W² = (-N) • 1 is central; that is the content of frickeGL_mul_mapGL and mapGL_mul_frickeGL, which carry the invertibility hypothesis. At N = 0 the formula still defines a matrix, but a degenerate one; see the Level section of the module docstring.

Equations

• TauCeti.frickeConjSL σ = ⟨!![↑↑σ 1 1, -(↑↑σ 1 0 / ↑N); -↑N * ↑↑σ 0 1, ↑↑σ 0 0], ⋯⟩

@[simp]

theorem TauCeti.coe_frickeConjSL {N : ℕ} (σ : ↥(CongruenceSubgroup.Gamma0 N)) : ↑(frickeConjSL σ) = !![↑↑σ 1 1, -(↑↑σ 1 0 / ↑N); -↑N * ↑↑σ 0 1, ↑↑σ 0 0]

The underlying matrix of frickeConjSL σ, with the exact quotient c / N of the lower-left entry c written out.

theorem TauCeti.frickeConjSL_mem_Gamma0 {N : ℕ} (σ : ↥(CongruenceSubgroup.Gamma0 N)) : frickeConjSL σ ∈ CongruenceSubgroup.Gamma0 N

frickeConjSL preserves Γ₀(N): its lower-left entry -N·b is visibly divisible by N. This maps Γ₀(N) into Γ₀(N) at every level; that W normalizes the subgroup is frickeConjGamma0MulEquiv, which needs [NeZero N].

theorem TauCeti.frickeConjSL_mem_Gamma1 {N : ℕ} (σ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (hσ : σ ∈ CongruenceSubgroup.Gamma1 N) : frickeConjSL ⟨σ, ⋯⟩ ∈ CongruenceSubgroup.Gamma1 N

frickeConjSL preserves Γ₁(N): the formula swaps the two diagonal entries, so both remain ≡ 1 (mod N). Note that this needs σ ∈ Γ₁(N), not merely σ ∈ Γ₀(N). As for Γ₀(N) it maps the subgroup into itself at every level; normalization is frickeConjGamma1MulEquiv.

@[simp]

theorem TauCeti.frickeConjSL_one {N : ℕ} : frickeConjSL 1 = 1

frickeConjSL sends 1 to 1.

@[simp]

theorem TauCeti.frickeConjSL_mul {N : ℕ} (σ τ : ↥(CongruenceSubgroup.Gamma0 N)) : frickeConjSL (σ * τ) = frickeConjSL σ * frickeConjSL τ

frickeConjSL is multiplicative. Conjugation by W is a group homomorphism, and the entry formula records that at every level — including N = 0, where it is not a conjugation.

def TauCeti.frickeConjGamma0 {N : ℕ} : ↥(CongruenceSubgroup.Gamma0 N) →* ↥(CongruenceSubgroup.Gamma0 N)

The Fricke entry formula as a group endomorphism Γ₀(N) →* Γ₀(N). This is the bundled form of frickeConjSL_mem_Gamma0, and it is what a consumer needs in order to transport a subgroup along the map.

Like frickeConjSL it exists at every level, so on its own it records that the entry formula preserves Γ₀(N) rather than that W normalizes it. At nonzero level it is an isomorphism, frickeConjGamma0MulEquiv, and that is the declaration that states the normalization.

Equations

• TauCeti.frickeConjGamma0 = { toFun := fun (σ : ↥(CongruenceSubgroup.Gamma0 N)) => ⟨TauCeti.frickeConjSL σ, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.coe_frickeConjGamma0 {N : ℕ} (σ : ↥(CongruenceSubgroup.Gamma0 N)) : ↑(frickeConjGamma0 σ) = frickeConjSL σ

The SL(2, ℤ) matrix underlying frickeConjGamma0 σ is frickeConjSL σ: the characterizing lemma for the bundled map.

def TauCeti.frickeConjGamma1 {N : ℕ} : ↥(CongruenceSubgroup.Gamma1 N) →* ↥(CongruenceSubgroup.Gamma1 N)

The Fricke entry formula restricted to Γ₁(N), as a group endomorphism Γ₁(N) →* Γ₁(N); the Γ₁ counterpart of frickeConjGamma0, bundling frickeConjSL_mem_Gamma1, and like it defined at every level.

Equations

• TauCeti.frickeConjGamma1 = { toFun := fun (σ : ↥(CongruenceSubgroup.Gamma1 N)) => ⟨TauCeti.frickeConjSL ⟨↑σ, ⋯⟩, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.coe_frickeConjGamma1 {N : ℕ} (σ : ↥(CongruenceSubgroup.Gamma1 N)) : ↑(frickeConjGamma1 σ) = frickeConjSL ⟨↑σ, ⋯⟩

The SL(2, ℤ) matrix underlying frickeConjGamma1 σ is frickeConjSL σ: the characterizing lemma for the bundled map, as coe_frickeConjGamma0 is at level Γ₀(N).

theorem TauCeti.gamma0Map_frickeConjGamma0_mul {N : ℕ} (σ : ↥(CongruenceSubgroup.Gamma0 N)) : (CongruenceSubgroup.Gamma0Map N) (frickeConjGamma0 σ) * (CongruenceSubgroup.Gamma0Map N) σ = 1

The Fricke conjugation inverts the diamond label. Gamma0Map reads the lower-right entry mod N; conjugation swaps the two diagonal entries, so it reads a where it read d, and a · d ≡ 1 (mod N) because det σ = 1 and N ∣ c.

Stated at the ZMod level, which is where Gamma0Map lands; the unit-valued form is toHomUnits_gamma0Map_frickeConjGamma0_eq_inv, derived from this one. Without it a consumer computing a nebentypus along the Fricke involution has to redo the determinant argument.

@[simp]

theorem TauCeti.toHomUnits_gamma0Map_frickeConjGamma0_eq_inv {N : ℕ} (σ : ↥(CongruenceSubgroup.Gamma0 N)) : (CongruenceSubgroup.Gamma0Map N).toHomUnits (frickeConjGamma0 σ) = ((CongruenceSubgroup.Gamma0Map N).toHomUnits σ)⁻¹

The unit-valued form of gamma0Map_frickeConjGamma0_mul: on units, the Gamma0Map image of frickeConjGamma0 σ is the inverse of that of σ. This is the shape the diamond-character and nebentypus consumers work in, obtained from the ZMod identity through Mathlib's MonoidHom.toHomUnits.

theorem TauCeti.frickeConjSL_frickeConjSL {N : ℕ} [NeZero N] (σ : ↥(CongruenceSubgroup.Gamma0 N)) : frickeConjSL ⟨frickeConjSL σ, ⋯⟩ = ↑σ

Applying the entry map twice is the identity, at nonzero level, on SL(2, ℤ) itself: this is the entrywise content of the involution, stated where a consumer holding a plain frickeConjSL σ can use it without wrapping into Γ₀(N). The two bundled involutions below are Subtype.ext of this.

This genuinely needs N ≠ 0. At level zero the lower-left entry -N·b of frickeConjSL σ is 0 whatever b is, so the formula forgets b and cannot be undone; see the Level section of the module docstring.

@[simp]

theorem TauCeti.frickeConjGamma0_frickeConjGamma0 {N : ℕ} [NeZero N] (σ : ↥(CongruenceSubgroup.Gamma0 N)) : frickeConjGamma0 (frickeConjGamma0 σ) = σ

The Fricke conjugation is an involution at nonzero level: applying it twice is the identity on Γ₀(N). This is frickeConjSL_frickeConjSL read through Subtype.ext.

theorem TauCeti.frickeConjGamma0_involutive {N : ℕ} [NeZero N] : Function.Involutive ⇑frickeConjGamma0

frickeConjGamma0 is involutive, in the form Function.Involutive consumes.

def TauCeti.frickeConjGamma0MulEquiv {N : ℕ} [NeZero N] : ↥(CongruenceSubgroup.Gamma0 N) ≃* ↥(CongruenceSubgroup.Gamma0 N)

The Fricke conjugation as an automorphism of Γ₀(N), for nonzero level: the isomorphism Γ₀(N) ≃* Γ₀(N) that frickeConjGamma0 becomes once it is known to be involutive. It is its own inverse.

This is the declaration that expresses that W normalizes Γ₀(N): frickeConjGamma0 maps the subgroup into itself at every level, and the level hypothesis is what upgrades that to an isomorphism.

Equations

• TauCeti.frickeConjGamma0MulEquiv = { toEquiv := Function.Involutive.toPerm ⇑TauCeti.frickeConjGamma0 ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.frickeConjGamma0MulEquiv_apply {N : ℕ} [NeZero N] (σ : ↥(CongruenceSubgroup.Gamma0 N)) : frickeConjGamma0MulEquiv σ = frickeConjGamma0 σ

frickeConjGamma0MulEquiv acts as frickeConjGamma0. This is its defining lemma and, with frickeConjGamma0MulEquiv_symm, the intended interface: a consumer simplifies through these rather than through the body of the bundled definition.

@[simp]

theorem TauCeti.frickeConjGamma0MulEquiv_symm {N : ℕ} [NeZero N] : frickeConjGamma0MulEquiv.symm = frickeConjGamma0MulEquiv

frickeConjGamma0MulEquiv is its own inverse. The underlying map is an involution, so symm returns the automorphism unchanged; this is the simp lemma that normalizes e.symm.

@[simp]

theorem TauCeti.frickeConjGamma1_frickeConjGamma1 {N : ℕ} [NeZero N] (σ : ↥(CongruenceSubgroup.Gamma1 N)) : frickeConjGamma1 (frickeConjGamma1 σ) = σ

The Γ₁(N) counterpart of frickeConjGamma0_frickeConjGamma0.

theorem TauCeti.frickeConjGamma1_involutive {N : ℕ} [NeZero N] : Function.Involutive ⇑frickeConjGamma1

frickeConjGamma1 is involutive, in the form Function.Involutive consumes.

def TauCeti.frickeConjGamma1MulEquiv {N : ℕ} [NeZero N] : ↥(CongruenceSubgroup.Gamma1 N) ≃* ↥(CongruenceSubgroup.Gamma1 N)

The Fricke conjugation as an automorphism of Γ₁(N), for nonzero level; the Γ₁ counterpart of frickeConjGamma0MulEquiv.

Equations

• TauCeti.frickeConjGamma1MulEquiv = { toEquiv := Function.Involutive.toPerm ⇑TauCeti.frickeConjGamma1 ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.frickeConjGamma1MulEquiv_apply {N : ℕ} [NeZero N] (σ : ↥(CongruenceSubgroup.Gamma1 N)) : frickeConjGamma1MulEquiv σ = frickeConjGamma1 σ

frickeConjGamma1MulEquiv acts as frickeConjGamma1; the Γ₁(N) counterpart of frickeConjGamma0MulEquiv_apply.

@[simp]

theorem TauCeti.frickeConjGamma1MulEquiv_symm {N : ℕ} [NeZero N] : frickeConjGamma1MulEquiv.symm = frickeConjGamma1MulEquiv

The Γ₁(N) counterpart of frickeConjGamma0MulEquiv_symm.

theorem TauCeti.frickeGL_mul_mapGL {N : ℕ} (K : Type u_1) [Field K] [NeZero ↑N] (σ : ↥(CongruenceSubgroup.Gamma0 N)) : frickeGL K N * (Matrix.SpecialLinearGroup.mapGL K) ↑σ = (Matrix.SpecialLinearGroup.mapGL K) (frickeConjSL σ) * frickeGL K N

The normalization identity W · σ = (W σ W⁻¹) · W in GL (Fin 2) K, for σ ∈ Γ₀(N). This is the form that moves W from the left of σ to its right, which is what a slash-action computation needs.

theorem TauCeti.mapGL_frickeConjSL {N : ℕ} (K : Type u_1) [Field K] [NeZero ↑N] (σ : ↥(CongruenceSubgroup.Gamma0 N)) : (Matrix.SpecialLinearGroup.mapGL K) (frickeConjSL σ) = frickeGL K N * (Matrix.SpecialLinearGroup.mapGL K) ↑σ * (frickeGL K N)⁻¹

frickeConjSL σ is the Fricke conjugate, in the form the name asserts: mapGL K (frickeConjSL σ) = W · σ · W⁻¹. This is frickeGL_mul_mapGL with W moved across, and it is the characterization the frickeConj* names advertise.

theorem TauCeti.mapGL_mul_frickeGL {N : ℕ} (K : Type u_1) [Field K] [NeZero ↑N] (σ : ↥(CongruenceSubgroup.Gamma0 N)) : (Matrix.SpecialLinearGroup.mapGL K) ↑σ * frickeGL K N = frickeGL K N * (Matrix.SpecialLinearGroup.mapGL K) (frickeConjSL σ)

The mirror normalization identity σ · W = W · (W σ W⁻¹) in GL (Fin 2) K, for σ ∈ Γ₀(N); equivalently frickeConjSL σ = W⁻¹ · σ · W.