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, ℤ).

class Subgroup.HasDetPlusMinusOne {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [CommRing R] (Γ : Subgroup (GL n R)) : Prop

Typeclass saying that a subgroup of GL(2, ℝ) has determinant contained in {±1}. Necessary so that the typeclass system can detect when the slash action is multiplicative.

• det_eq {g : GL n R} (hg : g ∈ Γ) : Matrix.GeneralLinearGroup.det g = 1 ∨ Matrix.GeneralLinearGroup.det g = -1

theorem Subgroup.HasDetPlusMinusOne.abs_det {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [CommRing R] {Γ : Subgroup (GL n R)} [LinearOrder R] [IsOrderedRing R] [Γ.HasDetPlusMinusOne] {g : GL n R} (hg : g ∈ Γ) : |↑(Matrix.GeneralLinearGroup.det g)| = 1

class Subgroup.HasDetOne {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [CommRing R] (Γ : Subgroup (GL n R)) : Prop

Typeclass saying that a subgroup of GL(n, R) is contained in SL(n, R). Necessary so that the typeclass system can detect when the slash action is ℂ-linear.

• det_eq {g : GL n R} (hg : g ∈ Γ) : Matrix.GeneralLinearGroup.det g = 1

instance Subgroup.instHasDetOneMapSpecialLinearGroupGeneralLinearGroupToGL {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [CommRing R] (Γ : Subgroup (Matrix.SpecialLinearGroup n R)) : (map Matrix.SpecialLinearGroup.toGL Γ).HasDetOne

instance Subgroup.instHasDetOneMapSpecialLinearGroupGeneralLinearGroupMapGL {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [CommRing R] {S : Type u_3} [CommRing S] [Algebra S R] (Γ : Subgroup (Matrix.SpecialLinearGroup n S)) : (map (Matrix.SpecialLinearGroup.mapGL R) Γ).HasDetOne

instance Subgroup.instHasDetPlusMinusOneOfHasDetOne {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [CommRing R] (Γ : Subgroup (GL n R)) [Γ.HasDetOne] : Γ.HasDetPlusMinusOne

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.

instance Subgroup.instHasDetPlusMinusOneFinOfNatNatRealOfIsArithmetic {Γ : Subgroup (GL (Fin 2) ℝ)} [h : Γ.IsArithmetic] : Γ.HasDetPlusMinusOne

instance Matrix.SpecialLinearGroup.discreteSpecialLinearGroupIntRange {n : Type u_1} [Fintype n] [DecidableEq n] : DiscreteTopology ↥(mapGL ℝ).range

theorem Matrix.SpecialLinearGroup.isClosedEmbedding_mapGLInt {n : Type u_1} [Fintype n] [DecidableEq n] : Topology.IsClosedEmbedding ⇑(mapGL ℝ)