Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 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.

A commuting split family is simultaneously triangularisable

Statement

Let A be a family of pairwise commuting endomorphisms of a finite-dimensional F-vector space V. If χS splits over F for every S∈A, then A is simultaneously triangularisable. The family may be empty.

Facts & Assumptions

Given: A finite-dimensional F-vector space V and a pairwise commuting family A⊆End⁡F(V) such that every χS splits over F.

[L1]

An endomorphism whose characteristic polynomial splits is triangularisable (T is triangularisable iff its minimal polynomial splits iff its characteristic polynomial splits).

[L2]

If W is invariant under S, then χS=χS∣WχSˉ (For invariant W, χT=χT∣WχTˉ).

[L3]

A basis is upper triangular for an operator exactly when its initial spans form an invariant flag (Complete invariant flags are equivalent to upper-triangular matrices).

[L4]

Invariance makes every quotient operator well defined and linear (Invariance makes the induced quotient operator well defined and linear, with πT=Tˉπ).

[L5]

A quotient basis lifts after a basis of the subspace to an adapted basis of the whole space (A quotient basis lifts to a basis adapted to W).

Proof

technique · induction
1.1base

If dim⁡V=0, the empty basis simultaneously triangularises every family.

1.2L1L2chooseih

Assume dim⁡V>0 and the theorem in smaller dimensions; if A is empty or all its members are scalar, any basis works, while otherwise choose a nonscalar A∈A, use [L1] to obtain a nonzero proper eigenspace E, observe that every S∈A preserves E because SA=AS, and use [L2] plus induction on E to obtain a common eigenvector v∈E.

2.1step 1.2L2L4ih

Put W=Fv; it is invariant under every S∈A, the induced quotient operators commute by direct evaluation on cosets, and [L2] shows each quotient characteristic polynomial splits, so induction gives a common triangular basis of V/W.

3.1step 1.2step 2.1L3L5discharge-induction∎

Lift that quotient basis after v by [L5]; its initial spans are invariant for every S by the quotient construction, so [L3] makes every representing matrix upper triangular in the same basis, and this also covers the empty and all-scalar branches.

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