Gamma0Map — Mathlib

English

There is a natural monoid homomorphism from Gamma0(N) to ZMod N given by extracting the bottom-right entry.

Русский

Существует естественный односвязный гомоморфизм из Gamma0(N) в ZMod N, который берет нижний правый элемент.

LaTeX

$$Gamma0Map(N) : Gamma0(N) →* ZMod N where toFun g = g_{11}$$

Lean4

/-- The group homomorphism from `CongruenceSubgroup.Gamma0` to `ZMod N` given by
mapping a matrix to its lower right-hand entry. -/
def Gamma0Map (N : ℕ) : Gamma0 N →* ZMod N where
  toFun g := g.1 1 1
  map_one' := by simp
  map_mul' := by
    rintro ⟨A, hA⟩ ⟨B, _⟩
    simp only [MulMemClass.mk_mul_mk, Fin.isValue, coe_mul, (two_mul_expl A.1 B).2.2.2, Int.cast_add, Int.cast_mul,
      Gamma0_mem.mp hA, zero_mul, zero_add]

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