PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 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.

The underlying-set functor on fields has no left adjoint

Statement

The underlying-set functor $U : F i e l d \to S e t$ has no left adjoint, where field homomorphisms preserve $1$ .

Facts & Assumptions

Given: The category of fields and unital field homomorphisms.

[F1]

A field has $0 \neq 1$ , is an abelian group under addition, has associative commutative multiplication with unit and inverses for nonzero elements, and satisfies distributivity (Field).

[F2]

A field homomorphism satisfies $φ (x + y) = φ (x) + φ (y)$ , $φ (x y) = φ (x) φ (y)$ , and $φ (1_{F}) = 1_{G}$ , and is automatically injective because its kernel is an ideal of a field and does not contain $1_{F}$ (Field homomorphism and embedding).

[F3]

The characteristic of a unital ring is the least positive natural $n$ with $n \cdot 1_{R} = 0_{R}$ , if such an $n$ exists, and is $0$ otherwise (The characteristic of a ring: the least $n \geq 1$ with $n \cdot 1_{R} = 0$ when one exists, and $0$ otherwise).

[F4]

For every prime $p$ , $Z / p$ is a field (For every prime $p$ , the two operations on $Z / p$ make it a field).

[L1]

If $F ⊣ U$ , then $F i e l d (F (X), K) ≅ S e t (X, U (K))$ naturally (Under local smallness, transposition gives the natural hom-set bijection, and conversely).

Proof

technique · contradiction

1.1assume-contra

Suppose, for contradiction, that a left adjoint $F$ to $U$ exists.

1.2L1

Taking $X = \emptyset$ in [L1], the right hom-set is a singleton for every field $K$ , so there is exactly one field homomorphism $F (\emptyset) \to K$ ; hence $F (\emptyset)$ is an initial field.

1.3F1F2F3

Let $φ : K \to L$ be a field homomorphism. By [F2] it sends $n \cdot 1_{K}$ to $n \cdot 1_{L}$ for every natural $n$ and is injective. If $char K = p > 0$ then $p \cdot 1_{L} = φ (p \cdot 1_{K}) = φ (0) = 0$ ; dividing $p$ by $char L$ with remainder and using the minimality in [F3] shows $char L$ divides $p$ , and $char L = 1$ is impossible because $0 \neq 1$ in [F1], so $char L = p$ . If $char K = 0$ then $n \cdot 1_{K} \neq 0$ for every $n \geq 1$ , so injectivity gives $n \cdot 1_{L} \neq 0$ and $char L = 0$ . Thus a field homomorphism preserves characteristic exactly.

2.1step 1.2step 1.3F3F4

In $Z / p$ the element $n \cdot 1$ is the class of $n$ , which vanishes exactly when $p ∣ n$ , so [F3] and [F4] give $char F_{2} = 2$ and $char F_{3} = 3$ . The initial field would have homomorphisms to both, and step 1.3 would force its characteristic to equal $2$ and to equal $3$ .

3.1step 2.1discharge-contradiction∎

The contradiction shows that $U$ has no left adjoint.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

26 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

Emily Riehl, Category Theory in Context, 2nd ed., Example 4.1.12 (standard reference, not scraped)
Tom Leinster, Basic Category Theory, Example 6.3.5 (standard reference, not scraped)