Unramified interior fibres of Fuchsian quotient maps

When the stabilizer acts trivially on the subgroup cosets, the fibre of an induced map of compactified quotients has exactly the subgroup index many points. In particular, this holds at points with trivial stabilizer in the larger group. Such fibres give the unramified count used in the global degree formula. For an infinite index, both sides of the cardinality theorem are zero by Mathlib's Nat.card and subgroup-index conventions. The group-theoretic coset equivalence is in TauCeti.GroupTheory.DoubleCoset.Fiber.

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

Over an interior orbit, the compactified fibre has cardinality [Γ : Δ] when the stabilizer acts trivially on the cosets of Δ in Γ.

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

The fibre of the compactified quotient map over a free interior point has cardinality [Γ : Δ].