TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-02

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.

First isomorphism theorem for rings: $R/\ker f\cong\operatorname{im}f$

Statement

First isomorphism theorem for rings: $R/\ker f\cong\operatorname{im}f$ .

Facts & Assumptions

Given: A ring homomorphism $f:R\to S$ .

[L1]

A ring homomorphism whose kernel contains a two-sided ideal factors uniquely through the quotient ring (A ring homomorphism whose kernel contains a two-sided ideal factors uniquely through the quotient ring).

[L2]

$\ker f$ is an ideal (The kernel of a ring homomorphism is a two-sided ideal).

[L3]

Ring homomorphisms preserve additive inverses and products (A ring homomorphism satisfies $f(0) = 0$ , $f(-a) = -f(a)$ and $f(ma) = m f(a)$ for $m \in \mathbb{Z}$ , carries units to units, and has a subring as its image; composites of ring homomorphisms are ring homomorphisms).

[L4]

The underlying group map is isomorphic modulo its kernel to its image (First isomorphism theorem for groups: $G/\ker f\cong\operatorname{im}f$ ).

[L5]

A ring homomorphism preserves $1$ (Ring homomorphism: additive, multiplicative, and required to send $1$ to $1$ ).

Proof

technique · direct

1.1

By [L2] and [L1], $f$ induces a ring homomorphism $\bar f:R/\ker f\to\operatorname{im}f$ with $\bar f(r+\ker f)=f(r)$ .

L1L2L3L4L5givenconstruct

2.1

This map is surjective by the definition of image, and its additive kernel is trivial, hence it is injective by [L4].

step 1.1L1L2L3L4L5givenalgebra

3.1

Thus $\bar f$ is a ring isomorphism.

step 2.1∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 53 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

Judson, Abstract Algebra: Theory and Applications, Ring Homomorphisms and Ideals (standard reference, not scraped)

First isomorphism theorem for rings: R/ker⁡f≅im⁡fR/\ker f\cong\operatorname{im}fR/kerf≅imf