1.7 Selected Results on Primary Decomposition
Given a prime ideal \(\mathfrak {p}\) of the ring \(R\), an ideal \(I\) is \(\mathfrak {p}\)-primary if for all \(x, y \in I\), either \(x \in I\) or \(y^n \in I\) for some \(n\). (This is already in mathlib)
If \(\mathfrak {q}\) is a primary ideal, then \(\sqrt{q}\) is a prime ideal.
Let \(I_{1}, \ldots , I_{n}\) be \(\mathfrak {p}\)-primary ideals. Then their intersection is \(\mathfrak {p}\)-primary.
“isPrimary_inf” in mathlib is this but for only two ideals, so just use induction.
A primary decomposition of an ideal \(I \subset R\) is an expression of \(I\) as an intersection of primary ideals, that is a collection of ideals \(\mathfrak {q}_{i}\), \(1 \leq i \leq n\), such that
An ideal \(I\) is decomposable there exists a primary decomposition with intersection \(I\).
A minimal primary decomposition is a primary decomposition such that
The ideals \(\sqrt{\mathfrak {q}_{i}}\) are distinct
- \[ \bigcap _{i \neq j}^{} \mathfrak {q}_{j} \not\subset \mathfrak {q}_{i} \]
for all \(1 \leq i \leq n\).
Any decomposable ideal has a minimal primary decomposition
Reduce to the case where there is a single prime ideal per primary ideal by lemma 1.7.3, and then if there are any superflous terms breaking condition (ii), remove them.
See Atiyah-MacDonald, Theorem 4.5