English
An element A of SL(2, Z) lies in Gamma1(N) if and only if its bottom row is congruent to (0,1) mod N (equivalently certain diagonal entries are ≡1 mod N and the bottom-left entry is ≡0 mod N).
Русский
Элемент A из SL(2, Z) принадлежит Γ1(N) тогда и только тогда, когда его нижняя строка совпадает по модулю N с (0,1) (эквивалентно A_{11} ≡ 1, A_{22} ≡ 1 и A_{21} ≡ 0 по модулю N).
LaTeX
$$$$ A \in SL(2,\mathbb{Z}) \;\Longleftrightarrow\; A_{2,1} \equiv 0 \pmod{N} \land A_{2,2} \equiv 1 \pmod{N} \land A_{1,1} \equiv 1 \pmod{N}. $$$$
Lean4
@[simp]
theorem Gamma1_mem (N : ℕ) (A : SL(2, ℤ)) :
A ∈ Gamma1 N ↔ (A 0 0 : ZMod N) = 1 ∧ (A 1 1 : ZMod N) = 1 ∧ (A 1 0 : ZMod N) = 0 :=
by
constructor
· intro ha
simp_rw [Gamma1, Subgroup.mem_map] at ha
obtain ⟨⟨x, hx⟩, hxx⟩ := ha
rw [Gamma1_to_Gamma0_mem] at hx
simp only [Subgroup.mem_top, true_and] at hxx
rw [← hxx]
convert hx
· intro ha
simp_rw [Gamma1, Subgroup.mem_map]
have hA : A ∈ Gamma0 N := by simp [ha.right.right, Gamma0_mem]
have HA : (⟨A, hA⟩ : Gamma0 N) ∈ Gamma1' N :=
by
simp only [Gamma1_to_Gamma0_mem]
exact ha
refine ⟨(⟨(⟨A, hA⟩ : Gamma0 N), HA⟩ : (Gamma1' N : Subgroup (Gamma0 N))), ?_⟩
simp
