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

Instances

source

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

source

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

source

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

Instances

source

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

source

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

source

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

source

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

Γ.HasDetPlusMinusOne

source

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

(Γ ⊓ Γ').HasDetOne

source

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

(Γ' ⊓ Γ).HasDetOne

source

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 "𝒮ℒ")

Instances For

source

@[implicit_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 ℝ) }

source

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

Instances

source

instance Subgroup.instIsArithmeticRangeSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGL :

(Matrix.SpecialLinearGroup.mapGL ℝ).range.IsArithmetic

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

source

theorem Subgroup.isArithmetic_iff_finiteIndex {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} :

(map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ).IsArithmetic ↔ Γ.FiniteIndex

source

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.

source

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.

source

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

Γ.HasDetPlusMinusOne

source

instance Subgroup.IsArithmetic.isFiniteRelIndexSL (𝒢 : Subgroup (GL (Fin 2) ℝ)) [𝒢.IsArithmetic] :

𝒢.IsFiniteRelIndex (Matrix.SpecialLinearGroup.mapGL ℝ).range

source

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

(Γ ⊓ Γ').IsArithmetic

source

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.

source

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.

source

theorem Matrix.SpecialLinearGroup.isClosedEmbedding_mapGLInt {n : Type u_1} [Fintype n] [DecidableEq n] :

Topology.IsClosedEmbedding ⇑(mapGL ℝ)

source

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

DiscreteTopology ↥𝒢

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

source

def Subgroup.adjoinNegOne {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [Ring R] (𝒢 : Subgroup (GL n R)) :

Subgroup (GL n R)

Given a subgroup 𝒢 of GL n R, this is the subgroup generated by 𝒢 and -1.

Equations

𝒢.adjoinNegOne = { carrier := {g : GL n R | g ∈ 𝒢 ∨ -g ∈ 𝒢}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

Instances For

source

@[simp]

theorem Subgroup.mem_adjoinNegOne_iff {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [Ring R] {𝒢 : Subgroup (GL n R)} {g : GL n R} :

g ∈ 𝒢.adjoinNegOne ↔ g ∈ 𝒢 ∨ -g ∈ 𝒢

source

theorem Subgroup.le_adjoinNegOne {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [Ring R] (𝒢 : Subgroup (GL n R)) :

𝒢 ≤ 𝒢.adjoinNegOne

source

theorem Subgroup.negOne_mem_adjoinNegOne {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [Ring R] (𝒢 : Subgroup (GL n R)) :

-1 ∈ 𝒢.adjoinNegOne

source

@[simp]

theorem Subgroup.adjoinNegOne_eq_self_iff {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [Ring R] {𝒢 : Subgroup (GL n R)} :

𝒢.adjoinNegOne = 𝒢 ↔ -1 ∈ 𝒢

source

theorem Subgroup.relindex_adjoinNegOne_eq_two {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [Ring R] {𝒢 : Subgroup (GL n R)} (h𝒢 : -1 ∉ 𝒢) :

𝒢.relIndex 𝒢.adjoinNegOne = 2

source

theorem Subgroup.relIndex_adjoinNegOne_ne_zero {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [Ring R] (𝒢 : Subgroup (GL n R)) :

𝒢.relIndex 𝒢.adjoinNegOne ≠ 0

source

instance instIsFiniteRelIndexGeneralLinearGroupAdjoinNegOne {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [Ring R] (𝒢 : Subgroup (GL n R)) :

𝒢.IsFiniteRelIndex 𝒢.adjoinNegOne

source

theorem Subgroup.commensurable_adjoinNegOne_self {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [Ring R] (𝒢 : Subgroup (GL n R)) :

𝒢.adjoinNegOne.Commensurable 𝒢

source

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

source

@[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

source

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

source

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

𝒢.adjoinNegOne.HasDetPlusMinusOne

source

instance instHasDetOneAdjoinNegOneOfFactEvenNatCard {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

source

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

𝒢.adjoinNegOne.IsArithmetic

Documentation

Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Arithmetic subgroups of `GL(2, ℝ)` #

Arithmetic subgroups of GL(2, ℝ) #

Arithmetic subgroups of `GL(2, ℝ)` #