TheoremStatement: Literature-sourcedProof: Literature-sourcedSession-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 character dual of a flat module is injective

Statement

Let $R$ be a commutative ring, let $P$ be a flat $R$ -module, and let $D$ be an injective $Z$ -module. Define the character dual

$P^{+} : = {Hom}_{Z} (P, D)$

with $R$ -action

$(r ϕ) (p) : = ϕ (r p) .$

Then $P^{+}$ is an injective $R$ -module.

Facts & Assumptions

Given: A commutative ring $R$ , a flat $R$ -module $P$ , and an injective $Z$ -module $D$ .

[L1]

Flatness makes $u \otimes 1_{P}$ injective whenever $u$ is an injection of $R$ -modules (Flat and faithfully flat modules and ring homomorphisms).

[L2]

Balanced maps into an abelian group correspond uniquely to group homomorphisms from a tensor product (Universal property of the tensor product for balanced maps into abelian groups).

[L3]

An injective module has the extension property along every injective module homomorphism (Injective modules and the extension property).

[L4]

${Hom}_{Z} (P, D)$ is an abelian group under pointwise addition (The abelian group ${Hom}_{R} (M, N)$ and maps induced by pre- and postcomposition).

Proof

technique · direct

1.1

The displayed formula makes $P^{+}$ an $R$ -module: $(r s) ϕ$ and $r (s ϕ)$ agree at every $p$ , and all other module laws hold pointwise in the abelian group [L4].

givenL4algebra

1.2

Let $u : A \to B$ be an injective $R$ -module homomorphism and let $v : A \to P^{+}$ be $R$ -linear. By [L1], $u \otimes 1_{P} : A \otimes_{R} P \to B \otimes_{R} P$ is injective.

givenL1

2.1

For every $R$ -module $M$ , an $R$ -linear map $v : M \to P^{+}$ determines the balanced map $(m, p) \mapsto v (m) (p)$ , and [L2] gives a group homomorphism $\hat{v} : M \otimes_{R} P \to D$ . Conversely a group homomorphism $h : M \otimes_{R} P \to D$ gives $m \mapsto [p \mapsto h (m \otimes p)]$ ; the balance relation makes this map $R$ -linear. These constructions are inverse.

step 1.1L2

3.1

A group homomorphism between abelian groups is automatically $Z$ -linear because additivity gives compatibility with positive integer multiples and with negatives. Thus the group homomorphisms in step 2.1 are precisely the $Z$ -module homomorphisms to which injectivity of $D$ applies.

algebra

4.1

Transpose $v$ by step 2.1 to $\hat{v} : A \otimes_{R} P \to D$ . By step 3.1 and injectivity [L3] at the ring $Z$ , extend it along $u \otimes 1_{P}$ to a homomorphism $\hat{w} : B \otimes_{R} P \to D$ .

step 2.1step 3.1step 1.2L3choose

5.1

Transpose $\hat{w}$ back by step 2.1 to an $R$ -linear map $w : B \to P^{+}$ . Naturality of the evaluation formulas gives $w \circ u = v$ .

step 2.1step 4.1

6.1

Every $R$ -linear map into $P^{+}$ therefore extends along every injection, so [L3] makes $P^{+}$ injective.

step 5.1L3∎

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: 40 results over 19 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

M. Barr, Acyclic Models, Proposition 5.17 (standard reference, not scraped)