English
A Gamma1 element maps to Gamma0 with exact residue conditions on diagonals.
Русский
Элемент Gamma1 отображается в Gamma0 с точными условиями по диагоналям.
LaTeX
$$A ∈ Gamma1'(N) ⇒ (A.1 0 0 : ZMod N) = 1 ∧ ...$$
Lean4
theorem Gamma1_to_Gamma0_mem {N} (A : Gamma0 N) :
A ∈ Gamma1' N ↔ ((A.1 0 0 : ℤ) : ZMod N) = 1 ∧ ((A.1 1 1 : ℤ) : ZMod N) = 1 ∧ ((A.1 1 0 : ℤ) : ZMod N) = 0 :=
by
constructor
· intro ha
have adet : (A.1.1.det : ZMod N) = 1 := by simp only [A.1.property, Int.cast_one]
rw [Matrix.det_fin_two] at adet
simp only [Gamma1_mem', Gamma0Map, MonoidHom.coe_mk, OneHom.coe_mk, Int.cast_sub, Int.cast_mul] at *
simpa only [Gamma1_mem', Gamma0Map, MonoidHom.coe_mk, OneHom.coe_mk, Int.cast_sub, Int.cast_mul, ha,
Gamma0_mem.mp A.property, and_self_iff, and_true, mul_one, mul_zero, sub_zero] using adet
· intro ha
simp only [Gamma1_mem', Gamma0Map, MonoidHom.coe_mk]
exact ha.2.1
