Local linearizing coordinates at a point of finite stabilizer

Let Γ ≤ PSL(2, ℝ) and let z be a point of the upper half-plane whose stabilizer has finite order m. A local linearizing coordinate at z is a biholomorphic coordinate on the invariant hyperbolic disc of positive radius ε about z which sends z to the centre and in which the stabilizer of z acts by rotations: it is a biholomorphic reparametrization ψ of the Euclidean disc of radius tanh (ε / 2), the image of the invariant disc in the disc coordinate centred at z, fixing 0 and intertwining the rotation action of the m-th roots of unity on the disc with the rotation action on its image (Subgroup.LinearizingCoordinate). The stabilizer of z acts on the invariant hyperbolic disc itself, and the disc coordinate centred at z turns that action into the rotation action of the m-th roots of unity, so the rotation by which a stabilizer element acts in a local linearizing coordinate is Subgroup.stabilizerRotation in every one of them (Subgroup.LinearizingCoordinate.coordinate_smul).

A local linearizing coordinate is genuinely local: its image is its own open set, the target of the partial equivalence Subgroup.LinearizingCoordinate.toEquiv of the reparametrization, which is not required to be the whole unit disc, and the equivariant biholomorphic reparametrizations of a disc are not all rotations. In particular w ↦ w (1 + a w ^ m) is such a reparametrization for small a, and the transition between two local linearizing coordinates is in general a non-trivial automorphism of the quotient.

What does not depend on the choice of the local linearizing coordinate is the local complex structure defined by the local quotient coordinate Subgroup.LinearizingCoordinate.quotientCoordinate, the m-th power of the coordinate: the quotient coordinates of two local linearizing coordinates are related by a biholomorphic transition, not by equality. The local quotient coordinate is constant on the orbits of the stabilizer (Subgroup.LinearizingCoordinate.quotientCoordinate_smul), its level sets are exactly those orbits (Subgroup.LinearizingCoordinate.quotientCoordinate_eq_iff), so it is a coordinate on the quotient of the invariant disc by the stabilizer of z; and the quotient coordinates of two local linearizing coordinates are related by a map that is holomorphic with holomorphic inverse between the open sets of quotient-coordinate values — a biholomorphic transition (Subgroup.LinearizingCoordinate.quotientCoordinateTrans, holomorphic on the first open set (Subgroup.LinearizingCoordinate.differentiableOn_quotientCoordinateTrans) into the second (Subgroup.LinearizingCoordinate.quotientCoordinateTrans_mem_quotientImage) and inverse to the transition in the other direction (Subgroup.LinearizingCoordinate.quotientCoordinateTrans_quotientCoordinateTrans)) — obtained by descending the change of coordinate through u ↦ u ^ m with TauCeti.differentiableOn_descendPow. Since the rotation by which an element of the stabilizer acts is Subgroup.stabilizerRotation, the same rotation appears in every local linearizing coordinate (Subgroup.LinearizingCoordinate.coordinate_smul). The coordinate, and with it the local quotient coordinate, is holomorphic on the invariant hyperbolic disc (Subgroup.LinearizingCoordinate.mdifferentiableOn_coordinate, Subgroup.LinearizingCoordinate.mdifferentiableOn_quotientCoordinate).

The two coordinates available by construction, for 0 < ε, are the disc coordinate centred at z and its rotation by a root of unity (Subgroup.LinearizingCoordinate.discCoordinate, Subgroup.LinearizingCoordinate.rotation); for the disc coordinate the quotient coordinate is discCoordinate z τ ^ m, the coordinate of Subgroup.stabilizerBallQuotientHomeomorph and Subgroup.stabilizerBallQuotientChart, and a rotation leaves it unchanged (Subgroup.LinearizingCoordinate.quotientCoordinate_rotation). Independence from the choice of the invariant disc is Subgroup.stabilizerBallQuotientChart_trans_apply.

Main declarations

• Subgroup.LinearizingCoordinate: a local biholomorphic coordinate linearizing the stabilizer of z on the invariant disc of radius ε, the positivity of which is stored in the structure as Subgroup.LinearizingCoordinate.ε_pos.
• Subgroup.LinearizingCoordinate.coordinate, …_smul, …_injective and …_mdifferentiableOn_coordinate: the coordinate of a point of the invariant disc, the action of the stabilizer on it, and its holomorphy on the invariant disc.
• Subgroup.LinearizingCoordinate.toEquiv, …_isOpen_target, …_mem_target_iff: the open image of the reparametrization, the set of coordinate values.
• Subgroup.LinearizingCoordinate.transEquiv, …_transEquiv_coordinate, …_transEquiv_transEquiv and Subgroup.LinearizingCoordinate.differentiableOn_transEquiv: the biholomorphic change of local linearizing coordinate between two local linearizing coordinates.
• Subgroup.LinearizingCoordinate.discCoordinate and …_rotation: the two reparametrizations available by construction, with …_quotientCoordinate and …_quotientCoordinate_rotation computing their quotient coordinates.

References

• Hershel Farkas and Irwin Kra, Riemann Surfaces, second edition, Chapter IV §9: the stabilizer of a point of a group of Möbius transformations is cyclic when it is finite, and at an elliptic fixed point it is generated by the rotation z ↦ e ^ (2 * π * I / v) * z, the quotient carrying the local coordinate z ^ v, the v-th power, which that rotation leaves fixed (§IV.9.11).
• Svetlana Katok, Fuchsian Groups, University of Chicago Press, 1992, §2.4.

structure Subgroup.LinearizingCoordinate (Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) (z : UpperHalfPlane) (ε : ℝ) [Finite ↥(MulAction.stabilizer (↥Γ) z)] : Type

A local linearizing coordinate at z on the invariant hyperbolic disc of radius ε, which is positive, that hypothesis being stored as Subgroup.LinearizingCoordinate.ε_pos so that the disc is a neighbourhood of z: a partial equivalence toEquiv of ℂ from the Euclidean disc of radius Real.tanh (ε / 2), the image of the invariant disc in the disc coordinate centred at z, to its own image, which fixes 0 and intertwines the rotation action of the Nat.card (stabilizer Γ z)-th roots of unity on the disc with the rotation action on that image. The coordinate of a point τ of the invariant disc is then Subgroup.LinearizingCoordinate.coordinate ψ τ = toEquiv (discCoordinate z τ), a biholomorphic coordinate of the invariant disc; the stabilizer of z acts on that disc, and by Subgroup.LinearizingCoordinate.coordinate_smul it acts in this coordinate by the rotation Subgroup.stabilizerRotation, so the quotient by the stabilizer is the power map u ↦ u ^ m, m = Nat.card (stabilizer Γ z).

The target of the reparametrization, its image on that disc, is only required to be open, not to be the whole Euclidean disc: local linearizing coordinates are not all rotations of the disc coordinate, the equivariant biholomorphic reparametrizations of a disc being an infinite-dimensional family. Biholomorphy is the requirement that toFun and invFun be holomorphic on the disc and on the target respectively and inverse to one another there. Both holomorphy conditions are stored explicitly, being hypotheses of the structure, so that the biholomorphic reparametrization is available without deriving the holomorphy of the inverse from that of toFun by the holomorphic inverse function theorem. The target is open by Subgroup.LinearizingCoordinate.isOpen_target.

• ε_pos : 0 < ε

  the radius of the invariant disc is positive, the invariant disc and its disc coordinate then being non-empty and containing the centre z, as a local coordinate about z is

• toEquiv : PartialEquiv ℂ ℂ

  the reparametrization of the disc coordinate, a partial equivalence of ℂ whose source is the disc of the invariant disc and whose target is its image

• toEquiv_source : self.toEquiv.source = Metric.ball 0 (Real.tanh (ε / 2))

  the source of the reparametrization is the disc of the invariant disc

• differentiableOn : DifferentiableOn ℂ (↑self.toEquiv) (Metric.ball 0 (Real.tanh (ε / 2)))

  the reparametrization is holomorphic on the disc of the invariant disc

• differentiableOn_invFun : DifferentiableOn ℂ self.toEquiv.invFun self.toEquiv.target

  the inverse reparametrization is holomorphic on the image of the reparametrization

• map_zero : ↑self.toEquiv 0 = 0

  the reparametrization fixes the centre

• toFun_eq_id (w : ℂ) : w ∉ Metric.ball 0 (Real.tanh (ε / 2)) → ↑self.toEquiv w = w

  the reparametrization is the identity outside the disc of the invariant disc, the choice which leaves the disc coordinate the identity reparametrization; it makes a local linearizing coordinate determined by its values on that disc (Subgroup.LinearizingCoordinate.ext)

• invFun_eq_id (w : ℂ) : w ∉ self.toEquiv.target → self.toEquiv.invFun w = w

  the inverse reparametrization is the identity outside the image of the reparametrization, so that it too is determined by the values of the reparametrization on the disc of the invariant disc (Subgroup.LinearizingCoordinate.ext)

• map_smul (ζ : ↥(rootsOfUnity (Nat.card ↥(MulAction.stabilizer (↥Γ) z)) ℂ)) (w : ℂ) : w ∈ Metric.ball 0 (Real.tanh (ε / 2)) → ↑self.toEquiv (ζ • w) = ζ • ↑self.toEquiv w

  the reparametrization intertwines the rotation action of the roots of unity on the disc with the rotation action on its image

theorem Subgroup.LinearizingCoordinate.toFun_injOn_ball {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (ψ : Γ.LinearizingCoordinate z ε) : Set.InjOn (↑ψ.toEquiv) (Metric.ball 0 (Real.tanh (ε / 2)))

The reparametrization of a local linearizing coordinate is injective on the disc of the invariant disc, being a partial equivalence on its source.

theorem Subgroup.LinearizingCoordinate.mem_ball_invFun {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (ψ : Γ.LinearizingCoordinate z ε) {u : ℂ} (hu : u ∈ ψ.toEquiv.target) : ψ.toEquiv.invFun u ∈ Metric.ball 0 (Real.tanh (ε / 2))

The inverse reparametrization of a local linearizing coordinate takes a point of the image back into the disc of the invariant disc.

noncomputable def Subgroup.LinearizingCoordinate.coordinate {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (ψ : Γ.LinearizingCoordinate z ε) (τ : ↥(Γ.stabilizerBall z ε)) : ℂ

The coordinate of a point of the invariant disc in a local linearizing coordinate: the reparametrized disc coordinate, a biholomorphic coordinate on the invariant hyperbolic disc of radius ε about z centred at z in which the stabilizer of z acts by its rotation Subgroup.stabilizerRotation (Subgroup.LinearizingCoordinate.coordinate_smul), holomorphic there by Subgroup.LinearizingCoordinate.mdifferentiableOn_coordinate.

Equations

• ψ.coordinate τ = ↑ψ.toEquiv (z.discCoordinate ↑τ)

@[simp]

theorem Subgroup.LinearizingCoordinate.coordinate_eq_zero_iff {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (ψ : Γ.LinearizingCoordinate z ε) (τ : ↥(Γ.stabilizerBall z ε)) : ψ.coordinate τ = 0 ↔ ↑τ = z

A point of the invariant disc has coordinate 0 in a local linearizing coordinate exactly when it is the centre: the coordinate is centred at the centre.

theorem Subgroup.LinearizingCoordinate.coordinate_injective {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (ψ : Γ.LinearizingCoordinate z ε) : Function.Injective ψ.coordinate

The coordinate of a local linearizing coordinate is injective on the invariant disc.

@[simp]

theorem Subgroup.LinearizingCoordinate.coordinate_smul {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (ψ : Γ.LinearizingCoordinate z ε) (q : ↥(MulAction.stabilizer (↥Γ) z)) (τ : ↥(Γ.stabilizerBall z ε)) : ψ.coordinate (q • τ) = ↑↑((Γ.stabilizerRotation z) q) * ψ.coordinate τ

The stabilizer of z acts in the coordinate of a local linearizing coordinate by its rotation. The rotation does not depend on the local linearizing coordinate: it is Subgroup.stabilizerRotation Γ z q, the derivative of q at z.

@[simp]

theorem Subgroup.LinearizingCoordinate.mem_target_iff {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (ψ : Γ.LinearizingCoordinate z ε) (u : ℂ) : u ∈ ψ.toEquiv.target ↔ ∃ (τ : ↥(Γ.stabilizerBall z ε)), u = ψ.coordinate τ

A point is a coordinate value of a local linearizing coordinate exactly when it lies in the target of the reparametrization, its image on the disc of the invariant disc.

theorem Subgroup.LinearizingCoordinate.isOpen_target {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (ψ : Γ.LinearizingCoordinate z ε) : IsOpen ψ.toEquiv.target

The target of a local linearizing coordinate is open: it is the image of the disc of the invariant disc, an open set, under the reparametrization, which is holomorphic and injective there (TauCeti.isOpen_image_of_differentiableOn_of_injOn).

theorem Subgroup.LinearizingCoordinate.mdifferentiableOn_coordinate {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (ψ : Γ.LinearizingCoordinate z ε) : MDiff[Metric.ball z ε] fun (τ : UpperHalfPlane) => ↑ψ.toEquiv (z.discCoordinate τ)

The coordinate of a local linearizing coordinate is holomorphic on the invariant disc: on the ambient upper half-plane, the invariant disc being the ball Metric.ball z ε (Subgroup.mem_stabilizerBall), it is the composition of the disc coordinate, which is holomorphic by UpperHalfPlane.mdifferentiable_discCoordinate, with the reparametrization Subgroup.LinearizingCoordinate.differentiableOn, which is holomorphic on the disc of the invariant disc and which the disc coordinate maps the invariant disc into. Restricted to Subgroup.stabilizerBall Γ z ε that composition is Subgroup.LinearizingCoordinate.coordinate, so this is the holomorphy of that coordinate.

noncomputable def Subgroup.LinearizingCoordinate.quotientCoordinate {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (ψ : Γ.LinearizingCoordinate z ε) (τ : ↥(Γ.stabilizerBall z ε)) : ℂ

The local quotient coordinate in a local linearizing coordinate: the Nat.card (stabilizer Γ z)-th power of the coordinate, the model of the quotient of the invariant disc by the stabilizer of z, m = Nat.card (stabilizer Γ z). Its level sets are the orbits of that stabilizer (Subgroup.LinearizingCoordinate.quotientCoordinate_eq_iff), so it is a coordinate on that quotient, and it is independent of the local linearizing coordinate up to the biholomorphic transition Subgroup.LinearizingCoordinate.quotientCoordinateTrans, holomorphic there by Subgroup.LinearizingCoordinate.differentiableOn_quotientCoordinateTrans.

Equations

• ψ.quotientCoordinate τ = ψ.coordinate τ ^ Nat.card ↥(MulAction.stabilizer (↥Γ) z)

@[simp]

theorem Subgroup.LinearizingCoordinate.quotientCoordinate_smul {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (ψ : Γ.LinearizingCoordinate z ε) (q : ↥(MulAction.stabilizer (↥Γ) z)) (τ : ↥(Γ.stabilizerBall z ε)) : ψ.quotientCoordinate (q • τ) = ψ.quotientCoordinate τ

The local quotient coordinate is constant on the orbits of the stabilizer of z, since the stabilizer acts by a Nat.card (stabilizer Γ z)-th root of unity.

theorem Subgroup.LinearizingCoordinate.orbitRel_iff {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (ψ : Γ.LinearizingCoordinate z ε) (τ σ : ↥(Γ.stabilizerBall z ε)) : (MulAction.orbitRel ↥(MulAction.stabilizer (↥Γ) z) ↥(Γ.stabilizerBall z ε)) τ σ ↔ (MulAction.orbitRel ↥(rootsOfUnity (Nat.card ↥(MulAction.stabilizer (↥Γ) z)) ℂ) ℂ) (ψ.coordinate τ) (ψ.coordinate σ)

The orbits of the stabilizer of z on the invariant disc are the orbits of the roots of unity in the coordinate of a local linearizing coordinate: the reparametrization of the disc coordinate does not change which points lie in the same orbit, so the orbit relation of the stabilizer of z on the invariant disc does not depend on the local linearizing coordinate. The roots of unity act on ℂ by multiplication, as on the disc Subgroup.stabilizerBallHomeomorph_smul.

theorem Subgroup.LinearizingCoordinate.quotientCoordinate_eq_iff {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (ψ : Γ.LinearizingCoordinate z ε) (τ σ : ↥(Γ.stabilizerBall z ε)) : ψ.quotientCoordinate τ = ψ.quotientCoordinate σ ↔ (MulAction.orbitRel ↥(MulAction.stabilizer (↥Γ) z) ↥(Γ.stabilizerBall z ε)) τ σ

The local quotient coordinate is a complete invariant of the orbits of the stabilizer of z on the invariant disc: two points of the invariant disc have the same local quotient coordinate exactly when a single element of the stabilizer carries one to the other, that is, when they lie in the same orbit of the stabilizer of z. Hence the local quotient coordinate is a coordinate on the quotient of the invariant disc by that stabilizer, which the disc coordinate identifies with the coordinate of the chart Subgroup.stabilizerBallQuotientChart on the coarse orbit quotient Γ \ ℍ (Subgroup.LinearizingCoordinate.quotientCoordinate_discCoordinate).

def Subgroup.LinearizingCoordinate.quotientImage {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (ψ : Γ.LinearizingCoordinate z ε) : Set ℂ

The set of quotient-coordinate values of a local linearizing coordinate: the Nat.card (stabilizer Γ z)-th powers of the coordinate values, which is the image of the m-th power, m = Nat.card (stabilizer Γ z), of the target of the reparametrization, that is of its image, and is an open set by Subgroup.LinearizingCoordinate.isOpen_quotientImage.

Equations

• ψ.quotientImage = (fun (x : ℂ) => x ^ Nat.card ↥(MulAction.stabilizer (↥Γ) z)) '' ψ.toEquiv.target

@[simp]

theorem Subgroup.LinearizingCoordinate.mem_quotientImage_iff {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (ψ : Γ.LinearizingCoordinate z ε) (w : ℂ) : w ∈ ψ.quotientImage ↔ ∃ (τ : ↥(Γ.stabilizerBall z ε)), w = ψ.quotientCoordinate τ

A point is a quotient-coordinate value of a local linearizing coordinate exactly when it is the Nat.card (stabilizer Γ z)-th power of a coordinate value.

theorem Subgroup.LinearizingCoordinate.isOpen_quotientImage {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (ψ : Γ.LinearizingCoordinate z ε) : IsOpen ψ.quotientImage

The set of quotient-coordinate values of a local linearizing coordinate is open: it is the image of the open target of the reparametrization under the power map u ↦ u ^ m, which is an open map, being a non-constant holomorphic map (Complex.isOpenQuotientMap_pow).

theorem Subgroup.LinearizingCoordinate.mdifferentiableOn_quotientCoordinate {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (ψ : Γ.LinearizingCoordinate z ε) : MDiff[Metric.ball z ε] fun (τ : UpperHalfPlane) => ↑ψ.toEquiv (z.discCoordinate τ) ^ Nat.card ↥(MulAction.stabilizer (↥Γ) z)

The local quotient coordinate of a local linearizing coordinate is holomorphic on the invariant disc: it is the Nat.card (stabilizer Γ z)-th power of the holomorphic coordinate Subgroup.LinearizingCoordinate.mdifferentiableOn_coordinate. On Subgroup.stabilizerBall Γ z ε it is Subgroup.LinearizingCoordinate.quotientCoordinate, so this is the holomorphy of the local quotient coordinate.

def Subgroup.LinearizingCoordinate.transEquiv {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (ψ ψ' : Γ.LinearizingCoordinate z ε) : PartialEquiv ℂ ℂ

The change of local linearizing coordinate between two local linearizing coordinates on the invariant disc: the partial equivalence ψ.toEquiv.symm.trans ψ'.toEquiv, the reparametrization ψ' pulled back by the inverse reparametrization ψ, whose source is the target of ψ and whose target is the target of ψ' (Subgroup.LinearizingCoordinate.transEquiv_source, Subgroup.LinearizingCoordinate.transEquiv_target). On the target of ψ it is a biholomorphism onto the target of ψ' intertwining the rotation action (Subgroup.LinearizingCoordinate.transEquiv_smul), taking a coordinate value to the corresponding coordinate value (Subgroup.LinearizingCoordinate.transEquiv_coordinate), and its inverse being the change of coordinate in the other direction (Subgroup.LinearizingCoordinate.transEquiv_transEquiv).

Equations

• ψ.transEquiv ψ' = ψ.toEquiv.symm.trans ψ'.toEquiv

@[simp]

theorem Subgroup.LinearizingCoordinate.transEquiv_source {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (ψ ψ' : Γ.LinearizingCoordinate z ε) : (ψ.transEquiv ψ').source = ψ.toEquiv.target

The source of the change of local linearizing coordinate is the target of ψ, its image on the disc of the invariant disc.

@[simp]

theorem Subgroup.LinearizingCoordinate.transEquiv_target {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (ψ ψ' : Γ.LinearizingCoordinate z ε) : (ψ.transEquiv ψ').target = ψ'.toEquiv.target

The target of the change of local linearizing coordinate is the target of ψ', its image on the disc of the invariant disc.

theorem Subgroup.LinearizingCoordinate.transEquiv_mem_target {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (ψ ψ' : Γ.LinearizingCoordinate z ε) {u : ℂ} (hu : u ∈ ψ.toEquiv.target) : ↑(ψ.transEquiv ψ') u ∈ ψ'.toEquiv.target

The change of local linearizing coordinate takes a coordinate value to a coordinate value: it carries a point of the target of ψ to a point of the target of ψ', so the change of coordinate is a map between the two open sets of coordinate values.

@[simp]

theorem Subgroup.LinearizingCoordinate.transEquiv_coordinate {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (ψ ψ' : Γ.LinearizingCoordinate z ε) (τ : ↥(Γ.stabilizerBall z ε)) : ↑(ψ.transEquiv ψ') (ψ.coordinate τ) = ψ'.coordinate τ

The change of local linearizing coordinate takes a coordinate value to a coordinate value, which is how a point of the invariant disc is read in the second local linearizing coordinate once it is read in the first one.

theorem Subgroup.LinearizingCoordinate.invFun_smul {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (ψ : Γ.LinearizingCoordinate z ε) {u : ℂ} (hu : u ∈ ψ.toEquiv.target) (ζ : ↥(rootsOfUnity (Nat.card ↥(MulAction.stabilizer (↥Γ) z)) ℂ)) : ψ.toEquiv.invFun (ζ • u) = ζ • ψ.toEquiv.invFun u

The inverse reparametrization of a local linearizing coordinate is equivariant for the rotations: it intertwines the rotation action of the roots of unity on the image with the rotation action of the roots of unity on the disc.

@[simp]

theorem Subgroup.LinearizingCoordinate.transEquiv_smul {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (ψ ψ' : Γ.LinearizingCoordinate z ε) {u : ℂ} (hu : u ∈ ψ.toEquiv.target) (ζ : ↥(rootsOfUnity (Nat.card ↥(MulAction.stabilizer (↥Γ) z)) ℂ)) : ↑(ψ.transEquiv ψ') (ζ • u) = ζ • ↑(ψ.transEquiv ψ') u

The change of local linearizing coordinate intertwines the rotation action, being the pullback of an equivariant reparametrization by an equivariant inverse.

@[simp]

theorem Subgroup.LinearizingCoordinate.transEquiv_transEquiv {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (ψ ψ' : Γ.LinearizingCoordinate z ε) {u : ℂ} (hu : u ∈ ψ.toEquiv.target) : ↑(ψ'.transEquiv ψ) (↑(ψ.transEquiv ψ') u) = u

The changes of local linearizing coordinate in the two directions are inverse: the change of coordinate is a biholomorphism of the targets of the reparametrizations, being the symm of itself.

theorem Subgroup.LinearizingCoordinate.differentiableOn_transEquiv {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (ψ ψ' : Γ.LinearizingCoordinate z ε) : DifferentiableOn ℂ (↑(ψ.transEquiv ψ')) ψ.toEquiv.target

The change of local linearizing coordinate is holomorphic on the target of the reparametrization, being the composition of the inverse reparametrization, holomorphic there, with the reparametrization, holomorphic on the disc of the invariant disc.

noncomputable def Subgroup.LinearizingCoordinate.quotientCoordinateTrans {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (ψ ψ' : Γ.LinearizingCoordinate z ε) : ℂ → ℂ

The transition of the local quotient coordinates of two local linearizing coordinates: the descent through u ↦ u ^ m, m = Nat.card (stabilizer Γ z), of the m-th power of the change of local linearizing coordinate Subgroup.LinearizingCoordinate.transEquiv. It takes the quotient coordinate of a point of the invariant disc in the first local linearizing coordinate to its quotient coordinate in the second (Subgroup.LinearizingCoordinate.quotientCoordinateTrans_quotientCoordinate), and it is holomorphic on the set of quotient-coordinate values (Subgroup.LinearizingCoordinate.differentiableOn_quotientCoordinateTrans).

Equations

• ψ.quotientCoordinateTrans ψ' = TauCeti.descendPow (Nat.card ↥(MulAction.stabilizer (↥Γ) z)) fun (u : ℂ) => ↑(ψ.transEquiv ψ') u ^ Nat.card ↥(MulAction.stabilizer (↥Γ) z)

theorem Subgroup.LinearizingCoordinate.differentiableOn_quotientCoordinateTrans {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (ψ ψ' : Γ.LinearizingCoordinate z ε) : DifferentiableOn ℂ (ψ.quotientCoordinateTrans ψ') ψ.quotientImage

The transition of the local quotient coordinates is holomorphic on the set of quotient-coordinate values of the first local linearizing coordinate: it is the descent of the m-th power of a holomorphic function invariant under the rotations, by TauCeti.differentiableOn_descendPow.

@[simp]

theorem Subgroup.LinearizingCoordinate.quotientCoordinateTrans_quotientCoordinate {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (ψ ψ' : Γ.LinearizingCoordinate z ε) (τ : ↥(Γ.stabilizerBall z ε)) : ψ.quotientCoordinateTrans ψ' (ψ.quotientCoordinate τ) = ψ'.quotientCoordinate τ

The transition of the local quotient coordinates takes a quotient coordinate to a quotient coordinate, so it relates the local quotient coordinates of the two local linearizing coordinates.

theorem Subgroup.LinearizingCoordinate.quotientCoordinateTrans_mem_quotientImage {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (ψ ψ' : Γ.LinearizingCoordinate z ε) {w : ℂ} (hw : w ∈ ψ.quotientImage) : ψ.quotientCoordinateTrans ψ' w ∈ ψ'.quotientImage

The transition of the local quotient coordinates takes a quotient coordinate to a quotient coordinate, so it maps the set of quotient-coordinate values of the first local linearizing coordinate into that of the second.

@[simp]

theorem Subgroup.LinearizingCoordinate.quotientCoordinateTrans_quotientCoordinateTrans {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (ψ ψ' : Γ.LinearizingCoordinate z ε) {w : ℂ} (hw : w ∈ ψ.quotientImage) : ψ'.quotientCoordinateTrans ψ (ψ.quotientCoordinateTrans ψ' w) = w

The transitions of the local quotient coordinates in the two directions are inverse on the set of quotient-coordinate values: the transition Subgroup.LinearizingCoordinate.quotientCoordinateTrans ψ' ψ, the transition in the other direction, is the inverse of Subgroup.LinearizingCoordinate.quotientCoordinateTrans ψ ψ', so the transition is a biholomorphic change of the local quotient coordinate.

def Subgroup.LinearizingCoordinate.discCoordinate {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (hε : 0 < ε) : Γ.LinearizingCoordinate z ε

The disc coordinate centred at z is a local linearizing coordinate on the invariant disc of radius ε > 0: the reparametrization by the disc coordinate itself, whose coordinate is the disc coordinate Subgroup.LinearizingCoordinate.coordinate and whose quotient coordinate is discCoordinate z τ ^ Nat.card (stabilizer Γ z), the coordinate of Subgroup.stabilizerBallQuotientHomeomorph and of the chart Subgroup.stabilizerBallQuotientChart (Subgroup.LinearizingCoordinate.quotientCoordinate_discCoordinate).

Equations

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

@[simp]

theorem Subgroup.LinearizingCoordinate.coordinate_discCoordinate {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (hε : 0 < ε) (τ : ↥(Γ.stabilizerBall z ε)) : (discCoordinate hε).coordinate τ = z.discCoordinate ↑τ

The coordinate in the disc coordinate of a local linearizing coordinate is the disc coordinate itself.

@[simp]

theorem Subgroup.LinearizingCoordinate.quotientCoordinate_discCoordinate {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (hε : 0 < ε) (τ : ↥(Γ.stabilizerBall z ε)) : (discCoordinate hε).quotientCoordinate τ = z.discCoordinate ↑τ ^ Nat.card ↥(MulAction.stabilizer (↥Γ) z)

The local quotient coordinate in the disc coordinate of a local linearizing coordinate is the Nat.card (stabilizer Γ z)-th power of the disc coordinate, the coordinate of the chart Subgroup.stabilizerBallQuotientChart on the coarse orbit quotient.

theorem Subgroup.LinearizingCoordinate.ext {ε : ℝ} {z : UpperHalfPlane} {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [Finite ↥(MulAction.stabilizer (↥Γ) z)] {τ τ' : Γ.LinearizingCoordinate z ε} (hcoord : ∀ w ∈ Metric.ball 0 (Real.tanh (ε / 2)), ↑τ.toEquiv w = ↑τ'.toEquiv w) : τ = τ'

A local linearizing coordinate is determined by its reparametrization on the disc of the invariant disc: two local linearizing coordinates with the same reparametrization there agree everywhere, the ambient reparametrizations being the identity outside that disc (Subgroup.LinearizingCoordinate.toFun_eq_id), and so have the same target, being the image of the disc of the invariant disc; their inverse reparametrizations agree on the target, being mutual inverses of the reparametrization there (PartialEquiv.right_inv), and are the identity outside it (Subgroup.LinearizingCoordinate.invFun_eq_id).

theorem Subgroup.LinearizingCoordinate.ext_iff {ε : ℝ} {z : UpperHalfPlane} {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} [Finite ↥(MulAction.stabilizer (↥Γ) z)] {τ τ' : Γ.LinearizingCoordinate z ε} : τ = τ' ↔ ∀ w ∈ Metric.ball 0 (Real.tanh (ε / 2)), ↑τ.toEquiv w = ↑τ'.toEquiv w

noncomputable def Subgroup.LinearizingCoordinate.rotation {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (hε : 0 < ε) (ζ : ↥(rootsOfUnity (Nat.card ↥(MulAction.stabilizer (↥Γ) z)) ℂ)) : Γ.LinearizingCoordinate z ε

A rotation of the disc coordinate is a local linearizing coordinate on the invariant disc of radius ε > 0: the reparametrization of the disc of the invariant disc by a root of unity of order Nat.card (stabilizer Γ z), whose coordinate is the disc coordinate multiplied by that root of unity (Subgroup.LinearizingCoordinate.coordinate_rotation). The quotient coordinate of a rotation is the quotient coordinate of the disc coordinate itself (Subgroup.LinearizingCoordinate.quotientCoordinate_rotation), the rotation being an m-th root of unity.

Equations

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

@[simp]

theorem Subgroup.LinearizingCoordinate.coordinate_rotation {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (hε : 0 < ε) (ζ : ↥(rootsOfUnity (Nat.card ↥(MulAction.stabilizer (↥Γ) z)) ℂ)) (τ : ↥(Γ.stabilizerBall z ε)) : (rotation hε ζ).coordinate τ = ζ • z.discCoordinate ↑τ

The coordinate in a rotation of the disc coordinate is the disc coordinate multiplied by the root of unity of the rotation.

@[simp]

theorem Subgroup.LinearizingCoordinate.quotientCoordinate_rotation {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} {z : UpperHalfPlane} {ε : ℝ} [Finite ↥(MulAction.stabilizer (↥Γ) z)] (hε : 0 < ε) (ζ : ↥(rootsOfUnity (Nat.card ↥(MulAction.stabilizer (↥Γ) z)) ℂ)) (τ : ↥(Γ.stabilizerBall z ε)) : (rotation hε ζ).quotientCoordinate τ = z.discCoordinate ↑τ ^ Nat.card ↥(MulAction.stabilizer (↥Γ) z)

The local quotient coordinate in a rotation of the disc coordinate is the local quotient coordinate in the disc coordinate itself, the rotation being a Nat.card (stabilizer Γ z)-th root of unity.