TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16

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.

Commutative rings form a reflective full subcategory of rings

Statement

Let $C R i n g$ be the full subcategory of commutative unital rings inside the category $R i n g$ of unital rings. It is reflective. For a ring $R$ , let $C_{R}$ be the two-sided ideal generated by all commutators $a b - b a$ . The reflector sends $R ⟼ R / C_{R},$ and the reflection unit is the quotient map. If $C_{R} = R$ , the quotient is the zero ring; the unital-ring convention permits this degenerate case.

Facts & Assumptions

Given: A unital ring $R$ and the set $S_{R} = {a b - b a : a, b \in R}$ .

[L1]

Unital rings and unit-preserving homomorphisms form the category $R i n g$ (Unital rings and unit-preserving ring homomorphisms form the large locally small category $R i n g$ , Ring homomorphism: additive, multiplicative, and required to send $1$ to $1$ ).

[L2]

The ideal generated by a subset is the least two-sided ideal containing it (The ideal generated by a subset and principal ideals).

[L3]

For every two-sided ideal $I$ , the quotient $R / I$ is a ring; this includes $I = R$ , whose quotient is the zero ring (The quotient ring $R / I$ with $(r + I) (s + I) = r s + I$ , For a two-sided ideal $I$ , the additive cosets form a ring $R / I$ with identity $1 + I$ ).

[L4]

If $I \subseteq \ker f$ , a ring homomorphism $f : R \to S$ factors uniquely through $R / I$ (A ring homomorphism whose kernel contains a two-sided ideal factors uniquely through the quotient ring).

[L5]

Supplied universal arrows to a full inclusion assemble into a reflector (A full subcategory is reflectively structured exactly when universal arrows are supplied at every ambient object, Reflective full subcategory and reflector).

[L6]

The kernel of a ring homomorphism is a two-sided ideal (The kernel of a ring homomorphism is a two-sided ideal).

Proof

technique · constructive

1.1L1L2L3algebraconstruct

Put $C_{R} = (S_{R})$ using [L2]. In $R / C_{R}$ , $(a + C_{R}) (b + C_{R}) - (b + C_{R}) (a + C_{R}) = a b - b a + C_{R} = 0$ , so [L3] makes $R / C_{R}$ a commutative ring. This computation remains valid when $C_{R} = R$ : then $R / C_{R}$ is the permitted zero ring, so the construction is total.

2.1step 1.1L1L2L4L6algebra

Let $f : R \to A$ be a unit-preserving homomorphism to a commutative ring. Then $f (a b - b a) = f (a) f (b) - f (b) f (a) = 0$ , so $S_{R} \subseteq \ker f$ . The kernel of a ring homomorphism is a two-sided ideal by [L6], so leastness in [L2] gives $C_{R} \subseteq \ker f$ , and [L4] supplies a unique homomorphism $\overset{ˉ}{f} : R / C_{R} \to A$ with $f = \overset{ˉ}{f} q_{R}$ . Unit preservation is retained by [L4], including the zero-ring case.

3.1step 2.1L4L5discharge-construct∎

Step 2.1 is exactly the universal-arrow property of the quotient map $q_{R} : R \to R / C_{R}$ to the full inclusion $C R i n g ↪ R i n g$ . The family is supplied by the explicit formula $R \mapsto C_{R}$ , so [L5] assembles it into the reflector.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

31 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

E. Riehl, Category Theory in Context, example 4.5.13(ii) (standard reference, not scraped)