trace of endomorphism

Stream: maths

[Johan Commelin]

In mathlib, we define the trace of the endomorphism of a module as: if a finite basis exists, use it to turn the endomorphism into a matrix and take the trace, else 0.

I'm not an expert on the theory of traces. But I think this is restrictive...

Does anybody know the definitive most general way to treat traces of module endomorphisms?

[Damiano Testa]

Is this in a situation where there is no topology/convergence?

[Andrew Yang]

Are these relavent?
#mathlib4 > Algebra.norm for projective algebra extensions
#Is there code for X? > Determinant under restriction of scalars @ 💬

[Johan Commelin]

Yes, there is no topology/convergence. So we might still need a finiteness assumption. But freeness feels to strong.

[Damiano Testa]

Ok, so you are looking for something along the lines of " $\pm$ finite rank, plus whatever else is needed"?

[Adam Topaz]

You could always follow what people do in the Tannakian world...

[Oliver Nash]

Wasn't this just discussed here: #Is there code for X? > Determinant under restriction of scalars @ 💬 ?

Edit: oh sorry, already linked above :man_facepalming:

[Johan Commelin]

Lol! I manage to forget what was discussed on zulip < 1 week ago :man_facepalming:

[Kevin Buzzard]

Even in the infinite-dimensional case there is sometimes a good concept of a trace. The analysts know about trace class operators on Banach spaces but this involves convergence. However there's a purely algebraic concept for vector spaces over a field (and free modules over a ring and almost certainly for more general modules over a ring but I don't know how general it goes); if an endomorphism of a vector space has finite-dimensional image then there's a well-behaved concept of trace, which you can just compute by looking at the restriction of the endomorphism to the image (or more generally any finite-dimensional space containing the image) and taking the usual trace.

[Adam Topaz]

https://arxiv.org/pdf/1010.4527 seems relevant

[Dean Young]

One can define trace for an effective descent locally finite free module. If f : R → S is a effective descent and M ⊗_(R) S is finite free over S then one can define the f-extended R-trace using the S-trace over a finite free. I think one can then define the extended trace using a compatibility theorem.

[Dean Young]

Maybe det(I + tΦ) exists in this context as well (the context in which there is a pure extension in which the module becomes finite free). This applies to the ℝ-algebra of smooth functions on a manifold and those of its modules that arise from vector bundles.

[Dean Young]

I commented on the other thread with probably too much detail on how the characteristic polynomial of what's called the curvature form (which can be rearranged as a graded trace) is consistent with the projective view of trace, but it's pretty difficult to compare different definitions I think. For example, one can use the category smooth objects as the target or close under completion. I didn't know about the idea K.B. mentioned above.

One property of the trace that might dissapear in larger generality is the Cayley-Hamilton theorem for the graded trace assembled into the characteristic polynomial. For that one must have a surjection from some V such that End(V) ⊗_(k) k[t] ≅ End_(k[t])(V), which holds for finite free V using how product is coproduct for those and how hom on the left slot works well with it.

[Dean Young]

That view uses Lie algebra valued differential forms (which form monoid objects in complexes but potentially lack the squre zero condition) and their actional analogues in the case of principal bundles.

[Antoine Chambert-Loir]

Another relevant paper is https://projecteuclid-org.ezproxy.u-paris.fr/journals/nagoya-mathematical-journal/volume-40/issue-none/On-trace-for-modules/nmj/1118798127.full

[Dean Young]

https://www.cambridge.org/core/services/aop-cambridge-core/content/view/77CC4E91E32CF4EBDDAEA4B118CD66CD/S0027763000013891a.pdf/on-trace-for-modules.pdf