Alphabeta Math
PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16
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.

For invariant W, χT=χT∣WχTˉ

Statement

Let T:V→V be an endomorphism of a finite-dimensional vector space, and let W≤V be T-invariant. Then χT(x)=χT∣W(x) χTˉ(x), where Tˉ is the endomorphism induced on V/W.

Facts & Assumptions

Given: A finite-dimensional F-vector space V, an endomorphism T, and a T-invariant subspace W.

[L1]

Invariance defines the restriction T∣W and the quotient formula Tˉ(v+W)=T(v)+W (Invariant subspaces, restrictions, and induced quotient operators).

[L2]

A basis of W followed by representatives of a basis of V/W is a basis of V (A quotient basis lifts to a basis adapted to W).

[L3]

A block upper-triangular matrix with diagonal blocks A,D has characteristic polynomial χAχD, including zero-sized blocks (The characteristic polynomial of a block upper- or lower-triangular matrix is the product of the characteristic polynomials of its diagonal blocks).

[L4]

The characteristic polynomial of an endomorphism is the basis-independent characteristic polynomial of any representing matrix, and it is 1 on the zero space (The basis-independent characteristic polynomial χT of an endomorphism of a finite-dimensional space, including χT=1 in dimension zero).

[L5]

The formula Tˉ(v+W)=T(v)+W is well defined and linear (Invariance makes the induced quotient operator well defined and linear, with πT=Tˉπ).

Proof

technique · direct
1.1L1L2L5

Choose an ordered basis of W, a basis of V/W, and representatives of the latter; [L2] gives an adapted basis of V, in which invariance makes the matrix of T block upper triangular, with upper-left block representing T∣W and lower-right block representing the well-defined operator Tˉ.

2.1step 1.1L3L4∎

Applying [L3] to that matrix and then [L4] to identify its diagonal-block polynomials gives χT=χT∣WχTˉ; if W=0, W=V, or V=0, the missing block has characteristic polynomial 1, so the same identity remains valid.

Depends on

Used by

Dependency tree · two levels

16 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