Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-03
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.

Kernels and images of module homomorphisms are submodules, and injectivity is equivalent to trivial kernel

Statement

For an RR-module homomorphism f:M→Nf:M\to N, both ker⁡f\ker f and im⁡f\operatorname{im}f are submodules. Moreover,

f is injective⟺ker⁡f={0M}.f\text{ is injective}\quad\Longleftrightarrow\quad\ker f=\{0_M\}.

Facts & Assumptions

Given: A homomorphism f:M→Nf:M\to N of left RR-modules.

[L1]

A module homomorphism preserves addition and scalar multiplication, and the displayed definitions give its kernel and image (Module homomorphism and isomorphism, kernel, image and cokernel).

[L2]

A nonempty subset of a module is a submodule exactly when it is closed under ru+vru+v (The one-step submodule criterion; intersections and sums of submodules are submodules).

[L3]

The additive underlying function of a module homomorphism is a group homomorphism and therefore sends 0M0_M to 0N0_N; moreover r0N=0Nr0_N=0_N (Module homomorphism and isomorphism, kernel, image and cokernel, A group homomorphism automatically satisfies f(e)=e′f(e) = e' and f(g−1)=f(g)−1f(g^{-1}) = f(g)^{-1}, and f(gn)=f(g)nf(g^{n}) = f(g)^{n} for every n∈Zn \in \mathbb{Z}; for monoid homomorphisms preservation of the identity must be assumed, In a module, 0Rm=0M0_Rm=0_M, r0M=0Mr0_M=0_M, (−r)m=−(rm)(-r)m=-(rm) and r(−m)=−(rm)r(-m)=-(rm)).

[L4]

A group homomorphism is injective exactly when its kernel is trivial (A group homomorphism is injective if and only if its kernel is trivial).

Proof

technique · direct
1.1

The kernel contains 0M0_M because f(0M)=0Nf(0_M)=0_N. If u,v∈ker⁡fu,v\in\ker f and r∈Rr\in R, then f(ru+v)=rf(u)+f(v)=0Nf(ru+v)=rf(u)+f(v)=0_N, so ru+v∈ker⁡fru+v\in\ker f.

L1L3given
1.2

The image contains 0N=f(0M)0_N=f(0_M). If f(u),f(v)∈im⁡ff(u),f(v)\in\operatorname{im}f and r∈Rr\in R, then rf(u)+f(v)=f(ru+v)rf(u)+f(v)=f(ru+v) lies in the image.

L1L3given
1.3

The additive underlying function has the same kernel described in [L1], so the group-homomorphism theorem gives ff injective exactly when ker⁡f={0M}\ker f=\{0_M\}.

L1L4given
2.1

The submodule criterion applied to steps 1.1 and 1.2 proves that ker⁡f\ker f and im⁡f\operatorname{im}f are submodules.

step 1.1step 1.2L2
3.1

Together, steps 1.3 and 2.1 prove both assertions.

step 1.3step 2.1∎

Depends on

Used by

Cited to discharge well-definedness by Module homomorphism and isomorphism, kernel, image and cokernel.

Dependency tree · next 3 levels

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