LemmaStatement: Literature-sourcedProof: AI-adaptedSession-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.

Coextension of scalars ${Hom}_{R} (S, M)$ carries its canonical left $S$ -module structure

Statement

Let $φ : R \to S$ be a unital ring homomorphism and let $M$ be a left $R$ -module. Regard $S$ as a left $R$ -module by $r \cdot t = φ (r) t$ . Then ${Hom}_{R} (S, M)$ is a left $S$ -module under

$(s \cdot h) (t) : = h (t s) .$

For an $R$ -linear map $u : M \to M^{'}$ , postcomposition $h \mapsto u \circ h$ is $S$ -linear, so this construction is functorial in $M$ .

Facts & Assumptions

Given: A unital ring homomorphism $φ : R \to S$ , a left $R$ -module $M$ , elements $r \in R$ , $s, s^{'} \in S$ , and $h, h^{'} \in {Hom}_{R} (S, M)$ .

[F1]

A ring homomorphism preserves addition, multiplication, zero, and one (Ring homomorphism: additive, multiplicative, and required to send $1$ to $1$ ).

[F2]

A left module action satisfies distributivity, $(r s) m = r (s m)$ , and $1_{R} m = m$ (Unital left and right modules over a ring; unqualified module means left module).

[F3]

An $R$ -linear map satisfies $h (x + y) = h (x) + h (y)$ and $h (r x) = r h (x)$ (Module homomorphism and isomorphism, kernel, image and cokernel).

[F4]

The functions from one set to another form a set (The set $B^{A}$ of all functions $A \to B$ ).

Proof

technique · direct

1.1

The set ${Hom}_{R} (S, M)$ is a subset of the function set $M^{S}$ , which exists by [F4].

1.2

For $r \in R$ and $t \in S$ , $(s \cdot h) (φ (r) t) = h (φ (r) t s) = r h (t s) = r (s \cdot h) (t)$ , and additivity is similar, so $s \cdot h$ is $R$ -linear.

F1F3algebra

1.3

Pointwise, $((s s^{'}) \cdot h) (t) = h (t s s^{'}) = (s \cdot (s^{'} \cdot h)) (t)$ and $(1_{S} \cdot h) (t) = h (t)$ , so associativity and the unit law hold.

F1F2algebra

1.4

Pointwise additivity of $h$ gives $((s + s^{'}) \cdot h) (t) = (s \cdot h + s^{'} \cdot h) (t)$ , and linearity in $h$ gives $(s \cdot (h + h^{'})) (t) = (s \cdot h + s \cdot h^{'}) (t)$ .

F3algebra

2.1

Steps 1.1 through 1.4 verify all left $S$ -module axioms in [F2].

step 1.1step 1.2step 1.3step 1.4F2

3.1

If $u : M \to M^{'}$ is $R$ -linear, then $u \circ h$ is $R$ -linear and $u ((s \cdot h) (t)) = u (h (t s)) = (s \cdot (u \circ h)) (t)$ , so postcomposition is $S$ -linear. Identities and composites are preserved by associativity of function composition.

F3step 1.2∎

Depends on

Used by

Coextension of scalars is right adjoint to restriction of scalars Theorem

Dependency tree · next 3 levels

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

Emily Riehl, Category Theory in Context, 2nd ed., Example 4.1.10 (standard reference, not scraped)

Coextension of scalars Hom⁡R(S,M)HomR​(S,M) carries its canonical left SS-module structure