ExampleConstruction: AI-adaptedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-26

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.

${Hom}_{Z} (Z / m, Z / n) ≅ Z / \gcd (m, n)$ for $n \geq 1$

Example

Let $m \in N$ and let $n \geq 1$ . Then, as $Z$ -modules,

${Hom}_{Z} (Z / m, Z / n) ≅ Z / \gcd (m, n) .$

The hypothesis $n \geq 1$ cannot be dropped. At $n = 0$ the module $Z / 0$ is a copy of $Z$ , and for $m \geq 2$ the left-hand side is the zero module while $\gcd (m, 0) = m$ makes the right-hand side $Z / m$ , which is not zero.

Both modules here are finitely generated over $Z$ , so Over a Noetherian ring the homomorphism module between two finitely generated modules is finitely generated predicts that the homomorphism module is finitely generated; the computation below identifies it outright.

Facts & Assumptions

Given: Natural numbers $m$ and $n$ with $n \geq 1$ , and the classes $[a]_{m} \in Z / m$ and $[b]_{n} \in Z / n$ .

[L1]

The integers modulo $n$ are the congruence classes $[a]_{n} = {b \in Z : b \equiv a (m o d n)}$ , and $[a]_{n} = [b]_{n}$ exactly when $a \equiv b (m o d n)$ ; at $n = 0$ each class is a singleton (The congruence class $[a]_{n}$ and the quotient set $Z / n$ ).

[L2]

Addition and multiplication of congruence classes are given by $[a]_{n} + [b]_{n} = [a + b]_{n}$ and $[a]_{n} [b]_{n} = [a b]_{n}$ (Addition and multiplication on $Z / n$ by $[a]_{n} + [b]_{n} = [a + b]_{n}$ and $[a]_{n} [b]_{n} = [a b]_{n}$ ).

[L3]

For every $n \in N$ , $(Z / n, +, [0]_{n})$ is an abelian group with $- [a]_{n} = [- a]_{n}$ (For every natural $n$ , $(Z / n, +)$ is an abelian group, multiplication is a commutative monoid operation, and both distributive laws hold).

[L4]

Every abelian group carries a unique $Z$ -module structure whose scalar action is integer multiplication, and abelian groups and $Z$ -modules have the same objects and morphisms (Abelian groups and $Z$ -modules have the same objects and morphisms).

[L5]

A function $f ⁣ : M \to N$ between $R$ -modules is an $R$ -module homomorphism when $f (m + m^{'}) = f (m) + f (m^{'})$ and $f (r m) = r f (m)$ (Module homomorphism and isomorphism, kernel, image and cokernel).

[L6]

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

[L7]

Over a commutative ring $R$ the group ${Hom}_{R} (M, N)$ is an $R$ -module under $(r f) (x) = r f (x)$ , with the published addition unchanged (Over a commutative ring the homomorphism group ${Hom}_{R} (M, N)$ is an $R$ -module).

[L8]

For $a, b \in Z$ , $a Z + b Z = \gcd (a, b) Z$ ( $a Z + b Z = \gcd (a, b) Z$ and $a Z \cap b Z = lcm (a, b) Z$ ; equivalently, in $(Z, +)$ the subgroup generated by ${a, b}$ is $⟨ \gcd (a, b) ⟩$ and $⟨ a ⟩ \cap ⟨ b ⟩ = ⟨ lcm (a, b) ⟩$ ).

[L9]

$\gcd (a, b)$ is the greatest common divisor of $a$ and $b$ , with $\gcd (0, 0) : = 0$ ; it satisfies $\gcd (a, b) \geq 0$ always, and $\gcd (a, b) \geq 1$ unless $a = b = 0$ (Common divisor, and the greatest common divisor $\gcd (a, b)$ , with the convention $\gcd (0, 0) : = 0$ ).

[L10]

Over a Noetherian commutative ring the homomorphism module between two finitely generated modules is finitely generated (Over a Noetherian ring the homomorphism module between two finitely generated modules is finitely generated).

[L11]

$Z$ is a Noetherian ring (Fields and $Z$ are Noetherian, and so are their polynomial rings in finitely many variables).

Verification

technique · direct

1.1

Write $d : = \gcd (m, n)$ , so $d \geq 1$ because $n \geq 1$ , and $d$ divides both $m$ and $n$ . Both $Z / m$ and $Z / n$ are abelian groups and hence $Z$ -modules with the integer-multiplication action, and a $Z$ -module homomorphism between them is exactly an additive map; ${Hom}_{Z} (Z / m, Z / n)$ is a $Z$ -module under pointwise addition and the integer action. Each $Z / m$ is generated by $[1]_{m}$ , since $[a]_{m} = a [1]_{m}$ .

L1L2L3L4L5L6L7L9given

2.1

Evaluation at $[1]_{m}$ is a $Z$ -module isomorphism from ${Hom}_{Z} (Z / m, Z / n)$ onto $A : = {y \in Z / n : m y = 0}$ . It lands in $A$ , because $m [1]_{m} = [m]_{m} = [0]_{m}$ gives $m f ([1]_{m}) = f ([0]_{m}) = 0$ . It is injective, because $f ([a]_{m}) = a f ([1]_{m})$ determines $f$ . It is surjective: given $y \in A$ , the assignment $[a]_{m} \mapsto a y$ is well defined, since $[a]_{m} = [a^{'}]_{m}$ means $m$ divides $a - a^{'}$ and then $(a - a^{'}) y$ is a multiple of $m y = 0$ , and it is additive. Additivity and $Z$ -homogeneity of the evaluation map are immediate from the pointwise operations.

L1L2L5L6L7step 1.1

2.2

${b \in Z : n divides m b} = (n / d) Z$ . For the inclusion from right to left, $b = (n / d) t$ gives $m b = (m / d) n t$ , a multiple of $n$ , using that $d$ divides $m$ . For the other inclusion, Bézout in the form $m Z + n Z = d Z$ supplies integers $u, v$ with $d = u m + v n$ ; if $n$ divides $m b$ then $n$ divides $b d = u (m b) + v (b n)$ , say $b d = n s$ , and dividing by $d \geq 1$ gives $b = (n / d) s$ .

L8L9step 1.1

3.1

$A$ is the cyclic submodule generated by $[n / d]_{n}$ , and $A ≅ Z / d$ . Indeed $y = [b]_{n}$ lies in $A$ exactly when $[m b]_{n} = [0]_{n}$ , that is when $n$ divides $m b$ , which by step 2.2 says $b \in (n / d) Z$ ; so $A = {[(n / d) t]_{n} : t \in Z}$ . The map $Z / d \to Z / n$ sending $[c]_{d}$ to $[c (n / d)]_{n}$ is well defined, since $d$ dividing $c - c^{'}$ makes $n = (n / d) d$ divide $(c - c^{'}) (n / d)$ ; it is additive; its image is $A$ ; and it is injective, since $[c (n / d)]_{n} = [0]_{n}$ means $c (n / d) = n t = (n / d) d t$ for some $t$ , whence $c = d t$ because $n / d \geq 1$ is nonzero, so $[c]_{d} = [0]_{d}$ .

L1L2L3step 2.1step 2.2

4.1

Combining steps 2.1 and 3.1 gives ${Hom}_{Z} (Z / m, Z / n) ≅ Z / d$ with $d = \gcd (m, n)$ . This is consistent with the general finiteness statement: $Z$ is Noetherian and $Z / m$ , $Z / n$ are generated by one element each, so the homomorphism module had to be finitely generated, and here it is cyclic. The hypothesis $n \geq 1$ is used in step 1.1 to make $d \geq 1$ and in steps 2.2 and 3.1 to divide by $n / d$ ; at $n = 0$ the conclusion is false for $m \geq 2$ , since an additive $f ⁣ : Z / m \to Z / 0$ has $m f ([1]_{m}) = 0$ in a copy of $Z$ , forcing $f ([1]_{m}) = 0$ and $f = 0$ , while $\gcd (m, 0) = m$ makes the claimed answer $Z / m$ , which has more than one element.

L1L9L10L11step 2.1step 3.1∎

Remarks

The two boundary values behave differently, and only one of them is admitted. At $m = 0$ the module $Z / 0$ is a copy of $Z$ and the formula reads ${Hom}_{Z} (Z, Z / n) ≅ Z / n$ , which is correct and is the case $d = \gcd (0, n) = n$ . At $n = 0$ it fails, as step 4.1 records. The asymmetry is the asymmetry between the source and the target of a homomorphism, not an artefact of the $\gcd$ convention.
The displayed isomorphism is canonical for these quotient presentations. The classes $[1]_{m}$ and $[n / d]_{n}$ are distinguished by the standard quotient maps, not chosen generators. Evaluation at $[1]_{m}$ , followed by the inverse of $[c]_{d} \mapsto [c (n / d)]_{n}$ , therefore gives the isomorphism without an auxiliary choice.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

60 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

Cyclic group (Wikipedia), §Tensor product and Hom of cyclic groups (standard reference, not scraped)
A. Altman and S. Kleiman, A Term of Commutative Algebra, 13th ed., Exercise (16.20) (standard reference, not scraped)

Hom⁡Z(Z/m,Z/n)≅Z/gcd⁡(m,n)HomZ​(Z/m,Z/n)≅Z/gcd(m,n) for n≥1n≥1