Petersson-orthogonal complements

The Petersson pairing CuspForm.peterssonInnerCosets on S_k(Γ) is a positive-definite Hermitian form, so every subspace V ≤ S_k(Γ) has a Petersson-orthogonal complement

Vᗮ = {f ∈ S_k(Γ) | ⟪g, f⟫ = 0 for every g ∈ V},

and V and Vᗮ intersect only in 0. This file introduces that complement as TauCeti.CuspForm.peterssonOrthogonal and gives it the order-theoretic API the old/new decomposition of Layer 3 of the ModularForms roadmap needs: it reverses ≤, it turns a supremum of subspaces into an infimum of complements, and orthogonality to the range of a linear map is tested on the map's values alone.

The complement uses Mathlib's Submodule.orthogonalBilin, applied to the Petersson pairing bundled as a sesquilinear form. Deliberately, no InnerProductSpace instance on S_k(Γ) is derived from CuspForm.peterssonInnerCosetsCore; see the note on that definition.

Main definitions

• TauCeti.CuspForm.peterssonOrthogonal: the Petersson-orthogonal complement of a subspace of S_k(Γ).
• TauCeti.CuspForm.peterssonInnerCosetsₛₗ: the Petersson pairing as a sesquilinear form.

Main results

• TauCeti.CuspForm.isCompl_peterssonOrthogonal: a subspace and its Petersson-orthogonal complement are complements of one another, so every cusp form splits uniquely along them.

• TauCeti.CuspForm.mem_peterssonOrthogonal_iff': orthogonality may equivalently be tested in the other argument of the pairing, by Hermitian symmetry.

• TauCeti.CuspForm.map_mem_peterssonOrthogonal: a map whose Petersson adjoint preserves a subspace preserves its orthogonal complement.

• TauCeti.CuspForm.peterssonOrthogonal_disjoint: a subspace and its complement meet only in 0; this is positive definiteness.

• TauCeti.CuspForm.peterssonOrthogonal_peterssonOrthogonal: taking the complement twice recovers the original subspace.

• TauCeti.CuspForm.sup_peterssonOrthogonal_eq_top: a subspace and its complement span the full cusp-form space.

• TauCeti.CuspForm.peterssonOrthogonal_iSup: the complement of a supremum is the infimum of the complements.

• TauCeti.CuspForm.mem_peterssonOrthogonal_iff_le_ker: membership in a complement, restated as an inclusion of subspaces, which is how orthogonality is checked on a generating family.

• TauCeti.CuspForm.mem_peterssonOrthogonal_range_iff: orthogonality to the range of a linear map is orthogonality to each of its values.

References

• F. Diamond and J. Shurman, A first course in modular forms, Section 5.6.

noncomputable def TauCeti.CuspForm.peterssonInnerCosetsₛₗ {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [Γ.FiniteIndex] {k : ℤ} : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k →ₗ⋆[ℂ] CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k →ₗ[ℂ] ℂ

The Petersson pairing as a sesquilinear form: conjugate-linear in the first cusp form and linear in the second.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.CuspForm.peterssonInnerCosetsₛₗ_apply_apply {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [Γ.FiniteIndex] {k : ℤ} (f g : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k) : (peterssonInnerCosetsₛₗ f) g = f.peterssonInnerCosets g

noncomputable def TauCeti.CuspForm.peterssonOrthogonal {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [Γ.FiniteIndex] {k : ℤ} (V : Submodule ℂ (CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k)) : Submodule ℂ (CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k)

The Petersson-orthogonal complement of a subspace V of S_k(Γ): the cusp forms pairing to zero against every element of V. It is a subspace because the Petersson pairing is additive and ℂ-linear in its second argument.

Equations

• TauCeti.CuspForm.peterssonOrthogonal V = Submodule.orthogonalBilin TauCeti.CuspForm.peterssonInnerCosetsₛₗ V

@[simp]

theorem TauCeti.CuspForm.mem_peterssonOrthogonal_iff {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [Γ.FiniteIndex] {k : ℤ} {V : Submodule ℂ (CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k)} {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k} : f ∈ peterssonOrthogonal V ↔ ∀ g ∈ V, g.peterssonInnerCosets f = 0

Membership in the Petersson-orthogonal complement is orthogonality to every element.

theorem TauCeti.CuspForm.mem_peterssonOrthogonal_iff' {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [Γ.FiniteIndex] {k : ℤ} {V : Submodule ℂ (CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k)} {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k} : f ∈ peterssonOrthogonal V ↔ ∀ g ∈ V, f.peterssonInnerCosets g = 0

Orthogonality may be tested in either argument: the Petersson pairing is Hermitian, so one of ⟪g, f⟫ and ⟪f, g⟫ vanishes exactly when the other does.

theorem TauCeti.CuspForm.map_mem_peterssonOrthogonal {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [Γ.FiniteIndex] {k : ℤ} {V : Submodule ℂ (CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k)} {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k} {T S : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k → CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k} (hTS : ∀ (f g : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k), (T f).peterssonInnerCosets g = f.peterssonInnerCosets (S g)) (hV : ∀ g ∈ V, S g ∈ V) (hf : f ∈ peterssonOrthogonal V) : T f ∈ peterssonOrthogonal V

A map preserves the orthogonal complement of a subspace its adjoint preserves. If ⟪T f, g⟫ = ⟪f, S g⟫ for all f, g and S maps V into itself, then T maps peterssonOrthogonal V into itself.

theorem TauCeti.CuspForm.peterssonOrthogonal_le {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [Γ.FiniteIndex] {k : ℤ} {V W : Submodule ℂ (CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k)} (h : V ≤ W) : peterssonOrthogonal W ≤ peterssonOrthogonal V

The Petersson-orthogonal complement reverses inclusions.

@[simp]

theorem TauCeti.CuspForm.peterssonOrthogonal_bot {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [Γ.FiniteIndex] {k : ℤ} : peterssonOrthogonal ⊥ = ⊤

Everything is orthogonal to the zero subspace.

@[simp]

theorem TauCeti.CuspForm.peterssonOrthogonal_top {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [Γ.FiniteIndex] {k : ℤ} : peterssonOrthogonal ⊤ = ⊥

Only 0 is orthogonal to all of S_k(Γ): this is positive definiteness.

theorem TauCeti.CuspForm.peterssonOrthogonal_disjoint {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [Γ.FiniteIndex] {k : ℤ} (V : Submodule ℂ (CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k)) : Disjoint V (peterssonOrthogonal V)

A subspace and its Petersson-orthogonal complement meet only in 0. A form in both pairs with itself to zero, and the pairing is positive definite.

theorem TauCeti.CuspForm.le_peterssonOrthogonal_peterssonOrthogonal {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [Γ.FiniteIndex] {k : ℤ} (V : Submodule ℂ (CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k)) : V ≤ peterssonOrthogonal (peterssonOrthogonal V)

A subspace is contained in its double Petersson-orthogonal complement.

@[instance_reducible]

noncomputable def TauCeti.CuspForm.peterssonInnerCosetsCoreInstance {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [Γ.FiniteIndex] {k : ℤ} : InnerProductSpace.Core ℂ (CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k)

The Petersson core, installed locally to access Mathlib's inner-product-space API.

Equations

• TauCeti.CuspForm.peterssonInnerCosetsCoreInstance = CuspForm.peterssonInnerCosetsCore

@[instance_reducible]

noncomputable def TauCeti.CuspForm.peterssonNormedAddCommGroup {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [Γ.FiniteIndex] {k : ℤ} : NormedAddCommGroup (CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k)

The normed additive structure induced locally by the Petersson core.

Equations

• TauCeti.CuspForm.peterssonNormedAddCommGroup = InnerProductSpace.Core.toNormedAddCommGroup

@[instance_reducible]

noncomputable def TauCeti.CuspForm.peterssonInnerProductSpace {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [Γ.FiniteIndex] {k : ℤ} : InnerProductSpace ℂ (CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k)

The inner-product-space structure induced locally by the Petersson core.

Equations

• TauCeti.CuspForm.peterssonInnerProductSpace = InnerProductSpace.ofCore TauCeti.CuspForm.peterssonInnerCosetsCoreInstance.toCore

@[simp]

theorem TauCeti.CuspForm.peterssonOrthogonal_peterssonOrthogonal {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [Γ.FiniteIndex] {k : ℤ} (V : Submodule ℂ (CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k)) : peterssonOrthogonal (peterssonOrthogonal V) = V

Taking the Petersson-orthogonal complement twice recovers the original subspace.

theorem TauCeti.CuspForm.sup_peterssonOrthogonal_eq_top {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [Γ.FiniteIndex] {k : ℤ} (V : Submodule ℂ (CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k)) : V ⊔ peterssonOrthogonal V = ⊤

A subspace and its Petersson-orthogonal complement span the full cusp-form space.

theorem TauCeti.CuspForm.isCompl_peterssonOrthogonal {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [Γ.FiniteIndex] {k : ℤ} (V : Submodule ℂ (CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k)) : IsCompl V (peterssonOrthogonal V)

A subspace and its Petersson-orthogonal complement are complements of one another. Disjointness is positive definiteness of the pairing; codisjointness is the orthogonal decomposition of the finite-dimensional cusp-form space.

theorem TauCeti.CuspForm.peterssonOrthogonal_iSup {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [Γ.FiniteIndex] {k : ℤ} {ι : Sort u_1} (V : ι → Submodule ℂ (CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k)) : peterssonOrthogonal (⨆ (i : ι), V i) = ⨅ (i : ι), peterssonOrthogonal (V i)

The complement of a supremum is the infimum of the complements. Orthogonality to a family of subspaces spreads to the subspace they generate, since the pairing is additive in its first argument.

theorem TauCeti.CuspForm.mem_peterssonOrthogonal_iff_le_ker {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [Γ.FiniteIndex] {k : ℤ} {V : Submodule ℂ (CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k)} {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k} : f ∈ peterssonOrthogonal V ↔ V ≤ (peterssonInnerCosetsₛₗ f).ker

The orthogonal complement, as an adjunction. A form lies in Vᗮ exactly when V sits inside the kernel of pairing against it; this is the form in which orthogonality is checked on a generating family, since the right-hand side is an inequality of subspaces.

theorem TauCeti.CuspForm.mem_peterssonOrthogonal_range_iff {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [Γ.FiniteIndex] {k : ℤ} {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k} {E : Type u_1} [AddCommGroup E] [Module ℂ E] (L : E →ₗ[ℂ] CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k) : f ∈ peterssonOrthogonal L.range ↔ ∀ (e : E), (L e).peterssonInnerCosets f = 0

Orthogonality to a range is orthogonality to the values.