PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 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.

Module endomorphisms form a ring under pointwise addition and composition

Statement

For every left $R$ -module $M$ , pointwise addition and composition make ${End}_{R} (M)$ a unital ring with identity ${id}_{M}$ . See The endomorphism ring ${End}_{R} (M)$ under addition and composition.

Facts & Assumptions

Given: The hypotheses and objects in the Statement.

[L1]

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

[L2]

For left $R$ -modules $M, N$ , the set ${Hom}_{R} (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 ${Hom}_{R} (M, N)$ and maps induced by pre- and postcomposition).

[L3]

For left $R$ -modules $M, N$ , a function $f : M \to N$ is an $R$ -module homomorphism if $f (m + m^{'}) = f (m) + f (m^{'})$ and $f (r m) = r f (m)$ for all $m, m^{'} \in M$ and $r \in R$ (Module homomorphism and isomorphism, kernel, image and cokernel).

Proof

technique · direct

1.1L1L3givenalgebra

If $f, g \in {End}_{R} (M)$ then $f \circ g$ is again a module homomorphism, since $(f \circ g) (m + n) = f (g (m) + g (n)) = (f \circ g) (m) + (f \circ g) (n)$ and $(f \circ g) (r m) = f (r g (m)) = r (f \circ g) (m)$ . So composition is a binary operation on ${End}_{R} (M)$ .

1.2L1L2

Taking $N = M$ in [L2] makes $({End}_{R} (M), +)$ an abelian group, with the zero homomorphism as neutral element and $(- f) (m) = - f (m)$ as the inverse of $f$ .

1.3L1algebra

Composition is associative: for all $m$ , $(f \circ (g \circ h)) (m) = f (g (h (m))) = ((f \circ g) \circ h) (m)$ .

1.4L1L2L3algebra

Both distributive laws hold. For all $m$ , $(f \circ (g + h)) (m) = f (g (m) + h (m)) = f (g (m)) + f (h (m)) = (f \circ g + f \circ h) (m)$ , where the middle equality is additivity of $f$ ; and $((g + h) \circ f) (m) = g (f (m)) + h (f (m)) = (g \circ f + h \circ f) (m)$ directly from pointwise addition.

1.5L1L3algebra

The identity map ${id}_{M}$ satisfies ${id}_{M} (m + n) = m + n$ and ${id}_{M} (r m) = r m$ , so it lies in ${End}_{R} (M)$ , and $f \circ {id}_{M} = f = {id}_{M} \circ f$ for every $f$ .

2.1step 1.1step 1.2step 1.3step 1.4step 1.5algebra∎

Steps 1.1 through 1.5 are exactly the axioms of a unital ring for $({End}_{R} (M), +, \circ, {id}_{M})$ . For the zero module the only map $0 \to 0$ is ${id}_{0}$ , so ${End}_{R} (0)$ has one element and is the one-element ring, in which the identity coincides with the zero element. This proves the stated claim.

Depends on

Used by

Graded Fitting decomposition for degree-zero endomorphisms Lemma
Hom_G(V,W) is a k-vector space and End_G(V) is a k-algebra Proposition
End_R(_R R)≅ Rᵒᵖ Theorem
Schur's lemma for simple modules Theorem

Cited to discharge well-definedness by The endomorphism ring End_R(M) under addition and composition.

Dependency tree · two levels

8 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

William Crawley-Boevey, Noncommutative Algebra, Chapter 1 Sections 1.1-1.9 (standard reference, not scraped)