The holomorphic projective action on the upper half-plane

Every element of PSL(2, ℝ) acts on the upper half-plane by a biholomorphism. This file expresses holomorphy as a ContMDiffConstSMul instance, so each transformation is packaged by the generic Diffeomorph.constSmul constructor. Subgroups inherit the same holomorphic action, which is the input needed to put complex charts on their free orbit quotients.

Main declarations

• UpperHalfPlane.instContMDiffConstSMulPSL2: the action of each element of PSL(2, ℝ) is holomorphic.
• Subgroup.instContMDiffConstSMulPSL2: every subgroup of PSL(2, ℝ) acts holomorphically.

instance UpperHalfPlane.instContMDiffConstSMulPSL2 : ContMDiffConstSMul (modelWithCornersSelf ℂ ℂ) (↑⊤) (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ) UpperHalfPlane

The action of each element of PSL(2, ℝ) on the upper half-plane is holomorphic.

instance Subgroup.instContMDiffConstSMulPSL2 (G : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)) : ContMDiffConstSMul (modelWithCornersSelf ℂ ℂ) (↑⊤) (↥G) UpperHalfPlane

Every subgroup of PSL(2, ℝ) inherits a holomorphic action on the upper half-plane.