TheoremStatement: Literature-sourcedProof: Literature-sourcedSession-authored (Fable 5 assisted)precheck 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.

Over a PID, injective modules are exactly divisible modules

Statement

Assume the Axiom of Choice through Baer's criterion. Over a principal ideal domain $R$ , a module is injective if and only if it is divisible. In particular, an abelian group is an injective $Z$ -module if and only if it is divisible.

The implication from injective to divisible is choice-free; the converse inherits the Zorn-lemma use in Baer's criterion.

Facts & Assumptions

Given: A principal ideal domain $R$ and an $R$ -module $D$ .

[F1]

Divisibility means that for every $0 \neq r \in R$ and $d \in D$ , some $x$ satisfies $r x = d$ (Divisible modules over an integral domain).

[F2]

Every ideal of a PID is principal, and a PID is an integral domain (Principal ideal domain).

[L1]

Under AC, a module is injective exactly when maps from left ideals extend to $R$ (Baer's criterion for injective modules).

Proof

technique · direct

1.1

Suppose $D$ is injective. For $0 \neq r \in R$ and $d \in D$ , define $f : r R \to D$ by $f (s r) = s d$ . This is well defined because $R$ is a domain, and injectivity extends it to $F : R \to D$ .

assume-hypF2L1

1.2

Conversely, suppose $D$ is divisible and let $f : J \to D$ be a homomorphism from an ideal. By [F2], $J = r R$ . If $r = 0$ , $J = 0$ and the zero map extends $f$ ; if $r \neq 0$ , put $d = f (r)$ and choose $x \in D$ with $r x = d$ by [F1].

assume-hypF1F2choose

2.1

With $x = F (1)$ , one has $r x = F (r) = f (r) = d$ , so $D$ is divisible by [F1].

step 1.1F1

2.2

The homomorphism $F : R \to D$ defined by $F (s) = s x$ satisfies $F (s r) = s (r x) = s d = f (s r)$ , so it extends $f$ . Baer's criterion [L1] therefore makes $D$ injective.

step 1.2L1algebra

3.1

Steps 1.1 and 2.1 prove that injective modules are divisible, while steps 1.2 and 2.2 prove that divisible modules are injective. Since $Z$ is a PID and its modules are abelian groups, the specialization follows.

step 2.1step 2.2∎

Depends on

Used by

Every injective module is projective (refuted under the Axiom of Choice) False statement
Module categories have enough injectives Theorem

Dependency tree · next 3 levels

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

A. Kleshchev, Lectures on Abstract Algebra for Graduate Students, sections 3.6, 3.14, and 3.15 (standard reference, not scraped)
The Stacks Project, Algebra (standard reference, not scraped)
P. Hekmati, Homological Algebra, section 3.1 (standard reference, not scraped)