conj — Mathlib

English

Conjugation by GL(2, Z) acts compatibly with the congruence subgroup structure: conjGL Γ g = (toConjAct g⁻¹) • Γ.

Русский

Конъуграция by GL(2, Z) сохраняет структуру конгруэнтных подгрупп: conjGL Γ g = (toConjAct g⁻¹) • Γ.

LaTeX

$$$$ \text{conjGL}(\Gamma, g) = (toConjAct\, g^{-1}) \cdot \Gamma. $$$$

Lean4

/-- Conjugation by `GL(2, ℚ)` preserves arithmetic subgroups. -/
theorem _root_.Subgroup.IsArithmetic.conj (𝒢 : Subgroup (GL (Fin 2) ℝ)) [𝒢.IsArithmetic] (g : GL (Fin 2) ℚ) :
    (toConjAct (g.map (Rat.castHom ℝ)) • 𝒢).IsArithmetic :=
  ⟨(Subgroup.IsArithmetic.is_commensurable.conj _).trans (isArithmetic_conj_SL2Z g).is_commensurable⟩

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