PropositionStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.1

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

assume-contra

1.2

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.3

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.

F1F2F3

2.1

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$ .

step 1.2step 1.3F3F4

3.1

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

step 2.1discharge-contradiction∎

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: 84 results over 20 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

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)