Divisors of finite-index maps of Fuchsian quotients

A finite-index inclusion of discrete projective subgroups induces a finite holomorphic map of compactified quotients. This file applies the generic divisor pullback and ramification-divisor constructions to that bundled map. Pullback weights at interior points are the indices of elliptic stabilizers; at cusps they are the indices of boundary stabilizers, or, equivalently, the ratios of widths in compatible normalized cusp data.

When the source compactification is compact, the ramification divisor has coefficient e - 1 at each point. Its total degree splits into the interior and cusp contributions. Compactness is an explicit hypothesis here: neither finite index nor the construction of the compactified carrier alone supplies it.

The constructions use TauCeti.RiemannSurface.divisorPullback and TauCeti.RiemannSurface.ramificationDivisor, without introducing separate Fuchsian divisors. The ramification count follows Diamond and Shurman, A First Course in Modular Forms, §3.1.

theorem TauCeti.Fuchsian.coeff_divisorPullback_ofQuotient {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] (h : Δ ≤ Γ) [Δ.IsFiniteRelIndex Γ] (D : AlgebraicGeometry.WeilDivisor Γ.CompactifiedQuotient) (z : UpperHalfPlane) : ((RiemannSurface.divisorPullback (compactifiedQuotientFiniteHolomorphicMap h)) D).coeff (Subgroup.CompactifiedQuotient.ofQuotient (Quotient.mk'' z)) = ↑(Subgroup.ellipticRamificationIndex h z) * D.coeff (Subgroup.CompactifiedQuotient.ofQuotient (Quotient.mk'' z))

Pullback at an interior orbit multiplies the coefficient by the relative index of the elliptic stabilizers.

theorem TauCeti.Fuchsian.coeff_divisorPullback_ofCusp {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] (h : Δ ≤ Γ) [Δ.IsFiniteRelIndex Γ] (D : AlgebraicGeometry.WeilDivisor Γ.CompactifiedQuotient) (c : ↥Δ.cuspPoints) : ((RiemannSurface.divisorPullback (compactifiedQuotientFiniteHolomorphicMap h)) D).coeff (Subgroup.CompactifiedQuotient.ofCusp (Subgroup.cuspOrbitMk c)) = ↑((Δ.subgroupOf Γ).relIndex (MulAction.stabilizer ↥Γ ↑c)) * D.coeff (Subgroup.CompactifiedQuotient.ofCusp (Subgroup.cuspOrbitMap h (Subgroup.cuspOrbitMk c)))

Pullback at a cusp multiplies the coefficient by the relative index of its boundary stabilizers. This formula requires no choice of scaling or generator.

theorem TauCeti.Fuchsian.coeff_divisorPullback_ofCusp_eq_widthIndex {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] (h : Δ ≤ Γ) [Δ.IsFiniteRelIndex Γ] (A : AlgebraicGeometry.WeilDivisor Γ.CompactifiedQuotient) (D : Δ.CuspDatum) (E : Γ.CuspDatum) (hσ : D.scaling = E.scaling) : ((RiemannSurface.divisorPullback (compactifiedQuotientFiniteHolomorphicMap h)) A).coeff (Subgroup.CompactifiedQuotient.ofCusp D.cuspOrbit) = ↑(Subgroup.CuspDatum.widthIndex h D E ⋯ hσ) * A.coeff (Subgroup.CompactifiedQuotient.ofCusp E.cuspOrbit)

With compatible normalized cusp data, pullback multiplies the coefficient by the positive cusp-width index.

theorem TauCeti.Fuchsian.coeff_ramificationDivisor_ofQuotient {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] (h : Δ ≤ Γ) [Δ.IsFiniteRelIndex Γ] [hcompact : CompactSpace Δ.CompactifiedQuotient] (z : UpperHalfPlane) : (RiemannSurface.ramificationDivisor (compactifiedQuotientFiniteHolomorphicMap h)).coeff (Subgroup.CompactifiedQuotient.ofQuotient (Quotient.mk'' z)) = ↑(Subgroup.ellipticRamificationIndex h z) - 1

The ramification coefficient at an interior orbit is the elliptic stabilizer index minus one. In particular it vanishes at an unramified interior orbit.

theorem TauCeti.Fuchsian.coeff_ramificationDivisor_ofCusp {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] (h : Δ ≤ Γ) [Δ.IsFiniteRelIndex Γ] [hcompact : CompactSpace Δ.CompactifiedQuotient] (c : ↥Δ.cuspPoints) : (RiemannSurface.ramificationDivisor (compactifiedQuotientFiniteHolomorphicMap h)).coeff (Subgroup.CompactifiedQuotient.ofCusp (Subgroup.cuspOrbitMk c)) = ↑((Δ.subgroupOf Γ).relIndex (MulAction.stabilizer ↥Γ ↑c)) - 1

The ramification coefficient at a cusp is its boundary stabilizer index minus one.

theorem TauCeti.Fuchsian.coeff_ramificationDivisor_ofCusp_eq_widthIndex_sub_one {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] (h : Δ ≤ Γ) [Δ.IsFiniteRelIndex Γ] [hcompact : CompactSpace Δ.CompactifiedQuotient] (D : Δ.CuspDatum) (E : Γ.CuspDatum) (hσ : D.scaling = E.scaling) : (RiemannSurface.ramificationDivisor (compactifiedQuotientFiniteHolomorphicMap h)).coeff (Subgroup.CompactifiedQuotient.ofCusp D.cuspOrbit) = ↑(Subgroup.CuspDatum.widthIndex h D E ⋯ hσ) - 1

With compatible normalized cusp data, the ramification coefficient is the positive cusp-width index minus one.

@[simp]

theorem TauCeti.Fuchsian.ramificationDivisor_apply_ofQuotient_ne_zero_iff {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] (h : Δ ≤ Γ) [Δ.IsFiniteRelIndex Γ] [hcompact : CompactSpace Δ.CompactifiedQuotient] (z : UpperHalfPlane) : (RiemannSurface.ramificationDivisor (compactifiedQuotientFiniteHolomorphicMap h)) (Subgroup.CompactifiedQuotient.ofQuotient (Quotient.mk'' z)) ≠ 0 ↔ 1 < Subgroup.ellipticRamificationIndex h z

The ramification coefficient at an interior point is nonzero exactly when the elliptic stabilizer index is greater than one.

@[simp]

theorem TauCeti.Fuchsian.ramificationDivisor_apply_ofCusp_ne_zero_iff {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] (h : Δ ≤ Γ) [Δ.IsFiniteRelIndex Γ] [hcompact : CompactSpace Δ.CompactifiedQuotient] (c : ↥Δ.cuspPoints) : (RiemannSurface.ramificationDivisor (compactifiedQuotientFiniteHolomorphicMap h)) (Subgroup.CompactifiedQuotient.ofCusp (Subgroup.cuspOrbitMk c)) ≠ 0 ↔ 1 < (Δ.subgroupOf Γ).relIndex (MulAction.stabilizer ↥Γ ↑c)

The ramification coefficient at a cusp is nonzero exactly when its boundary stabilizer index is greater than one.

theorem TauCeti.Fuchsian.ramificationDegree_eq_interior_add_cusps {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] (h : Δ ≤ Γ) [Δ.IsFiniteRelIndex Γ] [hcompact : CompactSpace Δ.CompactifiedQuotient] (z : MulAction.orbitRel.Quotient (↥Δ) UpperHalfPlane → UpperHalfPlane) (hz : ∀ (q : MulAction.orbitRel.Quotient (↥Δ) UpperHalfPlane), Quotient.mk'' (z q) = q) (c : Δ.CuspOrbit → ↥Δ.cuspPoints) (hc : ∀ (C : Δ.CuspOrbit), Subgroup.cuspOrbitMk (c C) = C) : RiemannSurface.ramificationDegree (Subgroup.compactifiedQuotientMap h) = ∑ᶠ (q : MulAction.orbitRel.Quotient (↥Δ) UpperHalfPlane), (Subgroup.ellipticRamificationIndex h (z q) - 1) + ∑ᶠ (C : Δ.CuspOrbit), ((Δ.subgroupOf Γ).relIndex (MulAction.stabilizer ↥Γ ↑(c C)) - 1)

Total ramification splits into the interior contribution and the contribution from adjoined cusps, with weights equal to stabilizer indices minus one. The formula holds for any choice of interior and cusp representatives, and both sums have finite support.