EisensteinSeries.gammaSet_one_eq
theorem EisensteinSeries.gammaSet_one_eq :
∀ (a a' : Fin 2 → ZMod 1), EisensteinSeries.gammaSet 1 a = EisensteinSeries.gammaSet 1 a'
The theorem `EisensteinSeries.gammaSet_one_eq` states that for the level `N` equal to 1, all gamma sets are equivalent. In other words, for any two functions `a` and `a'` that map from a 2-element finite set to the integers modulo 1, the corresponding gamma sets, which consist of pairs of coprime integers that are congruent to `a` and `a'` mod `N`, are identical.
More concisely: For the level 1, two functions mapping from a 2-element finite set to integers modulo 1 result in identical gamma sets consisting of coprime pairs congruent to the functions.
|
EisensteinSeries.eisSummand_SL2_apply
theorem EisensteinSeries.eisSummand_SL2_apply :
∀ (k : ℤ) (i : Fin 2 → ℤ) (A : Matrix.SpecialLinearGroup (Fin 2) ℤ) (z : UpperHalfPlane),
EisensteinSeries.eisSummand k i (A • z) =
UpperHalfPlane.denom (↑A) z ^ k * EisensteinSeries.eisSummand k (Matrix.vecMul i ↑A) z
This theorem describes how the `eisSummand` function, which is part of the definition of an Eisenstein series, changes under the Möbius action. For any integer `k`, any function `i` from `Fin 2` to integers, any `2x2` special linear matrix `A` with integer entries, and any point `z` in the upper half plane, the `eisSummand` of `k`, `i`, and `A` applied to `z` is equal to the `k-th` power of the denominator of the fractional linear transformation of `z` by `A`, multiplied by the `eisSummand` of `k`, the vector multiplication of `i` and `A`, and `z`. In mathematical terms, this means that the Eisenstein series is invariant under the action of the special linear group, which is a key property in the theory of modular forms.
More concisely: The Eisenstein series `eisSummand` is invariant under the special linear group action, that is, for any integer `k`, function `i` from `Fin 2` to integers, `2x2` special linear matrix `A` with integer entries, and point `z` in the upper half plane, `eisSummand k i A z = (det A)^k * eisSummand k (i . A) z`.
|
EisensteinSeries.vecMul_SL2_mem_gammaSet
theorem EisensteinSeries.vecMul_SL2_mem_gammaSet :
∀ {N : ℕ} {a : Fin 2 → ZMod N} {v : Fin 2 → ℤ},
v ∈ EisensteinSeries.gammaSet N a →
∀ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ),
Matrix.vecMul v ↑γ ∈
EisensteinSeries.gammaSet N
(Matrix.vecMul a ↑((Matrix.SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ))
This theorem states that for every natural number `N`, every function `a` from a 2-element finite set to the integers modulo `N`, and every function `v` from a 2-element finite set to the integers such that `v` belongs to the set of pairs of coprime integers congruent to `a` mod `N`, for every matrix `γ` in the Special Linear Group SL(2, ℤ) (2x2 integer matrices with determinant 1), the result of right-multiplying `v` by `γ` is in the set of pairs of coprime integers congruent to the result of right-multiplying `a` by the image of `γ` under the group homomorphism induced by the ring homomorphism from the integers to the integers modulo `N` (which maps `γ` to another matrix in the Special Linear Group). In other words, right-multiplication by a matrix in the Special Linear Group sends one set of pairs of coprime integers congruent mod `N` to another such set.
More concisely: For every natural number N, every function a from a 2-element set to integers modulo N, every function v from a 2-element set to coprime integers congruent to a modulo N, and every matrix γ in the Special Linear Group SL(2, ℤ), the image of v under γ is in the set of pairs of coprime integers congruent to the image of a under the induced homomorphism.
|