PropositionStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24

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.

Abelian groups and $Z$ -modules have the same objects and morphisms

Statement

Every abelian group carries a unique $Z$ -module structure whose scalar action is integer multiplication. Abelian groups and $Z$ -modules have the same objects and morphisms; their subgroups, generated subobjects, cyclic objects, finite generation, and quotients agree.

Facts & Assumptions

Given: An abelian group $G$ and the published additive integer-power construction.

[L1]

The integers form a commutative ring with multiplicative identity (The integers form a commutative ring).

[F1]

A group is abelian when its operation is commutative (Group and abelian group).

[F2]

A left $R$ -module is an abelian group with a unital distributive scalar action (Unital left and right modules over a ring; unqualified module means left module).

[F3]

A group homomorphism preserves the group operation (Monoid homomorphism and group homomorphism).

[F4]

An $R$ -module homomorphism preserves addition and scalar multiplication (Module homomorphism and isomorphism, kernel, image and cokernel).

[F5]

A subgroup is closed under the group operation and inverses (Subgroup).

[F6]

A submodule is an additive subgroup closed under scalars (Submodule of a module).

[F7]

The subgroup generated by $S$ is the smallest subgroup containing $S$ (The subgroup $⟨ S ⟩$ generated by a subset, the cyclic subgroup $⟨ g ⟩$ , and cyclic groups).

[F8]

The submodule generated by $S$ is the smallest submodule containing $S$ (Generated submodule, cyclic and finitely generated modules, module basis and free module).

[F9]

The quotient group $G / N$ consists of cosets when $N$ is normal (The quotient group $G / N$ and coset product $(g N) (h N) = g h N$ ).

[F10]

The quotient module $M / N$ has the same additive cosets with induced scalar action (Quotient module $M / N$ with scalar multiplication on additive cosets).

[L2]

Every subgroup of an abelian group is normal (Every subgroup of an abelian group is normal).

[F11]

In additive notation the integer power is written $n g$ (Powers $g^{n}$ : natural exponents in a monoid and integer exponents in a group, with $g^{0} = e$ ).

[L3]

Integer powers satisfy $(m + n) g = m g + n g$ (Exponent laws in a group: $g^{m + n} = g^{m} g^{n}$ and $(g^{m})^{n} = g^{m n}$ for all $m, n \in Z$ , and $(g h)^{n} = g^{n} h^{n}$ when $g$ and $h$ commute).

[L4]

Integer powers satisfy $n (m g) = (n m) g$ (Exponent laws in a group: $g^{m + n} = g^{m} g^{n}$ and $(g^{m})^{n} = g^{m n}$ for all $m, n \in Z$ , and $(g h)^{n} = g^{n} h^{n}$ when $g$ and $h$ commute).

[L5]

In an abelian group, integer powers satisfy $n (g + h) = n g + n h$ (Exponent laws in a group: $g^{m + n} = g^{m} g^{n}$ and $(g^{m})^{n} = g^{m n}$ for all $m, n \in Z$ , and $(g h)^{n} = g^{n} h^{n}$ when $g$ and $h$ commute).

Proof

technique · direct

1.1

Define $n \cdot g : = n g$ using [F11]. The integer-power laws [L3], [L4], and [L5], together with $1 g = g$ and $0 g = 0$ , give the four module axioms over the ring in [L1]; commutativity in [F1] supplies the hypothesis for [L5]. Thus every abelian group becomes a $Z$ -module.

L1F1F2F11L3L4L5

2.1

Conversely, any $Z$ -module action must satisfy $1 g = g$ and $(n + 1) g = n g + g$ , so induction forces the action of every nonnegative integer. The equation $0 = (- n + n) g = (- n) g + n g$ forces the negative action. Hence the action in step 1.1 is unique, including the zero scalar and the trivial group.

F2step 1.1algebra

2.2

An additive group homomorphism preserves repeated sums and negatives, hence preserves $n g$ for every integer $n$ and is $Z$ -linear. Every $Z$ -linear map is additive by definition, so group homomorphisms and module homomorphisms are the same maps.

F3F4step 1.1algebra

2.3

A subgroup of an abelian group is closed under every integer multiple and is therefore a $Z$ -submodule; every submodule is already an additive subgroup. Thus subgroups and submodules agree.

F5F6step 1.1algebra

3.1

Since the two families of subobjects agree, their intersections over subobjects containing $S$ agree. Hence generated subgroups and generated $Z$ -submodules coincide, including $S = \emptyset$ , so cyclicity and finite generation agree.

F7F8step 2.3

3.2

By [L2], every subgroup is normal. The quotient group and quotient module have the same cosets and addition, and the unique integer action on cosets is $n (g + N) = n g + N$ , so the quotient objects agree, including $N = 0$ and $N = G$ .

F9F10L2step 1.1step 2.3

4.1

Steps 1.1 and 2.1 identify the objects in both directions, step 2.2 identifies morphisms, steps 2.3 and 3.1 identify subobjects and generation, and step 3.2 identifies quotients. This proves the complete dictionary.

step 1.1step 2.1step 2.2step 2.3step 3.1step 3.2∎

Depends on

Used by

Dependency tree · two levels

48 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

K. Conrad, Introductory Notes on Modules, Section 4 (standard reference, not scraped)
M. Brussel, Finitely Generated Modules over a PID, Section 4 (standard reference, not scraped)

Abelian groups and ZZ-modules have the same objects and morphisms