TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (gpt-5.6-terra)audited 2026-08-28

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.

Isolated primary components are recovered by localization and contraction

Statement

Assume the Axiom of Choice.

Let $R$ be a Noetherian commutative ring, let $M$ be a finitely generated left $R$ -module, and let

N = Q_{1} \cap \dots \cap Q_{r}

be a minimal primary decomposition with each $Q_{i}$ $p_{i}$ -primary for a prime ideal $p_{i}$ . If $p_{i}$ is isolated, then

Q_{i} = M \cap N_{p_{i}}

inside $M_{p_{i}}$ . In particular, each isolated primary component is uniquely determined by $N \subseteq M$ .

Facts & Assumptions

Given: The Axiom of Choice, a Noetherian commutative ring $R$ , a finitely generated left $R$ -module $M$ , and a minimal primary decomposition $N = Q_{1} \cap \dots \cap Q_{r}$ with each $Q_{i}$ $p_{i}$ -primary for a prime ideal $p_{i}$ .

[L1]

In a minimal primary decomposition, isolated means minimal under inclusion among the component radicals, and the radicals are pairwise distinct (Primary decompositions, minimality, and isolated components).

[L2]

Assuming the Axiom of Choice, in the Noetherian finite-module setting, localizing a $p$ -primary component at its prime radical keeps it primary, while localizing at a multiplicative set meeting its radical gives the whole localized module (Localisation of a primary submodule either stays primary or becomes the whole module).

[L3]

In the Noetherian finite-module setting, a $p$ -primary component with prime radical is recovered by contracting its localization at a multiplicative set disjoint from $p$ (A primary component is recovered by contracting its localization away from the radical).

[L4]

Localisation commutes with finite intersections of submodules (Localisation commutes with finite intersections of submodules).

[L5]

In the Noetherian finite-module setting, the prime component radicals of a minimal primary decomposition are intrinsic and equal the associated primes of the quotient (The radicals in a minimal primary decomposition are intrinsic).

Proof

technique · direct

1.1

Fix an isolated component $Q_{i}$ . By [L1], if $j \neq i$ then $p_{j} ⊈ p_{i}$ , since otherwise minimality of $p_{i}$ would force $p_{j} = p_{i}$ , contradicting the distinct-radical part of [L1]. Hence for each $j \neq i$ we may choose $a_{j} \in p_{j} ∖ p_{i}$ . Localizing at $R ∖ p_{i}$ , fact [L2] gives $(Q_{j})_{p_{i}} = M_{p_{i}}$ for $j \neq i$ , while $(Q_{i})_{p_{i}}$ remains a proper primary submodule. Using [L4], $N_{p_{i}} = ⋂_{j = 1}^{r} (Q_{j})_{p_{i}} = (Q_{i})_{p_{i}} .$

L1L2L4choosealgebra

2.1

Fact [L3] recovers $Q_{i}$ by contracting $(Q_{i})_{p_{i}}$ back to $M$ . Since step 1.1 identifies $(Q_{i})_{p_{i}}$ with $N_{p_{i}}$ , this gives $Q_{i} = M \cap N_{p_{i}} .$ By [L5], the prime $p_{i}$ depends only on $M / N$ and occurs in every minimal primary decomposition. Applying the same localization-and-contraction argument to any such decomposition recovers its $p_{i}$ -component from the same right-hand side. Hence the isolated component is unique.

L3L5step 1.1

3.1

Therefore every isolated component is recovered by localization and contraction.

step 2.1∎

Depends on

Used by

Dependency tree · two levels

18 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

A. Altman and S. Kleiman, A Term of Commutative Algebra, 13th ed., Theorem (18.25) (standard reference, not scraped)
J. S. Milne, A Primer of Commutative Algebra, v4.03, Theorem 19.10 (standard reference, not scraped)