Upper-triangular slashes of a level-raise

For g slash-invariant under a group with 1 as a strict period, the level-raise V_p g = p^(1-k) • (g ∣[k] scaleGL p) (the function τ ↦ g (p τ)) is slashed by the upper-triangular matrix !![1, b; 0, p] back to p⁻¹ • g: (V_p g) ((τ + b) / p) = g (τ + b) = g τ, by the period-1 invariance of g. This is the upper-triangular part of the descent of a level-raise (Newforms/Descent/LevelRaise/Basic.lean).

Main results

• TauCeti.smul_slash_scaleGL_slash_upperTriRep: for g slash-invariant with period 1, (p^(1-k) • (g ∣[k] scaleGL p)) ∣[k] !![1, b; 0, p] = p⁻¹ • g.

Provenance

Adapted from the AINTLIB LeanModularForms project (Chris Birkbeck, Apache-2.0, https://github.com/CBirkbeck/AINTLIB @ eb9621e7bcb0ce220ad53983ec45d987cb5b9002), projects/LeanModularForms/LeanModularForms/StrongMultiplicityOne/HeckeDescent.lean (V_p_slash_upper_aux). The source's modularFormLevelRaise is this repository's ModularForm.levelRaise; the statement is re-proved on the underlying function, for any group with 1 as a strict period.

theorem TauCeti.smul_slash_scaleGL_slash_upperTriRep {p : ℕ} [NeZero p] (k : ℤ) {Γ : Subgroup (GL (Fin 2) ℝ)} (hper : 1 ∈ Γ.strictPeriods) {F : Type u_1} [FunLike F UpperHalfPlane ℂ] [SlashInvariantFormClass F Γ k] (g : F) (b : Fin p) : SlashAction.map k (HeckeRing.GL2.upperTriRep p b) (↑p ^ (1 - k) • SlashAction.map k (scaleGL p) ⇑g) = (↑p)⁻¹ • ⇑g

An upper-triangular matrix slashes a level-raise back to the form: for g slash-invariant under a group Γ with 1 as a strict period and V_p g = p^(1-k) • (g ∣[k] scaleGL p), (V_p g) ∣[k] !![1, b; 0, p] = p⁻¹ • g.