- Boxes
- definitions
- Ellipses
- theorems and lemmas
- Blue border
- the statement of this result is ready to be formalized; all prerequisites are done
- Blue background
- the proof of this result is ready to be formalized; all prerequisites are done
- Green border
- the statement of this result is formalized
- Green background
- the proof of this result is formalized
Let \(E\) be an additive subgroup of \(R\) which is multiplicatively closed. Let \(I_{1}, \ldots , I_{n}\) be ideals such that \(I_{3}, \ldots , I_{n}\) are prime. Then if \(E\) is not contained in any one of the \(I_{j}\), then \(E\) is not contained in their union.
Let \(R\) be a ring and \(\mathfrak {p}_{1}, \ldots , \mathfrak {p}_{m}\) be prime ideals. Let \(x\) be some element of \(R\) and let \(J\) be an ideal. Define \(I := (x) + J\). If \(I \not\subset \mathfrak {p}_{j}\) for all \(j\), then there exists some \(y \in J\) such that \(x + y \not\in \mathfrak {p}_{j}\) for all \(j\)
Let \(\mathfrak {p}_{1}, \ldots , \mathfrak {p}_{n}\) be prime ideals. Let \(I\) be an ideal contained in in their union. Then \(I \subset \mathfrak {p}_{i}\) for some \(i\).
Let \(I_{1}, \ldots , I_{n}\) be ideals, let \(\mathfrak {p}\) be a prime ideal containing the intersection of them all. Then \(I_{i} \subset \mathfrak {p}\) for some \(i\). If \(\mathfrak {p}\) is exactly the intersection, then \(I_{i} = \mathfrak {p}\) for some \(i\).
Let \((R,\mathfrak {m},k)\) be a local ring. Let \(M\) be an \(R\)-module. If the elements \(x_1, \ldots , x_n\) are elements in \(M\) that form a basis in the projection \(M / \mathfrak {m} M\), then \(x_1, ldots, x_n\) generate \(M\).
Let \(R\) be a ring, and \(\mathfrak {p}_{1}, \ldots , \mathfrak {p}_{m}\) be prime ideals. Let \(I\) be a finitely generated ideal of \(R\). Then if \(I \not\subset \mathfrak {p}_{j}\) for all \(j \in \{ 1, \ldots , m\} \), then there exists an \(x \in I\) such that \(x \not\in \mathfrak {p}_{j}\) for all \(j\).
Let \(x \in R\) be an element which is not in any minimal prime ideal. Then \(\dim R / (x) \leq \dim R - 1\)
The annihilator of a module M is the ideal of elements \(r \in R\) such that \(rm = 0\) for all \(m \in M\).
The set \(\operatorname {Assoc}_R (M)\) is the set of primes satisfying the preivious proposition
An ideal \(I\) is decomposable there exists a primary decomposition with intersection \(I\).
A free resolution of \(M\) over \(R\) is a projective resolution whose components \(P^i\) are free.
The global dimension of a ring \(R\) is the supremum over all \(R\)-modules of \(\text{proj dim}M\).
The height of an ideal \(I \subset R\) is the infimum of the heights of prime ideals containing \(I\).
Let \(R\) be a ring, and \(\mathfrak {p}\) be a prime ideal in \(R\). Then the height of \(\mathfrak {p}\) is the sup of the lengths of chains
The Krull dimension of the \(R\) is the supremum of heights of prime ideals \(\mathfrak {p} \subset R\).
The length of a projective resolution \(P_\cdot \) is the highest \(i\) such that \(P^i\) is nonzero. If there exists no such \(i\), the length is infinity
Let \((R,\mathfrak {m},k)\) be a local (noetherian?) ring. Let \(\nu (R)\) be the minimum of the lengths of generating sets of \(\mathfrak {m}\)-primary ideals.
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\).
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)
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 \(\mathfrak {p}\)-primary if it’s radical is equal to \(\mathfrak {p}\).
Let \(M\) be an \(R\)-module. Then \(\text{proj dim}M\) is the minimum length of a projective resolution of \(M\). It lives in the set \(\mathbb {N} \cap \infty \).
Let \(R\) be a ring. Let \(M\) be an \(R\)-module. A projective resolution of \(M\) over \(R\) Is an exact sequence
. That is to say, a projective resolution is a quasi-isomorphism of complexes between the inclusion of \(M\) into chain complexes over \(R\) (i.e. the complex which has \(M\) in degree zero, trivial everywhere else, with trivial maps) and a bounded—below complex whose components are projective \(R\)-modules.
Let \(M\) be an \(R\)-module. An element \(x \in R\) is \(M\)-regular if it does not annihilate any element in \(M\). In colon notation, it is non a member of the ideal \(( 0 : M )\). If \(x\) is an \(R\)-regular element, we simply say it is a regular element.
A local ring \(R\) is regular if \(\mathfrak {m}\) is generated by a system of parameters.
A ring \(R\) is regular if \(R_{\mathfrak {p}}\) is regular for every \(\mathfrak {p} \in R\).
Let \(M\) be an \(R\)-module. An \(M\)-regular sequence is a weak \(M\)-regular sequence such that \(M / (x_1, \ldots , x_n) M \neq 0\). If \(M = R\), we simply call this a regular sequence.
The support of a module is the set of prime ideals \(\mathfrak {p} \subset R\) such that \(M_{\mathfrak {p}} \neq 0\).
Let \(M\) be an \(R\)-module. Then a weak \(M\)-regular sequence is a sequence \(x_1, \ldots , x_n\) with \(x_i \in R\) for all \(i\), such that \(x_i\) is a \(M / (x_1, \ldots , x_{i-1}) M\)-regular element for all \(i\). If \(M = R\), we say that \(x_1, \ldots , x_n\) is a weak regular sequence.
The zero locus of the annihilator of a module is the same as the support of that module. I.e. the set of prime ideals containing the \(\operatorname {Ann}_R(M)\) is the support of \(M\).
The assocated primes of \(M\) are precisely the primes which are minimal in the support of \(M\).
An element \(x \in R\) is a zero-divisor iff it is in an associated prime. (geometrically, it vanishes at an associated point)
Let \(R\) a ring and \(\mathfrak {p}\) a prime ideal, then
If there exists a projective resolution of \(M\) with finite length, then \(\text{proj dim}M {\lt} \infty \).
Let \(I_{1}, \ldots , I_{n}\) be \(\mathfrak {p}\)-primary ideals. Then their intersection is \(\mathfrak {p}\)-primary.
Let \(M\) be an \(R\)-module. Let \(S\) be a multiplicative set. Let \(\ldots \to A_2 \to A_1 \to A_0 \to M \to 0\) be a free resoltion of \(M\). Then \(\ldots S^{-1}(A_2) \to S^{-1}(A_1) \to S^{-1}(A_0) \to S^{-1}M \to 0\) is a free resolution of \(S^{-1}M\).
(See BH 1.2.2) Let \(R\) be a ring, and \(\mathfrak {p}_{1}, \ldots , \mathfrak {p}_{m}\) be prime ideals. Let \(M\) be an \(R\)-module, and let \(x_{1}, \ldots , x_{n} \in M\). Let \(N\) be the submodule generated by \(x_{1}, \ldots , x_{n}\).
If \(N_{\mathfrak {p}_{j}} \not\subset \mathfrak {p}_{j}M_{\mathfrak {p}_{j}}\) for all \(j \in \{ 1, \ldots , m\} \), then there exist \(a_{2}, \ldots , a_{n} \in R\) such that \(x_{1} + \sum _{i=2}^{n} a_{i}x_{i} \not\in \mathfrak {p}_{j} M_{\mathfrak {p}_{j}} \) for all \(j \in \{ 1, \ldots , m\} \).
Let \(R\) be a regular local ring. Then \(R\) has finite global dimension. That is, any finitely generated module \(R\) has finite projective dimension.
\(R\) is regular if and only if the minimal number of generators of its maximal ideal is equal to the (Krull) dimension of \(R\)
Let \(f : M \to M\) be a surjection of modules (over a local ring?). Then \(f\) is an isomorphism.
Let \(R\) a ring, and \(M\) an \(R\)-module. Let \(\mathfrak {p}\) be a prime ideal, then the following are equivalent:
\(\mathfrak {p} = \operatorname {Ann}_R (m)\) for some element \(m \in M\).
\(R / \mathfrak {p}\) embeds into \(M\).
There exists a free resolution \(F_\cdot \) of \(M\) such that length of \(F_\cdot \) is equal to the projective dimension of \(M\).
The following are equivalent Firstly, \(R\) is regular. Secondly, the zariski cotangent space is a vector space of dimension \(\dim R\).
A local ring \(R\) is regular if and only if its maximal ideal is generated by a regular sequence.
Let \(R\) be a regular local ring. Then \(R / I\) is regular local if and only if \(I\) is generated by a (regular) system of parameters (I.e. a generating set for \(\mathfrak {m}\)).
Let \((R,\mathfrak {m},k\) be a noetherian local ring. The following are equivalent:
\(R\) is regular.
\(R\) has finite global dimension.
\(\text{proj dim}k {\lt} \infty \)
Let \((R,\mathfrak {m},k)\) be a local noetherian ring. Let \(n \in \mathbb {N}\). Then the following are equivalent
\(\dim R = n\)
\(\operatorname {height}\mathfrak {m} = n\)
\(\nu (R) = n\).
Let \((R,\mathfrak {m},k)\) be a local noetherian ring. Let \(I\) be a nonzero ideal with finite projective dimension. If \(I / I^2\) is a free \(R\)-module, then \(I\) is generated by a regular sequence.
Let \(R\) a noetherian ring, and \(I\) a proper ideal of height \(n\). Then for all \(1 \leq i \leq n\), there exist elements \(x_{1}, \ldots , x_{i}\) such that \(\operatorname {height}(x_{1}, \ldots , x_{i}) = i\).
Let \(I = (x_{1}, \ldots , x_{n})\) be an ideal. Then each minimal prime over \(I\) has height at most \(n\).
Let \(R\) be a noetherian ring, and \(I\) a prinicpal ideal. Then each minimal prime ideal over \(I\) (i.e. minimal among primes containing I) has height at most 1.
Let \(R\) be a ring, and \(M\) an \(R\)-module. Let \(x\) be an \(M\)-regular element. Then \(\dim M / xM \leq \dim M - 1\).
Let \(R\) be a regular local ring, and let \(\mathfrak {p}\) be a prime ideal in \(R\). Then \(R_{\mathfrak {p}}\) is a regular local ring.