Transitivity and properness of actions

We show that the actions of SL(2, ℝ) and GL(2, ℝ) on the upper half-plane are jointly continuous, and the action of SL(2, ℝ) is proper. (These results require more imports than in UpperHalfPlane.Topology, because they use the topology on the group as well)

TODO: Show properness of the action of PGL(2, ℝ) once this is defined.

theorem UpperHalfPlane.num_continuous : Continuous ↿num

theorem UpperHalfPlane.denom_continuous : Continuous ↿denom

theorem UpperHalfPlane.continuous_toSL2R : Continuous toSL2R

instance UpperHalfPlane.instContinuousSMulSL2R : ContinuousSMul (Matrix.SpecialLinearGroup (Fin 2) ℝ) UpperHalfPlane

The action of SL(2, ℝ) on ℍ is jointly continuous.

theorem UpperHalfPlane.σ_eventuallyEq (g : GL (Fin 2) ℝ) : σ =ᶠ[nhds g] fun (x : GL (Fin 2) ℝ) => σ g

instance UpperHalfPlane.instContinuousSMulGL2R : ContinuousSMul (GL (Fin 2) ℝ) UpperHalfPlane

The action of GL(2, ℝ) on ℍ is jointly continuous.

theorem UpperHalfPlane.isProperMap_smul_I : IsProperMap fun (g : Matrix.SpecialLinearGroup (Fin 2) ℝ) => g • I

The orbit map g ↦ g • I is a proper map SL(2, ℝ) → ℍ.

instance UpperHalfPlane.instProperSMul : ProperSMul (Matrix.SpecialLinearGroup (Fin 2) ℝ) UpperHalfPlane