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

theorem Subgroup.hasDetPlusMinusOne_iff_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}, 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 R S] (Γ : Subgroup (Matrix.SpecialLinearGroup n R)) : (map (Matrix.SpecialLinearGroup.mapGL S) Γ).HasDetOne

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

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

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

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

instance Subgroup.instHasDetOneHSMulConjActGeneralLinearGroup {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [CommRing R] (Γ : Subgroup (GL n R)) [Γ.HasDetOne] (g : ConjAct (GL n R)) : (g • Γ).HasDetOne

instance Subgroup.instHasDetPlusMinusOneHSMulConjActGeneralLinearGroup {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [CommRing R] (Γ : Subgroup (GL n R)) [Γ.HasDetPlusMinusOne] (g : ConjAct (GL n R)) : (g • Γ).HasDetPlusMinusOne

noncomputable def Subgroup.detOnePart {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [CommRing R] (G : Subgroup (GL n R)) : Subgroup (GL n R)

The determinant-one part of a subgroup of GL(2, ℝ).

Equations

• G.detOnePart = G ⊓ Matrix.SpecialLinearGroup.toGL.range

@[simp]

theorem Subgroup.mem_detOnePart {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [CommRing R] {G : Subgroup (GL n R)} {g : GL n R} : g ∈ G.detOnePart ↔ g ∈ G ∧ Matrix.GeneralLinearGroup.det g = 1

theorem Subgroup.detOnePart_le {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [CommRing R] (G : Subgroup (GL n R)) : G.detOnePart ≤ G

instance Subgroup.instHasDetOneDetOnePart {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [CommRing R] (G : Subgroup (GL n R)) : G.detOnePart.HasDetOne

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_reducible]

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

theorem Subgroup.isArithmetic_iff (𝒢 : Subgroup (GL (Fin 2) ℝ)) : 𝒢.IsArithmetic ↔ 𝒢.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 Subgroup.IsArithmetic.isFiniteRelIndex (G H : Subgroup (GL (Fin 2) ℝ)) [G.IsArithmetic] [H.IsArithmetic] : G.IsFiniteRelIndex H

instance Subgroup.IsArithmetic.inter {Γ Γ' : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] [Γ'.IsArithmetic] : (Γ ⊓ Γ').IsArithmetic

instance Subgroup.instIsArithmeticDetOnePartFinOfNatNatReal (G : Subgroup (GL (Fin 2) ℝ)) [G.IsArithmetic] : G.detOnePart.IsArithmetic

The determinant-one part of an arithmetic subgroup is arithmetic.

theorem Subgroup.isArithmetic_conj_of_mem {K H : Subgroup (GL (Fin 2) ℝ)} [K.IsArithmetic] [H.IsArithmetic] {r : GL (Fin 2) ℝ} (hr : r ∈ H) : (ConjAct.toConjAct r • K).IsArithmetic

Conjugation by an element of an arithmetic group preserves arithmeticity.

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

The image of SL(n, ℤ) in GL(n, ℝ) is discrete.

instance Matrix.SpecialLinearGroup.discreteSpecialLinearGroupIntRangeSL {n : Type u_1} [Fintype n] [DecidableEq n] : DiscreteTopology ↥(map (Int.castRingHom ℝ)).range

The image of SL(n, ℤ) in SL(n, ℝ) is discrete.

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

instance Subgroup.IsArithmetic.discreteTopology {𝒢 : Subgroup (GL (Fin 2) ℝ)} [𝒢.IsArithmetic] : DiscreteTopology ↥𝒢

Arithmetic subgroups of GL(2, ℝ) are discrete.

def Subgroup.adjoinNegOne {G : Type u_2} [Group G] [HasDistribNeg G] (𝒢 : Subgroup G) : Subgroup G

Given a subgroup 𝒢 of a group with compatible negation, this is the subgroup generated by 𝒢 and -1.

Equations

• 𝒢.adjoinNegOne = { carrier := {g : G | g ∈ 𝒢 ∨ -g ∈ 𝒢}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

@[simp]

theorem Subgroup.mem_adjoinNegOne_iff {G : Type u_2} [Group G] [HasDistribNeg G] {𝒢 : Subgroup G} {g : G} : g ∈ 𝒢.adjoinNegOne ↔ g ∈ 𝒢 ∨ -g ∈ 𝒢

theorem Subgroup.le_adjoinNegOne {G : Type u_2} [Group G] [HasDistribNeg G] (𝒢 : Subgroup G) : 𝒢 ≤ 𝒢.adjoinNegOne

theorem Subgroup.neg_one_mem_adjoinNegOne {G : Type u_2} [Group G] [HasDistribNeg G] (𝒢 : Subgroup G) : -1 ∈ 𝒢.adjoinNegOne

@[deprecated Subgroup.neg_one_mem_adjoinNegOne (since := "2026-09-14")]

theorem Subgroup.negOne_mem_adjoinNegOne {G : Type u_2} [Group G] [HasDistribNeg G] (𝒢 : Subgroup G) : -1 ∈ 𝒢.adjoinNegOne

Alias of Subgroup.neg_one_mem_adjoinNegOne.

@[simp]

theorem Subgroup.adjoinNegOne_eq_self_iff {G : Type u_2} [Group G] [HasDistribNeg G] {𝒢 : Subgroup G} : 𝒢.adjoinNegOne = 𝒢 ↔ -1 ∈ 𝒢

theorem Subgroup.relIndex_adjoinNegOne_eq_two {G : Type u_2} [Group G] [HasDistribNeg G] {𝒢 : Subgroup G} (h𝒢 : -1 ∉ 𝒢) : 𝒢.relIndex 𝒢.adjoinNegOne = 2

@[deprecated Subgroup.relIndex_adjoinNegOne_eq_two (since := "2026-09-14")]

theorem Subgroup.relindex_adjoinNegOne_eq_two {G : Type u_2} [Group G] [HasDistribNeg G] {𝒢 : Subgroup G} (h𝒢 : -1 ∉ 𝒢) : 𝒢.relIndex 𝒢.adjoinNegOne = 2

Alias of Subgroup.relIndex_adjoinNegOne_eq_two.

theorem Subgroup.relIndex_adjoinNegOne_ne_zero {G : Type u_2} [Group G] [HasDistribNeg G] (𝒢 : Subgroup G) : 𝒢.relIndex 𝒢.adjoinNegOne ≠ 0

instance Subgroup.instIsFiniteRelIndexAdjoinNegOne {G : Type u_2} [Group G] [HasDistribNeg G] (𝒢 : Subgroup G) : 𝒢.IsFiniteRelIndex 𝒢.adjoinNegOne

theorem Subgroup.commensurable_adjoinNegOne_self {G : Type u_2} [Group G] [HasDistribNeg G] (𝒢 : Subgroup G) : 𝒢.adjoinNegOne.Commensurable 𝒢

theorem Subgroup.map_adjoinNegOne {G : Type u_2} [Group G] [HasDistribNeg G] {H : Type u_3} [Group H] [HasDistribNeg H] (𝒢 : Subgroup G) (f : G →* H) (hf : ∀ (g : G), f (-g) = -f g) : map f 𝒢.adjoinNegOne = (map f 𝒢).adjoinNegOne

Adjoining -1 commutes with taking images under a homomorphism that preserves negation.

theorem Subgroup.adjoinNegOne_mono {G : Type u_2} [Group G] [HasDistribNeg G] {𝒢 ℋ : Subgroup G} (h : 𝒢 ≤ ℋ) : 𝒢.adjoinNegOne ≤ ℋ.adjoinNegOne

Adjoining -1 preserves inclusion.

theorem Subgroup.adjoinNegOne_conj {G : Type u_2} [Group G] [HasDistribNeg G] (𝒢 : Subgroup G) (g : ConjAct G) : (g • 𝒢).adjoinNegOne = g • 𝒢.adjoinNegOne

Adjoining -1 commutes with conjugation.

instance instDiscreteTopologySubtypeGeneralLinearGroupMemSubgroupAdjoinNegOneOfIsTopologicalRingOfT2Space {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [Ring R] [TopologicalSpace R] [IsTopologicalRing R] [T2Space R] (𝒢 : Subgroup (GL n R)) [DiscreteTopology ↥𝒢] : DiscreteTopology ↥𝒢.adjoinNegOne

@[simp]

theorem Subgroup.hasDetPlusMinusOne_adjoinNegOne_iff {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_3} [CommRing R] {𝒢 : Subgroup (GL n R)} : 𝒢.adjoinNegOne.HasDetPlusMinusOne ↔ 𝒢.HasDetPlusMinusOne

theorem Subgroup.hasDetOne_adjoinNegOne_iff {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_3} [CommRing R] {𝒢 : Subgroup (GL n R)} (hn : Even (Fintype.card n)) : 𝒢.adjoinNegOne.HasDetOne ↔ 𝒢.HasDetOne

instance instHasDetPlusMinusOneAdjoinNegOneGeneralLinearGroup {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_3} [CommRing R] {𝒢 : Subgroup (GL n R)} [𝒢.HasDetPlusMinusOne] : 𝒢.adjoinNegOne.HasDetPlusMinusOne

instance instHasDetOneAdjoinNegOneGeneralLinearGroupOfFactEvenNatCard {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_3} [CommRing R] {𝒢 : Subgroup (GL n R)} [𝒢.HasDetOne] [Fact (Even (Fintype.card n))] : 𝒢.adjoinNegOne.HasDetOne

theorem adjoinNegOne_detOnePart {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_3} [CommRing R] {G : Subgroup (GL n R)} (hn : Even (Fintype.card n)) : G.detOnePart.adjoinNegOne = G.adjoinNegOne.detOnePart

instance Subgroup.instIsArithmeticAdjoinNegOne {𝒢 : Subgroup (GL (Fin 2) ℝ)} [𝒢.IsArithmetic] : 𝒢.adjoinNegOne.IsArithmetic