Topology on PSL(2, ℝ)

The quotient topology on the projective special linear group PSL(2, ℝ) is Hausdorff because the center of SL(2, ℝ) is finite, hence closed. Conjugation preserves discrete subgroups. The natural injection PSL(2, ℤ) → PSL(2, ℝ) is a topological embedding, so its range is discrete. Finally, the translations Matrix.ProjectiveSpecialLinearGroup.upperRightHom x depend continuously on x.

Main results

• isEmbedding_psl2zToPSL2R: the natural injection from the integral projective special linear group to the real one is a topological embedding.
• Matrix.ProjectiveSpecialLinearGroup.continuous_upperRightHom: projective translations depend continuously on their parameter.

instance TauCeti.instT2SpaceProjectiveSpecialLinearGroupFinOfNatNatReal_tauCeti : T2Space (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)

The projective special linear group PSL(2, ℝ) is Hausdorff.

theorem TauCeti.isEmbedding_psl2zToPSL2R : Topology.IsEmbedding ⇑psl2zToPSL2R

The natural injection PSL(2, ℤ) → PSL(2, ℝ) is a topological embedding.

Thus PSL(2, ℤ) has the topology induced from PSL(2, ℝ) on its image; in particular, the projective integral image is a discrete subgroup.

instance TauCeti.instDiscreteTopologySubtypeProjectiveSpecialLinearGroupFinOfNatNatRealMemSubgroupRangeIntPsl2zToPSL2R : DiscreteTopology ↥psl2zToPSL2R.range

The image of PSL(2, ℤ) in PSL(2, ℝ) is a discrete subgroup.

theorem Matrix.ProjectiveSpecialLinearGroup.continuous_upperRightHom {R : Type u_1} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] : Continuous ⇑upperRightHom

The translation upperRightHom x ∈ PSL(2, R) depends continuously on x.