LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-31

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 finite rank-one projective module embeds as a fractional ideal

Statement

Let $R$ be a domain with fraction field $K$ . If $P$ is a finite projective $R$ -module such that $P \otimes_{R} K ≅ K$ , then there is an injective $R$ -linear map $P ↪ K$ whose image is a fractional ideal of $R$ . In particular, $P$ is isomorphic to a fractional ideal.

Facts & Assumptions

Given: A domain $R$ with fraction field $K$ , and a finite projective $R$ -module $P$ with $P \otimes_{R} K ≅ K$ .

[F1]

The fraction field $K$ is the localisation obtained by inverting the nonzero elements of $R$ (The field of fractions $Frac (D) = (D ∖ {0})^{- 1} D$ of an integral domain).

[L1]

A projective module splits off a free cover (Equivalent characterizations of projective modules).

Proof

technique · direct

1.1

By [L1], there is a finite free module $F$ and maps $i : P \to F$ , $p : F \to P$ with $p i = {id}_{P}$ . Since $R$ is a domain, the free module $F$ is torsion-free, and therefore its direct summand $P$ is torsion-free. The canonical map $F \to F \otimes_{R} K$ is injective, so if $x \in P$ maps to $0$ in $P \otimes_{R} K$ , then $i (x)$ maps to $0$ in $F \otimes_{R} K$ and hence $i (x) = 0$ . Because $i$ is injective, this forces $x = 0$ . Thus the canonical map $P \to P \otimes_{R} K$ is injective.

F1L1givenalgebra

2.1

Choose an isomorphism $φ : P \otimes_{R} K \to K$ . Composing the canonical injection from step 1.1 with $φ$ gives an injective map $P ↪ K$ . If $p_{1}, \dots, p_{n}$ generate the finite module $P$ , write their images as $a_{j} / b_{j} \in K$ and choose $d = b_{1} \dots b_{n}$ . Then $d P \subseteq R$ , so the image is a fractional ideal of $R$ .

F1step 1.1givenchoose

3.1

The image of the injective map in step 2.1 is a fractional ideal isomorphic to $P$ as an $R$ -module.

step 2.1∎

Depends on

Used by

Invertible fractional ideals are exactly the rank-one projective modules Theorem

Dependency tree · two levels

10 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

J. P. May, Notes on Dedekind Rings (standard reference, not scraped)
The Stacks Project, Section 10.78: Finite projective modules (standard reference, not scraped)