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.

Downward-closed intersections of primary components are intrinsic

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}$ . Let $Σ \subseteq {Ass}_{R} (M / N)$ be downward-closed under inclusion. Then

⋂_{p_{i} \in Σ} Q_{i}

depends only on $N \subseteq M$ and on $Σ$ , not on the chosen minimal decomposition. When $Σ = \emptyset$ , the empty intersection is interpreted as $M$ .

Facts & Assumptions

Given: The Axiom of Choice, a Noetherian commutative ring $R$ , a finitely generated left $R$ -module $M$ , a submodule $N \subseteq 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 the Noetherian finite-module setting, a minimal primary decomposition whose component radicals are prime has radical set ${p_{1}, \dots, p_{r}} = {Ass}_{R} (M / N)$ (The radicals in a minimal primary decomposition are intrinsic).

[L2]

Assuming the Axiom of Choice, in the Noetherian finite-module setting, localizing a primary component away from its prime radical keeps it, while localizing at a set meeting its radical turns it into 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 primary component with prime radical is recovered by contracting its localization at a multiplicative set disjoint from that radical (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]

If an ideal is contained in a finite union of prime ideals, then it lies in one of them (An ideal contained in a finite union of prime ideals lies in one of them).

[L6]

For a multiplicative subset $S$ , the canonical localization map is $λ_{M} : M \to S^{- 1} M$ , $m \mapsto m / 1$ (Localisation of a module at a multiplicative subset).

Proof

technique · direct

1.1

Let $Σ \subseteq {Ass}_{R} (M / N)$ be downward-closed, and set $S = R ∖ ⋃_{p \in Σ} p .$ Because the members of $Σ$ are prime, $S$ is multiplicative. If $p_{i} \in Σ$ , then $S \cap p_{i} = \emptyset$ by definition. If $p_{i} \notin Σ$ and $S \cap p_{i} = \emptyset$ , then $p_{i} \subseteq ⋃_{p \in Σ} p$ , so [L5] forces $p_{i} \subseteq p$ for some $p \in Σ$ . Since $p_{i} \in {Ass}_{R} (M / N)$ by [L1] and $Σ$ is downward-closed, this would imply $p_{i} \in Σ$ , a contradiction. Hence $S \cap p_{i} = \emptyset ⟺ p_{i} \in Σ .$

L1L5givenalgebra

2.1

By [L4], $S^{- 1} N = ⋂_{i = 1}^{r} S^{- 1} Q_{i} .$ For $p_{i} \in Σ$ , step 1.1 and [L2] say that $S^{- 1} Q_{i}$ remains a proper localized primary component. For $p_{i} \notin Σ$ , step 1.1 and [L2] give $S^{- 1} Q_{i} = S^{- 1} M$ . Therefore $S^{- 1} N = ⋂_{p_{i} \in Σ} S^{- 1} Q_{i} .$ When $Σ = \emptyset$ , the right-hand side is the empty intersection $S^{- 1} M$ , which matches the fact that $0 \in S$ and hence $S^{- 1} N = S^{- 1} M = 0$ .

L2L4step 1.1algebra

3.1

Let $λ_{M} : M \to S^{- 1} M$ be the canonical map of [L6]. Contracting the equality of step 2.1 back to $M$ gives $λ_{M}^{- 1} (S^{- 1} N) = ⋂_{p_{i} \in Σ} λ_{M}^{- 1} (S^{- 1} Q_{i}),$ because inverse image commutes with intersections. For every $p_{i} \in Σ$ , step 1.1 and [L3] identify $λ_{M}^{- 1} (S^{- 1} Q_{i})$ with $Q_{i}$ . Hence $λ_{M}^{- 1} (S^{- 1} N) = ⋂_{p_{i} \in Σ} Q_{i} .$

L3L6step 1.1step 2.1algebra

4.1

The left-hand side of step 3.1 depends only on $N \subseteq M$ and the set $S$ , hence only on $N \subseteq M$ and on $Σ$ . By [L1], any other minimal primary decomposition has the same associated-prime set, so it yields the same $S$ and therefore the same intersection.

L1step 3.1

5.1

Thus the intersection of the primary components indexed by any downward-closed subset of ${Ass}_{R} (M / N)$ is intrinsic.

step 4.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

19 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 and isolated-component discussion (standard reference, not scraped)