conjGL — Mathlib

English

A simplified membership equivalence for conjGL under the action.

Русский

Упрощенное равенство принадлежности для conjGL при действии.

LaTeX

$$$$ x \in \text{conjGL}(\Gamma, g) \iff \exists y \in \Gamma: y = g x g^{-1}. $$$$

Lean4

/-- If `Γ` is a congruence subgroup, then so is `g⁻¹ Γ g ∩ SL(2, ℤ)` for any `g ∈ GL(2, ℚ)`. -/
theorem conjGL {Γ : Subgroup SL(2, ℤ)} (hΓ : IsCongruenceSubgroup Γ) (g : GL (Fin 2) ℚ) :
    IsCongruenceSubgroup (conjGL Γ (g.map <| Rat.castHom ℝ)) :=
  by
  obtain ⟨M, hN, hΓM⟩ := hΓ
  haveI _ : NeZero M := ⟨hN⟩
  obtain ⟨N, hN, hN'⟩ := exists_Gamma_le_conj' g M
  rw [Subgroup.pointwise_smul_subset_iff] at hN'
  refine ⟨N, ‹_›, fun x hx ↦ ?_⟩
  obtain ⟨y, hy, hy'⟩ := Subgroup.mem_inv_pointwise_smul_iff.mp <| hN' ⟨x, hx, rfl⟩
  exact mem_conjGL.mpr ⟨y, hΓM hy, hy'⟩

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