CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-13

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.

Fields of fractions are uniquely isomorphic over their embedded domain

Statement

Let $D$ be an integral domain. Suppose $K$ and $L$ are fields containing embedded copies of $D$ , and every element of either field is a quotient of two elements from that copy with nonzero denominator. Then there is a unique field isomorphism $K \to L$ fixing $D$ pointwise.

Facts & Assumptions

Given: Fields $K, L$ with the stated embeddings and quotient-generation property.

[F1]

An injective map from a domain into a field extends uniquely to an injective homomorphism from its field of fractions, with $a / b$ sent to the corresponding quotient (Every injective ring map from a domain into a field factors uniquely through its field of fractions).

Proof

technique · direct

1.1

By [F1], the embeddings of $D$ produce injective homomorphisms $ϕ : Frac (D) \to K$ and $ψ : Frac (D) \to L$ . Their images contain every quotient of embedded elements of $D$ , so the quotient-generation hypothesis makes both maps surjective.

2.1

The composite $ψ ϕ^{- 1} : K \to L$ is therefore a field isomorphism fixing $D$ . If $θ : K \to L$ also fixes $D$ , then for every $a / b \in K$ one has $θ (a / b) = a / b$ , so $θ = ψ ϕ^{- 1}$ .

step 1.1algebra∎

Depends on

Every injective ring map from a domain into a field factors uniquely through its field of fractions

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

5 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

The CRing Project, Chapter 13: Fields and Extensions (standard reference, not scraped)