Documentation

Atlas.EllipticCurves.code.ModularCurves

class ComplexStructure (X : Type u_1) [TopologicalSpace X] extends ChartedSpace X :
Type u_1

Definition 18.4 (Complex structure): a ComplexStructure on a topological space X is a ChartedSpace ℂ X together with the property that X is a real-analytic manifold modelled on (i.e., the transition maps between charts are holomorphic).

Instances
    class RiemannSurface (X : Type u_1) [TopologicalSpace X] extends ComplexStructure X :
    Type u_1

    Definition 18.5 (Riemann surface): a Riemann surface is a connected Hausdorff topological space equipped with a one-dimensional ComplexStructure.

    Instances

      The reduction-mod-N group homomorphism SL₂(ℤ) → SL₂(ℤ/Nℤ).

      Instances For

        Definition 18.11: the principal congruence subgroup Γ(N) ⊆ SL₂(ℤ), consisting of matrices congruent to the identity modulo N.

        Instances For
          theorem Def1811.mem_principalCongruenceSubgroup {N : } {γ : Matrix.SpecialLinearGroup (Fin 2) } :
          γ PrincipalCongruenceSubgroup N (γ 0 0) = 1 (γ 0 1) = 0 (γ 1 0) = 0 (γ 1 1) = 1

          Membership criterion for Γ(N): a matrix γ ∈ SL₂(ℤ) lies in Γ(N) iff its entries reduce mod N to the identity matrix.

          The Hecke-type congruence subgroup Γ₀(N) ⊆ SL₂(ℤ) of matrices that are upper triangular modulo N.

          Instances For

            The Hecke-type congruence subgroup Γ₁(N) ⊆ SL₂(ℤ) of matrices that are upper-unitriangular modulo N.

            Instances For
              theorem Def1811.mem_congruenceSubgroup1 (N : ) (A : Matrix.SpecialLinearGroup (Fin 2) ) :
              A CongruenceSubgroup1 N (A 0 0) = 1 (A 1 1) = 1 (A 1 0) = 0

              Membership criterion for Γ₁(N): a matrix A lies in Γ₁(N) iff its diagonal entries are ≡ 1 (mod N) and its lower-left entry is ≡ 0 (mod N).

              Inclusion Γ(N) ⊆ Γ₁(N): every matrix congruent to the identity mod N is in particular upper-unitriangular mod N.

              Definition 18.11: a subgroup H ⊆ SL₂(ℤ) is a congruence subgroup if it contains some principal congruence subgroup Γ(N).

              Instances For

                Γ(N) is itself a congruence subgroup (for N ≠ 0).

                Γ₁(N) is a congruence subgroup (for N ≠ 0).

                Γ₀(N) is a congruence subgroup (for N ≠ 0).

                The open modular curve Y_Γ := Γ \ ℍ, the quotient of the upper half-plane by a congruence subgroup Γ.

                Instances For

                  The extended upper half-plane ℍ* = ℍ ∪ ℚ ∪ {∞} (cusps adjoined), modelled here as an opaque type pending a formal definition.

                  Axiom: there is a natural SL₂(ℤ)-action on ℍ*.

                  Instances For
                    @[implicit_reducible]

                    The SL₂(ℤ)-action on the extended upper half-plane, registered as an instance.

                    Axiom: ℍ* has a natural topology (extending the topology on with neighborhoods of cusps).

                    Instances For
                      @[implicit_reducible]

                      The topology on ℍ*, registered as an instance.

                      Axiom: ℍ* is compact (adjoining cusps to produces a compactification).

                      Compactness of ℍ*, registered as an instance.

                      Connectedness of ℍ*, registered as an instance.

                      The Hausdorff property of ℍ*, registered as an instance.

                      Local compactness of ℍ*, registered as an instance.

                      Continuity of the SL₂(ℤ)-action on ℍ*, registered as an instance.

                      Axiom: the SL₂(ℤ)-action on ℍ* is properly discontinuous (the key topological input for the modular curve to be Hausdorff).

                      Proper discontinuity of the SL₂(ℤ)-action on ℍ*, registered as an instance.

                      Definition 18.11: the (compactified) modular curve X_Γ := Γ \ ℍ* for a congruence subgroup Γ.

                      Instances For
                        @[reducible, inline]
                        noncomputable abbrev X1 :

                        The full modular curve X(1) = SL₂(ℤ) \ ℍ*.

                        Instances For
                          @[implicit_reducible]
                          noncomputable instance X1.topologicalSpace :

                          The topology on X(1) inherited as a quotient of ℍ*.

                          X(1) is compact, since it is a quotient of the compact space ℍ*.

                          X(1) is Hausdorff, since the SL₂(ℤ)-action on ℍ* is properly discontinuous and ℍ* is T2.

                          X(1) is connected, since it is a quotient of the connected space ℍ*.

                          Theorem 18.3: X(1) is a connected compact Hausdorff space.

                          noncomputable def SL2Stabilizer.ρ :

                          The cube root of unity ρ = -1/2 + i√3/2 ∈ ℍ, one of the two elliptic points (along with i) in the standard fundamental domain 𝓕.

                          Instances For

                            The translate ρ' = ρ + 1 = 1/2 + i√3/2 ∈ ℍ, the other corner of the fundamental domain 𝓕.

                            Instances For

                              Part of Lemma 18.7: for a generic point z in the fundamental domain (not i, ρ, or ρ'), its SL₂(ℤ)-stabilizer is the center {±I}, isomorphic to ℤ/2ℤ.

                              Lemma 18.7 at z = i: the stabilizer of i in SL₂(ℤ) is the cyclic group of order 4 generated by S = ((0,-1),(1,0)).

                              Lemma 18.7 at z = ρ: the stabilizer of ρ in SL₂(ℤ) is the cyclic group of order 6 generated by S * T.

                              Lemma 18.7 at the cusp : the stabilizer of in SL₂(ℤ) consists of matrices with lower-left entry 0, i.e., powers of ±T.

                              The matrix S = ((0,-1),(1,0)) ∈ SL₂(ℤ) has order 4.

                              The product S*T ∈ SL₂(ℤ) has order 6.

                              theorem int_sq_bounded_finite (N : ) :
                              {n : | n ^ 2 N}.Finite

                              Auxiliary lemma: the set of integers n with n² ≤ N is finite (it is contained in [-⌈√N⌉, ⌈√N⌉]). Used in the proof of Lemma 18.1 to bound matrix entries.

                              The classical identity |cz + d|² = Im(z) / Im(γz) for γ = ((a,b),(c,d)) ∈ SL₂(ℤ) acting on the upper half-plane.

                              Expansion of |cz + d|² = (c·Re(z) + d)² + (c·Im(z))² as a sum of two squares of real numbers, used to extract bounds on the matrix entries c, d.

                              theorem lemma_18_1 (A B : Set UpperHalfPlane) (hA : IsCompact A) (hB : IsCompact B) :
                              {γ : Matrix.SpecialLinearGroup (Fin 2) | τA, γ τ B}.Finite

                              Lemma 18.1: for any compact sets A, B ⊆ ℍ, the set of γ ∈ SL₂(ℤ) such that γA ∩ B ≠ ∅ is finite. Proved by bounding the four entries a, b, c, d of γ using |cτ + d|² = Im(τ)/Im(γτ) and the compactness of A, B.

                              theorem iterate_mem_ball_of_mapsTo {R : } {f : } (hf_maps : Set.MapsTo f (Metric.ball 0 R) (Metric.ball 0 R)) (k : ) {z : } (hz : z Metric.ball 0 R) :

                              If f maps ball 0 R into itself, then so does its k-th iterate.

                              theorem iterate_eq_pow_mul_on_ball {ζ : } {R : } {f : } (hf_maps : Set.MapsTo f (Metric.ball 0 R) (Metric.ball 0 R)) (hf_eq : zMetric.ball 0 R, f z = ζ * z) (k : ) {z : } (hz : z Metric.ball 0 R) :
                              f^[k] z = ζ ^ k * z

                              If f(z) = ζ·z on ball 0 R and f maps the ball to itself, then f^k(z) = ζ^k · z for every iterate.

                              theorem disk_aut_fixing_origin_is_rotation {R : } (hR : 0 < R) {f g : } (hf_diff : DifferentiableOn f (Metric.ball 0 R)) (hf_maps : Set.MapsTo f (Metric.ball 0 R) (Metric.ball 0 R)) (hf_zero : f 0 = 0) (hg_diff : DifferentiableOn g (Metric.ball 0 R)) (hg_maps : Set.MapsTo g (Metric.ball 0 R) (Metric.ball 0 R)) (hg_zero : g 0 = 0) (hgf : zMetric.ball 0 R, g (f z) = z) :
                              ∃ (ζ : ), ζ = 1 zMetric.ball 0 R, f z = ζ * z

                              Schwarz lemma / disk-automorphism rigidity: any holomorphic self-map of an open disk fixing the origin that admits a holomorphic inverse (also fixing 0) must be a rotation z ↦ ζz for some unimodular ζ.

                              theorem disk_aut_primitive_root {R : } (hR : 0 < R) {f g : } {n : } (hn : 0 < n) (hf_diff : DifferentiableOn f (Metric.ball 0 R)) (hf_maps : Set.MapsTo f (Metric.ball 0 R) (Metric.ball 0 R)) (hf_zero : f 0 = 0) (hg_diff : DifferentiableOn g (Metric.ball 0 R)) (hg_maps : Set.MapsTo g (Metric.ball 0 R) (Metric.ball 0 R)) (hg_zero : g 0 = 0) (hgf : zMetric.ball 0 R, g (f z) = z) (hiter : zMetric.ball 0 R, f^[n] z = z) (hmin : ∀ (k : ), 0 < kk < nzMetric.ball 0 R, f^[k] z z) :
                              ∃ (ζ : ), IsPrimitiveRoot ζ n zMetric.ball 0 R, f z = ζ * z

                              Strengthening of the rotation lemma: if additionally f^n = id on the ball with n minimal, then the rotation constant ζ is a primitive n-th root of unity. This is the analytic core used in proving Lemma 18.8.

                              noncomputable def deltaMap (τ_x : UpperHalfPlane) (τ : ) :

                              The Cayley-type uniformizer δ_x(τ) = (τ - τ_x)/(τ - conj(τ_x)) mapping the upper half-plane biholomorphically to the open unit disk, sending τ_x ↦ 0. Used in Lemma 18.8 to transfer disk automorphism rigidity to the upper half-plane.

                              Instances For
                                theorem lemma_18_8 (τ_x : UpperHalfPlane) {φ : UpperHalfPlaneUpperHalfPlane} {n : } (hn : 0 < n) (hφ_fix : φ τ_x = τ_x) (hφ_iter : ∀ (τ : UpperHalfPlane), φ^[n] τ = τ) (hφ_min : ∀ (k : ), 0 < kk < n∃ (τ : UpperHalfPlane), φ^[k] τ τ) {f g : } (hf_diff : DifferentiableOn f (Metric.ball 0 1)) (hf_maps : Set.MapsTo f (Metric.ball 0 1) (Metric.ball 0 1)) (hf_zero : f 0 = 0) (hg_diff : DifferentiableOn g (Metric.ball 0 1)) (hg_maps : Set.MapsTo g (Metric.ball 0 1) (Metric.ball 0 1)) (hg_zero : g 0 = 0) (hgf : zMetric.ball 0 1, g (f z) = z) (hf_compat : ∀ (τ : UpperHalfPlane), f (deltaMap τ_x τ) = deltaMap τ_x (φ τ)) (hδ_maps : ∀ (τ : UpperHalfPlane), deltaMap τ_x τ Metric.ball 0 1) (hf_iter : zMetric.ball 0 1, f^[n] z = z) (hf_min : ∀ (k : ), 0 < kk < nzMetric.ball 0 1, f^[k] z z) :
                                ∃ (ζ : ), IsPrimitiveRoot ζ n ∀ (τ : UpperHalfPlane), deltaMap τ_x (φ τ) = ζ * deltaMap τ_x τ

                                Lemma 18.8: let τ_x ∈ ℍ and φ : ℍ → ℍ be holomorphic with φ(τ_x) = τ_x and φ^n = id with n minimal. Then there exists a primitive n-th root of unity ζ such that δ_x(φ(τ)) = ζ · δ_x(τ) for every τ ∈ ℍ. Proved by conjugating with the Cayley-type map deltaMap and applying disk_aut_primitive_root.

                                The action map τ ↦ γ • τ on the upper half-plane is continuous for every γ ∈ SL₂(ℤ).

                                theorem lemma_18_2 (τ₁ τ₂ : UpperHalfPlane) :
                                ∃ (U₁ : Set UpperHalfPlane) (U₂ : Set UpperHalfPlane), IsOpen U₁ IsOpen U₂ τ₁ U₁ τ₂ U₂ ∀ (γ : Matrix.SpecialLinearGroup (Fin 2) ), (∃ zU₁, γ z U₂) γ τ₁ = τ₂

                                Lemma 18.2: for any τ₁, τ₂ ∈ ℍ*, there exist open neighborhoods U₁, U₂ of τ₁, τ₂ such that for every γ ∈ SL₂(ℤ), some z ∈ U₁ has γ•z ∈ U₂ iff γ•τ₁ = τ₂. In particular each τ has a neighborhood in which it is the unique representative of its Γ-orbit.

                                Axiom: the open cover {U_x} and atlas {ψ_x} of X(1) (from §18.3) give a charted-space structure modelled on .

                                Instances For
                                  @[implicit_reducible]
                                  noncomputable instance X1.chartedSpace :

                                  The charted-space structure on X(1) modelled on , registered as an instance.

                                  Axiom: the atlas on X(1) is real-analytic, making it a complex manifold.

                                  X(1) is a real-analytic (hence holomorphic) complex 1-manifold.

                                  @[implicit_reducible]
                                  noncomputable instance X1.complexStructure :

                                  Assemble the complex structure on X(1) from the charted space and manifold instances.

                                  @[implicit_reducible]
                                  noncomputable instance X1.riemannSurface :

                                  X(1) is a Riemann surface: it carries a complex structure and is Hausdorff and connected (from Theorem 18.3).

                                  Theorem 18.9: the cover and atlas {ψ_x} define a complex structure on X(1), i.e., X(1) is a compact complex manifold of dimension 1.

                                  structure Triangulation (X : Type u_1) [TopologicalSpace X] :

                                  A combinatorial triangulation of a topological space, recording the number of vertices V, edges E, faces F, and genus g, subject to the Euler characteristic identity V - E + F = 2 - 2g.

                                  Instances For
                                    noncomputable def X1.triangulation :

                                    An explicit triangulation of X(1) with V = 3, E = 3, F = 2, giving genus 0 (the three vertices being the orbits of i, ρ, ∞).

                                    Instances For

                                      The chosen triangulation of X(1) has 3 vertices.

                                      The chosen triangulation of X(1) has 3 edges.

                                      The chosen triangulation of X(1) has 2 faces.

                                      The chosen triangulation of X(1) has genus 0 (computed from V - E + F = 2).

                                      Theorem 18.10: X(1) is a compact Riemann surface of genus 0. The genus claim is extracted from the explicit triangulation.

                                      Strengthening of Theorem 18.10: X(1) is homeomorphic to the Riemann sphere ℂ ∪ {∞} (which is the unique compact Riemann surface of genus 0).