Congruence subgroups of matrices

The level names which matrix transformations are kept and which are sent to zero.

Start with a concrete example

Think of a two-by-two table as instructions for moving a point. Here the table is [1, 0; c, 1]. For one actual example of a level-3 restriction, the lower-left entry c must be divisible by 3. Change c. Weight has a different role: it is an exponent in the transformation rule. Compare 2¹ = 2 with 2² = 4 to see what changing an exponent does; this arithmetic alone is not the full transformation rule.

Move the number or condition

c = 3; remainder after division by 3 is 0.

How this example differs from the definition

The diagram illustrates the Γ₀(3) matrix condition with determinant 1. Weight is a separate exponent in the transformation rule; it is not the number of notes or a physical weight.

A small check: try the idea

Compare the numbers in the question with the diagram you are moving. You can try again.

Which lower-left value fits the illustrated Γ₀(3) condition?

Read the answer and reasoning

6. 6 is 3×2, while 4 leaves remainder 1. The displayed matrices already have determinant 1; we are testing the lower-left restriction.

Build the idea in three steps

Arithmetic conditions can select subgroups of integer matrices. Different conditions give different congruence subgroups; Γ₀(N) does not require every entry to match the identity modulo N.
Γ₀(N) — the identifier Gamma0 in Lean — collects exactly the determinant-one integer tables whose bottom-left entry becomes 0 in ZMod N.
Gamma0Map supplies a numeric readout: it sends each collected table to its bottom-right entry in ZMod N, and multiplication of tables is preserved.

A small example

At level 5, the table with rows (1, 2) and (10, 21) has bottom-left entry 10, a multiple of 5, so it belongs to Γ₀(5).

Lean definition · original excerpt

Mathlib · db584cd · CongruenceSubgroups.lean

93/-- The group homomorphism from `CongruenceSubgroup.Gamma0` to `ZMod N` given by94mapping a matrix to its lower right-hand entry. -/95def Gamma0Map (N : ℕ) : Gamma0 N →* ZMod N where96  toFun g := g.1 1 197  map_one' := by simp98  map_mul' := by99    rintro ⟨A, hA⟩ ⟨B, _⟩

How to read this Lean

A group homomorphism is a map that respects the identity and multiplication; the declared fields toFun, map_one′ and map_mul′ state exactly that. The membership test A 1 0 = 0 appears in the adjacent theorem Gamma0_mem.

Original source ↗ · L93–99 Open the complete saved source

Where this idea is used

8. The secret duet 10. A three-note audition

Congruence subgroups of matrices

Start with a concrete example

A small check: try the idea

Build the idea in three steps

A small example

Lean definition · original excerpt

How to read this Lean

Where this idea is used

Mika’s help desk

One thing at a time

In simpler words

A small clue