conjGL — Mathlib

English

The subgroup conjGL(Γ, g) is equal to the conjugate of Γ by g, i.e., g⁻¹ Γ g ∩ SL(2, Z) under the appropriate map.

Русский

Подгруппа conjGL(Γ, g) равна конъугату Γ по g, то есть g⁻¹ Γ g ∩ SL(2, Z) под соответствующим отображением.

LaTeX

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

Lean4

/-- The subgroup `SL(2, ℤ) ∩ g⁻¹ Γ g`, for `Γ` a subgroup of `SL(2, ℤ)` and `g ∈ GL(2, ℝ)`. -/
def conjGL (Γ : Subgroup SL(2, ℤ)) (g : GL (Fin 2) ℝ) : Subgroup SL(2, ℤ) :=
  ((toConjAct g⁻¹) • (Γ.map <| mapGL ℝ)).comap (mapGL ℝ)

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