Arithmetic subgroups of GL(2, ℝ)

We define a subgroup of GL (Fin 2) ℝ to be arithmetic if it is commensurable with the image of SL(2, ℤ).

def MatrixGroups.term𝒮ℒ : Lean.ParserDescr

The image of the modular group SL(2, ℤ), as a subgroup of GL(2, ℝ).

Equations

• MatrixGroups.term𝒮ℒ = Lean.ParserDescr.node `MatrixGroups.term𝒮ℒ 1024 (Lean.ParserDescr.symbol "𝒮ℒ")

instance Subgroup.instCoeSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupReal : Coe (Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (Subgroup (GL (Fin 2) ℝ))

Coercion from subgroups of SL(2, ℤ) to subgroups of GL(2, ℝ) by mapping along the obvious inclusion homomorphism.

Equations

• Subgroup.instCoeSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupReal = { coe := Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) }

class Subgroup.IsArithmetic (𝒢 : Subgroup (GL (Fin 2) ℝ)) : Prop

A subgroup of GL(2, ℝ) is arithmetic if it is commensurable with the image of SL(2, ℤ).

• is_commensurable : Commensurable 𝒢 (Matrix.SpecialLinearGroup.mapGL ℝ).range

instance Subgroup.instIsArithmeticRangeSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGL : (Matrix.SpecialLinearGroup.mapGL ℝ).range.IsArithmetic

The image of SL(2, ℤ) in GL(2, ℝ) is arithmetic.

theorem Subgroup.isArithmetic_iff_finiteIndex {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} : (map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ).IsArithmetic ↔ Γ.FiniteIndex

instance Subgroup.instIsArithmeticMapSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGLOfFiniteIndex (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) [Γ.FiniteIndex] : (map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ).IsArithmetic

Images in GL(2, ℝ) of finite-index subgroups of SL(2, ℤ) are arithmetic.

instance Subgroup.IsArithmetic.finiteIndex_comap (𝒢 : Subgroup (GL (Fin 2) ℝ)) [𝒢.IsArithmetic] : (comap (Matrix.SpecialLinearGroup.mapGL ℝ) 𝒢).FiniteIndex

If Γ is arithmetic, its preimage in SL(2, ℤ) has finite index.