SlashAction.neg_slash
theorem SlashAction.neg_slash :
∀ {β : Type u_1} {G : Type u_2} {α : Type u_3} {γ : Type u_4} [inst : Group G] [inst_1 : AddGroup α]
[inst_2 : SMul γ α] [inst_3 : SlashAction β G α γ] (k : β) (g : G) (a : α),
SlashAction.map γ k g (-a) = -SlashAction.map γ k g a
This theorem, `SlashAction.neg_slash`, states that for any types `β`, `G`, `α`, and `γ`, given `G` is a Group, `α` is an AddGroup, and multiplication between `γ` and `α` is defined, and given a `SlashAction` is defined between `β`, `G`, `α`, and `γ`, for any elements `k` from `β`, `g` from `G`, and `a` from `α`, the map of `SlashAction` applied to `k`, `g`, and the negation of `a`, equals the negation of the map of `SlashAction` applied to `k`, `g`, and `a`. In other words, the `SlashAction` map respects the negation operation from the `AddGroup` structure.
More concisely: For any SlashAction of types `β`, `G`, `α`, and `γ` with `G` being a Group, `α` an AddGroup, and multiplication between `γ` and `α` defined, the map of SlashAction applied to `k` from `β`, `g` from `G`, and the negation of `a` from `α`, equals the negation of the map of SlashAction applied to `k`, `g`, and `a`.
|
ModularForm.slash_action_eq'_iff
theorem ModularForm.slash_action_eq'_iff :
∀ (k : ℤ) (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (f : UpperHalfPlane → ℂ) (γ : ↥Γ)
(z : UpperHalfPlane), SlashAction.map ℂ k γ f z = f z ↔ f (γ • z) = (↑(↑↑↑γ 1 0) * ↑z + ↑(↑↑↑γ 1 1)) ^ k * f z
The theorem `ModularForm.slash_action_eq'_iff` states that for every integer `k`, subgroup `Γ` of `2x2` special linear group of integers, function `f` from upper half plane to complex numbers, element `γ` from `Γ`, and `z` from upper half plane, the slash-action map applied to these parameters is equal to `f(z)` if and only if `f(γ•z)` is equal to `(c*z+d)^k * f(z)`, where `γ` is a 2x2 matrix represented as `![![a, b], ![c, d]]`, and the action on `ℍ` is via Möbius transformations. This effectively describes a property of a function being slash-invariant, of weight `k` and level `Γ`.
More concisely: For every integer `k`, subgroup `Γ` of the special linear group of 2x2 matrices over the integers, function `f` from the upper half plane to the complex numbers, matrix `γ` in `Γ`, and `z` in the upper half plane, the equation `f(γ•z) = (c*z+d)^k * f(z)` holds if and only if the slash-action of `f` by `γ` is equal to the slash-action of `f` on `z` in the sense of modular forms of weight `k` and level `Γ`.
|
ModularForm.is_invariant_one
theorem ModularForm.is_invariant_one : ∀ (A : Matrix.SpecialLinearGroup (Fin 2) ℤ), SlashAction.map ℂ 0 A 1 = 1 := by
sorry
The theorem `ModularForm.is_invariant_one` states that the constant function 1 is invariant under the action of any element of the special linear group of 2x2 integer matrices, often denoted as `SL(2, ℤ)`. In more mathematical terms, for any matrix `A` from `SL(2, ℤ)`, the application of the slash action on `A` to the complex number 1 doesn't change the value, it remains 1. Here, the slash action is a certain mathematical operation defined on the complex numbers, with the input parameters being an element from the group `SL(2, ℤ)` and a complex number.
More concisely: The constant function 1 is fixed under the action of any element in the special linear group SL(2, ℤ).
|
ModularForm.is_invariant_const
theorem ModularForm.is_invariant_const :
∀ (A : Matrix.SpecialLinearGroup (Fin 2) ℤ) (x : ℂ),
SlashAction.map ℂ 0 A (Function.const UpperHalfPlane x) = Function.const UpperHalfPlane x
The theorem `ModularForm.is_invariant_const` states that for any 2x2 matrix `A` with integer entries from the Special Linear Group (i.e., matrices with determinant equals to 1) and for any complex number `x`, the application of the action `SlashAction.map` with `ℂ` and 0 as arguments on the constant function with value `x` over the Upper Half Plane, equals to the constant function itself. In other words, the `SlashAction.map` action leaves the constant function invariant, irrespective of the matrix and the complex number chosen.
More concisely: For any 2x2 integer matrix A from the Special Linear Group and complex number x, the SlashAction.map operation with ℂ and 0 as arguments applied to the constant function equal to x over the Upper Half Plane results in the same constant function.
|