ModularForm.ext
theorem ModularForm.ext :
∀ {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} {f g : ModularForm Γ k},
(∀ (x : UpperHalfPlane), f x = g x) → f = g
The theorem `ModularForm.ext` states that for any subgroup `Γ` of the special linear group of 2 by 2 matrices with integer entries, and for any integer `k`, if `f` and `g` are modular forms of weight `k` with respect to `Γ`, then if `f` and `g` are equal for every point in the upper half plane, then `f` and `g` are equal. In other words, a modular form is completely determined by its values in the upper half plane.
More concisely: For any subgroup of the special linear group of 2 by 2 matrices with integer entries Γ and integer weight k, two modular forms f and g are equal if and only if they have the same value at every point in the upper half plane.
|
ModularForm.gradedMonoid_eq_of_cast
theorem ModularForm.gradedMonoid_eq_of_cast :
∀ {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {a b : GradedMonoid (ModularForm Γ)} (h : a.fst = b.fst),
ModularForm.mcast h a.snd = b.snd → a = b
The theorem `ModularForm.gradedMonoid_eq_of_cast` states that for any subgroup `Γ` of the special linear group of 2 by 2 matrices with integer coefficients, and any two elements `a` and `b` of the graded monoid of `ModularForm`s over the subgroup `Γ`, if the first part (`fst`) of `a` and `b` are equal, and if the modular form obtained by casting the second part (`snd`) of `a` using this equality is equal to the second part of `b`, then `a` and `b` must be the same element of the graded monoid. This theorem essentially provides a condition under which two elements of the graded monoid of modular forms can be considered equal.
More concisely: If `Γ` is a subgroup of the special linear group of 2 by 2 matrices with integer coefficients, `a` and `b` are elements of the graded monoid of `ModularForm`s over `Γ`, and `fst a = fst b` and `cast (snd a) = snd b`, then `a = b`.
|