Orders along the norm map

The general-level valence formula reads the level-one formula off the norm ModularForm.norm, so it needs the orders of a form to distribute over the norm's coset product. This file records that distribution at interior points, for a form on any subgroup of finite relative index: each coset factor is nonzero when the form is, and the vanishing order of the norm is the sum of the orders of the factors.

Main declarations

• TauCeti.SlashInvariantForm.quotientFunc_ne_zero: a coset factor of the norm of a nonzero form is nonzero.
• TauCeti.ModularForm.orderOfVanishingAt_norm: the vanishing order of the norm at a point is the sum, over the coset space, of the vanishing orders of the coset factors.
• TauCeti.ModularForm.orderOfVanishingAt_quotientFunc_le_orderOfVanishingAt_norm: each coset factor vanishes to at most the order the norm does, with TauCeti.ModularForm.orderOfVanishingAt_le_orderOfVanishingAt_norm as the identity-coset corollary — so the zeros of the norm dominate those of the form.
• TauCeti.ModularForm.finite_image_orbit_mk_setOf_orderOfVanishingAt_ne_zero_subgroup: the consumer of that domination — at any level of finite relative index in 𝒮ℒ, the image in 𝒢 \ ℍ of the points at which a form has nonzero vanishing order is finite. Equivalently, those points meet only finitely many 𝒢-orbits.

References

• The two-step route used here — order domination under the norm carries the support into the finite support of the level-one norm, and finite index makes the fibres of the orbit comparison finite — was arrived at independently of, and concurrently with, PR #3330, which gives the same argument for a subgroup of SL(2, ℤ) of finite index. That work has since landed; nothing here depends on it, and the two remain independent derivations rather than one building on the other.

  The statements differ in the group: this one takes 𝒢 ≤ GL (Fin 2) ℝ of finite relative index in 𝒮ℒ, which need not lie inside 𝒮ℒ. That is also why the order is not descended to the quotient here — 𝒢 may contain elements of negative determinant, under which the vanishing order is not known to be invariant (orderOfVanishingAt_smul asks for 0 < det) — so only the image of the nonzero-order set in 𝒢 \ ℍ is claimed, not an order function on it.

theorem TauCeti.SlashInvariantForm.quotientFunc_ne_zero {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {k : ℤ} [SlashInvariantFormClass F 𝒢 k] {f : F} (hf : ⇑f ≠ 0) (q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ) : SlashInvariantForm.quotientFunc f q ≠ 0

A coset factor of the norm of a nonzero form is nonzero: the factor is a slash translate of the form, and the slash action of a group element kills only 0.

theorem TauCeti.ModularForm.orderOfVanishingAt_norm {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {k : ℤ} [𝒢.IsFiniteRelIndex ℋ] [ℋ.HasDetPlusMinusOne] [ModularFormClass F 𝒢 k] (f : F) (hf : ⇑f ≠ 0) (p : UpperHalfPlane) : orderOfVanishingAt (⇑(ModularForm.norm ℋ f)) p = ∑ᶠ (q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ), orderOfVanishingAt (SlashInvariantForm.quotientFunc f q) p

The vanishing order of the norm at an interior point is the sum of the vanishing orders of its coset factors.

theorem TauCeti.ModularForm.orderOfVanishingAt_quotientFunc_le_orderOfVanishingAt_norm {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {k : ℤ} [𝒢.IsFiniteRelIndex ℋ] [ℋ.HasDetPlusMinusOne] [ModularFormClass F 𝒢 k] (f : F) (q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ) (p : UpperHalfPlane) : orderOfVanishingAt (SlashInvariantForm.quotientFunc f q) p ≤ orderOfVanishingAt (⇑(ModularForm.norm ℋ f)) p

Each coset factor of the norm of a form vanishes at a point to at most the order the norm itself does.

theorem TauCeti.ModularForm.orderOfVanishingAt_le_orderOfVanishingAt_norm {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {k : ℤ} [𝒢.IsFiniteRelIndex ℋ] [ℋ.HasDetPlusMinusOne] [ModularFormClass F 𝒢 k] (f : F) (p : UpperHalfPlane) : orderOfVanishingAt (⇑f) p ≤ orderOfVanishingAt (⇑(ModularForm.norm ℋ f)) p

The norm vanishes at a point to at least the order the form itself does: the zeros of the norm dominate the zeros of the form.

theorem TauCeti.ModularForm.finite_image_orbit_mk_setOf_orderOfVanishingAt_ne_zero_subgroup {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {k : ℤ} {𝒢 : Subgroup (GL (Fin 2) ℝ)} [𝒢.IsFiniteRelIndex (Matrix.SpecialLinearGroup.mapGL ℝ).range] [ModularFormClass F 𝒢 k] (f : F) : (Quotient.mk'' '' {p : UpperHalfPlane | orderOfVanishingAt (⇑f) p ≠ 0}).Finite

At any level of finite relative index in 𝒮ℒ, the nonzero-order points of a form meet only finitely many 𝒢-orbits: the image in 𝒢 \ ℍ of {p | orderOfVanishingAt f p ≠ 0} is finite.

⚠ This is not stated as finite support of an order divisor on 𝒢 \ ℍ, and cannot be: no order function descends to that quotient here, because 𝒢 need not lie inside 𝒮ℒ and its negative-determinant elements are not known to preserve the order. The claim is about the image of a set of points, nothing more.

The nonzero-order set is covered by the finitely many SL(2, ℤ)-orbits its points lie on, and each of those meets only finitely many 𝒢-orbits.