Kernels of commuting endomorphisms

A linear map f intertwining endomorphisms d and e, that is with f ∘ d = e ∘ f, sends the kernel of d into the kernel of e (LinearMap.map_mem_ker_of_comp_eq); this is how a chain map acts on cycles.

Let r₁ and r₂ be endomorphisms of a module M with ker r₁ ⊓ ker r₂ = ⊥, let l₁ and l₂ be endomorphisms commuting with both, and let Y ≤ ker r₁ and Z ≤ ker r₂ be submodules. If ξ ∈ Y ⊔ Z satisfies r₁ ξ ∈ ker l₂ and r₂ ξ ∈ ker l₁, then ξ ∈ (Y ⊓ ker l₁) ⊔ (Z ⊓ ker l₂).

This is the exactness step in the proof of §3 Theorem 2 of Popa and Zagier, with r₁, r₂ the right multiplications by π_S, π_U on their ℛ (whose kernels meet trivially by the right-action form of their Lemma 2), l₁, l₂ the left multiplications by 1 - π_S, 1 - π_U, Y = ℛ (1 - π_S) and Z = ℛ (1 - π_U): an element of Y + Z in their ℬ (6) is in their 𝒥 (7).

Main results

• LinearMap.map_mem_ker_of_comp_eq: an intertwining map sends kernel to kernel.
• TauCeti.End.mem_inf_ker_sup_inf_ker_of_mem_sup: the splitting statement above.

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, proof of Theorem 2.

theorem LinearMap.map_mem_ker_of_comp_eq {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {d : M →ₗ[R] M} {e : N →ₗ[R] N} (f : M →ₗ[R] N) (hf : f ∘ₗ d = e ∘ₗ f) {x : M} (hx : x ∈ d.ker) : f x ∈ e.ker

A linear map f with f ∘ d = e ∘ f sends the kernel of d into the kernel of e.

theorem TauCeti.End.mem_inf_ker_sup_inf_ker_of_mem_sup {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {l₁ l₂ r₁ r₂ : Module.End R M} (h₁₁ : Commute l₁ r₁) (h₁₂ : Commute l₁ r₂) (h₂₁ : Commute l₂ r₁) (h₂₂ : Commute l₂ r₂) (hr : Disjoint (LinearMap.ker r₁) (LinearMap.ker r₂)) {Y Z : Submodule R M} (hY : Y ≤ LinearMap.ker r₁) (hZ : Z ≤ LinearMap.ker r₂) {ξ : M} (hξ : ξ ∈ Y ⊔ Z) (hr₁ξ : r₁ ξ ∈ LinearMap.ker l₂) (hr₂ξ : r₂ ξ ∈ LinearMap.ker l₁) : ξ ∈ Y ⊓ LinearMap.ker l₁ ⊔ Z ⊓ LinearMap.ker l₂

Splitting along disjoint kernels of commuting endomorphisms: let r₁ and r₂ have disjoint kernels and let l₁, l₂ commute with both. If ξ ∈ Y ⊔ Z for submodules Y ≤ ker r₁ and Z ≤ ker r₂, and r₁ ξ ∈ ker l₂, r₂ ξ ∈ ker l₁, then ξ ∈ Y ⊓ ker l₁ ⊔ Z ⊓ ker l₂.