diff --git a/TauCetiRoadmap/FuchsianOrbifolds/README.md b/TauCetiRoadmap/FuchsianOrbifolds/README.md new file mode 100644 index 00000000..2ccddf78 --- /dev/null +++ b/TauCetiRoadmap/FuchsianOrbifolds/README.md @@ -0,0 +1,428 @@ +# Roadmap: Fuchsian groups and orbifold Riemann surfaces + +This roadmap develops discrete subgroups of `PSL(2,R)`, their action on the upper half-plane, +the quotient Riemann surfaces and orbifold points produced by elliptic stabilizers, and the +compactification produced by adjoining cusp orbits. It exposes the actual group action, +stabilizers, quotient maps, local coordinates, and compact Riemann surface. Orbifold signatures +and presentations are theorems derived from those objects, not substitutes for constructing +them. + +The main reusable endpoint is a compactification theorem for cofinite Fuchsian groups. A +second endpoint applies it to the level-one modular group in the mathematically correct order: +first construct the compact Riemann surface, then descend and extend the normalized modular +`j`-function, then prove that map has degree one, and only then identify the surface +biholomorphically with the Riemann sphere. + +Suggested homes: `TauCeti/Analysis/Complex/Fuchsian/` for groups, polygons, and cusps, and +`TauCeti/Geometry/RiemannSurface/Orbifold/` for quotient charts and compactification. + +## Scope and completion criterion + +The scope is orientation-preserving Fuchsian groups acting on the upper half-plane, with special +attention to cofinite groups, finite elliptic stabilizers, cusp compactification, triangle +groups, polygon presentations, and descent of invariant meromorphic functions. It proves the +standard presentation of the acting Fuchsian group; it does not introduce a general orbifold +groupoid or orbifold fundamental-group carrier. + +Teichmüller theory, general Kleinian groups, higher-dimensional locally symmetric spaces, +automorphic representations, and the classification of all two-dimensional orbifolds are +outside this roadmap. Congruence-subgroup arithmetic, Hecke operators, modular-form dimension +formulas, and the construction and q-expansion of modular forms remain with the modular-forms +roadmap. + +The roadmap is complete when Tau Ceti proves the following. + +1. `PSL(2,R)` has its effective continuous faithful holomorphic action on Mathlib's + `UpperHalfPlane`. Discrete subgroups act properly discontinuously, and all stabilizers are + finite. +2. The free locus has the standard orbit quotient, covering projection, and complex-manifold + structure. At an elliptic point of stabilizer order `m`, a linearizing coordinate identifies + the local quotient with `z |-> z^m`; the quotient surface remains smooth and the quotient map + has ramification index `m`. +3. Parabolic fixed points, cusps, normalized cusp data, precisely invariant horodiscs, and + q-coordinates are constructed. Cusp width belongs to the chosen normalized scaling datum rather + than to the cusp alone. For a cofinite group there are finitely many cusp orbits. +4. Adjoining those cusp orbits to the coarse quotient gives a compact Hausdorff + second-countable Riemann surface. The inclusion of the uncompactified quotient is open, and + the q-coordinate gives every cusp chart. +5. Invariant holomorphic and meromorphic functions descend through the quotient and extend + across cusps under exact q-expansion or growth hypotheses. Local orders upstairs and + downstairs account for elliptic ramification and cusp widths. +6. A generic compact-Riemann-surface API for local multiplicity, degree, divisor pullback, the + degree-one biholomorphism theorem, and Riemann--Hurwitz is constructed here, then applied to + Fuchsian quotients and finite-index maps. +7. Fundamental polygons and the Poincaré polygon theorem produce the expected presentations, + orbifold signatures, genus formula, and triangle-group examples. +8. The level-one modular quotient is constructed and compactified before any identification + with `P^1`; the descended normalized `j`-map has degree one and supplies that identification. + +## Ownership and dependencies + +- **Mathlib owns the upper half-plane and matrix action.** Consume `UpperHalfPlane`, + `SL(2,R)`, the Möbius action, fixed-point classification, continuous and proper actions, and + the theorem that a discrete subgroup of `SL(2,R)` acts properly discontinuously. +- **This roadmap owns the effective projective action.** Factor the `SL(2,R)` action through + its center to `PSL(2,R)`, install the quotient topology and topological-group structure, and + prove faithfulness and holomorphy. A subgroup of `PSL(2,R)` is the public Fuchsian-group + input; no bespoke structure repeats a subgroup, topology, action, and discreteness fields. +- **The complex-manifolds roadmap owns `P^1`, general free complex quotients, compatible atlas + gluing, and the underlying complex-manifold vocabulary.** This roadmap applies its free + quotient theorem on the free locus and supplies the elliptic and cusp charts needed beyond + that theorem. +- **The universal-covers roadmap owns universal covers, deck groups, lifting criteria, and + induced maps on homotopy groups.** This roadmap identifies the upper-half-plane quotient as + an instance of that theory and contributes the Fuchsian and orbifold presentations. +- **The conformal-mapping roadmap owns the Riemann mapping theorem, analytic continuation, and + Schwarz reflection.** These are consumed in polygon uniformization and local extension + arguments. +- **The algebraic-topology roadmap owns finite CW models and Euler characteristic.** The + independent `RiemannSurface.Degree` module imports its + `TauCeti.AlgebraicTopology.Cellular.FiniteCW` module, applies + `compactManifoldFiniteCWType` in real dimension two, and transports + `finiteCWEulerCharacteristic` to the compact surface. No analytic Riemann--Roch theorem is + used to define genus or prove Riemann--Hurwitz. +- **The modular-forms roadmap owns modular forms and functions before descent, including the + normalized level-one `j`-function, modular invariance, q-expansion, and exact elliptic orders; + it also owns congruence-subgroup arithmetic, analytic Riemann--Roch, automorphy sheaves, and + dimension formulas.** It consumes this roadmap's quotient, compactification, local-multiplicity, + degree, divisor-pullback, degree-one, and Riemann--Hurwitz declarations. This roadmap does not + reconstruct modular forms, cohomology, or Riemann--Roch in its level-one application. +- **The algebraic-curves roadmap owns algebraic curves and their function fields.** This + roadmap constructs analytic Riemann surfaces. It proves no GAGA equivalence and creates no + algebraic curve by declaration. + +This roadmap supplies the shared module `TauCeti.Analysis.Complex.RiemannSurface.Degree`. Its +public contract is `RiemannSurface.genus`, `RiemannSurface.localMultiplicity`, +`RiemannSurface.degree`, +`RiemannSurface.degree_comp`, `RiemannSurface.biholomorph_of_degree_eq_one`, +`RiemannSurface.divisor_pullback`, and `RiemannSurface.riemannHurwitz`, all on the compact-surface +and finite holomorphic-map carriers pinned in `Suggested.lean`. These are Layer 5 deliverables, +not imports from a prospective supplier. If matching Mathlib declarations appear, replace the +local declarations and update imports immediately; no work waits for upstream changes. + +The import graph is strict: + +```text +TauCeti.AlgebraicTopology.Cellular.FiniteCW + -> TauCeti.Analysis.Complex.RiemannSurface.Degree + |-> Fuchsian compactification applications + `-> TauCeti.Analysis.Complex.ModularForms.DimensionFormula + +TauCeti.Analysis.Complex.ModularForms.LevelOne.JInputs + -> TauCeti.Analysis.Complex.Fuchsian.LevelOne +``` + +`RiemannSurface.Degree` imports neither `ModularForms` nor any analytic Riemann--Roch, +automorphy-sheaf, or dimension-formula module. The separate level-one application consumes the +lower `TauCeti.Analysis.Complex.ModularForms.LevelOne.JInputs` module, which contains only the +normalized `j`-function, its invariance, q-expansion, and elliptic orders. Thus the apparent +roadmap-level cycle is resolved by literal module boundaries rather than by an intended proof +order. + +## Pinned conventions + +These conventions prevent silent inversions and non-effective actions. + +- `PSL(2,R)` means Mathlib's `Matrix.ProjectiveSpecialLinearGroup (Fin 2) R`, the quotient of + `SL(2,R)` by its center. The action on `UpperHalfPlane` is the factor of Mathlib's `SL(2,R)` + action. Results about stabilizers use this effective action, not an `SL(2,R)` lift containing + a central element that fixes every point. +- A Fuchsian group is a `Subgroup PSL(2,R)` with the inherited topology and a proof of + discreteness. Proper discontinuity is obtained as a theorem or typeclass from that input. +- Hyperbolic area on `UpperHalfPlane` is Mathlib's existing `UpperHalfPlane.volume`, whose density + is `y⁻² dx dy`; consume its local-finiteness and `GL(2,ℝ)`-invariance theorems. This roadmap + identifies it with Riemannian volume, defines the covolume of a Fuchsian group from a measurable + fundamental domain, and proves independence of that domain. A group is cofinite exactly when + this covolume is finite. +- Quotients are `MulAction.orbitRel.Quotient`; projections are the ordinary quotient maps. The + free-locus projection is a covering and local biholomorphism. The full coarse quotient is not + falsely claimed to be a covering at elliptic points. +- Stabilizers are `MulAction.stabilizer Γ z`. Elliptic order is the finite cardinality of that + subgroup, proved cyclic from the derivative action in a local disc coordinate. +- A cusp is an orbit of a parabolic fixed point in Mathlib's boundary carrier `OnePoint ℝ`. + A cusp datum stores an actual representative `c`, a projective scaling `σ` with `σ(c)=∞`, a + positive element `γ`, the equality `⟨γ⟩ = stabilizer Γ c`, its width `w > 0`, and the + formula `σγσ⁻¹(z)=z+w`. Thus the conjugated full stabilizer is exactly `wℤ`; replacing `γ` + by a proper power is rejected. Width is not an invariant of the bare cusp. Replacing `σ` by + `z ↦ a σ(z)+b`, with `a>0`, sends `w` to `a w` and multiplies the q-coordinate by + `exp(2πib/(aw))`; the compactified complex structure is independent of this choice. +- The coordinate attached to cusp datum `(σ,w)` is + `q(z)=exp(2*pi*i*σ(z)/w)`. Its selected positive generator fixes `q`. Meridians are + counterclockwise-positive around `q=0`; prove the associated deck-generator convention and its + orientation-reversal law. +- Elliptic charts use a coordinate centered at the fixed point in which a generator acts by a + primitive `m`th root of unity. The quotient coordinate is `u=z^m`. Ramification order is + defined from this map-level local normal form. +- The compactified carrier is the displayed inductive disjoint sum with constructors + `ofQuotient : MulAction.orbitRel.Quotient Γ UpperHalfPlane → CompactifiedQuotient Γ` and + `ofCusp : CuspOrbit Γ → CompactifiedQuotient Γ`, together with its explicit equivalence to the + corresponding `Sum`. The topology glues punctured cusp neighbourhoods across those constructors + and the charts are subsequently proved. It is neither opaque nor a classified surface. +- Orbifold signature is derived from the genus of the compactification, the list of elliptic + stabilizer orders, and the number of cusp orbits. Public theorems continue to expose those + underlying objects. +- A finite holomorphic map's local multiplicity, degree, divisor pullback, degree-one theorem, and + Riemann--Hurwitz formula use the exact shared declarations owned in Layer 5 of this roadmap. + Degree is derived from fibre sums, not supplied as a field of a map record. +- `P^1` is the Riemann sphere supplied by the complex-manifolds roadmap. A quotient becomes + `P^1` only through a named biholomorphism proved after the quotient has been compactified. + +## Existing foundations to consume + +The development starts from the following material. + +- `Mathlib/Analysis/Complex/UpperHalfPlane/`: the topology and complex manifold on + `UpperHalfPlane`, the Möbius action of `SL(2,R)`, fixed points, and properness of the action. +- `Mathlib/Topology/Algebra/Group/DiscontinuousSubgroup.lean` and + `ProperlyDiscontinuousSMul`, including finiteness of stabilizers and local separation. +- `MulAction.orbitRel.Quotient`, quotient topology, quotient-covering maps on the free locus, + and Mathlib's charted-space construction for free properly discontinuous quotients. +- Mathlib's complex analytic functions, isolated zeros, removable singularities, power series, + exponential, winding and argument principles, and one-point compactification. +- `Mathlib.Analysis.Complex.UpperHalfPlane.Measure`, including + `UpperHalfPlane.volume_def`, local finiteness, and the `GL(2,ℝ)` invariant-measure instance. This + roadmap constructs only the Riemannian-volume comparison, measurable-fundamental-domain + covolume, its independence, and Gauss--Bonnet applications. +- The complex-manifolds roadmap's Riemann sphere, complex quotient theorem, atlas gluing, and + holomorphic local-diffeomorphism/descent APIs. +- The universal-covers roadmap's covering and deck-transformation results. +- The conformal-mapping roadmap's Riemann mapping and Schwarz-reflection results. +- The modular-forms roadmap's normalized level-one `j`, its invariance, q-expansion, and exact + orders at elliptic points. + +## Layer 0: the effective projective Möbius action + +1. Equip `PSL(2,R)` with the quotient topology from `SL(2,R)` and prove it is a Hausdorff + second-countable topological group. Relate the quotient map to Mathlib's algebraic quotient + by the center. +2. Construct the canonical homomorphism `PSL(2,R) → PGL(2,R)` and restrict Mathlib's existing + projective Möbius action along it. Prove compatibility with the `SL(2,R)` action, faithfulness, + joint continuity of `PSL(2,R) × UpperHalfPlane → UpperHalfPlane`, and that every element acts by + a biholomorphism. Do not export an unrelated permutation action as a second public action. +3. Prove that a discrete subgroup `Γ <= PSL(2,R)` acts properly discontinuously. Relate this + theorem to Mathlib's result for discrete subgroups of `SL(2,R)` through projective lifts, + without forcing a choice of lift into the public interface. +4. Prove finiteness of every stabilizer. Classify a nontrivial stabilizer as finite cyclic, + generated by an elliptic element, and identify its order with the order of the derivative in + a disc coordinate. +5. Define the free locus by `stabilizer Γ z = bot`; prove it is open and invariant. Apply the + generic quotient theorem there and prove the projection is a covering and local + biholomorphism. + +**Source spine:** Beardon, Chapters 7--8; Katok, §§2.1--2.4; Mathlib's +`UpperHalfPlane/ProperAction.lean` and `UpperHalfPlane/FixedPoints.lean`. + +## Layer 1: elliptic points and coarse quotient charts + +1. For an elliptic fixed point `z` of order `m`, construct an invariant disc whose translates + are disjoint outside its stabilizer. Conjugate the stabilizer action holomorphically to + multiplication by the `m`th roots of unity. +2. Prove the finite cyclic quotient theorem for a disc: `u -> u^m` is the orbit map, its target + is a disc, it is a local biholomorphism away from zero, and its local multiplicity at zero is + exactly `m`. +3. Glue these elliptic quotient charts to the free quotient atlas. Prove the full coarse + quotient is Hausdorff, second countable, and a Riemann surface; the quotient projection is + holomorphic and ramified exactly at elliptic orbits. +4. Prove independence from the invariant discs, linearizing coordinates, and stabilizer + generators. Record the exact transition law under replacement of a generator by another + primitive generator. +5. Prove descent and pullback criteria for holomorphic and meromorphic functions, with the local + order formula + `ord_z(f upstairs) = m * ord_[z](f descended)` at a point of stabilizer order `m`. + +**Source spine:** Farkas--Kra, Chapter I §§4--5; Miranda, Chapter III §§3--4; Katok, §2.4. + +## Layer 2: hyperbolic polygons and cofinite groups + +1. Consume Mathlib's invariant `UpperHalfPlane.volume`. Compare it with hyperbolic Riemannian + volume, define measurable fundamental domains, prove their areas agree, define covolume and + cofiniteness, and derive the Gauss--Bonnet area formula for finite hyperbolic polygons. +2. Develop geodesics, half-planes, convex hyperbolic polygons, sides, vertices, side pairings, + cycles, and angles using Mathlib's upper-half-plane metric and topology. Prove the local + finiteness facts required for translated polygons. +3. Define the input to the Poincaré polygon theorem by separate hypotheses: geodesic + finite-sidedness; an orientation-reversing fixed-point-free involution on sides; projective + side-pairing transformations; the exact side-identification law; vertex cycles and angle sums; + ideal-vertex parabolic cycles; and translated-interior no-overlap plus local finiteness. Prove + the theorem from these hypotheses, including discreteness, the fundamental-set theorem, and the + presentation. +4. Prove the converse from a non-elementary finite-covolume group and a Dirichlet centre with + trivial stabilizer. Construct the finite-sided Dirichlet polygon, its locally finite translates, + ideal vertices, side pairings, and cycles before deriving the equivalence with cofiniteness. +5. Extract elliptic cycles, parabolic cycles, cusp orbits, genus, and the standard presentation + from the polygon. Prove the relation between orientation of the boundary word and orientation + of meridians in the quotient. +6. Introduce a finite-or-cusp parameter with constructors `elliptic m` carrying `2 ≤ m` and + `cusp`; its reciprocal is `1/m` and `0`, respectively. Construct hyperbolic triangle groups from + polygon reflections for triples satisfying the typed inequality that the reciprocal sum is + less than one. Prove discreteness, faithfulness of the presentation, elliptic orders, and cusp + count in one theorem family; `(p,q,cusp)` is not untyped infinity notation. + +**Source spine:** Beardon, Chapters 9--11; Katok, Chapters 3--4; Stillwell, Chapter 5. + +## Layer 3: cusps and q-coordinates + +1. Classify parabolic elements and their unique boundary fixed points. Define cusp orbits in + `OnePoint ℝ` and prove finiteness for cofinite groups. +2. For each cusp representative `c`, construct a cusp datum: choose a projective + transformation `σ` with `σ(c)=∞`, prove the full stabilizer is infinite cyclic, orient it, + select its primitive positive generator `γ`, and prove both `⟨γ⟩ = stabilizer Γ c` and + `σγσ⁻¹(z)=z+w` for `w>0`. Equivalently, the conjugated full stabilizer is exactly `wℤ`. + Prove uniqueness only relative to this normalized datum. +3. Construct sufficiently high horodiscs which are precisely invariant under the cusp + stabilizer. Prove distinct cusp-orbit horodiscs have disjoint images after shrinking and that + the complement of their images in a finite-area fundamental polygon is compact. +4. Define `q(z)=exp(2*pi*i*σ(z)/w)`. Prove invariance under the selected generator, identify the + punctured-disc quotient biholomorphically, and prove `q → 0` along the cusp. For a second datum + `σ'=aσ+b`, prove `w'=aw` and + `q'=exp(2πib/(aw))q`, then prove that this nonzero scalar change gives the same compactified + complex structure. +5. Prove the Laurent/q-expansion criterion: an invariant holomorphic function descends on the + punctured cusp; boundedness gives a removable singularity, polynomial exponential growth gives + a pole of controlled order, and decay gives a zero of controlled order. + +**Source spine:** Diamond--Shurman, §§2.3--2.4; Katok, §§3.4 and 4.2; Forster, §19. + +## Layer 4: compactified quotient Riemann surfaces + +The construction order in this layer is normative. + +1. Form the carrier as the explicit inductive disjoint sum of the coarse orbit quotient and the + subtype of parabolic boundary orbits. Use the displayed constructors and sum equivalence in + `Suggested.lean`. Define cusp neighbourhoods from the precisely invariant horodiscs and prove + the topology is independent of all height choices. +2. Prove the carrier is Hausdorff and second countable. For a cofinite group, use the compact + truncated fundamental polygon plus finitely many cusp discs to prove compactness. +3. Extend the quotient atlas with the q-coordinate at every new point. Verify transitions with + free and elliptic charts, then prove `ChartedSpace` and `IsManifold 𝓘(ℂ, ℂ) ∞`. +4. Prove that the original quotient is an open dense submanifold and that the compactifying + points are exactly the complement. Prove functoriality for conjugate groups. For every + finite-index inclusion `Γ' ≤ Γ`, extend the quotient map to cusps and prove that compatible data + give `e_cusp = w_{Γ'}/w_Γ ∈ ℕ`. Compute elliptic ramification from stabilizer indices, + prove multiplicativity in subgroup towers, and prove the fibre-cardinality and degree formulas. +5. Derive the orbifold signature from the compact surface, elliptic stabilizer orders, and cusp + set. Prove the orbifold Euler-characteristic and area formula, including all factors of + `2*pi` and the effective `PSL` convention. + +No step identifies the carrier with `P^1`, a torus, or another classified surface by definition. + +**Source spine:** Katok, Chapter 4; Diamond--Shurman, §§2.4--2.5; Forster, §§18--19. + +## Layer 5: compact-surface degree theory and Fuchsian applications + +1. In the independent lower module `TauCeti.Analysis.Complex.RiemannSurface.Degree`, consume + AlgebraicTopology's finite CW model of a compact smooth surface and its homotopy-invariant + Euler characteristic. Define topological genus by `chi(X) = 2 - 2 * genus(X)` and prove that it + agrees with the usual analytic genus. This module imports neither ModularForms nor analytic + Riemann--Roch. +2. In that same lower module, define finite nonconstant holomorphic maps, local multiplicity from + the local analytic normal form, and degree as the sum of local multiplicities over a fibre. + Prove positivity, fibre finiteness, independence of the chosen fibre, multiplicativity under + composition, and the degree-one biholomorphism theorem. +3. Define pullback of finite divisors by local multiplicity and construct the ramification + divisor. Prove first the branched-cover Euler-characteristic formula + `chi(X) = degree(f) * chi(Y) - ramificationDegree(f)` by excising pairwise-disjoint branch + discs, applying finite-cover multiplicativity to their complement, and adding back the discs. + Derive Riemann--Hurwitz by rewriting both Euler characteristics as `2 - 2g`; do not use the + canonical-divisor formula or Riemann--Roch in this proof spine. The exact public names are + represented in `Suggested.lean`. +4. Prove that a `Γ`-invariant holomorphic or meromorphic function descends uniquely to the + coarse quotient. Combine the elliptic local-order formula and cusp q-expansion criterion to + extend it to the compactification. +5. Apply the generic declarations to finite-index compactified quotient maps. Reprove neither + generic fibre finiteness nor independence of the degree sum; identify the local multiplicities + with the cusp-width and elliptic-stabilizer ratios from Layer 4. +6. Derive the Fuchsian Riemann--Hurwitz and orbifold Euler-characteristic formulas, with the chosen + effective-action and orientation conventions explicit. + +**Source spine:** Forster, §§10, 17, and 19; Miranda, Chapter III §§3--4; Farkas--Kra, +Chapter II §4. + +## Layer 6: the level-one modular quotient, in construction order + +This layer consumes the modular-forms roadmap's normalized `j`-function, modular invariance, +q-expansion, and exact elliptic orders. + +1. Apply Layers 0--4 to the effective level-one modular group. Construct its coarse quotient, + elliptic charts, unique cusp, and compact Riemann surface `X(1)`. Prove its signature from + the standard fundamental polygon. +2. Descend the normalized `j : UpperHalfPlane -> C` to the uncompactified quotient. Use its + q-expansion to extend it meromorphically over the cusp and its elliptic orders to compute all + local multiplicities on `X(1)`. +3. Regard the extension as a holomorphic map `X(1) -> P^1`. Prove it has a single simple pole + over infinity, equivalently degree one, using Layer 5's fibre-counting theorem. +4. Apply the degree-one theorem to obtain a named biholomorphism `X(1) ≃ P^1`. Normalize it by + the cusp and elliptic images and prove that this biholomorphism is the descended `j`-map. +5. Transfer no atlas backward by fiat: every statement about `P^1` is obtained through this + proved biholomorphism after the compact quotient already exists. + +**Source spine:** Diamond--Shurman, §§2.3--2.5; Serre, Chapter VII; the modular-forms roadmap's +`j` targets. + +## Dependency order and parallel work + +| Track | Depends on | Feeds | +| --- | --- | --- | +| L0 effective action and free locus | Mathlib, complex manifolds | L1--L4 | +| L1 elliptic charts | L0, complex-manifold gluing | L4--L6 | +| L2 polygons and presentations | L0, conformal mapping | L3--L4, L6 | +| L3 cusps and q-coordinates | L0, L2 | L4--L6 | +| L4 compactification | L1--L3 | L5--L6 | +| L5 degree theory and applications | complex analysis, compact surfaces, L4 | L6, modular forms | +| L6 level-one example | L0--L5, modular forms | normalized `X(1) ≃ P^1` | + +L1 and L2 can proceed in parallel after L0. The local q-coordinate calculation in L3 can proceed +while the global polygon results are completed. The generic part of Layer 5 can proceed in +parallel with Layers 0--4; its Fuchsian applications begin after Layer 4. Matching Mathlib APIs +replace local declarations when available, but no layer waits for them. + +## Acceptance checks + +- The projective action is effective: an element acting trivially on `UpperHalfPlane` is the + identity in `PSL(2,R)`. +- A discrete subgroup's stabilizer is finite. The free-locus quotient projection is a covering, + while an elliptic point of order `m` has local quotient map `z |-> z^m` and is not mislabeled a + covering point. +- A cyclic rotation of a disc yields a smooth disc quotient with ramification index equal to the + group order. +- A cusp datum records a representative sent to infinity and a selected generator whose powers + are exactly the full stabilizer. A proper power is rejected even though it has a positive + translation formula. Its q-coordinate descends under the whole stabilizer; replacing `σ` by + `aσ+b` changes `w` and `q` by the exact formulas above but not the compactified atlas. +- Mathlib's upper-half-plane volume is imported and compared with hyperbolic volume; no second + invariant measure is constructed. +- A finite-sided cofinite polygon produces a compact surface after one point is adjoined for each + cusp orbit, with the carrier visibly the coarse quotient plus cusp-orbit subtype and compactness + proved from a truncated fundamental polygon. +- The triangle-group theorem uses the typed finite-or-cusp parameter and derives the presentation + and signature from side pairings. +- Invariant functions descend through `MulAction.orbitRel.Quotient`; no choice-based quotient + section occurs in the public construction. +- Local orders downstairs multiply by elliptic stabilizer order on pullback. Cusp orders use the + q-coordinate and width from a chosen compatible cusp datum and are proved independent of it. +- The generic degree is a fibre-independent sum of positive local multiplicities, composes + multiplicatively, pulls back divisors, proves Riemann--Hurwitz, and turns degree one into a + biholomorphism; these declarations are supplied here rather than attributed to another roadmap. +- The level-one compact quotient is a compact Riemann surface before the normalized `j`-function + is descended. The proof of `X(1) ≃ P^1` passes through the theorem that the descended map has + degree one. +- A structure whose fields assert compactness, the orbifold signature, degree, or the final + biholomorphism does not satisfy the roadmap. + +## References + +- Alan Beardon, *The Geometry of Discrete Groups*, Graduate Texts in Mathematics 91, + Springer, 1983, especially Chapters 7--11. +- Svetlana Katok, *Fuchsian Groups*, Chicago Lectures in Mathematics, University of Chicago + Press, 1992, especially Chapters 2--4. +- Fred Diamond and Jerry Shurman, *A First Course in Modular Forms*, Graduate Texts in + Mathematics 228, Springer, 2005, §§2.3--2.5. +- Otto Forster, *Lectures on Riemann Surfaces*, Graduate Texts in Mathematics 81, + Springer, 1981, especially §§10 and 17--19. +- Hershel Farkas and Irwin Kra, *Riemann Surfaces*, Graduate Texts in Mathematics 71, + Springer, second edition, 1992. +- Rick Miranda, *Algebraic Curves and Riemann Surfaces*, Graduate Studies in Mathematics 5, + American Mathematical Society, 1995, Chapter III. +- Jean-Pierre Serre, *A Course in Arithmetic*, Graduate Texts in Mathematics 7, + Springer, 1973, Chapter VII. +- John Stillwell, *Geometry of Surfaces*, Universitext, Springer, 1992, Chapter 5. diff --git a/TauCetiRoadmap/FuchsianOrbifolds/Suggested.lean b/TauCetiRoadmap/FuchsianOrbifolds/Suggested.lean new file mode 100644 index 00000000..995c5248 --- /dev/null +++ b/TauCetiRoadmap/FuchsianOrbifolds/Suggested.lean @@ -0,0 +1,435 @@ +import Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints +import Mathlib.Analysis.Complex.UpperHalfPlane.Manifold +import Mathlib.Analysis.Complex.UpperHalfPlane.Measure +import Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction +import Mathlib.Geometry.Manifold.Diffeomorph +import Mathlib.Geometry.Manifold.Instances.Quotient +import Mathlib.LinearAlgebra.Matrix.ProjectiveSpecialLinearGroup +import Mathlib.Topology.Compactification.OnePoint.ProjectiveLine + +/-! +# Fuchsian groups and orbifold Riemann surfaces: target signatures + +**This file is not the roadmap and is not exhaustive.** The definitive document is +`README.md`. These declarations pin the effective projective action, the standard orbit +quotient and free locus, invariant-function descent, primitive cusp data, the compactification +carrier, and the compact-Riemann-surface degree API owned by this roadmap. + +Elliptic quotient charts and the topology and atlas on the displayed compactification carrier +remain roadmap targets. They are specified in the markdown rather than represented by empty +`Prop` wrappers. +-/ + +namespace TauCetiRoadmap.FuchsianOrbifolds + +open MeasureTheory +open Matrix MulAction +open scoped ContDiff Manifold MatrixGroups UpperHalfPlane + +private abbrev SL₂R := SL(2, ℝ) +private abbrev PSL₂R := PSL(2, ℝ) + +/-! ## Effective projective action -/ + +/-- The Möbius action of `SL(2,R)` factors through its center. This named homomorphism is the +canonical projective action; any `MulAction` and continuous-action instances are derived from it +without exporting a competing action. -/ +noncomputable def pslAction : PSL₂R →* Equiv.Perm ℍ := by + sorry + +/-- The projective Möbius action is effective. -/ +theorem pslAction_injective : Function.Injective pslAction := by + sorry + +/-- Every element of the projective group acts holomorphically on the upper half-plane. -/ +theorem pslAction_mdifferentiable (g : PSL₂R) : MDiff (pslAction g : ℍ → ℍ) := by + sorry + +/-- The effective action is jointly continuous. Its construction is the restriction of Mathlib's +projective action along the canonical map `PSL(2,ℝ) → PGL(2,ℝ)`. -/ +theorem continuous_pslAction : Continuous fun p : PSL₂R × ℍ ↦ pslAction p.1 p.2 := by + sorry + +/-- Restrict the one canonical action to a subgroup; a Fuchsian input is the subgroup together +with `[DiscreteTopology Γ]`, not a record duplicating either datum. -/ +@[instance_reducible] +noncomputable def pslSubgroupMulAction (Γ : Subgroup PSL₂R) : MulAction Γ ℍ := by + sorry + +/-- The effective projective action on the ideal boundary `P¹(R) = OnePoint R`. It is obtained +from the projective action rather than by choosing matrix representatives. -/ +noncomputable def pslBoundaryAction : PSL₂R →* Equiv.Perm (OnePoint ℝ) := by + sorry + +/-- Restriction of the canonical boundary action to a projective subgroup. -/ +@[instance_reducible] +noncomputable def pslBoundarySubgroupMulAction (Γ : Subgroup PSL₂R) : + MulAction Γ (OnePoint ℝ) := by + sorry + +/-- The trivial-stabilizer locus for the effective subgroup action. -/ +noncomputable def pslFreeLocus (Γ : Subgroup PSL₂R) : Set ℍ := + letI := pslSubgroupMulAction Γ + {z | MulAction.stabilizer Γ z = ⊥} + +/-- Discreteness of a projective subgroup supplies proper discontinuity for its effective action. -/ +theorem properlyDiscontinuous_pslSubgroup (Γ : Subgroup PSL₂R) [DiscreteTopology Γ] : + letI := pslSubgroupMulAction Γ + ProperlyDiscontinuousSMul Γ ℍ := by + sorry + +/-- The roadmap consumes Mathlib's invariant measure rather than constructing another one. -/ +example : IsLocallyFiniteMeasure (volume : Measure ℍ) := inferInstance + +/-! ## Existing properly-discontinuous and free-locus anchors -/ + +/-- Mathlib already proves proper discontinuity for every discrete subgroup of `SL(2,R)`. +The roadmap proves the effective `PSL(2,R)` form and does not infer freeness from this result. -/ +example (Γ : Subgroup SL₂R) [DiscreteTopology Γ] : ProperlyDiscontinuousSMul Γ ℍ := + inferInstance + +/-- Proper discontinuity gives finite stabilizers, not trivial stabilizers. -/ +example (Γ : Subgroup SL₂R) [DiscreteTopology Γ] (z : ℍ) : + (MulAction.stabilizer Γ z : Set Γ).Finite := + ProperlyDiscontinuousSMul.finite_stabilizer z + +/-- The ordinary quotient projection is a covering on exactly the trivial-stabilizer locus. +Elliptic points are handled by the separate cyclic quotient chart of the roadmap. -/ +example (Γ : Subgroup SL₂R) [DiscreteTopology Γ] : + IsCoveringMapOn (Quotient.mk <| MulAction.orbitRel Γ ℍ) <| + (Quotient.mk <| MulAction.orbitRel Γ ℍ) '' + {z | MulAction.stabilizer Γ z = ⊥} := + isCoveringMapOn_quotientMk_of_properlyDiscontinuousSMul + +/-! ## Descent through the standard orbit quotient -/ + +private abbrev OrbitQuotient (Γ : Type*) [Group Γ] [MulAction Γ ℍ] := + MulAction.orbitRel.Quotient Γ ℍ + +/-- An invariant function descends through `MulAction.orbitRel.Quotient`; no quotient section is +chosen. Holomorphic and meromorphic descent add the corresponding map-level hypotheses. -/ +def descendInvariant {Γ Y : Type*} [Group Γ] [MulAction Γ ℍ] (f : ℍ → Y) + (hf : ∀ (g : Γ) (z : ℍ), f (g • z) = f z) : OrbitQuotient Γ → Y := + Quotient.lift f fun a b hab ↦ by + rcases hab with ⟨g, rfl⟩ + exact hf g b + +@[simp] +theorem descendInvariant_quotientMk {Γ Y : Type*} [Group Γ] [MulAction Γ ℍ] + (f : ℍ → Y) (hf : ∀ (g : Γ) (z : ℍ), f (g • z) = f z) (z : ℍ) : + descendInvariant f hf (Quotient.mk'' z) = f z := + rfl + +/-! ## Choice-dependent cusp data and coordinates -/ + +/-- Parabolicity in the effective projective group. The implementation is obtained by descending +Mathlib's matrix classification and is independent of a lift to `SL(2,R)`. -/ +def IsParabolic (g : PSL₂R) : Prop := + ∃ lift : SL₂R, + QuotientGroup.mk' (Subgroup.center SL₂R) lift = g ∧ + (Matrix.SpecialLinearGroup.toGL lift).IsParabolic + +/-- A boundary point is a cusp when a nontrivial parabolic element of the subgroup fixes it. -/ +def IsCuspPoint (Γ : Subgroup PSL₂R) (c : OnePoint ℝ) : Prop := + ∃ g : Γ, g ≠ 1 ∧ IsParabolic g ∧ pslBoundaryAction g c = c + +/-- The full subgroup stabilizer of a boundary point. -/ +noncomputable def cuspStabilizer (Γ : Subgroup PSL₂R) (c : OnePoint ℝ) : Subgroup Γ := + letI := pslBoundarySubgroupMulAction Γ + MulAction.stabilizer Γ c + +/-- The orbit relation on the projective boundary for the effective subgroup action. -/ +noncomputable def boundaryOrbitRel (Γ : Subgroup PSL₂R) : Setoid (OnePoint ℝ) := + letI := pslBoundarySubgroupMulAction Γ + MulAction.orbitRel Γ (OnePoint ℝ) + +/-- Boundary orbits before restricting to parabolic fixed points. -/ +abbrev BoundaryOrbit (Γ : Subgroup PSL₂R) := Quotient (boundaryOrbitRel Γ) + +/-- Being a cusp is invariant under the subgroup action and therefore descends to boundary +orbits. -/ +def IsCuspOrbit (Γ : Subgroup PSL₂R) (C : BoundaryOrbit Γ) : Prop := + ∃ c : OnePoint ℝ, IsCuspPoint Γ c ∧ Quotient.mk (boundaryOrbitRel Γ) c = C + +theorem isCuspOrbit_quotientMk {Γ : Subgroup PSL₂R} (c : OnePoint ℝ) : + IsCuspOrbit Γ (Quotient.mk (boundaryOrbitRel Γ) c) ↔ IsCuspPoint Γ c := by + sorry + +/-- The actual cusp-orbit carrier adjoined in the compactification. -/ +abbrev CuspOrbit (Γ : Subgroup PSL₂R) := {C : BoundaryOrbit Γ // IsCuspOrbit Γ C} + +/-- Normalized data at an actual cusp representative. The selected element generates the full +stabilizer, the scaling sends the cusp to infinity, and the generator becomes translation by the +positive width. Thus a proper power of the primitive generator cannot masquerade as cusp data. -/ +structure CuspDatum (Γ : Subgroup PSL₂R) where + cusp : OnePoint ℝ + isCusp : IsCuspPoint Γ cusp + scaling : PSL₂R + scaling_cusp : pslBoundaryAction scaling cusp = OnePoint.infty + positiveGenerator : Γ + width : ℝ + width_pos : 0 < width + zpowers_generator : Subgroup.zpowers positiveGenerator = cuspStabilizer Γ cusp + conjugates_generator : ∀ z : ℍ, + pslAction scaling (pslAction positiveGenerator z) = width +ᵥ pslAction scaling z + +/-- The cusp orbit underlying normalized cusp data. -/ +noncomputable def CuspDatum.orbit {Γ : Subgroup PSL₂R} (D : CuspDatum Γ) : CuspOrbit Γ := + ⟨Quotient.mk (boundaryOrbitRel Γ) D.cusp, + (isCuspOrbit_quotientMk (Γ := Γ) D.cusp).2 D.isCusp⟩ + +/-- Membership in the full cusp stabilizer is exactly being an integral power of the selected +positive generator. -/ +theorem CuspDatum.mem_stabilizer_iff {Γ : Subgroup PSL₂R} (D : CuspDatum Γ) (g : Γ) : + g ∈ cuspStabilizer Γ D.cusp ↔ ∃ n : ℤ, g = D.positiveGenerator ^ n := by + sorry + +/-- After scaling, the full stabilizer is exactly the translation group `width * Z`; the selected +generator corresponds to the positive translation `+width`. -/ +theorem CuspDatum.conjugates_stabilizer_iff {Γ : Subgroup PSL₂R} (D : CuspDatum Γ) (g : Γ) : + g ∈ cuspStabilizer Γ D.cusp ↔ + ∃ n : ℤ, g = D.positiveGenerator ^ n ∧ ∀ z : ℍ, + pslAction D.scaling (pslAction g z) = + ((n : ℝ) * D.width) +ᵥ pslAction D.scaling z := by + sorry + +/-- The q-coordinate associated to a positive cusp width `w`. -/ +noncomputable def cuspCoordinate (w : ℝ) (z : ℍ) : ℂ := + Complex.exp (2 * (Real.pi : ℂ) * Complex.I * (z : ℂ) / w) + +/-- Positive translation by the cusp width fixes the q-coordinate. -/ +theorem cuspCoordinate_vadd (w : ℝ) (hw : 0 < w) (z : ℍ) : + cuspCoordinate w (w +ᵥ z) = cuspCoordinate w z := by + sorry + +/-- A cusp coordinate takes values in the punctured plane before compactification. -/ +theorem cuspCoordinate_ne_zero (w : ℝ) (z : ℍ) : cuspCoordinate w z ≠ 0 := by + exact Complex.exp_ne_zero _ + +/-- The q-coordinate associated to all of the normalized cusp datum. -/ +noncomputable def CuspDatum.coordinate {Γ : Subgroup PSL₂R} (D : CuspDatum Γ) (z : ℍ) : ℂ := + cuspCoordinate D.width (pslAction D.scaling z) + +/-- The q-coordinate descends under every element of the full cusp stabilizer, not only under the +selected generator. -/ +theorem CuspDatum.coordinate_eq_of_mem_stabilizer {Γ : Subgroup PSL₂R} (D : CuspDatum Γ) + (g : Γ) (hg : g ∈ cuspStabilizer Γ D.cusp) (z : ℍ) : + D.coordinate (pslAction g z) = D.coordinate z := by + sorry + +/-- Under `σ' = aσ+b`, width scales by `a` and q-coordinates differ by the displayed nonzero +constant. This is the transition map used to prove independence of compactification. -/ +theorem CuspDatum.coordinate_change {Γ : Subgroup PSL₂R} (D D' : CuspDatum Γ) + (a b : ℝ) (ha : 0 < a) (hwidth : D'.width = a * D.width) + (hscale : ∀ z : ℍ, (pslAction D'.scaling z : ℂ) = + a * (pslAction D.scaling z : ℂ) + b) (z : ℍ) : + D'.coordinate z = Complex.exp (2 * Real.pi * Complex.I * b / (a * D.width)) * + D.coordinate z := by + sorry + +/-! ## Typed triangle parameters -/ + +/-- A triangle vertex is either elliptic of a stated finite order or a cusp. -/ +inductive TriangleOrder where + | elliptic (m : ℕ) (hm : 2 ≤ m) + | cusp + +/-- The reciprocal contribution to the hyperbolic triangle inequality. -/ +noncomputable def TriangleOrder.reciprocal : TriangleOrder → ℝ + | .elliptic m _ => (m : ℝ)⁻¹ + | .cusp => 0 + +/-! ## Elliptic local coordinate anchor -/ + +/-- The coordinate map for a cyclic stabilizer of order `m`. The roadmap proves that the full +local orbit map is biholomorphically conjugate to this map. -/ +def cyclicQuotientCoordinate (m : ℕ) (z : ℂ) : ℂ := z ^ m + +theorem cyclicQuotientCoordinate_differentiable (m : ℕ) : + Differentiable ℂ (cyclicQuotientCoordinate m) := by + sorry + +theorem cyclicQuotientCoordinate_eq_zero {m : ℕ} (hm : 0 < m) (z : ℂ) : + cyclicQuotientCoordinate m z = 0 ↔ z = 0 := by + sorry + +/-! ## Compactification carrier -/ + +/-- The effective coarse orbit relation on the upper half-plane. -/ +noncomputable def coarseOrbitRel (Γ : Subgroup PSL₂R) : Setoid ℍ := + letI := pslSubgroupMulAction Γ + MulAction.orbitRel Γ ℍ + +/-- The coarse quotient before adjoining cusps. -/ +abbrev CoarseQuotient (Γ : Subgroup PSL₂R) := Quotient (coarseOrbitRel Γ) + +/-- The compactification carrier is visibly the disjoint sum of the coarse orbit quotient and one +point for each cusp orbit. Its topology glues punctured cusp neighbourhoods across these +constructors; the carrier is not an arbitrary type or a classified surface. -/ +inductive CompactifiedQuotient (Γ : Subgroup PSL₂R) where + | ofQuotient (point : CoarseQuotient Γ) + | ofCusp (cusp : CuspOrbit Γ) + +/-- The compactification carrier has exactly the promised sum construction. -/ +def CompactifiedQuotient.equivSum {Γ : Subgroup PSL₂R} : + CompactifiedQuotient Γ ≃ CoarseQuotient Γ ⊕ CuspOrbit Γ where + toFun + | .ofQuotient point => Sum.inl point + | .ofCusp cusp => Sum.inr cusp + invFun + | Sum.inl point => .ofQuotient point + | Sum.inr cusp => .ofCusp cusp + left_inv point := by cases point <;> rfl + right_inv point := by cases point <;> rfl + +noncomputable instance compactifiedTopologicalSpace (Γ : Subgroup PSL₂R) + [DiscreteTopology Γ] : TopologicalSpace (CompactifiedQuotient Γ) := by + sorry + +@[instance_reducible] +noncomputable def compactifiedChartedSpace (Γ : Subgroup PSL₂R) [DiscreteTopology Γ] : + ChartedSpace ℂ (CompactifiedQuotient Γ) := by + sorry + +/-- Elliptic and cusp charts give the compactified carrier its Riemann-surface structure. -/ +theorem compactified_isManifold (Γ : Subgroup PSL₂R) [DiscreteTopology Γ] : + letI := compactifiedChartedSpace Γ + IsManifold 𝓘(ℂ, ℂ) ∞ (CompactifiedQuotient Γ) := by + sorry + +/-! +The level-one application first constructs a compact Riemann surface, then descends `j`, proves +the extended map to `OnePoint ℂ` has degree one, and only then obtains a biholomorphism with the +Riemann sphere. No target here installs a sphere atlas on the quotient by assumption. +-/ + +end TauCetiRoadmap.FuchsianOrbifolds + +/-! ## Generic compact-Riemann-surface degree API owned by this roadmap + +These declarations target `TauCeti.Analysis.Complex.RiemannSurface.Degree`. They use genuine maps, +finite fibres, local multiplicities, and divisors rather than records carrying their desired +conclusions as fields. + +The target module imports `TauCeti.AlgebraicTopology.Cellular.FiniteCW` and nothing from +`ModularForms`. Its Euler characteristic is the literal transport of +`TauCetiRoadmap.AlgebraicTopology.finiteCWEulerCharacteristic` along the model supplied by +`TauCetiRoadmap.AlgebraicTopology.compactManifoldFiniteCWType 2`. Those roadmap-namespace names +are import checks, not declarations to duplicate in the implementation. +-/ + +namespace RiemannSurface + +open scoped ContDiff Manifold + +/-- A nonconstant holomorphic map with finite fibres. For connected compact Riemann surfaces, +this is the map carrier used by local multiplicity and degree. -/ +structure FiniteHolomorphicMap (X Y : Type*) [TopologicalSpace X] [ChartedSpace ℂ X] + [TopologicalSpace Y] [ChartedSpace ℂ Y] where + toFun : X → Y + holomorphic : MDiff toFun + nonconstant : ∃ x x', toFun x ≠ toFun x' + finite_fiber : ∀ y, {x | toFun x = y}.Finite + +instance {X Y : Type*} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] + [ChartedSpace ℂ Y] : CoeFun (FiniteHolomorphicMap X Y) fun _ ↦ X → Y := + ⟨FiniteHolomorphicMap.toFun⟩ + +section CompactSurfaces + +variable {X Y Z : Type*} +variable [TopologicalSpace X] [ChartedSpace ℂ X] [T2Space X] [CompactSpace X] + [ConnectedSpace X] [IsManifold 𝓘(ℂ, ℂ) ∞ X] +variable [TopologicalSpace Y] [ChartedSpace ℂ Y] [T2Space Y] [CompactSpace Y] + [ConnectedSpace Y] [IsManifold 𝓘(ℂ, ℂ) ∞ Y] +variable [TopologicalSpace Z] [ChartedSpace ℂ Z] [T2Space Z] [CompactSpace Z] + [ConnectedSpace Z] [IsManifold 𝓘(ℂ, ℂ) ∞ Z] + +/-- Composition stays in the finite nonconstant holomorphic-map carrier. -/ +noncomputable def FiniteHolomorphicMap.comp (g : FiniteHolomorphicMap Y Z) + (f : FiniteHolomorphicMap X Y) : FiniteHolomorphicMap X Z := by + sorry + +/-- The positive local multiplicity of a finite holomorphic map at a point. -/ +noncomputable def localMultiplicity (f : FiniteHolomorphicMap X Y) (x : X) : ℕ := by + sorry + +theorem localMultiplicity_pos (f : FiniteHolomorphicMap X Y) (x : X) : + 0 < localMultiplicity f x := by + sorry + +/-- The fibre-independent sum of local multiplicities. -/ +noncomputable def degree (f : FiniteHolomorphicMap X Y) : ℕ := by + sorry + +theorem degree_eq_fiber_sum (f : FiniteHolomorphicMap X Y) (y : Y) : + degree f = ∑ x ∈ (f.finite_fiber y).toFinset, localMultiplicity f x := by + sorry + +theorem localMultiplicity_comp (g : FiniteHolomorphicMap Y Z) + (f : FiniteHolomorphicMap X Y) (x : X) : + localMultiplicity (g.comp f) x = localMultiplicity g (f x) * localMultiplicity f x := by + sorry + +theorem degree_comp (g : FiniteHolomorphicMap Y Z) (f : FiniteHolomorphicMap X Y) : + degree (g.comp f) = degree g * degree f := by + sorry + +/-- A degree-one finite holomorphic map is a biholomorphism, not merely a homeomorphism. -/ +noncomputable def biholomorph_of_degree_eq_one (f : FiniteHolomorphicMap X Y) + (hf : degree f = 1) : X ≃ₘ⟮𝓘(ℂ, ℂ), 𝓘(ℂ, ℂ)⟯ Y := by + sorry + +/-- Divisors are integral finite formal sums of points. -/ +abbrev Divisor (X : Type*) := X →₀ ℤ + +/-- Pullback weights each point by the map's local multiplicity. -/ +noncomputable def divisor_pullback (f : FiniteHolomorphicMap X Y) : + Divisor Y →+ Divisor X := by + sorry + +/-- The Euler characteristic transported from AlgebraicTopology's finite CW model of the compact +surface. The implementation is the literal application of `compactManifoldFiniteCWType 2` and +`finiteCWEulerCharacteristic`; it does not introduce an analytic or Riemann--Roch definition. -/ +noncomputable def surfaceEulerCharacteristic (X : Type*) [TopologicalSpace X] + [ChartedSpace ℂ X] [T2Space X] [CompactSpace X] [ConnectedSpace X] + [IsManifold 𝓘(ℂ, ℂ) ∞ X] : ℤ := by + sorry + +/-- Genus is defined topologically from Euler characteristic. The preceding finite-CW theorem +proves that `2 - chi(X)` is a nonnegative even integer. -/ +noncomputable def genus (X : Type*) [TopologicalSpace X] [ChartedSpace ℂ X] [T2Space X] + [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ, ℂ) ∞ X] : ℕ := + Int.toNat ((2 - surfaceEulerCharacteristic X) / 2) + +/-- The defining Euler-characteristic identity for topological genus. Analytic compatibility is +then proved independently of the higher ModularForms Riemann--Roch layer. -/ +theorem surfaceEulerCharacteristic_eq_two_sub_two_mul_genus : + surfaceEulerCharacteristic X = 2 - 2 * (genus X : ℤ) := by + sorry + +/-- Degree of the ramification divisor `sum_x (e_x - 1)[x]`. -/ +noncomputable def ramificationDegree (f : FiniteHolomorphicMap X Y) : ℕ := by + sorry + +/-- The acyclic proof spine: excise branch discs, use finite-cover multiplicativity on their +complement, and add the discs back. This theorem depends only on finite-CW Euler characteristic +and local normal forms, never on canonical divisors or Riemann--Roch. -/ +theorem branchedCover_eulerCharacteristic (f : FiniteHolomorphicMap X Y) : + surfaceEulerCharacteristic X = + (degree f : ℤ) * surfaceEulerCharacteristic Y - (ramificationDegree f : ℤ) := by + sorry + +/-- Riemann--Hurwitz is an algebraic rewrite of the topological branched-cover formula. -/ +theorem riemannHurwitz (f : FiniteHolomorphicMap X Y) : + 2 * (genus X : ℤ) - 2 = + (degree f : ℤ) * (2 * (genus Y : ℤ) - 2) + (ramificationDegree f : ℤ) := by + have hX := surfaceEulerCharacteristic_eq_two_sub_two_mul_genus (X := X) + have hY := surfaceEulerCharacteristic_eq_two_sub_two_mul_genus (X := Y) + have hχ := branchedCover_eulerCharacteristic f + rw [hX, hY] at hχ + linarith + +end CompactSurfaces + +end RiemannSurface diff --git a/TauCetiRoadmap/ModularForms/README.md b/TauCetiRoadmap/ModularForms/README.md index bb9e26fa..e5346a45 100644 --- a/TauCetiRoadmap/ModularForms/README.md +++ b/TauCetiRoadmap/ModularForms/README.md @@ -23,7 +23,9 @@ resting throughout on complex analysis, Fourier analysis, and the arithmetic of The hardest target is the **dimension formulas** for `M_k(Γ)` and `S_k(Γ)` at general level (Diamond–Shurman Thms 3.5.1 and 3.6.1), proved by the **classical analytic route**: the valence formula and the elliptic-point and cusp counts of the quotient `Γ\ℍ` for the upper bounds, and -analytic Riemann–Roch on `X(Γ)` — built inside Layer 10, not assumed — for the lower bounds. Mere +analytic Riemann–Roch on `X(Γ)` — built inside Layer 10, not assumed — for the lower bounds. +The Fuchsian-orbifolds roadmap supplies the compact quotient and its generic degree and +Riemann–Hurwitz API; this roadmap supplies the modular and Riemann–Roch inputs. Mere *finite-dimensionality* at general level is **not** the hard part — it arrives in Mathlib by the elementary Sturm-bound route (see Layer 10) and this roadmap consumes it. What this roadmap adds is the **exact dimension formula** of Diamond–Shurman Thm 3.5.1 — `dim M_k(Γ)` and `dim S_k(Γ)` @@ -31,11 +33,34 @@ in terms of the genus `g` of `X(Γ)`, the numbers `ε₂` and `ε₃` of ellipti and `3`, and the number `ε∞` of cusps — which means computing those four invariants for a given `Γ`, not just knowing the spaces are finite-dimensional. The modular curve here **is** the analytic quotient `Γ\ℍ`, compactified by adjoining the cusps to a compact Riemann -surface — defined directly, with no functor, no representability, and no algebraic moduli -problem. +surface by the Fuchsian-orbifolds roadmap. This roadmap specializes that construction to +congruence subgroups and adds no competing quotient carrier, functor, representability claim, +or algebraic moduli problem. Suggested home: `TauCeti/NumberTheory/ModularForms/`. +The cross-roadmap import graph is a required module split, not merely a proof order: + +```text +TauCeti.Analysis.Complex.ModularForms.LevelOne.JInputs + -> TauCeti.Analysis.Complex.Fuchsian.LevelOne + +TauCeti.AlgebraicTopology.Cellular.FiniteCW + -> TauCeti.Analysis.Complex.RiemannSurface.Degree + |-> TauCeti.Analysis.Complex.Fuchsian.LevelOne + `-> TauCeti.Analysis.Complex.ModularForms.DimensionFormula + +TauCeti.Analysis.Complex.Fuchsian.Compactification + -> TauCeti.Analysis.Complex.ModularForms.DimensionFormula +``` + +`LevelOne.JInputs` contains only the normalized `j`-function, modular invariance, its +`q`-expansion, and the exact elliptic orders; it imports no Fuchsian or dimension-formula module. +The generic `RiemannSurface.Degree` module imports neither ModularForms nor analytic +Riemann--Roch. Only the higher `ModularForms.DimensionFormula` module imports the Fuchsian +compactification and shared degree contracts. This is the literal import discipline for the +implementation. + A large body of this theory — `sorry`-free apart from three flagged gaps (see *Provenance*) — already exists in the AINTLIB `LeanModularForms` project (~250 source files). This roadmap specifies the **mathematics**; the file-by-file @@ -211,12 +236,14 @@ signs; the L-function of a modular form with its **Euler product**, **completed **functional equation**, and **analytic continuation**; the **coefficient field** and the proof that it is a number field — both **already constructed in AINTLIB**, so this one is a migration (§Layer 8, §Provenance); the LMFDB invariants (Satake parameters, Hecke characteristic -polynomials, Galois orbits, labels, …); the **modular curve** `X(Γ)` as the compactified analytic -quotient `Γ\ℍ`, with its cusps, elliptic points, and genus; the **dimension formulas** for -`M_k(Γ)` and `S_k(Γ)` — the valence formula for the upper bounds, the lower bounds by **analytic -Riemann–Roch on `X(Γ)`, built inside Layer 10** (finiteness of `H¹`, Serre duality, -Riemann–Hurwitz — see there); and the level-one **Eichler–Selberg trace -formula** together with the **Hurwitz class numbers** it needs (absent from Mathlib). Apart from +polynomials, Galois orbits, labels, …); the arithmetic specialization of the Fuchsian roadmap's +compactified quotient to congruence subgroups, including explicit cusp and elliptic counts; the +**dimension formulas** for `M_k(Γ)` and `S_k(Γ)` — the valence formula for the upper bounds and +the lower bounds by **analytic Riemann–Roch on `X(Γ)`, built inside Layer 10** (finiteness of +`H¹` and Serre duality). The generic quotient, compactification, local multiplicity, degree, +divisor pullback, degree-one theorem, and Riemann–Hurwitz are consumed from the +Fuchsian-orbifolds roadmap. This roadmap also owns the level-one **Eichler–Selberg trace +formula** and the **Hurwitz class numbers** it needs (absent from Mathlib). Apart from the abstract Hecke ring and the Sturm-bound finiteness now landing in Mathlib (consumed above), none of this is upstream. @@ -230,6 +257,14 @@ expressible in `TauCeti/`, its milestones go into `Suggested.lean` (with `sorry` below sketches signatures; it is illustrative, not required to compile. ### Layer 0: diamond operators and modular forms with character (nebentypus) +- **Isolate the level-one `j` inputs in their own lower module.** + `TauCeti.Analysis.Complex.ModularForms.LevelOne.JInputs` defines the normalized + `j = E₄³/Δ`, proves modular invariance and its `q`-expansion, and proves the exact orders at + `ρ` and `i`. It imports Mathlib's level-one modular-form files only. In particular it imports + neither FuchsianOrbifolds, `RiemannSurface.Degree`, analytic Riemann--Roch, nor + `ModularForms.DimensionFormula`. The Fuchsian level-one application is the sole geometric + consumer of these declarations; later ModularForms layers consume the resulting geometric + contracts in the other direction. - **Diamond operators first — from the slash action alone.** `Γ₁(N) ⊴ Γ₀(N)` with `Γ₀(N)/Γ₁(N) ≅ (ℤ/N)ˣ` via the lower-right entry, so slashing by (any lift of) `d ∈ (ZMod N)ˣ` is a well-defined `ℂ`-linear endomorphism of `M_k(Γ₁(N))` and of `S_k(Γ₁(N))`: the **diamond @@ -987,9 +1022,19 @@ Each is a named definition with its basic API, mostly short once Layers 8 and 8G - **Bad primes** (#54): `badPrimes f = N.primeFactors`. ### Layer 10: the modular curve `Γ\ℍ` and the dimension formulas -The modular curve here is the **analytic quotient `Γ\ℍ`**, compactified to a compact Riemann -surface `X(Γ) = Γ\ℍ*` by adjoining the cusps `Γ\ℙ¹(ℚ)` — defined directly, with **no functor, no -representability, no moduli problem**. +The Fuchsian-orbifolds roadmap constructs the **analytic quotient `Γ\ℍ`** and compactifies it to +a compact Riemann surface by adjoining cusp orbits. This layer specializes that construction to +congruence subgroups, identifies the cusps with `Γ\ℙ¹(ℚ)`, and builds the modular and +cohomological inputs for dimension formulas. It introduces no second quotient carrier or moduli +problem. +The higher implementation module is +`TauCeti.Analysis.Complex.ModularForms.DimensionFormula`. It imports the independent +`TauCeti.Analysis.Complex.RiemannSurface.Degree` module and the Fuchsian compactification +application modules, with literal checks for `RiemannSurface.genus`, +`RiemannSurface.localMultiplicity`, `RiemannSurface.degree`, `RiemannSurface.degree_comp`, +`RiemannSurface.divisor_pullback`, `RiemannSurface.biholomorph_of_degree_eq_one`, and +`RiemannSurface.riemannHurwitz`. It does not import `ModularForms.LevelOne.JInputs` through a +Fuchsian module: that lower module points only toward `Fuchsian.LevelOne` as displayed above. - **The Sturm bound and finite-dimensionality — consume level one, build the general case.** A nonzero `f ∈ M_k(Γ)` has `q`-order at `∞` at most `k·[SL₂(ℤ):Γ]/12`; consequently `M_k(Γ)` @@ -1006,39 +1051,26 @@ representability, no moduli problem**. the LMFDB layer's equality checks (Layer 9) become finite computations. #### 10A — the analytic modular curve -- **The analytic theory of cusps and compactification.** Build `X(Γ) = Γ\ℍ*` as a compact - Riemann surface — with the point-set work stated as milestones, not assumed: the effective - `PSL₂` action, proper discontinuity (Mathlib's `ProperlyDiscontinuous.lean`), Hausdorffness - of the quotient including the separation of cusp neighborhoods, second countability, - compactness after adjoining the finitely many cusps, and chart compatibility. The charts: at - ordinary points the quotient chart; at an elliptic point, `w ↦ w^{e_P}` in the - stabilizer-linearizing coordinate `w = (τ − τ₀)/(τ − τ̄₀)` (not in `τ` itself); at the cusps - the `q`-disc chart; the **cusp count** `ε∞ = #Γ\ℙ¹(ℚ)` - and the **elliptic-point counts** `ε₂, ε₃` (periods `2, 3`, counted in the `PSL₂(ℤ)`-image where - the elliptic stabilizers are cyclic of order `2, 3`); and the **genus** `g` of `X(Γ)` — defined - **analytically**, `g := finrank ℂ H¹(X(Γ), 𝒪)` — a definition available only *after* the - finiteness theorem below, so the order is `H¹`, finiteness, then `g` (equivalently - `dim H⁰(Ω¹)`, by the duality below), - and computed by Riemann–Hurwitz over `X(1)` in the Riemann–Roch chain below, replacing - Diamond–Shurman's topological Euler-characteristic route (§3.1): no triangulations enter the - roadmap. These - counts and the genus are the inputs to the dimension formulas; building them is part of this - layer, not assumed. +- **The arithmetic specialization of the analytic curve.** Consume `X(Γ)` and its ordinary, + elliptic, and cusp charts from the Fuchsian-orbifolds roadmap. For congruence subgroups, prove + cofiniteness, identify its cusp-orbit subtype with `Γ\ℙ¹(ℚ)`, and compute the **cusp count** + `ε∞` and **elliptic-point counts** `ε₂, ε₃` (periods `2, 3`, counted in the effective + `PSL₂(ℤ)`-image). Define the cohomological genus only after the `H¹`-finiteness theorem + below, then identify it with the generic genus used by the shared Riemann–Hurwitz theorem. These + arithmetic counts and this comparison, not a second compactification, are built in this layer. - **The finite map to level one.** `X(Γ) → X(1)` as a finite holomorphic map of compact - Riemann surfaces, with the fiber-counting identities (`Σ e_x = d` over every fiber, the - stabilizer indices at elliptic orbits, the cusp-width sum `Σ h_s = d`) as named lemmas — - the inputs Riemann–Hurwitz consumes in 10B(vi). ⚠ This construction is **self-contained - relative to 10B's compact-surface API**: it consumes no Schwarz reflection, no boundary - correspondence, and no universal covers. + Riemann surfaces is the finite-index map supplied by the Fuchsian-orbifolds roadmap. Prove the + arithmetic identification of its degree with `[PSL₂(ℤ) : Γ̄]`; consume the generic fibre + sum, elliptic stabilizer-index formula, cusp-width sum, multiplicativity, and Riemann–Hurwitz + there. + No Schwarz reflection, boundary correspondence, or universal-cover argument is duplicated. #### 10B — compact-Riemann-surface cohomology -- **The Riemann–Roch input — built here, not assumed.** The lower bounds need analytic - Riemann–Roch on `X(Γ)`, and no compact-Riemann-surfaces roadmap exists to cite; so the - minimal chain is part of this layer (in the spirit of the PR #36 review's advice — analytic - curve, no GAGA — with Riemann–Roch actually supplied; Forster, *Lectures on Riemann - Surfaces*, GTM 81, §§14–17, is the reference for exactly this route). The milestones, in - order: +- **The Riemann–Roch input — built here, not assumed.** The Fuchsian-orbifolds roadmap supplies + the compact surface and the generic degree, divisor-pullback, degree-one, and Riemann–Hurwitz + APIs, but not cohomology or Riemann–Roch. The minimal cohomological chain remains in this layer + (analytic curve, no GAGA; Forster, *Lectures on Riemann Surfaces*, GTM 81, §§14–17). In order: (i) the structure sheaf and the sheaves `𝒪_D` of a divisor on a compact Riemann surface, Čech `H⁰` and `H¹` (refinement-independent via Forster's degree-one Leray theorem: a cover by `𝒪`-acyclic opens computes `H¹`, with acyclicity of discs from the **local `∂̄`-lemma** @@ -1060,22 +1092,19 @@ representability, no moduli problem**. pairing (Forster §17): `H¹(𝒪_D)^* ≅ H⁰(Ω_{−D})`, whence `ℓ(D) − ℓ(K−D) = deg D + 1 − g`, `dim H⁰(Ω¹) = g`, `deg K = 2g − 2`, and the vanishing `H¹(𝒪_D) = 0` for `deg D > 2g − 2` that the exact formulas below actually use. - (v) **Riemann–Hurwitz** for a finite holomorphic map of compact Riemann surfaces, from the - local normal form and the canonical-divisor pullback — with the fiber-counting identities as - explicit inputs: `Σ_{x ↦ y} e_x = d` for every `y`, the stabilizer-index formula at the - elliptic orbits, and the cusp-width sum `Σ_s h_s = d`. - (vi) `X(1) ≅ ℙ¹` via the `j`-function, as an explicit lemma chain: `j` descends through the - elliptic charts (the orders of `j` and `j − 1728` at `ρ` and `i` are what make the descended - map regular there), one simple pole at the cusp and no others, the degree of a map to `ℙ¹` - equals the degree of its pole divisor, nonconstant maps from a compact surface are proper, - open, and surjective, and degree one forces a biholomorphism **via the local normal form** - (a continuous bijection gives only a homeomorphism). Then the **genus of `X(Γ)`** falls out - of (v) applied to `X(Γ) → X(1)`, with ramification from the stabilizer indices at the - elliptic orbits and the cusp widths: - `g = 1 + d/12 − ε₂/4 − ε₃/3 − ε∞/2`, `d = [PSL₂(ℤ) : Γ̄]` — ⚠ the `PSL₂`-index, not - `[SL₂(ℤ) : Γ]`. `dim S₂(Γ) = g` is then `S₂(Γ) ≅ H⁰(X(Γ), Ω¹)` plus (iv). - A fuller compact-Riemann-surfaces roadmap (Abel–Jacobi, uniformization, …) remains - desirable later and would absorb and extend (i)–(v); nothing here waits for it. + (v) identify `g := dim H¹(X, 𝒪)` with `RiemannSurface.genus X`; then consume + `RiemannSurface.riemannHurwitz` and the Fuchsian finite-index local-multiplicity formulas. + (vi) Consume the named `X(1) ≃ ℙ¹` and `RiemannSurface.genus X(1) = 0` theorems from + `Fuchsian.LevelOne`. The normalized `j = E₄³/Δ`, the identity + `j − 1728 = E₆²/Δ`, modular invariance, q-expansion, and exact orders at `ρ` and `i` were + already supplied by the independent Layer-0 `ModularForms.LevelOne.JInputs` module. They are + not redefined in this higher module. Fuchsian-orbifolds owns descent through its quotient, + extension over its cusp, the local multiplicities, the degree-one calculation, and the final + biholomorphism. + Applying the shared Riemann–Hurwitz theorem to `X(Γ) → X(1)` with the Fuchsian elliptic and + cusp local-multiplicity formulas gives + `g = 1 + d/12 − ε₂/4 − ε₃/3 − ε∞/2`, where `d = [PSL₂(ℤ) : Γ̄]`, not + `[SL₂(ℤ) : Γ]`; then `S₂(Γ) ≅ H⁰(X(Γ), Ω¹)` and (iv) give `dim S₂(Γ) = g`. #### 10C — modular forms as section spaces, and the dimension formulas - **The automorphy sheaf, constructed and not gestured at.** The weight-`k` transformation @@ -1084,9 +1113,7 @@ representability, no moduli problem**. at an elliptic point the invariant sections in the linearizing coordinate, at a (regular or irregular) cusp the sections in the width parameter with the errata order convention — and the local transition-function computation at each chart overlap is its own milestone, since - the `⌊·⌋`-corrections of the divisor are precisely its output. The `j`-function enters 10C - concretely: `j = E₄³/Δ`, `j − 1728 = E₆²/Δ`, with the orders of `j` and `j − 1728` at `ρ` - and `i` read off these identities — the inputs 10B(vi) needs. + the `⌊·⌋`-corrections of the divisor are precisely its output. - **The dimension formulas** (Diamond–Shurman Thm 3.5.1 for even weight, Thm 3.6.1 for odd) — honest about their two halves. The Layer-1 valence formula with the `ε₂, ε₃, ε∞` counts and the genus `g` above yields the @@ -1155,8 +1182,8 @@ representability, no moduli problem**. `dim S_2(Γ₀(23)) = 2`, `dim S_2(Γ₀(2)) = 0`, `dim M_2(Γ₀(11)) = 2`, and the non-`Γ₀` instance `dim S_2(Γ₁(13)) = 2`. The general even-weight formula above is the layer's headline target; it is stated here in the README (its inputs are - the `ε₂, ε₃, ε∞, g` of `X(Γ)` from this same layer **plus the Riemann–Roch chain above, built in - this same layer**; the concrete instances below consume that same general theorem — their + the arithmetic counts on the Fuchsian roadmap's `X(Γ)`, the cohomological-genus comparison, + and the Riemann–Roch chain built here; the concrete instances consume that theorem — their role is acceptance, not independent grounding), and is **not** seeded as a free-parameter `example` in `Suggested.lean`, since with `g, ε₂, ε₃, ε∞` as free variables it is @@ -1509,8 +1536,9 @@ table; "three" counts literal source `sorry`s, not every unfinished target of th - **Dimensions / curve (L10):** `Modularforms/DimensionFormulas.lean` with `Modularforms/DimGenCongLevels/*` (`dim_gen_cong_levels` — general-level finite-dimensionality by the norm-map route, the content being upstreamed as the Mathlib Sturm - stack #39000; `cuspform_weight_lt_12_zero`); the general-level analytic - cusp/compactification theory and the general dimension formula are **new** here. + stack #39000; `cuspform_weight_lt_12_zero`). The generic quotient, cusp compactification, and + degree theory are supplied by the Fuchsian-orbifolds roadmap; the congruence-subgroup arithmetic, + cohomological Riemann–Roch, automorphy sheaves, and general dimension formula are **new** here. - **Trace formula (L11):** no AINTLIB source — entirely **new**; route B's substrate is the `ModularSymbols` subtree above. diff --git a/TauCetiRoadmap/ModularForms/Suggested.lean b/TauCetiRoadmap/ModularForms/Suggested.lean index 0313cb63..5372a2b6 100644 --- a/TauCetiRoadmap/ModularForms/Suggested.lean +++ b/TauCetiRoadmap/ModularForms/Suggested.lean @@ -1,4 +1,5 @@ import Mathlib +import TauCetiRoadmap.FuchsianOrbifolds.Suggested /-! # Modular forms — Hecke theory, newforms, and L-functions: target signatures @@ -18,64 +19,87 @@ forms, no eigenform/newform theory, no L-function of a modular form, no valence **general-level dimension formulas**. We build the classical arithmetic theory in `TauCeti/NumberTheory/ModularForms/`. -⚠ Signature seeding beyond the dimension instances — the `EigenformAwayFromLevel`/`Eigenform` -split, the newform–newform cross-level strong multiplicity one, the good- and bad-prime `Tₚ` -coefficient formulas, the exact fixed-`χ` oldspace, period-map injectivity and equivariance, -`CharacterField χ ≤ CoefficientField f` and Galois stability (Layer 8G), the headline -Riemann–Roch theorem (Layer 10B), and the level-one trace formula (Layer 11) — requires the -skeleton types those layers introduce; freezing names here against placeholder structures would -not check interface coherence. Those signatures are added to this file as each layer's types -land; until then the README's layer sections carry the intended statements. +The README pins the `EigenformAwayFromLevel`/`Eigenform` split, cross-level strong multiplicity +one, the prime coefficient formulas, the fixed-`χ` oldspace, period-map injectivity and +equivariance, coefficient-field results, analytic Riemann–Roch, and the trace formula. +This file seeds interfaces that are expressible using established carriers. For milestones whose +carriers are themselves roadmap targets, the README remains definitive; placeholder structures +would not check interface coherence. + +The signatures below therefore represent concrete acceptance interfaces, not an exhaustive API. This file seeds the **Layer 10 dimension-formula** milestones at levels other than one (Diamond–Shurman Thm 3.5.1; the same numbers are tabulated in Stein, *Modular Forms: A Computational Approach*). The general even-weight formula -`dim M_k(Γ) = (k-1)(g-1) + ⌊k/4⌋ε₂ + ⌊k/3⌋ε₃ + (k/2)ε∞` (and `(k/2-1)ε∞` for `S_k`, even `k ≥ 4`) -is stated in the README. Its inputs are the genus `g` of the compact Riemann surface -`X(Γ) = Γ\ℍ*` together with the counts `ε₂, ε₃` of elliptic points of period 2, 3 and the number -of cusps `ε∞` — all built analytically in Layer 10 — **plus analytic Riemann–Roch on `X(Γ)`, -built inside Layer 10 itself** (sublayers 10A–10C: the analytic curve, the compact-Riemann-surface -cohomology with the `H¹`-finiteness theorem, residue Serre duality and Riemann–Hurwitz, and the -automorphy sheaves; nothing is gated on any future roadmap — the valence formula supplies the -upper bounds; see Layer 10 in `README.md`). The concrete instances below are **acceptance -criteria consuming that general theorem**: they are not independently grounded, and their role -is to exercise the interfaces at both `Γ₀` and `Γ₁` levels once the theorem lands. (The -level-`11` eta quotient and the weight-`2` Eisenstein series of the worked examples witness -*nonvanishing* — one explicit cusp form, one explicit Eisenstein series — not these dimension -counts.) We do **not** seed that formula as -a free-parameter `example` here: with `g, ε₂, ε₃, ε∞` as free variables it would be *false* for the -wrong data (it is a theorem only when they are the genuine invariants of `X(Γ)`). Instead we seed -concrete, verifiable instances whose invariants are known constants — centred on -`dim S_2(Γ) = genus X(Γ)`, at both `Γ₀` and `Γ₁` levels. They use the `SL(2,ℤ) → GL(2,ℝ)` coercion -(`mapGL`), so `ModularForm (↑(Gamma0 N)) k` and `CuspForm (↑(Gamma1 N)) k` elaborate; this is the -general-level counterpart of Mathlib's level-one `ModularForm.dimension_level_one`. +`dim M_k(Γ) = (k-1)(g-1) + ⌊k/4⌋ε₂ + ⌊k/3⌋ε₃ + (k/2)ε∞` +(and `(k/2-1)ε∞` for `S_k`, even `k ≥ 4`) is stated in the README. Its inputs are the +genus `g` of the compact Riemann surface `X(Γ) = Γ\ℍ*`, its degree/Riemann–Hurwitz API, +and its cusp and elliptic local data, all supplied by the Fuchsian-orbifolds roadmap. +Layer 10 specializes those data to congruence subgroups and builds analytic Riemann–Roch +on `X(Γ)`: the `H¹`-finiteness theorem, residue Serre duality, the comparison of +cohomological and generic genus, and the automorphy sheaves. The valence formula supplies +the upper bounds; the local Riemann–Roch chain supplies the lower bounds. +The concrete instances below are acceptance criteria consuming that general theorem; +they are not independently grounded. Their role is to exercise the interfaces at both +`Γ₀` and `Γ₁` levels and verify the general theorem. The level-`11` eta quotient and the +weight-`2` Eisenstein series of the worked examples witness nonvanishing—one explicit cusp +form and one explicit Eisenstein series—not these dimension counts. +We do **not** seed the formula as a free-parameter `example`: with `g, ε₂, ε₃, ε∞` as free +variables it would be false for the wrong data. Instead, the file seeds concrete, +verifiable instances whose invariants are known constants, centred on +`dim S_2(Γ) = genus X(Γ)` at both `Γ₀` and `Γ₁` levels. They use the +`SL(2,ℤ) → GL(2,ℝ)` coercion (`mapGL`), so `ModularForm (↑(Gamma0 N)) k` and +`CuspForm (↑(Gamma1 N)) k` elaborate. This is the general-level counterpart of +Mathlib's level-one `ModularForm.dimension_level_one`. ## Provenance (migrate and clean from AINTLIB `LeanModularForms`) Migrated from the AINTLIB `LeanModularForms` project ([github.com/CBirkbeck/AINTLIB](https://github.com/CBirkbeck/AINTLIB)); the per-layer file map is in -`README.md`'s *Provenance* section. General-level **finite-dimensionality** is AINTLIB's -`dim_gen_cong_levels` (`Modularforms/DimGenCongLevels/*`), now heading into Mathlib as the -finite-index **Sturm bound** stack — mathlib4#39000 with #39083/#39086/#39087/#39088, on top of -the merged level-one #38993 — whose `Module.Finite ℂ (ModularForm 𝒢 k)` instance is the substrate -these `finrank` instances sit on; the general-level *formula* via the analytic theory of `Γ\ℍ*` -(Layer 10) is **new**. The Main Lemma is proved in AINTLIB; the open `sorry`s to discharge -elsewhere are the weight-1 Hecke-stable lattice `exists_HeckeStableLattice_one` (closed by -sublayer 8W), the Eichler–Shimura Stokes step `interior_edges_cancel_sum` (Layer 8; the Bol -route avoids it), and the bad-prime newspace stability -`peterssonInner_aggregate_eq_zero_of_new_old` (Layer 3, route pinned). The Galois-stability -sublayer 8G and Layers 10–11 have no AINTLIB counterpart and are new formalization. The targets discharge -LeanBridge "def-wanted" issues #13, #18, #19, #30–#35, #37, #38, #42, #54, #55 (the geometric -specs #27, #36, #39–#41, #68–#70 are out of scope here). +`README.md`'s *Provenance* section. AINTLIB supplies general-level finite-dimensionality as +`dim_gen_cong_levels` (`Modularforms/DimGenCongLevels/*`). The corresponding Mathlib design is +recorded in #39000, #39083, #39086, #39087, and #39088, on top of the merged level-one result +#38993. Its `Module.Finite ℂ (ModularForm 𝒢 k)` instance supports these `finrank` instances. +The Fuchsian-orbifolds roadmap supplies the analytic quotient, compactification, and degree +substrate; Layer 10 owns the congruence-subgroup arithmetic, Riemann–Roch/automorphy-sheaf +chain, and resulting general formula. AINTLIB proves the Main Lemma. This roadmap supplies +the weight-1 Hecke-stable lattice `exists_HeckeStableLattice_one` and the Eichler–Shimura +Stokes theorem `interior_edges_cancel_sum`; its bad-prime newspace-stability target is +`peterssonInner_aggregate_eq_zero_of_new_old`. +The Galois-stability sublayer 8G and Layers 10–11 have no AINTLIB counterpart. +The targets discharge LeanBridge "def-wanted" issues #13, #18, #19, #30–#35, #37, #38, +#42, #54, and #55. The geometric specifications #27, #36, #39–#41, and #68–#70 are out +of scope here. -/ namespace TauCetiRoadmap.ModularForms open CongruenceSubgroup +/-! ## Cross-roadmap import checks + +These checks stand in the higher target module +`TauCeti.Analysis.Complex.ModularForms.DimensionFormula`. That module imports the independent +`TauCeti.Analysis.Complex.RiemannSurface.Degree` and Fuchsian compactification modules. The lower +target module `TauCeti.Analysis.Complex.ModularForms.LevelOne.JInputs`, which supplies normalized +`j` data to `TauCeti.Analysis.Complex.Fuchsian.LevelOne`, contains none of these imports. Keeping +the checks here rather than alongside the level-one inputs makes the roadmap dependency acyclic. +-/ + +#check TauCetiRoadmap.FuchsianOrbifolds.CompactifiedQuotient +#check TauCetiRoadmap.FuchsianOrbifolds.compactifiedChartedSpace +#check RiemannSurface.FiniteHolomorphicMap +#check RiemannSurface.genus +#check RiemannSurface.localMultiplicity +#check RiemannSurface.degree +#check RiemannSurface.degree_comp +#check RiemannSurface.divisor_pullback +#check RiemannSurface.biholomorph_of_degree_eq_one +#check RiemannSurface.riemannHurwitz + /-- **Weight-two cusp forms ↔ genus, level 11** (Diamond–Shurman Thm 3.5.1, `k = 2`): -`dim_ℂ S_2(Γ₀(11)) = 1`. The genus of `X₀(11)` is `1`, and `S_2(Γ)` is the space of holomorphic -differentials on `X(Γ)`, so its dimension is the genus — the *analytic* genus of the compact +`dim_ℂ S_2(Γ₀(11)) = 1`. The genus of `X₀(11)` is `1`, and `S_2(Γ)` is the space of +holomorphic differentials on `X(Γ)`, so its dimension is the *analytic* genus of the compact Riemann surface throughout; no identification with the Jacobian Challenge's algebraic `H¹(X, 𝒪_X)` genus is claimed or consumed here. (`X₀(11)` is the elliptic curve `11a`.) -/ example : Module.finrank ℂ (CuspForm (Gamma0 11 : Subgroup (GL (Fin 2) ℝ)) 2) = 1 := @@ -87,20 +111,24 @@ example : Module.finrank ℂ (CuspForm (Gamma0 11 : Subgroup (GL (Fin 2) ℝ)) 2 example : Module.finrank ℂ (CuspForm (Gamma0 23 : Subgroup (GL (Fin 2) ℝ)) 2) = 2 := sorry -/-- **A genus-zero level** (Diamond–Shurman Thm 3.5.1, `k = 2`): `dim_ℂ S_2(Γ₀(2)) = 0`, since +/-- **A genus-zero level** (Diamond–Shurman Thm 3.5.1, `k = 2`): +`dim_ℂ S_2(Γ₀(2)) = 0`, since `X₀(2)` has genus `0`, so there are no weight-two cusp forms. -/ example : Module.finrank ℂ (CuspForm (Gamma0 2 : Subgroup (GL (Fin 2) ℝ)) 2) = 0 := sorry -/-- **Holomorphic forms add the Eisenstein part, level 11** (Diamond–Shurman Thm 3.5.1, `k = 2`): -`dim_ℂ M_2(Γ₀(11)) = 2` — the genus-one cusp form plus the one-dimensional weight-two Eisenstein +/-- **Holomorphic forms add the Eisenstein part, level 11** +(Diamond–Shurman Thm 3.5.1, `k = 2`): +`dim_ℂ M_2(Γ₀(11)) = 2` — the genus-one cusp form plus the one-dimensional +weight-two Eisenstein space (`ε∞ − 1 = 1`), i.e. `dim M_2 = g + ε∞ − 1 = 2`. -/ example : Module.finrank ℂ (ModularForm (Gamma0 11 : Subgroup (GL (Fin 2) ℝ)) 2) = 2 := sorry -/-- **A non-`Γ₀` level: weight-two cusp forms at level `Γ₁(13)`** (Diamond–Shurman Thm 3.5.1, -`k = 2`): `dim_ℂ S_2(Γ₁(13)) = 2`, since `X₁(13)` has genus `2`. A sharp contrast with `Γ₀`: at -level 13, `X₀(13)` has genus `0`, so `dim S_2(Γ₀(13)) = 0`, whereas `S_2(Γ₁(13)) = ⊕_χ S_2(13, χ)` +/-- **A non-`Γ₀` level: weight-two cusp forms at level `Γ₁(13)`** +(Diamond–Shurman Thm 3.5.1, `k = 2`): `dim_ℂ S_2(Γ₁(13)) = 2`, since `X₁(13)` has +genus `2`. A sharp contrast with `Γ₀`: at level 13, `X₀(13)` has genus `0`, so +`dim S_2(Γ₀(13)) = 0`, whereas `S_2(Γ₁(13)) = ⊕_χ S_2(13, χ)` collects every nebentypus and has dimension `2`. Exercises the `Γ₁`-level coercion (`Gamma1`, the same `Subgroup SL(2, ℤ)` type as `Gamma0`). -/ example : Module.finrank ℂ (CuspForm (Gamma1 13 : Subgroup (GL (Fin 2) ℝ)) 2) = 2 :=