Operators of order two and three: Choie–Zagier criterion, Popa–Zagier's projection and exactness

The group PSL(2, ℤ) is generated by S of order two and U of order three, and T = U S. Popa and Zagier's proof of the Eichler–Selberg trace formula works in the rational vector space ℛ = ℚ[ℳ] spanned by integral matrices of positive determinant modulo ±1, on which PSL(2, ℤ) acts on both sides. The idempotents π_S = (1 + S) / 2 and π_U = (1 + U + U²) / 3 generate the right ideal

𝓘 = π_S ℛ + π_U ℛ

(their (5)). This file records the linear algebra behind their Lemmas 1 and 3 and the exactness step in the proof of their §3 Theorem 2, for endomorphisms σ and υ of a module M with σ ^ 2 = 1 and υ ^ 3 = 1, which are the left multiplications by S and U; the right multiplications by S and U give a second such pair σ', υ', commuting with the first. The ideal 𝓘 becomes the submodule range (1 + σ) ⊔ range (1 + υ + υ ^ 2): when 2 and 3 are invertible the unnormalised operators have the same ranges as the idempotents, and the unnormalised form needs no invertibility where none is used.

Main results

• TauCeti.End.one_sub_apply_mem_range_one_sub_mul_iff: the Choie–Zagier criterion (Popa–Zagier, Lemma 1): if 2 and 3 are invertible and ker (1 + σ) and ker (1 + υ + υ ^ 2) are disjoint, then x ∈ range (1 + σ) ⊔ range (1 + υ + υ ^ 2) exactly when (1 - σ) x ∈ range (1 - υ * σ), that is, ξ ∈ 𝓘 ↔ (1 - S) ξ ∈ (1 - T) ℛ. The forward direction, TauCeti.End.one_sub_apply_mem_range_one_sub_mul_of_mem_sup, needs neither hypothesis.
• TauCeti.End.exists_mem_sup_one_add_apply_sub_mem: the existence half of Popa–Zagier's Lemma 3 for the idempotents (1 + σ) / 2 and (1 + υ + υ ^ 2) / 3, stated with the unnormalised operators: if (1 + σ) ξ and (1 + υ + υ ^ 2) ξ lie in P ⊔ Q, for submodules P and Q stable under 1 + υ + υ ^ 2 and 1 + σ, then ξ can be corrected by an element ι of P ⊔ Q so that (1 + σ) (ξ - ι) ∈ Q and (1 + υ + υ ^ 2) (ξ - ι) ∈ P.
• TauCeti.End.mem_sup_range_one_add_mul_one_sub: exactness in Popa–Zagier's §3 Theorem 2: if 2 and 3 are invertible and ker (1 + σ'), ker (1 + υ' + υ' ^ 2) are disjoint, then a vector ξ ∈ range (1 - σ') ⊔ range (1 - υ') with (1 + σ') ξ ∈ range (1 + υ + υ ^ 2) and (1 + υ' + υ' ^ 2) ξ ∈ range (1 + σ) lies in range ((1 + σ) (1 - σ')) ⊔ range ((1 + υ + υ ^ 2) (1 - υ')), that is, an element of their ℬ (6) whose right coset sums vanish lies in 𝒥 = π_S ℛ (1 - π_S) + π_U ℛ (1 - π_U) (7).
• TauCeti.one_sub_mul_one_add_add_sq: the ring identity (1 - σ) (1 + υ + υ ^ 2) = (1 - υ σ) (-σ (1 + υ + υ ^ 2)) for σ ^ 2 = 1 and υ ^ 3 = 1, and its mirror image TauCeti.one_add_add_sq_mul_one_sub, for right multiplications.
• TauCeti.one_sub_mul_one_add_of_sq_eq_one, TauCeti.one_add_mul_one_sub_of_sq_eq_one, TauCeti.one_sub_mul_one_add_add_sq_of_pow_three_eq_one, TauCeti.one_add_add_sq_mul_one_sub_of_pow_three_eq_one: (1 ∓ σ) (1 ± σ) = 0 for σ ^ 2 = 1, and (1 - υ) (1 + υ + υ ^ 2) = (1 + υ + υ ^ 2) (1 - υ) = 0 for υ ^ 3 = 1.
• TauCeti.End.range_one_add_eq_ker_one_sub, TauCeti.End.range_one_add_add_sq_eq_ker_one_sub: the fixed vectors of σ and of υ are the ranges of 1 + σ and of 1 + υ + υ ^ 2. The inclusions TauCeti.End.range_one_add_le_ker_one_sub and TauCeti.End.range_one_add_add_sq_le_ker_one_sub need no invertibility, and the reverse inclusions hold inside any submodule Y without the order hypotheses: TauCeti.End.inf_ker_one_sub_le_map_one_add and TauCeti.End.inf_ker_one_sub_le_map_one_add_add_sq (Y ⊓ ker (1 - σ) ≤ Y.map (1 + σ) when 2 is invertible, and likewise with 3).
• TauCeti.End.range_one_sub_le_ker_one_add, TauCeti.End.range_one_sub_le_ker_one_add_add_sq: dually, 1 + σ kills range (1 - σ) and 1 + υ + υ ^ 2 kills range (1 - υ).

Implementation notes

The ring identities are proved in an arbitrary ring and then applied in Module.End; the acyclicity hypothesis is stated as Disjoint (ker (1 + σ)) (ker (1 + υ + υ ^ 2)). The existence half of Lemma 3 for arbitrary idempotents is TauCeti.End.exists_mem_sup_apply_sub_mem_of_isIdempotentElem, and the exactness step for arbitrary commuting endomorphisms is TauCeti.End.mem_inf_ker_sup_inf_ker_iff.

References

• A. Popa and D. Zagier, An elementary proof of the Eichler–Selberg trace formula, J. Reine Angew. Math. 762 (2020), 105–122, arXiv:1711.00327, Section 3, Lemmas 1 and 3 and the proof of Theorem 2.
• Y. J. Choie and D. Zagier, Rational period functions for PSL(2, ℤ), Contemp. Math. 143 (1993), 89–108.

theorem TauCeti.one_sub_mul_one_add_of_sq_eq_one {A : Type u_1} [Ring A] {σ : A} (hσ : σ ^ 2 = 1) : (1 - σ) * (1 + σ) = 0

(1 - σ) (1 + σ) = 0 for σ ^ 2 = 1.

theorem TauCeti.one_add_mul_one_sub_of_sq_eq_one {A : Type u_1} [Ring A] {σ : A} (hσ : σ ^ 2 = 1) : (1 + σ) * (1 - σ) = 0

(1 + σ) (1 - σ) = 0 for σ ^ 2 = 1.

theorem TauCeti.one_sub_mul_one_add_add_sq_of_pow_three_eq_one {A : Type u_1} [Ring A] {υ : A} (hυ : υ ^ 3 = 1) : (1 - υ) * (1 + υ + υ ^ 2) = 0

(1 - υ) (1 + υ + υ²) = 0 for υ ^ 3 = 1.

theorem TauCeti.one_add_add_sq_mul_one_sub_of_pow_three_eq_one {A : Type u_1} [Ring A] {υ : A} (hυ : υ ^ 3 = 1) : (1 + υ + υ ^ 2) * (1 - υ) = 0

(1 + υ + υ²) (1 - υ) = 0 for υ ^ 3 = 1.

theorem TauCeti.one_sub_mul_one_add_add_sq {A : Type u_1} [Ring A] {σ υ : A} (hσ : σ ^ 2 = 1) (hυ : υ ^ 3 = 1) : (1 - σ) * (1 + υ + υ ^ 2) = (1 - υ * σ) * -(σ * (1 + υ + υ ^ 2))

(1 - σ) (1 + υ + υ²) lies in (1 - υ σ) A when σ ^ 2 = 1 and υ ^ 3 = 1. This is Popa–Zagier's relation (1 - S) π_U = (1 - T⁻¹) π_U for T = U S, rewritten through 1 - T⁻¹ = (1 - T) (-T⁻¹), and it is the forward direction of the Choie–Zagier criterion.

theorem TauCeti.one_add_add_sq_mul_one_sub {A : Type u_1} [Ring A] {σ υ : A} (hσ : σ ^ 2 = 1) (hυ : υ ^ 3 = 1) : (1 + υ + υ ^ 2) * (1 - σ) = -((1 + υ + υ ^ 2) * σ) * (1 - σ * υ)

(1 + υ + υ²) (1 - σ) = -((1 + υ + υ²) σ) (1 - σ υ) for σ ^ 2 = 1 and υ ^ 3 = 1: the mirror image of TauCeti.one_sub_mul_one_add_add_sq, for right multiplications.

theorem TauCeti.End.range_one_add_le_ker_one_sub {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommGroup M] [Module R M] {σ : Module.End R M} (hσ : σ ^ 2 = 1) : (1 + σ).range ≤ (1 - σ).ker

For σ ^ 2 = 1, the vectors (1 + σ) x are fixed by σ.

theorem TauCeti.End.range_one_sub_le_ker_one_add {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommGroup M] [Module R M] {σ : Module.End R M} (hσ : σ ^ 2 = 1) : (1 - σ).range ≤ (1 + σ).ker

For σ ^ 2 = 1, the vectors (1 - σ) x are killed by 1 + σ.

theorem TauCeti.End.inf_ker_one_sub_le_map_one_add {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommGroup M] [Module R M] {σ : Module.End R M} [Invertible 2] (Y : Submodule R M) : Y ⊓ (1 - σ).ker ≤ Submodule.map (1 + σ) Y

When 2 is invertible, a vector y ∈ Y fixed by σ is (1 + σ) (y / 2).

theorem TauCeti.End.range_one_add_eq_ker_one_sub {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommGroup M] [Module R M] {σ : Module.End R M} [Invertible 2] (hσ : σ ^ 2 = 1) : (1 + σ).range = (1 - σ).ker

The fixed vectors of an involution are the range of 1 + σ, when 2 is invertible.

theorem TauCeti.End.inf_ker_one_sub_le_map_one_add_add_sq {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommGroup M] [Module R M] {υ : Module.End R M} [Invertible 3] (Y : Submodule R M) : Y ⊓ (1 - υ).ker ≤ Submodule.map (1 + υ + υ ^ 2) Y

When 3 is invertible, a vector y ∈ Y fixed by υ is (1 + υ + υ²) (y / 3).

theorem TauCeti.End.range_one_add_add_sq_le_ker_one_sub {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommGroup M] [Module R M] {υ : Module.End R M} (hυ : υ ^ 3 = 1) : (1 + υ + υ ^ 2).range ≤ (1 - υ).ker

For υ ^ 3 = 1, the vectors (1 + υ + υ²) x are fixed by υ.

theorem TauCeti.End.range_one_sub_le_ker_one_add_add_sq {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommGroup M] [Module R M] {υ : Module.End R M} (hυ : υ ^ 3 = 1) : (1 - υ).range ≤ (1 + υ + υ ^ 2).ker

For υ ^ 3 = 1, the vectors (1 - υ) x are killed by 1 + υ + υ².

theorem TauCeti.End.range_one_add_add_sq_eq_ker_one_sub {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommGroup M] [Module R M] {υ : Module.End R M} [Invertible 3] (hυ : υ ^ 3 = 1) : (1 + υ + υ ^ 2).range = (1 - υ).ker

The fixed vectors of an endomorphism υ with υ ^ 3 = 1 are the range of 1 + υ + υ², when 3 is invertible.

theorem TauCeti.End.one_sub_apply_mem_range_one_sub_mul_of_mem_sup {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommGroup M] [Module R M] {σ υ : Module.End R M} (hσ : σ ^ 2 = 1) (hυ : υ ^ 3 = 1) {x : M} (hx : x ∈ (1 + σ).range ⊔ (1 + υ + υ ^ 2).range) : (1 - σ) x ∈ (1 - υ * σ).range

The Choie–Zagier criterion, forward direction (Popa–Zagier, Lemma 1, ⇒): for σ ^ 2 = 1 and υ ^ 3 = 1, if x ∈ range (1 + σ) ⊔ range (1 + υ + υ²) then (1 - σ) x ∈ range (1 - υ σ). No invertibility is needed.

theorem TauCeti.End.disjoint_range_one_sub_of_disjoint_ker {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommGroup M] [Module R M] {σ υ : Module.End R M} (hσ : σ ^ 2 = 1) (hυ : υ ^ 3 = 1) (hacyc : Disjoint (1 + σ).ker (1 + υ + υ ^ 2).ker) : Disjoint (1 - σ).range (1 - υ).range

The ranges of 1 - σ and 1 - υ are disjoint when σ ^ 2 = 1, υ ^ 3 = 1 and ker (1 + σ), ker (1 + υ + υ²) are disjoint.

theorem TauCeti.End.one_sub_apply_mem_range_one_sub_mul_iff {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommGroup M] [Module R M] {σ υ : Module.End R M} [Invertible 2] [Invertible 3] (hσ : σ ^ 2 = 1) (hυ : υ ^ 3 = 1) (hacyc : Disjoint (1 + σ).ker (1 + υ + υ ^ 2).ker) {x : M} : (1 - σ) x ∈ (1 - υ * σ).range ↔ x ∈ (1 + σ).range ⊔ (1 + υ + υ ^ 2).range

The Choie–Zagier criterion (Popa–Zagier, Lemma 1): for σ ^ 2 = 1 and υ ^ 3 = 1 with 2 and 3 invertible and ker (1 + σ), ker (1 + υ + υ²) disjoint, a vector x lies in range (1 + σ) ⊔ range (1 + υ + υ²) exactly when (1 - σ) x ∈ range (1 - υ σ).

theorem TauCeti.End.mem_sup_range_one_add_mul_one_sub {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommGroup M] [Module R M] {σ υ : Module.End R M} [Invertible 2] [Invertible 3] {σ' υ' : Module.End R M} (hσ : σ ^ 2 = 1) (hυ : υ ^ 3 = 1) (hσ' : σ' ^ 2 = 1) (hυ' : υ' ^ 3 = 1) (hσσ' : Commute σ σ') (hσυ' : Commute σ υ') (hυσ' : Commute υ σ') (hυυ' : Commute υ υ') (hacyc : Disjoint (1 + σ').ker (1 + υ' + υ' ^ 2).ker) {ξ : M} (hξ : ξ ∈ (1 - σ').range ⊔ (1 - υ').range) (hσ'ξ : (1 + σ') ξ ∈ (1 + υ + υ ^ 2).range) (hυ'ξ : (1 + υ' + υ' ^ 2) ξ ∈ (1 + σ).range) : ξ ∈ ((1 + σ) * (1 - σ')).range ⊔ ((1 + υ + υ ^ 2) * (1 - υ')).range

Exactness in Popa–Zagier's §3 Theorem 2: for σ ^ 2 = σ' ^ 2 = 1 and υ ^ 3 = υ' ^ 3 = 1, with σ and υ commuting with σ' and υ', 2 and 3 invertible and ker (1 + σ'), ker (1 + υ' + υ'²) disjoint: if ξ ∈ range (1 - σ') ⊔ range (1 - υ'), (1 + σ') ξ ∈ range (1 + υ + υ²) and (1 + υ' + υ'²) ξ ∈ range (1 + σ), then ξ ∈ range ((1 + σ) (1 - σ')) ⊔ range ((1 + υ + υ²) (1 - υ')).

For the left multiplications σ, υ and the right multiplications σ', υ' by S, U on ℛ, the hypotheses on ξ say that ξ ∈ ℛ (1 - S) + ℛ (1 - U), the elements whose right coset sums vanish, and that ξ lies in their ℬ = {ξ | ξ π_S ∈ π_U ℛ, ξ π_U ∈ π_S ℛ} (6); the conclusion is ξ ∈ 𝒥 = π_S ℛ (1 - π_S) + π_U ℛ (1 - π_U) (7).

theorem TauCeti.End.exists_mem_sup_one_add_apply_sub_mem {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {σ υ : Module.End R M} [Invertible 2] [Invertible 3] (hσ : σ ^ 2 = 1) (hυ : υ ^ 3 = 1) {P Q : Submodule R M} (hP : P ∈ (1 + υ + υ ^ 2).invtSubmodule) (hQ : Q ∈ (1 + σ).invtSubmodule) {ξ : M} (hσξ : (1 + σ) ξ ∈ P ⊔ Q) (hυξ : (1 + υ + υ ^ 2) ξ ∈ P ⊔ Q) : ∃ ι ∈ P ⊔ Q, (1 + σ) (ξ - ι) ∈ Q ∧ (1 + υ + υ ^ 2) (ξ - ι) ∈ P

Popa–Zagier's projection for operators of order two and three (Lemma 3, existence half): for σ ^ 2 = 1 and υ ^ 3 = 1 with 2 and 3 invertible, P stable under 1 + υ + υ² and Q under 1 + σ, if (1 + σ) ξ and (1 + υ + υ²) ξ lie in P ⊔ Q, then there is ι ∈ P ⊔ Q with (1 + σ) (ξ - ι) ∈ Q and (1 + υ + υ²) (ξ - ι) ∈ P. This is TauCeti.End.exists_mem_sup_apply_sub_mem_of_isIdempotentElem for the idempotents (1 + σ) / 2 and (1 + υ + υ²) / 3; the ring R need not be commutative, since 2 and 3 are central.