isArithmetic_conj_SL2Z — Mathlib

English

Gamma1 is a finite-index subgroup for NeZero N.

Русский

Gamma1 является подгруппой конечного индекса при N ≠ 0.

LaTeX

$$$$ [NeZero\ N] \Rightarrow (\Gamma_1(N)).FiniteIndex. $$$$

Lean4

/-- Conjugates of `SL(2, ℤ)` by `GL(2, ℚ)` are arithmetic subgroups. -/
theorem isArithmetic_conj_SL2Z (g : GL (Fin 2) ℚ) : (toConjAct (g.map (Rat.castHom ℝ)) • 𝒮ℒ).IsArithmetic :=
  by
  constructor
  rw [MonoidHom.range_eq_map]
  constructor
  · rw [← Subgroup.relIndex_comap, Subgroup.relIndex_top_right]
    exact (finiteIndex_conjGL g⁻¹).index_ne_zero
  · rw [← Subgroup.relIndex_pointwise_smul (toConjAct (g.map (Rat.castHom ℝ)))⁻¹, inv_smul_smul, ←
      Subgroup.relIndex_comap, Subgroup.relIndex_top_right]
    exact (finiteIndex_conjGL g).index_ne_zero

Похожие утверждения