Ramification in elliptic charts of Fuchsian quotients

For an inclusion Δ ≤ Γ of subgroups of PSL(2, ℝ), the relative index of their point stabilizers is the local power-map exponent when the stabilizers are finite. This file computes the induced map in the elliptic charts of the coarse quotients.

The local cyclic-disc model follows Farkas--Kra, Riemann Surfaces, Chapter I, §§4--5.

noncomputable def Subgroup.ellipticRamificationIndex {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (_h : Δ ≤ Γ) (z : UpperHalfPlane) : ℕ

The relative index of the smaller point stabilizer in the larger one. For finite stabilizers, this is the exponent of the local power map at the orbit of z.

Equations

• Subgroup.ellipticRamificationIndex _h z = (Subgroup.map Δ.subtype (MulAction.stabilizer (↥Δ) z)).relIndex (Subgroup.map Γ.subtype (MulAction.stabilizer (↥Γ) z))

theorem Subgroup.ellipticRamificationIndex_def {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (h : Δ ≤ Γ) (z : UpperHalfPlane) : ellipticRamificationIndex h z = (map Δ.subtype (MulAction.stabilizer (↥Δ) z)).relIndex (map Γ.subtype (MulAction.stabilizer (↥Γ) z))

The elliptic ramification index is the relative index of the ambient point stabilizers.

theorem Subgroup.ellipticRamificationIndex_smul {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (h : Δ ≤ Γ) (g : ↥Δ) (z : UpperHalfPlane) : ellipticRamificationIndex h (g • z) = ellipticRamificationIndex h z

The relative stabilizer index depends only on the source orbit.

@[simp]

theorem Subgroup.ellipticRamificationIndex_eq_one_iff {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (h : Δ ≤ Γ) (z : UpperHalfPlane) : ellipticRamificationIndex h z = 1 ↔ map Δ.subtype (MulAction.stabilizer (↥Δ) z) = map Γ.subtype (MulAction.stabilizer (↥Γ) z)

Ramification is trivial exactly when the two ambient point stabilizers agree.

@[simp]

theorem Subgroup.ellipticRamificationIndex_eq_one_of_stabilizer_eq_bot {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (h : Δ ≤ Γ) (z : UpperHalfPlane) (hz : MulAction.stabilizer (↥Γ) z = ⊥) : ellipticRamificationIndex h z = 1

The induced map is unramified at a free point of the larger group.

theorem Subgroup.card_stabilizer_mul_ellipticRamificationIndex {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (h : Δ ≤ Γ) (z : UpperHalfPlane) : Nat.card ↥(MulAction.stabilizer (↥Δ) z) * ellipticRamificationIndex h z = Nat.card ↥(MulAction.stabilizer (↥Γ) z)

The Nat.card of the larger point stabilizer equals that of the smaller stabilizer times the relative index. For finite stabilizers, this is an identity of group orders.

theorem Subgroup.ellipticRamificationIndex_eq_card_div {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (h : Δ ≤ Γ) (z : UpperHalfPlane) [Finite ↥(MulAction.stabilizer (↥Γ) z)] : ellipticRamificationIndex h z = Nat.card ↥(MulAction.stabilizer (↥Γ) z) / Nat.card ↥(MulAction.stabilizer (↥Δ) z)

For a finite point stabilizer, the relative index is the quotient of stabilizer orders.

theorem Subgroup.ellipticRamificationIndex_eq_index {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (h : Δ ≤ Γ) (z : UpperHalfPlane) [Finite ↥(MulAction.stabilizer (↥Γ) z)] : ellipticRamificationIndex h z = (stabilizerInclusion h z).range.index

For finite stabilizers, the relative index is the group index of the inclusion map.

theorem Subgroup.ellipticRamificationIndex_pos {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (h : Δ ≤ Γ) (z : UpperHalfPlane) [Finite ↥(MulAction.stabilizer (↥Γ) z)] : 0 < ellipticRamificationIndex h z

The elliptic ramification index is positive.

@[simp]

theorem Subgroup.ellipticRamificationIndex_self (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) (z : UpperHalfPlane) : ellipticRamificationIndex ⋯ z = 1

An identity inclusion has elliptic ramification index one.

theorem Subgroup.ellipticRamificationIndex_tower {Δ Γ Θ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (h : Δ ≤ Γ) (k : Γ ≤ Θ) (z : UpperHalfPlane) : ellipticRamificationIndex h z * ellipticRamificationIndex k z = ellipticRamificationIndex ⋯ z

Elliptic ramification indices multiply in a tower of subgroup inclusions.

theorem Subgroup.stabilizerBallQuotientChart_map_of_le {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (h : Δ ≤ Γ) (z τ : UpperHalfPlane) [Finite ↥(MulAction.stabilizer (↥Γ) z)] {ε : ℝ} (hε : 0 < ε) (hΔ : Topology.IsOpenEmbedding (Δ.stabilizerBallQuotientToQuotient z ε)) (hΓ : Topology.IsOpenEmbedding (Γ.stabilizerBallQuotientToQuotient z ε)) (_hτ : dist τ z < ε) : ↑(stabilizerBallQuotientChart hε hΓ) (Setoid.map_of_le ⋯ ⟦τ⟧) = ↑(stabilizerBallQuotientChart hε hΔ) ⟦τ⟧ ^ ellipticRamificationIndex h z

In elliptic charts centred at z, the map of orbit quotients is the power map whose exponent is the index of the two stabilizers.

theorem Subgroup.stabilizerBallQuotientChart_map_of_le_symm {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (h : Δ ≤ Γ) (z : UpperHalfPlane) [Finite ↥(MulAction.stabilizer (↥Γ) z)] {ε : ℝ} (hε : 0 < ε) (hΔ : Topology.IsOpenEmbedding (Δ.stabilizerBallQuotientToQuotient z ε)) (hΓ : Topology.IsOpenEmbedding (Γ.stabilizerBallQuotientToQuotient z ε)) {u : ℂ} (_hu : u ∈ (stabilizerBallQuotientChart hε hΔ).target) : ↑(stabilizerBallQuotientChart hε hΓ) (Setoid.map_of_le ⋯ (↑(stabilizerBallQuotientChart hε hΔ).symm u)) = u ^ ellipticRamificationIndex h z

On the entire target of the smaller elliptic chart, the coordinate expression of the quotient map is u ↦ u ^ ellipticRamificationIndex h z.

theorem Subgroup.exists_common_elliptic_chart_radius {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (z : UpperHalfPlane) [ProperlyDiscontinuousSMul (↥Δ) UpperHalfPlane] [ProperlyDiscontinuousSMul (↥Γ) UpperHalfPlane] : ∃ (ε : ℝ), 0 < ε ∧ Topology.IsOpenEmbedding (Δ.stabilizerBallQuotientToQuotient z ε) ∧ Topology.IsOpenEmbedding (Γ.stabilizerBallQuotientToQuotient z ε)

Two properly discontinuous actions admit a common positive chart radius at z.

theorem Subgroup.stabilizerBallQuotientChart_map_mk_eq_pow_ellipticRamificationIndex {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (h : Δ ≤ Γ) (z : UpperHalfPlane) [Finite ↥(MulAction.stabilizer (↥Γ) z)] {εΔ εΓ : ℝ} (hεΔ : 0 < εΔ) (hεΓ : 0 < εΓ) (hopenΔ : Topology.IsOpenEmbedding (Δ.stabilizerBallQuotientToQuotient z εΔ)) (hopenΓ : Topology.IsOpenEmbedding (Γ.stabilizerBallQuotientToQuotient z εΓ)) {τ : UpperHalfPlane} (hτΔ : dist τ z < εΔ) (hτΓ : dist τ z < εΓ) : have this := ⋯; ↑(stabilizerBallQuotientChart hεΓ hopenΓ) (Setoid.map_of_le ⋯ ⟦τ⟧) = ↑(stabilizerBallQuotientChart hεΔ hopenΔ) ⟦τ⟧ ^ ellipticRamificationIndex h z

For a representative lying in both chart balls centered at the same point, the map induced by Δ ≤ Γ has chart expression u ↦ u ^ e. The two chart radii may differ.

theorem Subgroup.map_mem_stabilizerBallQuotientChart_source {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (h : Δ ≤ Γ) (z : UpperHalfPlane) [Finite ↥(MulAction.stabilizer (↥Γ) z)] {ε : ℝ} (hε : 0 < ε) (hopenΔ : Topology.IsOpenEmbedding (Δ.stabilizerBallQuotientToQuotient z ε)) (hopenΓ : Topology.IsOpenEmbedding (Γ.stabilizerBallQuotientToQuotient z ε)) {q : MulAction.orbitRel.Quotient (↥Δ) UpperHalfPlane} : have this := ⋯; q ∈ (stabilizerBallQuotientChart hε hopenΔ).source → Setoid.map_of_le ⋯ q ∈ (stabilizerBallQuotientChart hε hopenΓ).source

The map of orbit quotients sends the source of a chart centered at z into the corresponding chart source for the larger group, when both use the same radius.

theorem Subgroup.stabilizerBallQuotientChart_map_eq_pow_ellipticRamificationIndex {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (h : Δ ≤ Γ) (z : UpperHalfPlane) [Finite ↥(MulAction.stabilizer (↥Γ) z)] {ε : ℝ} (hε : 0 < ε) (hopenΔ : Topology.IsOpenEmbedding (Δ.stabilizerBallQuotientToQuotient z ε)) (hopenΓ : Topology.IsOpenEmbedding (Γ.stabilizerBallQuotientToQuotient z ε)) {q : MulAction.orbitRel.Quotient (↥Δ) UpperHalfPlane} : have this := ⋯; q ∈ (stabilizerBallQuotientChart hε hopenΔ).source → ↑(stabilizerBallQuotientChart hε hopenΓ) (Setoid.map_of_le ⋯ q) = ↑(stabilizerBallQuotientChart hε hopenΔ) q ^ ellipticRamificationIndex h z

On the entire source of a common elliptic chart, the quotient map is the power map of degree equal to the elliptic ramification index.