English
If p is a projection on M with respect to f, then the trace of f on M equals the finite rank of p under suitable finiteness hypotheses on kernels and images.
Русский
Пусть p — проекция на M относительно f; тогда след f на M равен конечной размерности p при подходящих ограничениях на ядро и образ.
LaTeX
$$$ \operatorname{trace}_R M f = \operatorname{finrank}_R p \quad\text{given } h : IsProj
y{p}{f}. $$$
Lean4
theorem trace {p : Submodule R M} {f : M →ₗ[R] M} (h : IsProj p f) [Module.Free R p] [Module.Finite R p]
[Module.Free R (ker f)] [Module.Finite R (ker f)] : trace R M f = (finrank R p : R) := by
rw [h.eq_conj_prodMap, trace_conj', trace_prodMap', trace_id, map_zero, add_zero]
