Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-17
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.

Endomorphisms of a finite direct sum are matrices of Hom-groups

Statement

For nN and left R-modules M1,,Mn, endomorphisms of jMj correspond to n×n matrices (fij) with fijHomR(Mj,Mi), and composition is matrix multiplication using composition in the entries. For n=0, both sides are the one-element zero ring. See The endomorphism ring EndR(M) under addition and composition.

Facts & Assumptions

Given: The hypotheses and objects in the Statement.

[L1]

For a left R-module M, define EndR(M):=HomR(M,M). Addition is pointwise and multiplication is composition, (fg)(m):=f(g(m)). The ring laws and the identity endomorphism are established in prop-endomorphisms-form-a-ring. (The endomorphism ring EndR(M) under addition and composition).

[L2]

For left R-modules M,N, the set HomR(M,N) of module homomorphisms is an abelian group under pointwise addition, with zero the zero homomorphism and inverse (f)(m)=f(m) (def-module-homomorphism-kernel-image-and-cokernel, def-group). (The abelian group HomR(M,N) and maps induced by pre- and postcomposition).

[L3]

Let (Mi)iI be left R-modules and N a left R-module. For every family of homomorphisms fi:MiN, there is a unique homomorphism f:iIMiN such that fȷi=fi for every i. It is given by f((mi))=isupp(m)fi(mi). For I=, this is the unique map 0N. (Universal property of a direct sum of modules).

Proof

technique · direct
1.1

We use inclusions and projections to send f to entries fij=πifιj, and reconstruct f by finite sums.

L1L2L3givenalgebra
2.1

Composition becomes matrix multiplication because kιkπk=id on a finite direct sum, so the (i,j) entry of fg is πi(fg)ιj=πif(kιkπk)gιj=k(πifιk)(πkgιj)=kfikgkj, which is the matrix product with composition in the entries; the sum is finite because n is.

step 1.1L3algebra
3.1

For n=0 the direct sum is the zero module, EndR(0) has one element by [L1], and the set of 0×0 matrices also has exactly one element, so both sides are the one-element zero ring as the Statement records. For n=1 the matrix is the single entry f11=π1fι1=f, and the correspondence is the identity on EndR(M1). This proves the stated claim.

step 1.1step 2.1L1algebra

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 17 results over 14 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