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.

Extension of scalars is left adjoint to restriction of scalars

Statement

Let $f : R \to S$ be a homomorphism of commutative rings, let $M$ be an $R$ -module, and let $N$ be an $S$ -module. There is a natural bijection

${Hom}_{S} (S \otimes_{R} M, N) ≅ {Hom}_{R} (M, {Res}_{R}^{S} N) .$

It sends $F$ to $m \mapsto F (1_{S} \otimes m)$ . Its inverse sends $u : M \to {Res}_{R}^{S} N$ to the $S$ -linear map determined by

$s \otimes m ⟼ s u (m) .$

Facts & Assumptions

Given: A ring map $f : R \to S$ , an $R$ -module $M$ , and an $S$ -module $N$ .

[L1]

Restriction uses $r n = f (r) n$ , while extension is the $S$ -module $S \otimes_{R} M$ with $s^{'} (s \otimes m) = s^{'} s \otimes m$ (Restriction of scalars and extension of scalars $S \otimes_{R} M$ along a ring homomorphism $R \to S$ ).

[L2]

Balanced pairings induce unique homomorphisms from tensor products (Universal property of the tensor product for balanced maps into abelian groups).

[L3]

An elementary-tensor prescription descends exactly when its underlying pairing is balanced (A formula on elementary tensors defines a homomorphism exactly when its underlying pairing is balanced).

Proof

technique · direct

1.1

If $F : S \otimes_{R} M \to N$ is $S$ -linear, define $Θ (F) (m) = F (1 \otimes m)$ . Then $Θ (F) (r m) = F (1 \otimes r m) = F (f (r) \otimes m) = f (r) F (1 \otimes m)$ , so $Θ (F)$ is $R$ -linear into the restriction of $N$ .

givenL1algebra

1.2

If $u : M \to {Res}_{R}^{S} N$ is $R$ -linear, the pairing $(s, m) \mapsto s u (m)$ is $R$ -balanced because $(s f (r)) u (m) = s u (r m)$ . By [L2] and [L3] it induces a homomorphism $Λ (u) : S \otimes_{R} M \to N$ .

givenL1L2L3

2.1

The map $Λ (u)$ is $S$ -linear because $Λ (u) (s^{'} (s \otimes m)) = Λ (u) (s^{'} s \otimes m) = s^{'} s u (m) = s^{'} Λ (u) (s \otimes m)$ .

step 1.2L1algebra

2.2

For $u$ , one has $Θ (Λ (u)) (m) = Λ (u) (1 \otimes m) = u (m)$ .

step 1.1step 1.2

2.3

Precomposition in $M$ and postcomposition in $N$ commute with both displayed formulas, so the inverse bijections are natural in both modules.

step 1.1step 1.2algebra

3.1

For $F$ , one has $Λ (Θ (F)) (s \otimes m) = s F (1 \otimes m) = F (s \otimes m)$ by $S$ -linearity, so uniqueness on elementary tensors gives $Λ Θ (F) = F$ .

step 1.1step 1.2step 2.1L2

4.1

Steps 2.2, 2.3 and 3.1 prove that extension of scalars is left adjoint to restriction of scalars.

step 2.2step 3.1step 2.3∎

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: 38 results over 13 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

MIT 18.721 Algebraic Geometry notes, Lemma 2.1.35 (standard reference, not scraped)