Modular-forms basics: extensions of Mathlib's API

Small generic lemmas extending Mathlib/NumberTheory/ModularForms/Basic.lean and its slash actions: the conjugation σ is trivial on SL(2, ℤ)-matrices — a special case of UpperHalfPlane.σ_eq_refl_of_det_pos, which lives with σ itself in TauCeti/Analysis/Complex/UpperHalfPlane/MoebiusAction.lean — the CuspForm translation equations Mathlib does not yet provide (CuspForm.mcast_apply and the GL(2, ℝ)-level CuspForm.coe_translate_gl), and the weight-k slash action of -I (ModularForm.slash_neg_one), the source of every parity constraint on weights and nebentypus characters.

It also records how modular and cusp forms move between two nested groups Γ' ≤ Γ. Shrinking the group is unconditional (ModularForm.ofLe): slash invariance restricts, and every cusp of Γ' is a cusp of Γ (IsCusp.mono), so the boundedness conditions restrict as well. Enlarging it is not: a Γ'-form which happens to be Γ-slash invariant is bounded only at the cusps of Γ', so one needs to know that Γ has no further cusps, which ModularForm.ofSlashInvariant takes as its hypothesis. Two arithmetic groups always satisfy it (Subgroup.IsArithmetic.isCusp_of_isCusp: both have the cusps of SL(2, ℤ)). Under it the two constructions are mutually inverse: the image of M_k(Γ) → M_k(Γ') is exactly the Γ-invariant part of M_k(Γ') (ModularForm.mem_range_ofLeₗ_iff).

Translation by a positive-determinant matrix is packaged as the linear map ModularForm.translateₗ. General GL₂(ℝ) translation is only semilinear because a negative-determinant matrix applies complex conjugation, whereas a positive-determinant matrix acts ℂ-linearly.

The first group of lemmas was split out of the diamond-operator development ported from the AINTLIB LeanModularForms project (https://github.com/CBirkbeck/AINTLIB/tree/main/projects/LeanModularForms).

Main definitions

• ModularForm.ofLe, CuspForm.ofLe (and their ℂ-linear packagings ofLeₗ): a form for Γ read as a form for a subgroup Γ' ≤ Γ.
• ModularForm.ofSlashInvariant, CuspForm.ofSlashInvariant: a Γ'-form which is slash invariant under a group Γ all of whose cusps are cusps of Γ', read as a form for Γ.
• ModularForm.translateₗ: translation by a positive-determinant element of GL₂(ℝ) as a ℂ-linear map.

Main results

• ModularForm.slash_scalar: a real scalar matrix acts by its scalar to the power k - 2 under the weight-k slash action.
• SlashInvariantFormClass.SL_slash_eq: a form invariant under the image of Γ ≤ SL(2, ℤ) is fixed by the slash action of every element of Γ.
• SlashInvariantForm.slash_action_eqn_of_det_pos: the transformation law f (γ • τ) = |det γ| ^ (1 - k) * denom γ τ ^ k * f τ for γ of positive determinant, generalising Mathlib's slash_action_eqn'', which assumes det γ = 1.
• slash_zpow_eq_self_of_slash_eq, slash_zpow_mul_mul_zpow_eq_smul: slash invariance passes to integer powers, and an eigenvalue law survives multiplication on both sides by powers of an invariance.
• Subgroup.IsArithmetic.isCusp_of_isCusp: any two arithmetic groups have the same cusps.
• TauCeti.ModularForm.eq_zero_of_eq_const: a constant slash-invariant form of nonzero weight vanishes when its group has finite-index intersection with the modular group.
• ModularForm.mem_range_ofLeₗ_iff, CuspForm.mem_range_ofLeₗ_iff: for Γ' ≤ Γ with every cusp of Γ a cusp of Γ', a form for Γ' extends to Γ exactly when it is Γ-slash invariant.

theorem det_pos_of_mem_slGL {g : GL (Fin 2) ℝ} (hg : g ∈ (Matrix.SpecialLinearGroup.mapGL ℝ).range) : 0 < (↑g).det

Every element of 𝒮ℒ has positive determinant: it is the image of a matrix of determinant 1.

This is the hypothesis the positive-determinant slash lemmas take — σ_eq_refl_of_det_pos just below, and orderOfVanishingAt_slash / orderOfVanishingAt_smul in TauCeti.NumberTheory.ModularForms.Order.OfVanishing — and every modular call site discharges it the same way. Keying it on membership in 𝒮ℒ rather than on Matrix.SpecialLinearGroup.mapGL covers both shapes the call sites come in: a direct image mapGL ℝ γ (via MonoidHom.mem_range.mpr ⟨γ, rfl⟩) and an element of the image of a subgroup Γ ≤ SL(2, ℤ) (via Subgroup.map_le_range).

@[simp]

theorem σ_mapGL_real_eq_refl (s : Matrix.SpecialLinearGroup (Fin 2) ℤ) : UpperHalfPlane.σ ((Matrix.SpecialLinearGroup.mapGL ℝ) s) = ContinuousAlgEquiv.refl ℝ ℂ

The slash-action conjugation σ is the identity for matrices coming from SL₂(ℤ): their determinant is 1 > 0, so the σ branch picks ContinuousAlgEquiv.refl ℝ ℂ.

This keeps @[simp] even though UpperHalfPlane.σ_eq_refl_of_det_pos is also @[simp]: that one is conditional, and simp cannot discharge 0 < (↑(mapGL ℝ s)).det on its own — the determinant of a mapped SL(2, ℤ) matrix reduces through GeneralLinearGroup.det, not through Matrix.det of the entrywise map. So the two do not overlap in practice.

Slash invariance under a fixed matrix

Ported from the AINTLIB LeanModularForms project (Chris Birkbeck), Apache-2.0, file LeanModularForms/Eigenforms/ConductorTheorem.lean at commit 2baa76f742bdb4fb8ee323fabba41203bd390e08 (https://github.com/CBirkbeck/AINTLIB): slash_T_zpow_eq_self_of_slash_T_eq (:176) and conductor_slash_T_conj_eq (:186). The source states both for powers of ModularGroup.T in SL(2, ℤ); they are recorded here for GL (Fin 2) ℝ, which is all their proofs use.

theorem slash_zpow_eq_self_of_slash_eq (k : ℤ) (f : UpperHalfPlane → ℂ) {A : GL (Fin 2) ℝ} (hf : SlashAction.map k A f = f) (j : ℤ) : SlashAction.map k (A ^ j) f = f

Slash invariance passes to every integer power. If f ∣[k] A = f then f ∣[k] A ^ j = f for every j : ℤ: f is a fixed point of the slash action of A, and MulAction.mem_fixedBy_zpow carries a fixed point along every integer power.

theorem slash_zpow_mul_mul_zpow_eq_smul (k : ℤ) (f : UpperHalfPlane → ℂ) {δ γ : GL (Fin 2) ℝ} (hδdet : 0 < (↑δ).det) (hδ : SlashAction.map k δ f = f) {z : ℂ} (hγ : SlashAction.map k γ f = z • f) (i j : ℤ) : SlashAction.map k (δ ^ i * γ * δ ^ j) f = z • f

An eigenvalue law survives multiplication on both sides by powers of an invariance. If f is fixed by δ and slashing by γ multiplies it by z, then slashing by δ ^ i * γ * δ ^ j does too, for independent i and j — this is a conjugation only in the special case j = -i.

Nothing is asked of γ beyond that law. The determinant hypothesis on δ is exactly what keeps σ out of the conclusion: σ is then trivial on every power of δ, so the scalar z passes through the outer slash unconjugated. For δ in the image of SL(2, ℤ) that hypothesis is det_pos_of_mem_slGL.

The level-lowering step of the conductor theorem is the case δ = T, with γ the conjugate conjScale l γ' c supplied by the T-factorisation of Γ₀(N / l).

theorem CuspForm.mcast_apply {a b : ℤ} {Γ Γ' : Subgroup (GL (Fin 2) ℝ)} (h : a = b) (f : CuspForm Γ a) (hΓ : Γ' = Γ := by rfl) (z : UpperHalfPlane) : (mcast h f hΓ) z = f z

CuspForm.mcast does not change the pointwise values of a cusp form: the CuspForm analogue of Mathlib's ModularForm.mcast_apply, which Mathlib does not yet provide.

@[simp]

theorem CuspForm.coe_translate_gl {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} [CuspFormClass F Γ k] (f : F) (g : GL (Fin 2) ℝ) : ⇑(translate f g) = SlashAction.map k g ⇑f

GL(2, ℝ)-level coercion lemma for CuspForm.translate; Mathlib's CuspForm.coe_translate is specialized to SL(2, ℤ) arguments.

@[simp]

theorem ModularForm.slash_neg_one (k : ℤ) (f : UpperHalfPlane → ℂ) : SlashAction.map k (-1) f = (-1) ^ k • f

The weight-k slash action of -I is multiplication by (-1) ^ k: -I acts trivially on ℍ and has determinant 1, so the only surviving factor is its automorphy factor denom (-I) z ^ (-k) = (-1) ^ (-k) = (-1) ^ k.

This is the source of every parity constraint on weights and nebentypus characters.

theorem ModularForm.slash_def_of_det_pos (k : ℤ) {g : GL (Fin 2) ℝ} (hg : 0 < (↑g).det) (f : UpperHalfPlane → ℂ) : SlashAction.map k g f = fun (τ : UpperHalfPlane) => f (g • τ) * ↑|↑(Matrix.GeneralLinearGroup.det g)| ^ (k - 1) * UpperHalfPlane.denom g ↑τ ^ (-k)

The weight-k slash formula at a positive-determinant matrix, free of the σ twist:

f ∣[k] g = fun τ ↦ f (g • τ) * |det g| ^ (k - 1) * denom g τ ^ (-k).

Mathlib's ModularForm.slash_def carries σ g around the value of f, which is complex conjugation on the negative-determinant branch. ModularForm.SL_slash_def drops it because det = 1; here positivity alone is what does it.

theorem ModularForm.slash_apply_of_det_pos (k : ℤ) {g : GL (Fin 2) ℝ} (hg : 0 < (↑g).det) (f : UpperHalfPlane → ℂ) (τ : UpperHalfPlane) : SlashAction.map k g f τ = f (g • τ) * ↑|↑(Matrix.GeneralLinearGroup.det g)| ^ (k - 1) * UpperHalfPlane.denom g ↑τ ^ (-k)

The pointwise form of ModularForm.slash_def_of_det_pos, matching ModularForm.SL_slash_apply.

@[simp]

theorem ModularForm.smul_slash_of_det_pos {α : Type u_1} [SMul α ℂ] [IsScalarTower α ℂ ℂ] (k : ℤ) {g : GL (Fin 2) ℝ} (hg : 0 < (↑g).det) (f : UpperHalfPlane → ℂ) (c : α) : SlashAction.map k g (c • f) = c • SlashAction.map k g f

Scalars pass through the slash of a positive-determinant matrix. Mathlib's ModularForm.smul_slash carries the twist σ A c, which is complex conjugation when the determinant is negative, so scalars do not commute past a general slash. On the positive branch they do.

This is what makes a Hecke operator ℂ-linear: it is a sum of slashes by representatives of positive determinant. The scalar generality matches ModularForm.SL_smul_slash.

@[simp]

theorem ModularForm.slash_scalar (k : ℤ) (u : ℝˣ) (f : UpperHalfPlane → ℂ) : SlashAction.map k ((Matrix.GeneralLinearGroup.scalar (Fin 2)) u) f = ↑↑u ^ (k - 2) • f

A real scalar matrix acts trivially on the upper half-plane, and its weight-k slash is multiplication by the scalar to the power k - 2.

The calculation generalizes AINTLIB's slash_diag_scalar (Chris Birkbeck, Apache-2.0), in LeanModularForms/HeckeRIngs/GL2/Unified/NebentypusHeckeRingHom.lean at commit 2baa76f742bdb4fb8ee323fabba41203bd390e08.

theorem SlashInvariantFormClass.SL_slash_eq {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {k : ℤ} {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k] (f : F) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (hγ : γ ∈ Γ) : SlashAction.map k γ ⇑f = ⇑f

A form invariant under the image in GL(2, ℝ) of a subgroup Γ ≤ SL(2, ℤ) is fixed by the weight-k slash action of every element of Γ — the invariance condition read back at the SL₂(ℤ) level, where congruence subgroups are given.

theorem SlashInvariantForm.slash_action_eqn_of_det_pos {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [SlashInvariantFormClass F Γ k] (f : F) {γ : GL (Fin 2) ℝ} (hγ : γ ∈ Γ) (hdet : 0 < (↑γ).det) (τ : UpperHalfPlane) : f (γ • τ) = ↑|↑(Matrix.GeneralLinearGroup.det γ)| ^ (1 - k) * UpperHalfPlane.denom γ ↑τ ^ k * f τ

The transformation law of a slash-invariant form under a positive-determinant element. For γ ∈ Γ with 0 < det γ, f (γ • τ) = |det γ| ^ (1 - k) * denom γ τ ^ k * f τ.

Mathlib's SlashInvariantForm.slash_action_eqn'' is the det = 1 case, in which the first factor is 1 and disappears.

Translation by positive-determinant matrices

noncomputable def ModularForm.translateₗ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [Γ.HasDetOne] (g : GL (Fin 2) ℝ) (hg : 0 < ↑(Matrix.GeneralLinearGroup.det g)) : ModularForm Γ k →ₗ[ℂ] ModularForm (ConjAct.toConjAct g⁻¹ • Γ) k

Translation by g ∈ GL₂(ℝ) with 0 < det g as a linear map on modular forms.

Equations

• ModularForm.translateₗ g hg = { toFun := fun (f : ModularForm Γ k) => ModularForm.translate f g, map_add' := ⋯, map_smul' := ⋯ }

theorem ModularForm.translateₗ_apply {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [Γ.HasDetOne] (g : GL (Fin 2) ℝ) (hg : 0 < ↑(Matrix.GeneralLinearGroup.det g)) (f : ModularForm Γ k) : (translateₗ g hg) f = translate f g

Changing the invariance group

Throughout, Γ' ≤ Γ are subgroups of GL(2, ℝ).

theorem Subgroup.IsArithmetic.isCusp_of_isCusp {Γ Γ' : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] [Γ'.IsArithmetic] (c : OnePoint ℝ) (hc : IsCusp c Γ) : IsCusp c Γ'

Two arithmetic subgroups of GL(2, ℝ) have the same cusps, namely those of SL(2, ℤ). This is the standard way to supply the cusp hypothesis of ModularForm.ofSlashInvariant.

def ModularForm.ofLe {Γ Γ' : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (h : Γ' ≤ Γ) (f : ModularForm Γ k) : ModularForm Γ' k

A modular form for Γ is a modular form for any subgroup Γ' ≤ Γ: slash invariance restricts, and a cusp of Γ' is a cusp of Γ, so the boundedness conditions restrict too.

Equations

• ModularForm.ofLe h f = { toFun := ⇑f, slash_action_eq' := ⋯, holo' := ⋯, bdd_at_cusps' := ⋯ }

@[simp]

theorem ModularForm.coe_ofLe {Γ Γ' : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (h : Γ' ≤ Γ) (f : ModularForm Γ k) : ⇑(ofLe h f) = ⇑f

theorem ModularForm.ofLe_injective {Γ Γ' : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (h : Γ' ≤ Γ) : Function.Injective (ofLe h)

def ModularForm.ofLeₗ {Γ Γ' : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [Γ.HasDetOne] [Γ'.HasDetOne] (h : Γ' ≤ Γ) : ModularForm Γ k →ₗ[ℂ] ModularForm Γ' k

Restriction of the invariance group, as a ℂ-linear map.

Equations

• ModularForm.ofLeₗ h = { toFun := ModularForm.ofLe h, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem ModularForm.ofLeₗ_apply {Γ Γ' : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [Γ.HasDetOne] [Γ'.HasDetOne] (h : Γ' ≤ Γ) (f : ModularForm Γ k) : (ofLeₗ h) f = ofLe h f

theorem ModularForm.ofLeₗ_injective {Γ Γ' : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [Γ.HasDetOne] [Γ'.HasDetOne] (h : Γ' ≤ Γ) : Function.Injective ⇑(ofLeₗ h)

def ModularForm.ofSlashInvariant {Γ Γ' : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (hc : ∀ (c : OnePoint ℝ), IsCusp c Γ → IsCusp c Γ') (f : ModularForm Γ' k) (hf : ∀ γ ∈ Γ, SlashAction.map k γ ⇑f = ⇑f) : ModularForm Γ k

A modular form for Γ' which is slash invariant under a group Γ every cusp of which is a cusp of Γ' is a modular form for Γ. The hypothesis hc on cusps is what makes this legitimate: without it, enlarging the invariance group can create cusps at which nothing is known. Two arithmetic groups always satisfy it (Subgroup.IsArithmetic.isCusp_of_isCusp).

Equations

• ModularForm.ofSlashInvariant hc f hf = { toFun := ⇑f, slash_action_eq' := hf, holo' := ⋯, bdd_at_cusps' := ⋯ }

@[simp]

theorem ModularForm.coe_ofSlashInvariant {Γ Γ' : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (hc : ∀ (c : OnePoint ℝ), IsCusp c Γ → IsCusp c Γ') (f : ModularForm Γ' k) (hf : ∀ γ ∈ Γ, SlashAction.map k γ ⇑f = ⇑f) : ⇑(ofSlashInvariant hc f hf) = ⇑f

theorem ModularForm.mem_range_ofLeₗ_iff {Γ Γ' : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [Γ.HasDetOne] [Γ'.HasDetOne] (h : Γ' ≤ Γ) (hc : ∀ (c : OnePoint ℝ), IsCusp c Γ → IsCusp c Γ') (f : ModularForm Γ' k) : f ∈ (ofLeₗ h).range ↔ ∀ γ ∈ Γ, SlashAction.map k γ ⇑f = ⇑f

For Γ' ≤ Γ with every cusp of Γ a cusp of Γ', a modular form for Γ' comes from a modular form for Γ exactly when it is Γ-slash invariant.

def CuspForm.ofLe {Γ Γ' : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (h : Γ' ≤ Γ) (f : CuspForm Γ k) : CuspForm Γ' k

A cusp form for Γ is a cusp form for any subgroup Γ' ≤ Γ.

Equations

• CuspForm.ofLe h f = { toFun := ⇑f, slash_action_eq' := ⋯, holo' := ⋯, zero_at_cusps' := ⋯ }

@[simp]

theorem CuspForm.coe_ofLe {Γ Γ' : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (h : Γ' ≤ Γ) (f : CuspForm Γ k) : ⇑(ofLe h f) = ⇑f

theorem CuspForm.ofLe_injective {Γ Γ' : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (h : Γ' ≤ Γ) : Function.Injective (ofLe h)

def CuspForm.ofLeₗ {Γ Γ' : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [Γ.HasDetOne] [Γ'.HasDetOne] (h : Γ' ≤ Γ) : CuspForm Γ k →ₗ[ℂ] CuspForm Γ' k

Restriction of the invariance group, as a ℂ-linear map.

Equations

• CuspForm.ofLeₗ h = { toFun := CuspForm.ofLe h, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem CuspForm.ofLeₗ_apply {Γ Γ' : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [Γ.HasDetOne] [Γ'.HasDetOne] (h : Γ' ≤ Γ) (f : CuspForm Γ k) : (ofLeₗ h) f = ofLe h f

theorem CuspForm.ofLeₗ_injective {Γ Γ' : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [Γ.HasDetOne] [Γ'.HasDetOne] (h : Γ' ≤ Γ) : Function.Injective ⇑(ofLeₗ h)

def CuspForm.ofSlashInvariant {Γ Γ' : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (hc : ∀ (c : OnePoint ℝ), IsCusp c Γ → IsCusp c Γ') (f : CuspForm Γ' k) (hf : ∀ γ ∈ Γ, SlashAction.map k γ ⇑f = ⇑f) : CuspForm Γ k

A cusp form for Γ' which is slash invariant under a group Γ every cusp of which is a cusp of Γ' is a cusp form for Γ; see ModularForm.ofSlashInvariant for why the cusp hypothesis is needed.

Equations

• CuspForm.ofSlashInvariant hc f hf = { toFun := ⇑f, slash_action_eq' := hf, holo' := ⋯, zero_at_cusps' := ⋯ }

@[simp]

theorem CuspForm.coe_ofSlashInvariant {Γ Γ' : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} (hc : ∀ (c : OnePoint ℝ), IsCusp c Γ → IsCusp c Γ') (f : CuspForm Γ' k) (hf : ∀ γ ∈ Γ, SlashAction.map k γ ⇑f = ⇑f) : ⇑(ofSlashInvariant hc f hf) = ⇑f

theorem CuspForm.mem_range_ofLeₗ_iff {Γ Γ' : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [Γ.HasDetOne] [Γ'.HasDetOne] (h : Γ' ≤ Γ) (hc : ∀ (c : OnePoint ℝ), IsCusp c Γ → IsCusp c Γ') (f : CuspForm Γ' k) : f ∈ (ofLeₗ h).range ↔ ∀ γ ∈ Γ, SlashAction.map k γ ⇑f = ⇑f

For Γ' ≤ Γ with every cusp of Γ a cusp of Γ', a cusp form for Γ' comes from a cusp form for Γ exactly when it is Γ-slash invariant.

Constant forms at nonzero weight

theorem TauCeti.ModularForm.eq_zero_of_eq_const_of_weight_ne_zero {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] [SlashInvariantFormClass F Γ k] {f : F} {c : ℂ} (hf : ⇑f = Function.const UpperHalfPlane c) (hk : k ≠ 0) {γ : GL (Fin 2) ℝ} (hγ : γ ∈ Γ) (hdet : Matrix.GeneralLinearGroup.det γ = 1) (hc : ↑γ 1 0 ≠ 0) : c = 0

A constant slash-invariant form of nonzero weight vanishes if its group contains a determinant-one matrix with nonzero lower-left entry. No holomorphy or cusp condition is needed.

This extends Mathlib's level-one SlashInvariantForm.wt_eq_zero_of_eq_const: the nonconstant automorphy factor, rather than invariance under S itself, excludes a nonzero constant.

theorem TauCeti.ModularForm.exists_mem_lowerLeft_ne_zero {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsFiniteRelIndex (Matrix.SpecialLinearGroup.mapGL ℝ).range] : ∃ γ ∈ Γ ⊓ (Matrix.SpecialLinearGroup.mapGL ℝ).range, ↑γ 1 0 ≠ 0

A group with finite-index intersection with the modular group contains a matrix in that intersection with nonzero lower-left entry.

theorem TauCeti.ModularForm.eq_zero_of_eq_const {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [Γ.IsFiniteRelIndex (Matrix.SpecialLinearGroup.mapGL ℝ).range] {F : Type u_1} [FunLike F UpperHalfPlane ℂ] [SlashInvariantFormClass F Γ k] {f : F} {c : ℂ} (hf : ⇑f = Function.const UpperHalfPlane c) (hk : k ≠ 0) : c = 0

A slash-invariant form of nonzero weight whose group has finite-index intersection with the modular group cannot be a nonzero constant.