Correcting a vector by invariant submodules of two idempotents

Let e and f be idempotent endomorphisms, P a submodule stable under f and Q one stable under e. If e ξ and f ξ lie in P ⊔ Q, then ξ can be corrected by an element ι ∈ P ⊔ Q so that e (ξ - ι) ∈ Q and f (ξ - ι) ∈ P. This is the existence half of Lemma 3 of Popa and Zagier. There ℛ is the space spanned by integral matrices of positive determinant, on which PSL(2, ℤ) acts on both sides, and π_S = (1 + S) / 2 and π_U = (1 + U + U²) / 3 are idempotents. The maps are right multiplications, e ξ = ξ π_S and f ξ = ξ π_U, while P = π_S ℛ and Q = π_U ℛ are the images of left multiplication by π_S and π_U; they are stable under f and e because left and right multiplication commute. The hypotheses say that ξ lies in their set 𝒜, and ξ - ι = ξ - ξ_S - ξ_U is the image of ξ under their projection onto ℬ.

Main results

• TauCeti.End.exists_mem_sup_apply_sub_mem_of_isIdempotentElem: the correction ι ∈ P ⊔ Q above exists.

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, Lemma 3.

theorem TauCeti.End.exists_mem_sup_apply_sub_mem_of_isIdempotentElem {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {e f : Module.End R M} (he : IsIdempotentElem e) (hf : IsIdempotentElem f) {P Q : Submodule R M} (hP : P ∈ f.invtSubmodule) (hQ : Q ∈ e.invtSubmodule) {ξ : M} (heξ : e ξ ∈ P ⊔ Q) (hfξ : f ξ ∈ P ⊔ Q) : ∃ ι ∈ P ⊔ Q, e (ξ - ι) ∈ Q ∧ f (ξ - ι) ∈ P

Popa–Zagier's projection, existence half (Lemma 3): let e and f be idempotent, P a submodule stable under f and Q one stable under e. If e ξ and f ξ lie in P ⊔ Q, then there is ι ∈ P ⊔ Q with e (ξ - ι) ∈ Q and f (ξ - ι) ∈ P.

The scalars form a ring rather than a semiring: over a semiring a submodule need not be closed under negation, and the statement then fails.