ModularGroup.abs_c_le_one
theorem ModularGroup.abs_c_le_one :
β {g : Matrix.SpecialLinearGroup (Fin 2) β€} {z : UpperHalfPlane},
z β ModularGroup.fdo β g β’ z β ModularGroup.fdo β |βg 1 0| β€ 1
This theorem, `ModularGroup.abs_c_le_one`, states that for any 2x2 integer matrix `g` from the Special Linear Group (with determinant 1) and any point `z` from the upper half plane, if both `z` and the action of `g` on `z` belong to the standard open fundamental domain of the action of SL(2,β€) on the upper half plane, then the absolute value of the entry at the second row and the first column of `g` is less than or equal to 1.
More concisely: If matrices `g` in SL(2,β€) and `z` in the upper half plane have actions on `z` that lie within the standard open fundamental domain, then the absolute value of the entry in the second row and first column of `g` is less than or equal to 1.
|
ModularGroup.one_lt_normSq_T_zpow_smul
theorem ModularGroup.one_lt_normSq_T_zpow_smul :
β {z : UpperHalfPlane}, z β ModularGroup.fdo β β (n : β€), 1 < Complex.normSq β(ModularGroup.T ^ n β’ z)
The theorem `ModularGroup.one_lt_normSq_T_zpow_smul` states that for any point `z` in the open fundamental domain of the action of `SL(2,β€)` on the upper half plane, and for any integer `n`, the squared norm of the complex number obtained by applying the power `n` of the matrix `T` to `z` (denoted as `ModularGroup.T ^ n β’ z`) is greater than 1. The matrix `T` here is a 2x2 square matrix with elements [[1, 1], [0, 1]], and the operation `β’` denotes the action of the matrix on the point `z`. The squared norm of a complex number is the sum of the squares of its real and imaginary parts.
More concisely: For any integer `n` and point `z` in the open fundamental domain of the action of `SL(2,β€)` on the upper half plane, the squared norm of `ModularGroup.T ^ n β’ z` is strictly greater than 1.
|
ModularGroup.normSq_S_smul_lt_one
theorem ModularGroup.normSq_S_smul_lt_one :
β {z : UpperHalfPlane}, 1 < Complex.normSq βz β Complex.normSq β(ModularGroup.S β’ z) < 1
This theorem states that for any point `z` in the Upper Half Plane, if the squared norm of `z` (in complex numbers) is greater than 1, then the squared norm of the point obtained by the action of the special linear matrix `S` on `z` is less than 1. Here, the special linear matrix `S` represents the MobiΓΌs transformation `z β¦ -1/z`, and the Upper Half Plane refers to the set of complex numbers with positive imaginary part.
More concisely: For any complex number `z` in the Upper Half Plane with squared norm greater than 1, the squared norm of `S(z)` (where `S` is the MobiΓΌs transformation `-1/z`) is less than 1.
|
ModularGroup.exists_max_im
theorem ModularGroup.exists_max_im :
β (z : UpperHalfPlane), β g, β (g' : Matrix.SpecialLinearGroup (Fin 2) β€), (g' β’ z).im β€ (g β’ z).im
This theorem states that for any point `z` in the upper half plane, there exists a 2x2 integer matrix `g` (with determinant equal to 1, belonging to the special linear group SL(2,β€)), such that the imaginary part of the point resulting from the action of `g` on `z` (denoted as `(gβ’z).im`) is maximized. In other words, for any other 2x2 integer matrix `g'` (also with determinant equal to 1), the imaginary part of the point that results from `g'` acting on `z` is less than or equal to the imaginary part of the point resulting from `g` acting on `z`.
More concisely: For any point `z` in the upper half plane, there exists a 2x2 integer matrix `g` in SL(2,β€) maximizing the imaginary part of `(gβ’z)`.
|
ModularGroup.exists_smul_mem_fd
theorem ModularGroup.exists_smul_mem_fd : β (z : UpperHalfPlane), β g, g β’ z β ModularGroup.fd
This theorem, referred to as the First Fundamental Domain Lemma, states that for any point `z` in the open upper half plane, indicated by `β`, there exists an element `g` from the special linear group `SL(2,β€)` such that the result of the action of `g` on `z` (denoted by `g β’ z`) is within the standard fundamental domain `π` of the action of `SL(2,β€)` on `β`. The standard fundamental domain `π` is defined as the set of points `z` in the open upper half plane such that the square of the absolute value (or norm) of `z` is greater than or equal to 1 and the absolute value of the real part of `z` is less than or equal to 1/2.
More concisely: For every point `z` in the open upper half plane, there exists a matrix `g` in `SL(2,β€)` such that `g β’ z` lies within the standard fundamental domain of the action of `SL(2,β€)` on `β`, defined as the set of `z` with norm β₯ 1 and real part β€ 1/2.
|
ModularGroup.tendsto_lcRow0
theorem ModularGroup.tendsto_lcRow0 :
β {cd : Fin 2 β β€},
IsCoprime (cd 0) (cd 1) β
Filter.Tendsto (fun g => (ModularGroup.lcRow0 cd) β((Matrix.SpecialLinearGroup.map (Int.castRingHom β)) βg))
Filter.cofinite (Filter.cocompact β)
This theorem states that for any pair of integers `cd` (represented as a function from `Fin 2` to `β€`) that are coprime, the function `g` that applies `ModularGroup.lcRow0 cd` to the image under the ring homomorphism `Int.castRingHom β` (from integers to real numbers) of a special linear group element `g` (represented as a 2x2 matrix) has the property that preimages of cocompact sets are finite. This property is also known as the function `g` being proper. In mathematical terms, this means that for any compact set in the reals, the preimage under `g` is a finite set.
More concisely: For coprime integers `cd`, the function `g` obtained by applying `ModularGroup.lcRow0 cd` to the image of a special linear group element `g` under the ring homomorphism from integers to real numbers has the property that its preimages of compact sets are finite.
|
ModularGroup.eq_smul_self_of_mem_fdo_mem_fdo
theorem ModularGroup.eq_smul_self_of_mem_fdo_mem_fdo :
β {g : Matrix.SpecialLinearGroup (Fin 2) β€} {z : UpperHalfPlane},
z β ModularGroup.fdo β g β’ z β ModularGroup.fdo β z = g β’ z
The theorem named "Second Fundamental Domain Lemma" states that if a point `z` in the upper half plane and the image of `z` under the action of a 2x2 integer matrix `g` with determinant 1 (which belongs to the special linear group `SL(2, β€)`), both lie in the standard open fundamental domain of the action of `SL(2,β€)` on the upper half plane (denoted as `πα΅`), then the point `z` must equal its image under `g` (i.e., `z` is a fixed point of `g`). In other words, no point in the fundamental domain is mapped to another point in the same domain under the action of any element of `SL(2,β€)`.
More concisely: If two points in the standard open fundamental domain of the action of `SL(2,β€)` on the upper half plane map to each other under the action of some element in `SL(2,β€)`, then they are equal.
|
ModularGroup.im_lt_im_S_smul
theorem ModularGroup.im_lt_im_S_smul : β {z : UpperHalfPlane}, Complex.normSq βz < 1 β z.im < (ModularGroup.S β’ z).im
This theorem states that for every point `z` in the upper half plane, if the square of the complex norm of `z` is less than 1, then the imaginary part of `z` is strictly less than the imaginary part of the result when the modular group transformation `S` is applied to `z`. In mathematical terms, if `|z|^2 < 1`, then Im(z) < Im(Sz). Here, `S` is a special matrix that represents a MobiΓΌs transformation which can be thought of as a rotation operation.
More concisely: For every complex number `z` with square norm less than 1 in the upper half plane, the imaginary part of `Sz` is strictly greater than the imaginary part of `z`. (Note that the inequality should be reversed since the statement in the question has an error and `Im(Sz)` should be smaller than `Im(z)`).
|
ModularGroup.c_eq_zero
theorem ModularGroup.c_eq_zero :
β {g : Matrix.SpecialLinearGroup (Fin 2) β€} {z : UpperHalfPlane},
z β ModularGroup.fdo β g β’ z β ModularGroup.fdo β βg 1 0 = 0
This theorem, named `ModularGroup.c_eq_zero`, states that for any 2x2 integer matrix `g` that belongs to the special linear group (i.e., its determinant is equal to 1), and for any point `z` in the upper half plane, if `z` is in the standard open fundamental domain of the action of `SL(2,β€)` on the upper half plane, and `g` scaled by `z` is also in this fundamental domain, then the entry of `g` at position (1, 0) (using 0-based indexing) is equal to 0. The standard open fundamental domain of the action of `SL(2,β€)` on the upper half plane is the set of points with norm squared greater than 1 and absolute real part less than 1/2.
More concisely: For any 2x2 integer matrix `g` in the special linear group SL(2,β€) and any point `z` in the upper half plane with norm squared > 1 and absolute real part < 1/2, if `g` scaled by `z` is also in the fundamental domain, then the (1,0) entry of `g` is equal to 0.
|
ModularGroup.re_T_zpow_smul
theorem ModularGroup.re_T_zpow_smul : β (z : UpperHalfPlane) (n : β€), (ModularGroup.T ^ n β’ z).re = z.re + βn := by
sorry
The theorem `ModularGroup.re_T_zpow_smul` states that for any point `z` in the open upper half plane, and for any integer `n`, the real part of the result of scaling `z` by the `n`-th power of the matrix `T` (which is defined as a 2x2 matrix with entries [[1, 1], [0, 1]] in `SL(2, β€)`) is equal to the real part of `z` plus the integer `n`. In other words, multiplying `z` by the `n`-th power of `T` and taking the real part shifts the real part of `z` by `n` units.
More concisely: For any integer `n` and point `z` in the open upper half plane, the real part of `z` multiplied by the `n`-th power of the matrix `T` in `SL(2, β€)` equals the real part of `z` plus `n`.
|
ModularGroup.exists_row_one_eq_and_min_re
theorem ModularGroup.exists_row_one_eq_and_min_re :
β (z : UpperHalfPlane) {cd : Fin 2 β β€},
IsCoprime (cd 0) (cd 1) β
β g, βg 1 = cd β§ β (g' : Matrix.SpecialLinearGroup (Fin 2) β€), βg 1 = βg' 1 β |(g β’ z).re| β€ |(g' β’ z).re|
The theorem `ModularGroup.exists_row_one_eq_and_min_re` states that given any point `z` in the upper half plane and a pair of integers `(c, d)` that are coprime, there exists a 2x2 integer matrix `g` with determinant 1 (i.e., a member of the Special Linear Group SL(2, β€)) such that the bottom row of `g` is `(c, d)`, and for any other matrix `g'` in SL(2, β€) with the same bottom row, the real part of the complex number obtained by applying `g` to `z` (i.e., `(gβ’z).re`) has an absolute value that is less than or equal to the real part of the complex number obtained by applying `g'` to `z`. In other words, among all 2x2 matrices in SL(2, β€) with bottom row `(c, d)`, `g` minimizes the absolute value of the real part of the transformed point `(gβ’z).re`.
More concisely: Given any point `z` in the upper half plane and coprime integers `(c, d)`, there exists a 2x2 integer matrix `g` in SL(2, β€) with bottom row `(c, d)` such that among all matrices in SL(2, β€ with bottom row `(c, d)`, `g` minimizes the absolute value of the real part of the transformed point `(gβ’z).re`.
|
ModularGroup.tendsto_normSq_coprime_pair
theorem ModularGroup.tendsto_normSq_coprime_pair :
β (z : UpperHalfPlane),
Filter.Tendsto (fun p => Complex.normSq (β(p 0) * βz + β(p 1))) Filter.cofinite Filter.atTop
The theorem `ModularGroup.tendsto_normSq_coprime_pair` states that for any point `z` in the upper half plane, the function that maps a pair of coprime integers `(c, d)` to the square of the norm of the complex number `cz + d` has the property that any preimage of a set of real numbers that is bounded above (i.e., has a maximum) is a finite set. In other words, the values of this function tend to infinity as the magnitude of the input pair `(c, d)` increases. This is a property typically associated with proper functions.
More concisely: The map sending coprime integers `(c, d)` to the square of the norm of `cz + d` in the upper half plane has image that is bounded above if and only if its domain is finite.
|
ModularGroup.bottom_row_coprime
theorem ModularGroup.bottom_row_coprime :
β {R : Type u_1} [inst : CommRing R] (g : Matrix.SpecialLinearGroup (Fin 2) R), IsCoprime (βg 1 0) (βg 1 1) := by
sorry
The theorem `ModularGroup.bottom_row_coprime` states that, for any ring `R` with a commutative ring structure, if `g` is a special 2x2 linear matrix (i.e., a matrix with determinant 1) over `R`, then the two numbers `c` and `d` in the second (or bottom) row of `g` are coprime. In other words, there exist numbers `a` and `b` such that the linear combination `a * c + b * d` equals 1. This coprimality condition remains true regardless of the choice of the commutative ring `R` and the particular 2x2 matrix `g` in the special linear group.
More concisely: For any commutative ring `R` and any special 2x2 matrix `g` over `R` with determinant 1, the numbers in the second row `c` and `d` are coprime.
|
ModularGroup.smul_eq_lcRow0_add
theorem ModularGroup.smul_eq_lcRow0_add :
β {g : Matrix.SpecialLinearGroup (Fin 2) β€} (z : UpperHalfPlane) {p : Fin 2 β β€},
IsCoprime (p 0) (p 1) β
βg 1 = p β
β(g β’ z) =
β((ModularGroup.lcRow0 p) β((Matrix.SpecialLinearGroup.map (Int.castRingHom β)) g)) /
(β(p 0) ^ 2 + β(p 1) ^ 2) +
(β(p 1) * βz - β(p 0)) / ((β(p 0) ^ 2 + β(p 1) ^ 2) * (β(p 0) * βz + β(p 1)))
This theorem provides a new identity related to the modular group operation `g β’ z`. In the standard theory, this operation typically results in a real part equivalent to `a/c + *`, where `*` represents additional terms. The theorem presents an alternative where we do not need to consider whether `c = 0`. Specifically, for a member `g` of the Special Linear Group of 2x2 integer matrices and a point `z` in the upper half-plane, given a coprime pair `p = (p 0, p 1)`, `βg 1 = p` implies that `g β’ z` is equal to `(a c + b d) / (c^2 + d^2) + (d z - c) / ((c^2 + d^2) (c z + d))`. This new identity, which involves both real and imaginary parts, does not need to be decomposed depending on whether `c = 0`.
More concisely: Given a matrix `g` in the Special Linear Group of 2x2 integer matrices and a point `z` in the upper half-plane, if `g` has the first column equal to a coprime pair `p` and `βg 1 = p`, then `g β’ z` equals `(a c + b d) / (c^2 + d^2) + (d z - c) / ((c^2 + d^2) (c z + d))`, where `a`, `b`, `c`, and `d` are the matrix elements of `g`.
|
ModularGroup.bottom_row_surj
theorem ModularGroup.bottom_row_surj :
β {R : Type u_1} [inst : CommRing R], Set.SurjOn (fun g => βg 1) Set.univ {cd | IsCoprime (cd 0) (cd 1)}
This theorem states that for any pair of coprime integers `c` and `d`, there exists some 2x2 matrix `g` from the Special Linear group `SL(2,β€)` such that `c` and `d` form the bottom row of the matrix `g`. In other words, every pair of coprime integers can be found as the bottom row of some Special Linear group matrix. The Special Linear Group `SL(2,β€)` is the set of 2x2 matrices with integer entries and determinant 1. An integer pair is coprime if there exist some integers `a` and `b` such that `a*c + b*d = 1`.
More concisely: For every pair of coprime integers `c` and `d`, there exists a 2x2 matrix `g` in the Special Linear group `SL(2,β€)` with `c` and `d` as its bottom row.
|