TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17

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.

Integrality and finite-module characterizations for one element

Statement

Let $A \subseteq B$ be commutative rings with $A \neq 0$ , and let $b \in B$ . The following are equivalent: $b$ is integral over $A$ ; $A [b]$ is finitely generated as an $A$ -module; and there exists a faithful $A [b]$ -module that is finitely generated over $A$ , where faithful means that $r M = 0$ implies $r = 0$ for $r \in A [b]$ . See Integral elements over a commutative ring and algebraic integers.

Facts & Assumptions

Given: The hypotheses and objects in the Statement.

[L1]

Let $A \to B$ be a homomorphism of commutative rings. An element $b \in B$ is integral over $A$ when it is a root of a monic polynomial in $A [X]$ . The extension is integral when every element is integral. An algebraic integer is a complex number integral over $Z$ . (Integral elements over a commutative ring and algebraic integers).

[L2]

Let $M$ be a left $R$ -module and $S \subseteq M$ . The submodule generated by $S$ is $⟨ S ⟩_{R} : = ⋂ {N \leq M : S \subseteq N} .$ The family is nonempty because $M \leq M$ , and its intersection is a submodule by lem-submodule-criterion-sums-and-intersections. Thus $⟨ S ⟩_{R}$ is the smallest submodule of $M$ containing $S$ , just as def-generated-subgroup defines a generated subgroup. (Generated submodule, cyclic and finitely generated modules, module basis and free module).

[L3]

For a commutative ring $R$ , $n \geq 1$ , and $A \in M_{n} (R)$ , $A adj (A) = adj (A) A = \det (A) I_{n} .$ . (For every positive-sized square matrix over a commutative ring, $A adj (A) = adj (A) A = \det (A) I$ ).

Proof

technique · direct

1.1

If $b$ satisfies a monic equation of degree $d$ , every power $b^{m}$ with $m \geq d$ is an $A$ -linear combination of $1, b, \dots, b^{d - 1}$ ; hence $A [b]$ is finite over $A$ . Taking $A [b]$ itself gives a faithful $A [b]$ -module finite over $A$ .

L1L2L3givenalgebra

2.1

Conversely, let a faithful $A [b]$ -module $M$ be generated over $A$ by $m_{1}, \dots, m_{n}$ . Write $b m_{i} = \sum_{j} a_{i j} m_{j}$ with $a_{i j} \in A$ , so the matrix $b I - (a_{i j})$ annihilates the generating column.

step 1.1givenalgebra

3.1

Multiplying by the adjugate shows that the value $\det (b I - (a_{i j})) \in A [b]$ annihilates every $m_{i}$ . It therefore annihilates $M$ , so faithfulness makes it zero. The formal polynomial $\det (X I - (a_{i j})) \in A [X]$ is monic of degree $n$ and evaluates at $b$ to this element, giving a monic relation for $b$ over $A$ .

L3step 2.1givenalgebra

4.1

The case $n = 0$ cannot occur: then $M = 0$ , so faithfulness would force $A [b] = 0$ , contradicting $A \neq 0$ . Hence $n \geq 1$ , and the determinant in step 3.1 is a nonzero monic polynomial of positive degree. This proves the stated claim.

step 3.1givenalgebra∎

Depends on

Used by

Integral elements over a nonzero base ring form a subring Corollary

Dependency tree · next 3 levels

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

Eloisa Grifo, Commutative Algebra I, Section 1.4 (standard reference, not scraped)