Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-09
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 finite-dimensional algebra separates its split simple modules

Statement

Let A be a finite-dimensional unital k-algebra and (Si)i∈I a family of pairwise nonisomorphic simple left A-modules satisfying End⁡A(Si)=kid⁡Si. Then I is finite, every Si is finite-dimensional, and the action map A→∏i∈IEnd⁡k(Si) is surjective. The empty product is the zero algebra.

Facts & Assumptions

Given: A,k,Si as stated; simple modules are nonzero.

[F1]

A nonzero map between simple modules is an isomorphism (Schur's lemma for simple modules).

[F2]

Finite direct sums have componentwise actions; the empty sum is zero (The direct sum of an indexed family of modules).

Proof

1.1F2givenalgebra

Every submodule N of a finite sum W of simple modules has a complement that is a sum of simple modules of the listed types. Here is the induction proving this assertion. For W=0, take complement 0. Write W=S⊕T, with S simple, and suppose the assertion proved for T. If S⊆N, then N=S⊕(N∩T); a complement of N∩T in T complements N. Otherwise N∩S=0, and projection to T identifies N with a submodule N′ of T. Write T=N′⊕C by the induction hypothesis. There is an A-linear map f:N′→S with N={(f(t),t):t∈N′}. Every (s,t+c) equals (f(t),t)+(s−f(t),c), uniquely, so W=N⊕(S⊕C). These cases exhaust the possibilities since N∩S is a submodule of S.

1.2F3F4given

For each member of a finite selection of the Si, choose 0≠si∈Si. Simplicity gives Asi=Si. Images of a finite basis of A span Si. Scanning that list and retaining a vector precisely when it is outside the previous span gives an independent spanning list ei1,…,eidi, with 1≤di≤dim⁡kA. Only finitely many selections have been made.

2.1F1F3step 1.1step 1.2algebra

For this finite selection put W=⨁iSidi and v=(eij). If Av≠W, step 1.1 supplies a nonzero simple summand of a complement, isomorphic to some Sl, and projection onto it gives a nonzero A-linear F:W→Sl with F(Av)=0. Its restrictions to copies of Si vanish for i≠l by Schur, and on the copies of Sl are scalars cj. Since 1v=v, we have 0=F(v)=∑jcjelj. Independence gives cj=0 for all j, so F=0, a contradiction. Therefore Av=W.

3.1F3F4step 2.1algebra

Given any tuple of k-endomorphisms ui, step 2.1 supplies a∈A with av=(ui(eij)). Then aeij=ui(eij) for every basis vector, so a induces ui on all of Si. Thus the action map for every finite selection is surjective. Lifting a vector-space basis of the target gives an independent list in A (apply the map to any relation). Consequently ∑idi2≤dim⁡kA, in particular the size of the selection is at most dim⁡kA.

4.1step 3.1F2given∎

If I had more than dim⁡kA members, finite induction would select dim⁡kA+1 distinct indices, contradicting step 3.1. Thus I is finite and that step proves the asserted surjectivity. If I is empty, the unique map onto zero is surjective; if A=0, no nonzero unital simple module exists and this is the only case.

Remarks

The finite simultaneous-density argument supplies the surjectivity used in Yanqi Lake Theorem 11.2.2 without importing its radical or general density machinery.

Depends on

Used by

Dependency tree · two levels

25 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