LemmaStatement: AI-adaptedProof: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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 an object of a preadditive category form a ring

Statement

Let $C$ be a preadditive category and $P$ an object of $C$ . Then ${End}_{C} (P) : = C (P, P)$ , with addition inherited from the abelian group structure on the hom-set and multiplication given by composition, is a unital ring with identity $1_{P}$ ; composition is bilinear in both variables, and the ring with the reversed multiplication is the opposite ring ${End}_{C} (P)^{o p}$ . For $C$ the category of left $R$ -modules this is the published endomorphism ring ${End}_{R} (P)$ (The endomorphism ring ${End}_{R} (M)$ under addition and composition). No choice is used.

Facts & Assumptions

Given: A preadditive category $C$ and an object $P$ of $C$ ; write $E : = {End}_{C} (P) = C (P, P)$ , with addition the group operation of the hom-set and multiplication composition.

[F1]

In a preadditive category every hom-set is an abelian group and composition is bilinear: $h \circ (f + g) = h \circ f + h \circ g$ and $(f + g) \circ k = f \circ k + g \circ k$ whenever the composites are defined (Preadditive category); equivalently, the covariant and contravariant hom-functors take values in abelian groups (The hom-bifunctor of a preadditive category takes values in abelian groups).

[F2]

A ring is a set with an addition making it an abelian group, a multiplication making it a monoid with two-sided identity $1$ , and both distributive laws (Ring: an abelian group under addition and a monoid under multiplication, with multiplication distributing over addition on both sides).

[F3]

Composition in a category is associative and unital: $h \circ (g \circ f) = (h \circ g) \circ f$ and $1_{B} \circ f = f = f \circ 1_{A}$ for $f : A \to B$ (Category, object, morphism, domain, codomain, identity, composition, and hom-collection).

[F4]

For a unital ring $R$ the opposite ring $R^{o p}$ has the same underlying abelian group, identity and addition as $R$ , with multiplication $a ⋆ b : = b a$ , and these operations form a unital ring (The opposite ring $R^{o p}$ ).

[F5]

For a left $R$ -module $M$ , the published endomorphism ring is ${End}_{R} (M) = {Hom}_{R} (M, M)$ with pointwise addition and composition as multiplication (The endomorphism ring ${End}_{R} (M)$ under addition and composition).

Proof

technique · direct

1.1F1F2given

(Addition makes $E$ an abelian group.) The set $E = C (P, P)$ is a hom-set of the preadditive category $C$ , hence an abelian group under its addition, with zero $0_{P, P}$ and additive inverses $- f$ ; this is axiom (R1) of [F2] for $E$ .

1.2F3given

(Composition is an associative unital operation on $E$ .) If $f, g \in E$ then $g \circ f : P \to P$ , so composition restricts to a binary operation on $E$ ; it is associative by [F3], and the identity morphism $1_{P}$ lies in $E$ and satisfies $1_{P} \circ f = f = f \circ 1_{P}$ by [F3]. Hence $(E, \circ, 1_{P})$ is a monoid, which is axiom (R2).

1.3F1given

(Both distributive laws and bilinearity.) For $f, g, h \in E$ , bilinearity of composition in the preadditive category gives $h \circ (f + g) = h \circ f + h \circ g$ and $(f + g) \circ h = f \circ h + g \circ h$ ; these are the two distributive laws (R3) of [F2], and they say exactly that composition is bilinear in both variables on $E$ .

2.1F2step 1.1step 1.2step 1.3

( $E$ is a unital ring.) By steps 1.1, 1.2 and 1.3 the set $E$ with addition and composition satisfies (R1), (R2) and (R3) of [F2], so $E$ is a unital ring whose identity is $1_{P}$ ; no element outside the given category is chosen.

3.1F4step 2.1

(The reversed multiplication is the opposite ring.) Define $f ⋆ g : = g \circ f$ on $E$ ; then $(E, +, ⋆, 1_{P})$ is exactly the opposite ring of [F4] applied to the ring of step 2.1, because [F4] verifies the ring axioms for the reversed multiplication on the same abelian group with the same identity.

3.2F5step 2.1

(Module case.) If $C$ is the category of left $R$ -modules, then $C (P, P) = {Hom}_{R} (P, P)$ with pointwise addition and composition, so the ring constructed in step 2.1 is exactly the published endomorphism ring ${End}_{R} (P)$ of [F5].

4.1step 1.1step 1.2step 1.3step 2.1step 3.1step 3.2∎

Steps 1.1-1.3 verify the ring axioms for ${End}_{C} (P)$ and give the bilinearity of composition, step 2.1 assembles them into the unital ring structure with identity $1_{P}$ , step 3.1 identifies ${End}_{C} (P)^{o p}$ , and step 3.2 matches the published module-case definition; nothing outside $C$ is chosen and no choice principle is used.

Depends on

Used by

Dependency tree · two levels

18 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

W. Crawley-Boevey, Noncommutative Algebra, §3.12 (End(P)^op for an object of an abelian category) (standard reference, not scraped)
N. Johnson and D. Yau, 2-Dimensional Categories, §6.3, Lemma 6.3.1 (S = Hom_R(M,M) as a ring acting on M) (standard reference, not scraped)