The congruence n ∣ c d' - c' d + j c c'

For integer pairs (c, d) and (c', d'), the divisibility n ∣ c d' - c' d + j c c' for some integer j is the condition for two cusps of Γ₀(n) to be equivalent. This file records how it interacts with gcd(c, n).

Main results

• TauCeti.Int.isCoprime_div_gcd_div_gcd: dividing c and n by gcd(c, n) leaves coprime quotients.
• TauCeti.Int.gcd_dvd_of_dvd_mul_sub_mul_add_mul: if c is prime to d, the congruence forces gcd(c, n) ∣ c'.
• TauCeti.Int.gcd_eq_gcd_of_dvd_mul_sub_mul_add_mul: if both pairs are coprime, the congruence forces gcd(c, n) = gcd(c', n).
• TauCeti.Int.gcd_dvd_mul_sub_mul_of_dvd_mul_sub_mul_add_mul and TauCeti.Int.exists_dvd_mul_sub_mul_add_mul_of_gcd_dvd: writing n = g m, c = g c₁ and c' = g c₁', the congruence holds for some j exactly when gcd(g, m) ∣ c₁ d' - c₁' d (the converse needing c₁ and c₁' prime to m).

Their consumers are the cusp counts of Γ₀(N) and Γ₁(N) in TauCeti/NumberTheory/ModularForms/CongruenceSubgroups/Cusp/.

theorem TauCeti.Int.isCoprime_div_gcd_div_gcd {n : ℕ} (hn : n ≠ 0) (c : ℤ) : IsCoprime (c / ↑(c.gcd ↑n)) ↑(n / c.gcd ↑n)

Dividing an integer c and a nonzero natural number n by gcd(c, n) leaves coprime quotients. This is isCoprime_div_gcd_div_gcd with the gcd taken in ℕ, the form in which it describes c / gcd(c, n) as a residue modulo n / gcd(c, n).

theorem TauCeti.Int.gcd_dvd_of_dvd_mul_sub_mul_add_mul {n c d c' d' j : ℤ} (hcd : IsCoprime c d) (h : n ∣ c * d' - c' * d + j * c * c') : ↑(c.gcd n) ∣ c'

If n ∣ c d' - c' d + j c c' and c is prime to d, then gcd(c, n) divides c'.

theorem TauCeti.Int.gcd_eq_gcd_of_dvd_mul_sub_mul_add_mul {n c d c' d' j : ℤ} (hcd : IsCoprime c d) (hcd' : IsCoprime c' d') (h : n ∣ c * d' - c' * d + j * c * c') : c.gcd n = c'.gcd n

The congruence n ∣ c d' - c' d + j c c' between coprime pairs forces gcd(c, n) = gcd(c', n).

theorem TauCeti.Int.gcd_dvd_mul_sub_mul_of_dvd_mul_sub_mul_add_mul {n : ℤ} {g m : ℕ} {c c₁ d c' c₁' d' j : ℤ} (hg : g ≠ 0) (hn : n = ↑g * ↑m) (hc : c = ↑g * c₁) (hc' : c' = ↑g * c₁') (h : n ∣ c * d' - c' * d + j * c * c') : ↑(g.gcd m) ∣ c₁ * d' - c₁' * d

Write n = g m, c = g c₁ and c' = g c₁'. Then n ∣ c d' - c' d + j c c' implies gcd(g, m) ∣ c₁ d' - c₁' d.

theorem TauCeti.Int.exists_dvd_mul_sub_mul_add_mul_of_gcd_dvd {n : ℤ} {g m : ℕ} {c c₁ d c' c₁' d' : ℤ} (hn : n = ↑g * ↑m) (hc : c = ↑g * c₁) (hc' : c' = ↑g * c₁') (hc₁ : IsCoprime c₁ ↑m) (hc₁' : IsCoprime c₁' ↑m) (h : ↑(g.gcd m) ∣ c₁ * d' - c₁' * d) : ∃ (j : ℤ), n ∣ c * d' - c' * d + j * c * c'

Conversely, write n = g m, c = g c₁ and c' = g c₁'. If c₁ and c₁' are prime to m and gcd(g, m) ∣ c₁ d' - c₁' d, then some j satisfies n ∣ c d' - c' d + j c c'.