The trace of an endomorphism exchanging two subspaces

Let f be an endomorphism of a finite-dimensional vector space V that maps each of two subspaces A and B into the other. Then f preserves A ⊓ B and A ⊔ B, and its traces on the two agree. In particular, when A ⊔ B = ⊤ the trace of f is the trace of its restriction to A ⊓ B.

This is the linear algebra behind the trace reduction in Popa and Zagier's proof of the Eichler–Selberg trace formula: their modified Hecke operator exchanges A = ker(1 + S) and B = ker(1 + U + U²) in the space V_w of homogeneous polynomials of degree w, and over a field of characteristic zero and for positive even w we have A + B = V_w, so its trace on the period polynomials W_w = A ∩ B is its trace on V_w. This application is TauCeti.TraceFormulaMatrixModule.ExchangeRelations.trace_periodActionRestrict_eq_trace.

Main results

• LinearMap.trace_restrict_inf_eq_trace_restrict_sup: if f maps A and B into each other, then the traces of f on A ⊓ B and on A ⊔ B agree.
• LinearMap.trace_restrict_inf_eq_trace: if moreover A ⊔ B = ⊤, then the trace of f on A ⊓ B is the trace of f.

The proofs move traces between restrictions with two general lemmas: LinearMap.trace_restrict_congr (the traces of f on equal submodules agree) and LinearMap.trace_restrict_restrict (for p ≤ q, restricting f to q and then to p, viewed inside q, has the same trace as restricting f to p). A third general lemma, LinearMap.trace_restrict_eq_of_linearEquiv, transports the trace of a restriction along a linear equivalence intertwining two endomorphisms; it is used for graded traces of quotient algebras.

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

Traces of restrictions

theorem LinearMap.trace_restrict_congr {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {p q : Submodule R M} (hpq : p = q) (f : M →ₗ[R] M) (hp : ∀ x ∈ p, f x ∈ p) (hq : ∀ x ∈ q, f x ∈ q) : (trace R ↥p) (f.restrict hp) = (trace R ↥q) (f.restrict hq)

The traces of the restrictions of f to equal submodules agree.

theorem LinearMap.trace_restrict_restrict {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {p q : Submodule R M} (hpq : p ≤ q) {f : M →ₗ[R] M} (hp : ∀ x ∈ p, f x ∈ p) (hq : ∀ x ∈ q, f x ∈ q) (hpq' : ∀ x ∈ Submodule.comap q.subtype p, (f.restrict hq) x ∈ Submodule.comap q.subtype p := ⋯) : (trace R ↥(Submodule.comap q.subtype p)) ((f.restrict hq).restrict hpq') = (trace R ↥p) (f.restrict hp)

Restriction in two steps. If f preserves the submodules p ≤ q, then restricting f to q and then to p, viewed as the submodule p.comap q.subtype of q, gives the same trace as restricting f to p directly: the two restrictions are conjugate by Submodule.comapSubtypeEquivOfLe.

theorem LinearMap.trace_restrict_eq_of_linearEquiv {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] (e : M ≃ₗ[R] N) {p : Submodule R M} {p' : Submodule R N} (hpp' : Submodule.map (↑e) p = p') {f : M →ₗ[R] M} {f' : N →ₗ[R] N} (hf : ∀ (x : M), e (f x) = f' (e x)) (hp : ∀ x ∈ p, f x ∈ p) (hp' : ∀ x ∈ p', f' x ∈ p') : (trace R ↥p') (f'.restrict hp') = (trace R ↥p) (f.restrict hp)

Transport of restricted traces. If a linear equivalence e intertwines f and f' and carries a submodule p preserved by f onto a submodule p' preserved by f', then the traces of the two restrictions agree: they are conjugate by LinearEquiv.submoduleMap.

Endomorphisms exchanging two subspaces

theorem LinearMap.trace_restrict_inf_eq_trace {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {A B : Submodule K V} (hAB : Codisjoint A B) {f : V →ₗ[K] V} (hA : ∀ x ∈ A, f x ∈ B) (hB : ∀ x ∈ B, f x ∈ A) : (trace K ↥(A ⊓ B)) (f.restrict ⋯) = (trace K V) f

If f maps the subspaces A and B into each other and A ⊔ B = ⊤ (Codisjoint A B), then the trace of f is the trace of its restriction to A ⊓ B.

theorem LinearMap.trace_restrict_inf_eq_trace_restrict_sup {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {A B : Submodule K V} {f : V →ₗ[K] V} (hA : ∀ x ∈ A, f x ∈ B) (hB : ∀ x ∈ B, f x ∈ A) : (trace K ↥(A ⊓ B)) (f.restrict ⋯) = (trace K ↥(A ⊔ B)) (f.restrict ⋯)

Trace reduction to an intersection. If f maps the subspaces A and B into each other, then its traces on A ⊓ B and on A ⊔ B agree.