The Chinese remainder splitting of ZMod N at an exact divisor

For an exact divisor Q of N (Q ∣ N with Q coprime to N / Q) the Chinese remainder theorem splits ZMod N as ZMod Q × ZMod (N / Q). This file records the splitting through its idempotent, the residue e_Q that is 1 modulo Q and 0 modulo N / Q, rather than through a ring isomorphism with a product, so that no cast between ZMod N and ZMod (Q * (N / Q)) is ever needed.

Inverting the Q-component of a unit and fixing its N / Q-component is then the automorphism u ↦ e_Q u⁻¹ + (1 - e_Q) u of (ZMod N)ˣ, the instance of IsIdempotentElem.unitsInvPart at e_Q. On characters it is the operation χ_Q · χ_{N/Q} ↦ χ_Q⁻¹ · χ_{N/Q}, inverting the Q-part of a character and keeping its N / Q-part. This is how the Atkin–Lehner operator W_Q moves the nebentypus of a modular form of level N. At Q = N it is inversion, the shift χ ↦ χ⁻¹ of the Fricke operator, and at Q = 1 it is the identity.

Main definitions

• TauCeti.exactDivisorIdempotent N Q: the residue e_Q = (N / Q) · y of ZMod N, for the Bézout coefficient y of Q · x + (N / Q) · y = 1.
• TauCeti.Nat.IsExactDivisor.unitsInvPart: the automorphism of (ZMod N)ˣ inverting the residue modulo Q and fixing the residue modulo N / Q.

Main results

• TauCeti.Nat.IsExactDivisor.eq_of_castHom_eq: an element of ZMod N is determined by its residues modulo Q and modulo N / Q.
• TauCeti.Nat.IsExactDivisor.eq_exactDivisorIdempotent_iff: e_Q is the residue that is 1 modulo Q and 0 modulo N / Q; it is idempotent (TauCeti.Nat.IsExactDivisor.isIdempotentElem_exactDivisorIdempotent).
• TauCeti.Nat.IsExactDivisor.eq_unitsInvPart_iff: the unit unitsInvPart u is characterized by its residues, u⁻¹ modulo Q and u modulo N / Q.
• TauCeti.Nat.IsExactDivisor.comp_unitsInvPart: on a character χ_Q · χ_{N/Q} pulled back from the two factors, precomposition with unitsInvPart inverts χ_Q.
• TauCeti.Nat.IsExactDivisor.unitsInvPart_self, TauCeti.Nat.IsExactDivisor.unitsInvPart_one: at Q = N it is inversion, and at Q = 1 the identity.

References

• A. O. L. Atkin and W.-C. W. Li, Twists of newforms and pseudo-eigenvalues of W-operators, Invent. Math. 48 (1978), 221–243, §1.

def TauCeti.exactDivisorIdempotent (N Q : ℕ) : ZMod N

The residue e_Q of ZMod N that is 1 modulo Q and 0 modulo N / Q, when Q is an exact divisor of N (Nat.IsExactDivisor.eq_exactDivisorIdempotent_iff). It is (N / Q) · y for the Bézout coefficient y of Q · x + (N / Q) · y = 1, the coefficient that also builds the Atkin–Lehner matrix TauCeti.atkinLehnerMatrix N Q.

Equations

• TauCeti.exactDivisorIdempotent N Q = ↑(↑(N / Q) * Q.gcdB (N / Q))

theorem TauCeti.Nat.IsExactDivisor.eq_of_castHom_eq {N Q : ℕ} (h : IsExactDivisor Q N) {x y : ZMod N} (hQ : (ZMod.castHom ⋯ (ZMod Q)) x = (ZMod.castHom ⋯ (ZMod Q)) y) (hR : (ZMod.castHom ⋯ (ZMod (N / Q))) x = (ZMod.castHom ⋯ (ZMod (N / Q))) y) : x = y

An element of ZMod N is determined by its residues modulo Q and modulo N / Q, for an exact divisor Q of N: the injectivity half of the Chinese remainder theorem.

theorem TauCeti.Nat.IsExactDivisor.castHom_exactDivisorIdempotent_left {N Q : ℕ} (h : IsExactDivisor Q N) : (ZMod.castHom ⋯ (ZMod Q)) (exactDivisorIdempotent N Q) = 1

e_Q is 1 modulo Q.

theorem TauCeti.Nat.IsExactDivisor.castHom_exactDivisorIdempotent_right {N Q : ℕ} (h : IsExactDivisor Q N) : (ZMod.castHom ⋯ (ZMod (N / Q))) (exactDivisorIdempotent N Q) = 0

e_Q is 0 modulo N / Q.

theorem TauCeti.Nat.IsExactDivisor.eq_exactDivisorIdempotent_iff {N Q : ℕ} (h : IsExactDivisor Q N) {x : ZMod N} : x = exactDivisorIdempotent N Q ↔ (ZMod.castHom ⋯ (ZMod Q)) x = 1 ∧ (ZMod.castHom ⋯ (ZMod (N / Q))) x = 0

e_Q is the residue that is 1 modulo Q and 0 modulo N / Q.

theorem TauCeti.Nat.IsExactDivisor.isIdempotentElem_exactDivisorIdempotent {N Q : ℕ} (h : IsExactDivisor Q N) : IsIdempotentElem (exactDivisorIdempotent N Q)

e_Q is idempotent: e_Q ^ 2 has the same residues 1 and 0.

def TauCeti.Nat.IsExactDivisor.unitsInvPart {N Q : ℕ} (h : IsExactDivisor Q N) : (ZMod N)ˣ ≃* (ZMod N)ˣ

Inverting the residue modulo Q: for an exact divisor Q of N, the automorphism u ↦ e_Q u⁻¹ + (1 - e_Q) u of (ZMod N)ˣ, which inverts the residue of a unit modulo Q and fixes its residue modulo N / Q (Nat.IsExactDivisor.eq_unitsInvPart_iff).

Equations

• h.unitsInvPart = ⋯.unitsInvPart

theorem TauCeti.Nat.IsExactDivisor.coe_unitsInvPart {N Q : ℕ} (h : IsExactDivisor Q N) (u : (ZMod N)ˣ) : ↑(h.unitsInvPart u) = exactDivisorIdempotent N Q * ↑u⁻¹ + (1 - exactDivisorIdempotent N Q) * ↑u

The value of unitsInvPart at a unit u is e_Q u⁻¹ + (1 - e_Q) u.

@[simp]

theorem TauCeti.Nat.IsExactDivisor.unitsInvPart_symm {N Q : ℕ} (h : IsExactDivisor Q N) : h.unitsInvPart.symm = h.unitsInvPart

unitsInvPart is an involution: it is its own inverse.

@[simp]

theorem TauCeti.Nat.IsExactDivisor.unitsInvPart_unitsInvPart {N Q : ℕ} (h : IsExactDivisor Q N) (u : (ZMod N)ˣ) : h.unitsInvPart (h.unitsInvPart u) = u

unitsInvPart is an involution, applied twice to a unit.

@[simp]

theorem TauCeti.Nat.IsExactDivisor.unitsMap_unitsInvPart_left {N Q : ℕ} (h : IsExactDivisor Q N) (u : (ZMod N)ˣ) : (ZMod.unitsMap ⋯) (h.unitsInvPart u) = ((ZMod.unitsMap ⋯) u)⁻¹

unitsInvPart inverts the residue modulo Q.

@[simp]

theorem TauCeti.Nat.IsExactDivisor.unitsMap_unitsInvPart_right {N Q : ℕ} (h : IsExactDivisor Q N) (u : (ZMod N)ˣ) : (ZMod.unitsMap ⋯) (h.unitsInvPart u) = (ZMod.unitsMap ⋯) u

unitsInvPart fixes the residue modulo N / Q.

theorem TauCeti.Nat.IsExactDivisor.eq_unitsInvPart_iff {N Q : ℕ} (h : IsExactDivisor Q N) {u v : (ZMod N)ˣ} : v = h.unitsInvPart u ↔ (ZMod.unitsMap ⋯) v = ((ZMod.unitsMap ⋯) u)⁻¹ ∧ (ZMod.unitsMap ⋯) v = (ZMod.unitsMap ⋯) u

unitsInvPart u is the unit with residue u⁻¹ modulo Q and u modulo N / Q.

theorem TauCeti.Nat.IsExactDivisor.comp_unitsInvPart {N Q : ℕ} {G : Type u_1} [CommGroup G] (h : IsExactDivisor Q N) (ψ : (ZMod Q)ˣ →* G) (φ : (ZMod (N / Q))ˣ →* G) : (ψ.comp (ZMod.unitsMap ⋯) * φ.comp (ZMod.unitsMap ⋯)).comp h.unitsInvPart.toMonoidHom = ψ⁻¹.comp (ZMod.unitsMap ⋯) * φ.comp (ZMod.unitsMap ⋯)

The character shift χ_Q · χ_{N/Q} ↦ χ_Q⁻¹ · χ_{N/Q}: on a character of (ZMod N)ˣ pulled back from a character ψ modulo Q and a character φ modulo N / Q, precomposition with unitsInvPart inverts ψ and keeps φ.

@[simp]

theorem TauCeti.Nat.IsExactDivisor.unitsInvPart_self {N : ℕ} (h : IsExactDivisor N N) : h.unitsInvPart = MulEquiv.inv (ZMod N)ˣ

At Q = N the automorphism is inversion: every residue is a residue modulo Q.

@[simp]

theorem TauCeti.Nat.IsExactDivisor.unitsInvPart_one {N : ℕ} (h : IsExactDivisor 1 N) : h.unitsInvPart = MulEquiv.refl (ZMod N)ˣ

At Q = 1 the automorphism is the identity: every residue is a residue modulo N / Q.