LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-02

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The trace of a finite potent endomorphism exists and is unique

Statement

Assume the Axiom of Choice as inherited from the linear algebra suppliers (The Axiom of Choice). Let $k$ be a field and $V$ a $k$ -vector space (Vector space over a field), and let $θ$ be a $k$ -linear endomorphism of $V$ (Linear map between vector spaces over the same field). Call $θ$ finite potent when $θ^{n} (V)$ is finite-dimensional (Finite-dimensional vector space, and its dimension $\dim_{F} V$ ; infinite-dimensional means having no finite basis) for some $n \geq 0$ . Then there is a unique element ${Tr}_{V} (θ) \in k$ with the following three properties:

(T1) if $V$ is finite-dimensional, ${Tr}_{V} (θ)$ is the ordinary trace of $θ$ (The basis-independent trace of an endomorphism of a finite-dimensional vector space);
(T2) if $W$ is a $θ$ -stable subspace of $V$ , then ${Tr}_{V} (θ) = {Tr}_{W} (θ) + {Tr}_{V / W} (θ)$ (The quotient vector space $V / W$ and its canonical projection);
(T3) if $θ$ is nilpotent, then ${Tr}_{V} (θ) = 0$ .

Existence is by choosing $n$ with $W : = θ^{n} (V)$ finite-dimensional and $θ$ -stable and setting ${Tr}_{V} (θ) : = {Tr}_{W} (θ)$ ; the value is independent of $n$ and of $W$ , and any finite-dimensional $θ$ -stable $W$ containing $θ^{m} (V)$ for some $m$ computes it. In particular ${Tr}_{V}$ is unchanged when $V$ is replaced by any such $W$ .

Facts & Assumptions

Given: a field $k$ , a $k$ -vector space $V$ , and a $k$ -linear endomorphism $θ ⁣ : V \to V$ that is finite potent, together with an integer $n \geq 0$ such that $θ^{n} (V)$ is finite-dimensional. Here $θ^{0}$ is the identity and $θ^{m + 1} = θ \circ θ^{m}$ .

[F1]

$V$ is a $k$ -vector space, a linear map is additive and $k$ -homogeneous, the image of a subspace under a linear map is again a subspace, and a subspace $W \subseteq V$ is $θ$ -stable when $θ (W) \subseteq W$ . (Vector space over a field, Linear map between vector spaces over the same field)

[F2]

Assume the Axiom of Choice: every vector space over a field has a basis, and a basis of a subspace of a finite-dimensional vector space extends to a basis of the whole space. (The Axiom of Choice, Every vector space has a basis)

[F3]

Let $V$ be a finite-dimensional $k$ -vector space and $T ⁣ : V \to V$ linear. For any ordered basis $B$ of $V$ the trace $tr (T)$ is the sum of the diagonal entries of the matrix of $T$ in that basis, and this sum does not depend on $B$ ; the trace of the zero endomorphism is $0$ ; and for a linear isomorphism $S ⁣ : V \to V^{'}$ of finite-dimensional spaces one has $tr (S T S^{- 1}) = tr (T)$ . (The basis-independent trace of an endomorphism of a finite-dimensional vector space)

[F4]

(Rank-nullity) If $T ⁣ : V \to W$ is linear and $V$ is finite-dimensional, then $\dim_{k} V = \dim_{k} (\ker T) + \dim_{k} (im T)$ ; consequently every subspace $U \subseteq V$ of a finite-dimensional space is finite-dimensional with $\dim_{k} U \leq \dim_{k} V$ : extend a basis of $U$ to a basis of $V$ by [F2], and the projection onto $U$ along the span of the extra basis vectors is a linear retraction $r ⁣ : V \to U$ with $\dim_{k} V = \dim_{k} (\ker r) + \dim_{k} U$ . (Rank-nullity: $\dim_{F} V = nullity T + rank T$ , Finite-dimensional vector space, and its dimension $\dim_{F} V$ ; infinite-dimensional means having no finite basis, Every vector space has a basis)

[F5]

Let $U \subseteq V$ be a subspace of a finite-dimensional space. Then $V / U$ is a $k$ -vector space, the canonical projection $π ⁣ : V \to V / U$ is linear with kernel $U$ , and $\dim_{k} (V / U) = \dim_{k} V - \dim_{k} U$ ; for a further subspace $W \subseteq V$ there is a canonical isomorphism $(U + W) / W ≅ U / (U \cap W)$ ; and if $U$ is $θ$ -stable then $θ$ induces a linear map $\overset{ˉ}{θ}$ on $V / U$ with ${\overset{ˉ}{θ}}^{n} (π (v)) = π (θ^{n} (v))$ for every $n \geq 0$ and every $v \in V$ . (The quotient vector space $V / W$ and its canonical projection, Linear map between vector spaces over the same field)

[F6]

Let $V$ be finite-dimensional, $T ⁣ : V \to V$ linear, and $U \subseteq V$ a $T$ -stable subspace. Then ${tr}_{V} (T) = {tr}_{U} (T ∣_{U}) + {tr}_{V / U} (\overset{ˉ}{T})$ : a basis of $U$ extends to a basis of $V$ by [F2], and in that basis the matrix of $T$ is block upper triangular with diagonal blocks the matrices of $T ∣_{U}$ and of the induced map $\overset{ˉ}{T}$ , while traces are sums of diagonal entries by [F3]. (The basis-independent trace of an endomorphism of a finite-dimensional vector space, The quotient vector space $V / W$ and its canonical projection, Every vector space has a basis)

[F7]

Let $V$ be finite-dimensional and $T ⁣ : V \to V$ nilpotent, say $T^{N} = 0$ . Then $tr (T) = 0$ : the chain $V \supseteq T (V) \supseteq T^{2} (V) \supseteq \dots \supseteq 0$ consists of $T$ -stable subspaces, and a basis of $V$ adapted to this chain, built successively by [F2], gives a matrix that is strictly upper triangular, so every diagonal entry vanishes. (The basis-independent trace of an endomorphism of a finite-dimensional vector space, Every vector space has a basis)

[F8]

For every $m \geq 0$ one has $θ^{m + 1} (V) \subseteq θ^{m} (V)$ , and $θ^{m} (V)$ is $θ$ -stable. (Linear map between vector spaces over the same field)

Proof

technique · direct

1.1givenF1F4F8

By hypothesis $θ$ is finite potent, so fix $n \geq 0$ with $W : = θ^{n} (V)$ finite-dimensional; by [F8] each $θ^{m} (V)$ is $θ$ -stable, $W$ is $θ$ -stable, and $θ^{m + 1} (V) \subseteq θ^{m} (V)$ for all $m$ , so that $θ^{m} (V) \subseteq W$ and $θ^{m} (V)$ is finite-dimensional by [F4] for every $m \geq n$ .

2.1F3step 1.1

Define ${Tr}_{V} (θ) : = {tr}_{W} (θ ∣_{W})$ , the ordinary trace of the restriction of $θ$ to the finite-dimensional space $W$ ; this is a well-defined element of $k$ by [F3], independent of any auxiliary basis chosen there.

3.1F4F5F6F7step 2.1

(Independence of the auxiliary index) Let $m \leq m^{'}$ be indices for which both $θ^{m} (V)$ and $θ^{m^{'}} (V)$ are finite-dimensional; then $θ^{m^{'}} (V) = θ^{m^{'} - m} (θ^{m} (V)) \subseteq θ^{m} (V)$ and both subspaces are $θ$ -stable. Applying [F6] to the $θ$ -stable subspace $θ^{m^{'}} (V)$ of the finite-dimensional space $θ^{m} (V)$ gives ${tr}_{θ^{m} (V)} (θ) = {tr}_{θ^{m^{'}} (V)} (θ) + {tr}_{θ^{m} (V) / θ^{m^{'}} (V)} (\overset{ˉ}{θ})$ , and the induced endomorphism $\overset{ˉ}{θ}$ of the quotient satisfies ${\overset{ˉ}{θ}}^{m^{'} - m} = 0$ , because ${\overset{ˉ}{θ}}^{m^{'} - m}$ sends the class of $x$ to the class of $θ^{m^{'} - m} (x)$ with $x \in θ^{m} (V)$ , and $θ^{m^{'} - m} (x) \in θ^{m^{'}} (V)$ ; hence the quotient trace vanishes by [F7] and the two traces agree. Consequently, applying this agreement with $m = n$ and step 1.1 whenever $m \geq n$ , and to the pair $(m, n)$ whenever $θ^{m} (V)$ is finite-dimensional with $m \leq n$ , one has ${Tr}_{V} (θ) = {tr}_{θ^{m} (V)} (θ)$ for every $m \geq 0$ with $θ^{m} (V)$ finite-dimensional.

3.2F3step 2.1

(T3) If $θ$ is nilpotent, say $θ^{N} = 0$ , then $W_{N} : = θ^{N} (V) = 0$ is finite-dimensional and $θ$ -stable, so step 2.1 applied with $n$ replaced by $N$ gives ${Tr}_{V} (θ) = {tr}_{W_{N}} (θ ∣_{0}) = 0$ , the zero endomorphism of the zero space having trace $0$ by [F3].

4.1F4F5F6F7step 3.1

(Any finite-dimensional computing subspace) Let $W^{'} \subseteq V$ be a finite-dimensional $θ$ -stable subspace containing $Z : = θ^{m} (V)$ for some $m \geq 0$ ; then $Z$ is a finite-dimensional $θ$ -stable subspace of $W^{'}$ by [F4]. Applying [F6] to $Z \subseteq W^{'}$ gives ${tr}_{W^{'}} (θ) = {tr}_{Z} (θ) + {tr}_{W^{'} / Z} (\overset{ˉ}{θ})$ , and ${\overset{ˉ}{θ}}^{m} = 0$ on $W^{'} / Z$ because $θ^{m} (W^{'}) \subseteq θ^{m} (V) = Z$ , so [F7] kills the quotient term; by step 3.1 the remaining term is ${Tr}_{V} (θ)$ . Hence every such $W^{'}$ computes the value ${Tr}_{V} (θ) = {tr}_{W^{'}} (θ)$ , and replacing $V$ by such a $W^{'}$ does not change the trace.

5.1F3step 2.1step 4.1

(T1) If $V$ itself is finite-dimensional, then $V$ is a finite-dimensional $θ$ -stable subspace containing $θ^{0} (V) = V$ , so step 4.1 with $W^{'} = V$ gives ${Tr}_{V} (θ) = {tr}_{V} (θ)$ ; that is, ${Tr}_{V} (θ)$ is the ordinary trace of $θ$ .

5.2F3F5F6F7step 3.1step 4.1

(T2) Let $W \subseteq V$ be a $θ$ -stable subspace and let $m \geq 0$ be such that $U : = θ^{m} (V)$ is finite-dimensional (for instance $m = n$ by step 1.1); then $Z : = θ^{m} (W) \subseteq U \cap W \subseteq U$ are finite-dimensional $θ$ -stable subspaces by [F4]. By step 3.1, ${Tr}_{V} (θ) = {tr}_{U} (θ)$ and ${Tr}_{W} (θ) = {tr}_{Z} (θ)$ , while $θ^{m} (V / W) = (U + W) / W$ by [F5], so step 4.1 applied to the induced endomorphism $\overset{ˉ}{θ}$ of $V / W$ gives ${Tr}_{V / W} (θ) = {tr}_{(U + W) / W} (\overset{ˉ}{θ})$ . Now [F6] applied to the $θ$ -stable subspaces $Z \subseteq U \cap W \subseteq U$ gives ${tr}_{U} (θ) = {tr}_{U \cap W} (θ) + {tr}_{U / (U \cap W)} (\overset{ˉ}{θ})$ and ${tr}_{U \cap W} (θ) = {tr}_{Z} (θ) + {tr}_{(U \cap W) / Z} (\overset{ˉ}{θ})$ , and the last term vanishes by [F7] because $θ^{m} (U \cap W) \subseteq θ^{m} (W) = Z$ makes the induced map nilpotent; finally the canonical isomorphism $U / (U \cap W) ≅ (U + W) / W$ of [F5] carries the map induced by $θ$ on $U / (U \cap W)$ to the map induced by $θ$ on $(U + W) / W$ , so by [F3] the two quotient traces are equal. Hence ${Tr}_{V} (θ) = {Tr}_{W} (θ) + {Tr}_{V / W} (θ)$ .

6.1F3F5step 3.2step 4.1step 5.1step 5.2

(Uniqueness) Let ${Tr}^{'}$ be any assignment $(V, θ) \mapsto {Tr}_{V}^{'} (θ) \in k$ , defined for all pairs $(V, θ)$ with $θ$ finite potent, that satisfies (T1)-(T3) of the statement; let $θ$ be finite potent on $V$ and choose $m \geq 0$ with $W : = θ^{m} (V)$ finite-dimensional. Applying (T2), as established in step 5.2, to the $θ$ -stable subspace $W$ gives ${Tr}_{V}^{'} (θ) = {Tr}_{W}^{'} (θ) + {Tr}_{V / W}^{'} (θ)$ ; the induced endomorphism of $V / W$ is nilpotent because $θ^{m} (V / W) = 0$ by [F5], so ${Tr}_{V / W}^{'} (θ) = 0$ by (T3), as established in step 3.2; and ${Tr}_{W}^{'} (θ) = {tr}_{W} (θ)$ by (T1), as established in step 5.1, since $W$ is finite-dimensional. Therefore ${Tr}_{V}^{'} (θ) = {tr}_{W} (θ) = {Tr}_{V} (θ)$ by steps 3.1 and 4.1, so the three properties determine the value.

7.1F2step 2.1step 3.1step 3.2step 4.1step 5.1step 5.2step 6.1∎

By step 2.1 the assignment $θ \mapsto {Tr}_{V} (θ)$ is defined by an ordinary trace on the finite-dimensional space $θ^{n} (V)$ , independent of every auxiliary choice by steps 3.1 and 4.1; by steps 5.1, 5.2 and 3.2 it satisfies (T1), (T2) and (T3); and by step 6.1 it is the only assignment with these three properties, so ${Tr}_{V} (θ)$ exists and is unique. The Axiom of Choice is used only through [F2], to select bases in the auxiliary finite-dimensional spaces, as in [F4], [F6] and [F7]; no other choice is made.

Depends on

Used by

Dependency tree · two levels

37 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

John Tate, Residues of differentials on curves, Ann. Sci. E.N.S. (4) 1 (1968) 149-159 (standard reference, not scraped)