LemmaStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28

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.

A ring homomorphism between fields is a field homomorphism in the published sense, and every such map is injective

Statement

Let $F$ and $G$ be fields (Field), regarded as rings by Every field is a commutative ring with $1 \ne 0$ ; it is an integral domain, and it is a commutative division ring, and let $f : F \to G$ be a function. Then:

$f$ is a ring homomorphism (Ring homomorphism: additive, multiplicative, and required to send $1$ to $1$ ) if and only if $f$ is a field homomorphism (Field homomorphism and embedding); the two definitions impose the same three conditions;
every such $f$ is injective (Injection, surjection, bijection).

So "ring homomorphism between fields" and "field homomorphism" name the same maps, and no second notion of homomorphism of fields is introduced.

Facts & Assumptions

Given: Fields $F$ and $G$ , with zeros $0_F, 0_G$ and identities $1_F, 1_G$ , and a function $f : F \to G$ (Field).

[L1]

$F$ and $G$ are commutative rings with $1 \ne 0$ , their ring operations, zeros and identities being the field ones (Every field is a commutative ring with $1 \ne 0$ ; it is an integral domain, and it is a commutative division ring, Ring: an abelian group under addition and a monoid under multiplication, with multiplication distributing over addition on both sides).

[L2]

A ring homomorphism is a map satisfying (RH1) $f(x+y) = f(x)+f(y)$ , (RH2) $f(xy) = f(x)f(y)$ and (RH3) $f(1_F) = 1_G$ (Ring homomorphism: additive, multiplicative, and required to send $1$ to $1$ ).

[L3]

A field homomorphism is a map satisfying $\varphi(x+y) = \varphi(x)+\varphi(y)$ , $\varphi(xy) = \varphi(x)\varphi(y)$ and $\varphi(1_F) = 1_G$ (Field homomorphism and embedding).

[L4]

A ring homomorphism satisfies $f(a-b) = f(a) - f(b)$ (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).

[L5]

In a ring, $0 \cdot x = x \cdot 0 = 0$ (In any ring $0 \cdot a = a \cdot 0 = 0$ , $(-a)b = a(-b) = -(ab)$ , $(-a)(-b) = ab$ , $(-1)a = -a$ and $a(b - c) = ab - ac$ ).

[L6]

In a field, every $x \ne 0$ has an inverse $x^{-1}$ with $x^{-1}x = 1$ , and $1_G \ne 0_G$ (Field).

[L7]

A map is injective when $f(a) = f(b)$ forces $a = b$ (Injection, surjection, bijection).

Proof

technique · direct

1.1

By [L1] the ring structures on $F$ and $G$ are the field structures, so the expressions $f(x)+f(y)$ , $f(x)f(y)$ , $1_F$ and $1_G$ mean the same thing in [L2] and in [L3].

2.1

Claim 1: the three conditions of [L2] and the three conditions of [L3] are the same three equations, so $f$ satisfies one triple exactly when it satisfies the other.

step 1.1L2L3

3.1

Let $f$ be such a map and suppose $f(a) = f(b)$ with $a \ne b$ . Then $a - b \ne 0_F$ , and $f(a-b) = f(a) - f(b) = 0_G$ by [L4].

step 2.1L4

4.1

Put $c := (a-b)^{-1}$ , which exists by [L6]. Then $1_G = f(1_F) = f(c(a-b)) = f(c)f(a-b) = f(c) \cdot 0_G = 0_G$ , using (RH3), (RH2) and [L5]. This contradicts $1_G \ne 0_G$ .

step 3.1L2L5L6

5.1

Hence $f(a) = f(b)$ forces $a = b$ , so $f$ is injective; with step 2.1 this proves both claims.

step 2.1step 4.1L7∎

Remarks

This is one of the page's bridges to the published vocabulary. Together with Every field is a commutative ring with $1 \ne 0$ ; it is an integral domain, and it is a commutative division ring and Every commutative division ring is a field, so "field" and "commutative division ring" name the same structures and the published definition and the ring-theoretic one agree, it means that everything proved on this page about rings, subrings and ring homomorphisms applies to the library's fields with no translation, and that a reader meeting Field homomorphism and embedding and Ring homomorphism: additive, multiplicative, and required to send $1$ to $1$ is meeting one notion twice, not two notions.
The injectivity proof here uses no ideals. The Remarks of Field homomorphism and embedding sketch the standard kernel-is-an-ideal argument; ideals are not defined on this page, and the argument above needs only an inverse and $0 \cdot x = 0$ .
Injectivity really does need $1_G \ne 0_G$ , that is, it needs the target to be a field rather than an arbitrary ring. The zero map from a field to the one-element ring satisfies (RH1), (RH2) and (RH3) there, since $1 = 0$ in that ring, and it is not injective.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

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

Ring homomorphism (Wikipedia) (standard reference, not scraped)
Field (mathematics) (Wikipedia) (standard reference, not scraped)
Thomas W. Judson, Abstract Algebra: Theory and Applications, §16.5: Ring Homomorphisms and Ideals (standard reference, not scraped)