Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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 SA, 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 AEndF(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=χSWχSˉ (For invariant W, χT=χTWχ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.1

If dimV=0, the empty basis simultaneously triangularises every family.

base
1.2

Assume dimV>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 AA, use [L1] to obtain a nonzero proper eigenspace E, observe that every SA preserves E because SA=AS, and use [L2] plus induction on E to obtain a common eigenvector vE.

L1L2chooseih
2.1

Put W=Fv; it is invariant under every SA, 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.

step 1.2L2L4ih
3.1

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.

step 1.2step 2.1L3L5discharge-induction

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 50 results over 13 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources