Fibres of compactified quotient maps

For a finite-index inclusion of projective subgroups, the map on compactified quotients has finite fibres. Both the coarse and cusp fibres are covered by the finite set of subgroup cosets. The same argument works for the boundary action even though its stabilizers need not be trivial.

Over an interior point z the fibre is identified with the orbit space of the stabilizer of z in the larger group acting on the subgroup cosets, which counts it exactly whenever it is finite; for an infinite fibre both sides of the cardinality formula are zero by the convention for Nat.card. At a free point the stabilizer action is trivial and the count is the subgroup index; in general stabilizer orbits record exactly which cosets represent the same fibre point.

def Subgroup.orbitFiberEquivCompactifiedFiber {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (h : Δ ≤ Γ) (p : MulAction.orbitRel.Quotient (↥Γ) UpperHalfPlane) : { q : MulAction.orbitRel.Quotient (↥Δ) UpperHalfPlane // Setoid.map_of_le ⋯ q = p } ≃ { y : Δ.CompactifiedQuotient // compactifiedQuotientMap h y = CompactifiedQuotient.ofQuotient p }

Over an interior point, the ordinary orbit fibre is equivalent to the compactified fibre.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Subgroup.orbitFiberEquivCompactifiedFiber_apply {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (h : Δ ≤ Γ) (p : MulAction.orbitRel.Quotient (↥Γ) UpperHalfPlane) (q : { q : MulAction.orbitRel.Quotient (↥Δ) UpperHalfPlane // Setoid.map_of_le ⋯ q = p }) : ↑((orbitFiberEquivCompactifiedFiber h p) q) = CompactifiedQuotient.ofQuotient ↑q

The interior-fibre equivalence inserts an ordinary orbit into the compactification.

noncomputable def Subgroup.stabilizerOrbitRelQuotientEquivCompactifiedFiber {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (h : Δ ≤ Γ) (z : UpperHalfPlane) : MulAction.orbitRel.Quotient (↥(MulAction.stabilizer (↥Γ) z)) (↥Γ ⧸ Δ.subgroupOf Γ) ≃ { y : Δ.CompactifiedQuotient // compactifiedQuotientMap h y = CompactifiedQuotient.ofQuotient (Quotient.mk'' z) }

The fibre of a compactified Fuchsian quotient map over the interior orbit of z is the orbit space of the stabilizer of z acting on the subgroup cosets.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Subgroup.stabilizerOrbitRelQuotientEquivCompactifiedFiber_mk {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (h : Δ ≤ Γ) (z : UpperHalfPlane) (q : ↥Γ ⧸ Δ.subgroupOf Γ) : ↑((stabilizerOrbitRelQuotientEquivCompactifiedFiber h z) (Quotient.mk'' q)) = CompactifiedQuotient.ofQuotient (TauCeti.orbitOfCosetTranslate z q)

The stabilizer-orbit equivalence sends the orbit of a coset to the compactified point represented by the corresponding inverse translate of z.

theorem Subgroup.card_fiber_compactifiedQuotientMap_eq_card_stabilizerOrbitRelQuotient {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (h : Δ ≤ Γ) (z : UpperHalfPlane) : Nat.card { y : Δ.CompactifiedQuotient // compactifiedQuotientMap h y = CompactifiedQuotient.ofQuotient (Quotient.mk'' z) } = Nat.card (MulAction.orbitRel.Quotient (↥(MulAction.stabilizer (↥Γ) z)) (↥Γ ⧸ Δ.subgroupOf Γ))

The cardinality of a compactified interior fibre is the number of stabilizer-orbits on the subgroup coset space. No discreteness or ramification hypothesis is required. In geometric applications satisfying the relevant hypotheses, where z is an elliptic fixed point of a discrete Γ, this counts the ramified fibre without treating the quotient map as a covering there.

theorem Subgroup.finite_fiber_cuspOrbitMap {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (h : Δ ≤ Γ) [Δ.IsFiniteRelIndex Γ] (C : Γ.CuspOrbit) : Finite { D : Δ.CuspOrbit // cuspOrbitMap h D = C }

A finite-index inclusion induces a map with finite fibres on cusp orbits.

theorem Subgroup.finite_fiber_compactifiedQuotientMap {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (h : Δ ≤ Γ) [Δ.IsFiniteRelIndex Γ] (x : Γ.CompactifiedQuotient) : Finite { y : Δ.CompactifiedQuotient // compactifiedQuotientMap h y = x }

Every fibre of the map of compactified quotients for a finite-index inclusion is finite.