English
Variant form of exists_Gamma_le_conj for rational maps and more general targets.
Русский
Вариант существования Gamma под конъуграцию для рациональных отображений и общих целей.
LaTeX
$$$$ \exists N \neq 0, \big( \text{toConjAct} \circ (g.map) \big) \Gamma_N \le \big( \Gamma_M \big).map(\cdot). $$$$
Lean4
/-- For any `g ∈ GL(2, ℚ)` and `M ≠ 0`, there exists `N` such that `g Γ(N) g⁻¹ ≤ Γ(M)`. -/
theorem exists_Gamma_le_conj' (g : GL (Fin 2) ℚ) (M : ℕ) [NeZero M] :
∃ N ≠ 0, (toConjAct <| g.map (Rat.castHom ℝ)) • (Gamma N).map (mapGL ℝ) ≤ (Gamma M).map (mapGL ℝ) :=
by
obtain ⟨N, hN, h⟩ := exists_Gamma_le_conj g M
refine ⟨N, hN, fun y hy ↦ ?_⟩
simp_rw [Subgroup.mem_pointwise_smul_iff_inv_smul_mem, Subgroup.mem_map, eq_inv_smul_iff] at hy
obtain ⟨x, hx, rfl⟩ := hy
obtain ⟨z, hz, hz'⟩ := h x hx
use z, hz
simpa only [Subtype.ext_iff, Units.ext_iff, map_mul] using congr_arg (GeneralLinearGroup.map (Rat.castHom ℝ)) hz'
