Maps between compactified Fuchsian quotients

An inclusion of discrete subgroups Δ ≤ Γ ≤ PSL(2, ℝ) induces a map from the compactified quotient of Δ to that of Γ. On the coarse quotient it sends the orbit of z to its larger orbit; at a cusp it sends the orbit of a parabolic fixed point to its larger orbit. The map is continuous also at the adjoined cusp points. The construction applies to arbitrary subgroup inclusions; finite index is needed only for subsequent finiteness and ramification results.

Cusp data with the same representative and scaling define the same horodiscs, even when their groups have different primitive cusp widths.

noncomputable def Subgroup.compactifiedQuotientMap {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (h : Δ ≤ Γ) : Δ.CompactifiedQuotient → Γ.CompactifiedQuotient

An inclusion of projective subgroups induces a map on their compactified quotients, agreeing with the ordinary orbit map away from the cusps.

Equations

• Subgroup.compactifiedQuotientMap h (Subgroup.CompactifiedQuotient.ofQuotient p) = Subgroup.CompactifiedQuotient.ofQuotient (Setoid.map_of_le ⋯ p)
• Subgroup.compactifiedQuotientMap h (Subgroup.CompactifiedQuotient.ofCusp C) = Subgroup.CompactifiedQuotient.ofCusp (Subgroup.cuspOrbitMap h C)

@[simp]

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

@[simp]

theorem Subgroup.compactifiedQuotientMap_ofCusp {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (h : Δ ≤ Γ) (C : Δ.CuspOrbit) : compactifiedQuotientMap h (CompactifiedQuotient.ofCusp C) = CompactifiedQuotient.ofCusp (cuspOrbitMap h C)

@[simp]

theorem Subgroup.compactifiedQuotientMap_self {Δ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} : compactifiedQuotientMap ⋯ = id

The compactified quotient map for a reflexive inclusion is the identity.

@[simp]

theorem Subgroup.compactifiedQuotientMap_compactifiedQuotientMap {Δ Γ Θ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (h : Δ ≤ Γ) (k : Γ ≤ Θ) (x : Δ.CompactifiedQuotient) : compactifiedQuotientMap k (compactifiedQuotientMap h x) = compactifiedQuotientMap ⋯ x

Two subgroup inclusions induce the map for their composite on each compactified point.

theorem Subgroup.compactifiedQuotientMap_comp {Δ Γ Θ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (h : Δ ≤ Γ) (k : Γ ≤ Θ) : compactifiedQuotientMap k ∘ compactifiedQuotientMap h = compactifiedQuotientMap ⋯

Compactified quotient maps compose along a tower of subgroup inclusions.

theorem Subgroup.compactifiedQuotientMap_comp_ofQuotient {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (h : Δ ≤ Γ) : compactifiedQuotientMap h ∘ CompactifiedQuotient.ofQuotient = CompactifiedQuotient.ofQuotient ∘ Setoid.map_of_le ⋯

The compactified map commutes with the coarse-quotient constructors.

theorem Subgroup.CompactifiedQuotient.image_compactifiedQuotientMap_cuspNhd_subset_cuspNhd {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (h : Δ ≤ Γ) (D : Δ.CuspDatum) (E : Γ.CuspDatum) (hσ : E.scaling = D.scaling) (A : ℝ) : compactifiedQuotientMap h '' cuspNhd D A ⊆ cuspNhd E A

The map induced by Δ ≤ Γ sends a cusp neighbourhood into the neighbourhood at the same boundary point and height, when the cusp data use the same scaling.

theorem Subgroup.CompactifiedQuotient.continuousAt_compactifiedQuotientMap_ofCusp {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] (h : Δ ≤ Γ) (D : Δ.CuspDatum) : ContinuousAt (compactifiedQuotientMap h) (ofCusp D.cuspOrbit)

The map of compactified quotients is continuous at each cusp point.

theorem Subgroup.CompactifiedQuotient.continuous_compactifiedQuotientMap {Δ Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [DiscreteTopology ↥Γ] (h : Δ ≤ Γ) : Continuous (compactifiedQuotientMap h)

The compactified orbit map induced by an inclusion of discrete projective subgroups is continuous, including at the added cusp points.