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 and left -modules , endomorphisms of correspond to matrices with , and composition is matrix multiplication using composition in the entries. For , both sides are the one-element zero ring. See The endomorphism ring under addition and composition.
Facts & Assumptions
Given: The hypotheses and objects in the Statement.
For a left -module , define Addition is pointwise and multiplication is composition, . The ring laws and the identity endomorphism are established in prop-endomorphisms-form-a-ring. (The endomorphism ring under addition and composition).
For left -modules , the set of module homomorphisms is an abelian group under pointwise addition, with zero the zero homomorphism and inverse (def-module-homomorphism-kernel-image-and-cokernel, def-group). (The abelian group and maps induced by pre- and postcomposition).
Let be left -modules and a left -module. For every family of homomorphisms , there is a unique homomorphism such that for every . It is given by For , this is the unique map . (Universal property of a direct sum of modules).
Proof
We use inclusions and projections to send to entries , and reconstruct by finite sums.
Composition becomes matrix multiplication because on a finite direct sum, so the entry of is which is the matrix product with composition in the entries; the sum is finite because is.
For the direct sum is the zero module, has one element by [L1], and the set of matrices also has exactly one element, so both sides are the one-element zero ring as the Statement records. For the matrix is the single entry , and the correspondence is the identity on . This proves the stated claim.
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
- William Crawley-Boevey, Noncommutative Algebra, Chapter 1 Sections 1.1-1.9 (standard reference, not scraped)