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.

E is a k-algebra, the E_i are ideals, and commutator traces vanish

Statement

Keep the notation of Commensurable subspaces and the ideals E_0, E_1, E_2 of E: $k$ is a field, $V$ a $k$ -vector space (Vector space over a field), $A \subseteq V$ a $k$ -subspace, $K$ a commutative $k$ -algebra acting on $V$ with $f A < A$ for all $f \in K$ , and $E, E_{1}, E_{2}, E_{0}$ are the $k$ -subspaces of ${End}_{k} (V)$ attached to $A$ . Assume the Axiom of Choice as inherited from the linear algebra suppliers (The Axiom of Choice). Then:

$E$ is a $k$ -subalgebra of ${End}_{k} (V)$ containing the image of $K$ , and $E_{1}, E_{2}$ are two-sided ideals of $E$ ;
$E_{1} + E_{2} = E$ and $E_{1} \cap E_{2} = E_{0}$ ;
$E_{0}$ is a finite potent subspace of ${End}_{k} (V)$ in the sense of Linearity and conjugation invariance of the finite potent trace, so the trace ${Tr}_{V}$ of The trace of a finite potent endomorphism exists and is unique is defined on $E_{0}$ and is $k$ -linear there (Linear map between vector spaces over the same field);
if $γ \in E_{0}$ and $ψ \in E$ , or if $γ \in E_{1}$ and $ψ \in E_{2}$ , then the commutator $[γ, ψ] = γ ψ - ψ γ$ lies in $E_{0}$ and ${Tr}_{V} ([γ, ψ]) = 0$ .

Facts & Assumptions

Given: a field $k$ , a $k$ -vector space $V$ , a $k$ -subspace $A \subseteq V$ , a commutative $k$ -algebra $K$ acting on $V$ with $f A < A$ for every $f \in K$ , and the associated $k$ -subspaces $E, E_{1}, E_{2}, E_{0} \subseteq {End}_{k} (V)$ ; also elements $γ, ψ \in {End}_{k} (V)$ satisfying one of the two membership hypotheses of claim 4 whenever that claim is invoked.

[F1]

$V$ is a $k$ -vector space, linear maps are additive and $k$ -homogeneous, composites and finite linear combinations of linear maps are linear, and ${End}_{k} (V)$ is a $k$ -vector space under pointwise operations with composition $k$ -bilinear. (Vector space over a field, Linear map between vector spaces over the same field)

[F2]

Assume the Axiom of Choice. A linear map defined on a subspace of a vector space extends to a linear map on the whole space, and there is a $k$ -linear projection $π ⁣ : V \to A$ with $π (a) = a$ for all $a \in A$ : extend a basis of $A$ to a basis of $V$ and let $π$ send the added basis vectors to $0$ . (The Axiom of Choice)

[F3]

For every finite potent endomorphism $θ$ of $V$ the trace ${Tr}_{V} (θ)$ exists, is unique, and for every finite-dimensional $θ$ -stable subspace $W \subseteq V$ containing $θ^{m} (V)$ for some $m \geq 0$ equals ${tr}_{W} (θ ∣_{W})$ . (The trace of a finite potent endomorphism exists and is unique)

[F4]

(T4)-(T6) of Linearity and conjugation invariance of the finite potent trace: ${Tr}_{V}$ is $k$ -linear on every finite potent subspace $F \subseteq {End}_{k} (V)$ ; if $φ ⁣ : V^{'} \to V$ and $ψ ⁣ : V \to V^{'}$ are $k$ -linear with $ψ φ$ finite potent, then $φ ψ$ is finite potent with ${Tr}_{V} (φ ψ) = {Tr}_{V^{'}} (ψ φ)$ ; and if $γ \in E_{0}$ , $ψ \in E$ , or $γ \in E_{1}$ , $ψ \in E_{2}$ , then $[γ, ψ] \in E_{0}$ with ${Tr}_{V} ([γ, ψ]) = 0$ .

[F5]

$A < B$ means that $(A + B) / B$ is finite-dimensional and $A \sim B$ means $A < B$ and $B < A$ ; the relation $<$ is reflexive, transitive, preserved by $k$ -linear maps and by finite sums, and unchanged on commensurable subspaces; $E = {θ : θ A < A}$ , $E_{1} = {θ : θ V < A}$ , $E_{2} = {θ : θ A finite-dimensional}$ , $E_{0} = E_{1} \cap E_{2} = {θ : θ V < A and θ A finite-dimensional}$ , and $E, E_{1}, E_{2}$ are $k$ -subspaces while $E_{0} = E_{1} \cap E_{2}$ ; the image of $K$ is contained in $E$ by the assumed $f A < A$ . (Commensurable subspaces and the ideals E_0, E_1, E_2 of E)

Proof

technique · direct

1.1givenF1F5

(Setup) We verify the four numbered claims with $E, E_{1}, E_{2}, E_{0}$ as in [F5], noting that $E_{0} = E_{1} \cap E_{2}$ by definition, that the image of $K$ lies in $E$ by hypothesis, and that all statements are statements about the linear endomorphisms $θ \in {End}_{k} (V)$ and their images of $A$ and $V$ .

2.1step 1.1F1F5

(Claim 1: $E$ is a $k$ -subalgebra) Since ${i d}_{V} (A) = A$ gives ${i d}_{V} \in E$ and finite sums and scalar multiples of elements of $E$ lie in $E$ by [F5], it remains to check composition: for $θ, θ^{'} \in E$ one has $θ θ^{'} (A) = θ (θ^{'} (A))$ , and $θ^{'} (A) < A$ gives $θ (θ^{'} (A)) < θ (A) < A$ by the linear-map rule and transitivity, so $θ θ^{'} \in E$ ; hence $E$ is a $k$ -subalgebra of ${End}_{k} (V)$ containing the image of $K$ .

3.1step 2.1F5algebra

(Claim 1: $E_{1}$ and $E_{2}$ are $k$ -subspaces) If $θ_{1}, θ_{2} \in E_{1}$ then $(θ_{1} + θ_{2}) (V) \subseteq θ_{1} (V) + θ_{2} (V) < A + A = A$ and $λ θ_{1} \in E_{1}$ , so $E_{1}$ is a $k$ -subspace by [F5]; and $E_{2}$ is a $k$ -subspace because $(θ_{1} + θ_{2}) (A) \subseteq θ_{1} (A) + θ_{2} (A)$ is a sum of two finite-dimensional spaces, hence finite-dimensional.

4.1step 3.1F5

(Claim 1: $E_{1}$ is a two-sided ideal) For $θ \in E$ and $η \in E_{1}$ we have $(θ η) (V) = θ (η V) < θ (A) < A$ by the linear-map rule, so $θ η \in E_{1}$ , while $(η θ) (V) \subseteq η (V) < A$ , so $η θ \in E_{1}$ ; hence $E_{1}$ is a two-sided ideal of $E$ .

5.1step 4.1F5algebra

(Claim 1: $E_{2}$ is a two-sided ideal) For $θ \in E$ and $η \in E_{2}$ we have $(θ η) (A) = θ (η A)$ , an image of the finite-dimensional space $η A$ under a linear map, hence finite-dimensional, so $θ η \in E_{2}$ ; and choosing a finite-dimensional $W$ with $θ A \subseteq A + W$ , we get $(η θ) (A) \subseteq η (A + W) = η A + η W$ , a sum of two finite-dimensional spaces, hence finite-dimensional, so $η θ \in E_{2}$ .

6.1step 5.1F2F5

(Claim 2: a projection is available) By [F2] fix a $k$ -linear projection $π ⁣ : V \to A$ with $π ∣_{A} = {i d}_{A}$ ; then $π (V) = A < A$ , so $π \in E_{1}$ , and $(1 - π) (A) = 0$ is finite-dimensional, so $1 - π \in E_{2}$ and also $1 - π \in E$ .

7.1step 6.1F5

(Claim 2: $E_{1} + E_{2} = E$ ) If $θ \in E$ , then $θ = π θ + (1 - π) θ$ with $π θ \in E_{1}$ and $(1 - π) θ \in E_{2}$ because $E_{1}$ and $E_{2}$ are two-sided ideals of $E$ and $π, 1 - π \in E$ ; conversely $η \in E_{1}$ satisfies $η (A) \subseteq η (V) < A$ , and $η \in E_{2}$ has $η (A)$ finite-dimensional, whence $η (A) < A$ by monotonicity, so both $E_{1}$ and $E_{2}$ are contained in $E$ ; hence $E_{1} + E_{2} = E$ .

8.1step 7.1F5

(Claim 2: the intersection) Since $E_{0} : = E_{1} \cap E_{2}$ by definition, the second half of claim 2 holds; combining with step 7.1 gives $E_{1} + E_{2} = E$ and $E_{1} \cap E_{2} = E_{0}$ .

9.1step 8.1F5algebra

(Claim 3: $E_{0}$ is finite potent) Let $θ_{1}, θ_{2} \in E_{0}$ ; then $θ_{1} (V) < A$ and $θ_{2} (V) < A$ , so with finite-dimensional $W$ such that $θ_{2} (V) \subseteq A + W$ we get $θ_{1} θ_{2} (V) \subseteq θ_{1} (A) + θ_{1} (W)$ , which is a sum of two finite-dimensional spaces because $θ_{1} (A)$ is finite-dimensional and $θ_{1} (W)$ is an image of a finite-dimensional space; thus every product of two elements of $E_{0}$ has finite-dimensional image, i.e. $E_{0}$ is a finite potent subspace with exponent $2$ .

10.1step 9.1F3F4

(Claim 3: linearity of the trace) By (T4) of [F4] applied to the finite potent subspace $E_{0}$ , the trace ${Tr}_{V}$ is defined and $k$ -linear on $E_{0}$ .

11.1step 10.1F4

(Claim 4) If $γ \in E_{0}$ and $ψ \in E$ , or if $γ \in E_{1}$ and $ψ \in E_{2}$ , then claim (T6)(b) of [F4] gives $[γ, ψ] \in E_{0}$ and ${Tr}_{V} ([γ, ψ]) = 0$ , which is claim 4.

12.1step 2.1step 4.1step 5.1step 7.1step 8.1step 9.1step 10.1step 11.1F2∎

All four claims are established: claim 1 in steps 2.1, 4.1 and 5.1, claim 2 in steps 7.1 and 8.1, claim 3 in steps 9.1 and 10.1, and claim 4 in step 11.1; the Axiom of Choice was used only through [F2], to extend a basis of $A$ to all of $V$ .

Depends on

Used by

Dependency tree · two levels

19 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)