- Boxes
- definitions
- Ellipses
- theorems and lemmas
- Blue border
- the statement of this result is ready to be formalized; all prerequisites are done
- Orange border
- the statement of this result is not ready to be formalized; the blueprint needs more work
- 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
- Dark green background
- the proof of this result and all its ancestors are formalized
- Dark green border
- this is in Mathlib
Let \(A\) be a Noetherian ring, \(M\) be a finitely generated torsion \(A\)-module. The characteristic ideal of \(M\), denoted by \(\operatorname{char}_A(M)\), or simply \(\operatorname{char}(M)\) if there is no risk of confusion, is defined to be
Let \(A\) be a Noetherian ring. Let \(0\to M'\to M\to M''\to 0\) be a short exact sequence of finitely generated \(A\)-modules. Then \(M\) is \(A\)-torsion if and only if \(M'\) and \(M''\) are \(A\)-torsion. If \(M\) is \(A\)-torsion, then \(\operatorname{char}_A(M)=\operatorname{char}_A(M')\operatorname{char}_A(M'')\).
Let \(A\) be a Noetherian ring, \(M\) be a finitely generated torsion \(A\)-module. Then for any height one prime \({\mathfrak {p}}\) of \(A\), \(M_{\mathfrak {p}}\) is an \(A_{\mathfrak {p}}\)-module of finite length. Moreover, there are only finitely many height one primes \({\mathfrak {p}}\) of \(A\) such that \(M_{\mathfrak {p}}\neq 0\).
Let \(K\) be a number field, \(p\) be a prime, \(K_\infty /K\) be a \({\mathbb {Z}}_p\)-extension. Then there exist integers \(\lambda ,\mu ,\nu \) such that for all sufficiently large \(n\), \(\operatorname{ord}_p(\# {\mathrm{Cl}}(K_n))=\mu p^n+\lambda n+\nu \).
If \(X\) is a finitely generated torsion \(\Lambda \)-module such that \(X/(\gamma ^{p^n}-1)X\) is finite for any \(n\geq 0\), then there exists some constant \(\nu =\nu (X)\) such that for all sufficiently large \(n\), \(\operatorname{ord}_p(\# (X/(\gamma ^{p^n}-1)X))=\mu (X)p^n +\lambda (X)n+\nu (X)\).
If \((A,{\mathfrak {m}},k)\) is a local ring, then a polynomial \(f(X)=\sum _{i=0}^na_iX^i\in A[X]\) is called a distinguished polynomial if \(a_n=1\) and \(a_i\in {\mathfrak {m}}\) for all \(0\leq i\leq n-1\).
(Mathlib: Polynomial.IsDistinguishedAt)
Let \(A\) be a domain, \(S\) be a subset of \({\mathrm{Spec}}(A)\) such that \(A_{\mathfrak {p}}\) is integrally closed for all \({\mathfrak {p}}\in S\) and \(\bigcap _{{\mathfrak {p}}\in S}A_{\mathfrak {p}}=A\) inside \({\mathrm{Frac}}(A)\). Then \(A\) itself is integrally closed.
(Mathlib: IsIntegrallyClosed.of_localization.)
Let \((A,{\mathfrak {m}},k)\) be a complete local ring, \(g(X)=\sum _{i=0}^n a_iX^i\in A[X]\) be a polynomial such that \(a_n\in A\setminus {\mathfrak {m}}\) and \(a_i\in {\mathfrak {m}}\) for all \(i{\lt}n\). Then the natural map \(A[X]/(g)\to A[[X]]/(g)\) is an isomorphism.
The Iwasawa algebra is defined as the completed group algebra
where the transition map \({\mathbb {Z}}_p[\Gamma _{n+1}]\to {\mathbb {Z}}_p[\Gamma _n]\) is induced by the natural projection \(\Gamma _{n+1}\to \Gamma _n\). Each \({\mathbb {Z}}_p[\Gamma _n]\) is a free \({\mathbb {Z}}_p\)-module of rank \(p^n\), we endow it with the \(p\)-adic topology, and endow \(\Lambda \) with the subspace topology of the product topology of \(\prod _{n=0}^\infty {\mathbb {Z}}_p[\Gamma _n]\).
There is an isomorphism of topological rings \({\mathbb {Z}}_p[[T]]\xrightarrow \sim \Lambda \) sending \(1+T\) to \(\gamma \), where \({\mathbb {Z}}_p[[T]]\) is endowed with \((p,T)\)-adic topology.
For each \(n\geq 0\), there is an isomorphism of \({\mathbb {Z}}_p\)-algebras
They are all free \({\mathbb {Z}}_p\)-modules of finite rank, we endow them with \(p\)-adic topology. By Proposition 4.2 we know that it is a homeomorphism of topological spaces.
(i) The \(\mu \)-invariant of \(X\) is defined to be \(\mu (X):=\sum _{j=1}^sn_j\), and the \(\lambda \)-invariant of \(X\) is defined to be \(\lambda (X):=\sum _{i=1}^mb_i\deg f_i\).
(ii) If \(f\in {\mathbb {Z}}_p[[T]]\) is not zero, then define \(\mu (f)\) be the integer such that \(f\in p^{\mu (f)}{\mathbb {Z}}_p[[T]]\) but \(f\notin p^{1+\mu (f)}{\mathbb {Z}}_p[[T]]\), define \(\lambda (f)\) be the leading degree of \((p^{-\mu (f)}f\bmod p)\in {\mathbb {F}}_p[[T]]\).
We have \(\mu (X)=\sum _{i=0}^\infty \operatorname{rank}_{{\mathbb {F}}_p[[T]]}X[p^{i+1}]/X[p^i]\), and \(\lambda (X)=\operatorname{rank}_{{\mathbb {Z}}_p}X/X[p^\infty ]\).
An integral domain \(A\) is called a Krull domain if it satisfies the following properties:
\(A_{\mathfrak {p}}\) is a discrete valuation ring for all height one primes \({\mathfrak {p}}\) of \(A\),
\(A=\bigcap _{{\mathfrak {p}}\in {\mathrm{Spec}}(A),{\mathrm{ht}}({\mathfrak {p}})=1}A_{\mathfrak {p}}\) inside \({\mathrm{Frac}}(A)\),
any nonzero element of \(A\) is contained in only a finitely many height one primes of \(A\).
Let \(A\) be a Noetherian ring. If \({\mathfrak {a}}=(a_1,\cdots ,a_n)\) is an ideal of \(A\) generated by \(n\) elements, and \({\mathfrak {p}}\) is a minimal prime over-ideal of \({\mathfrak {a}}\), then \({\mathrm{ht}}({\mathfrak {p}})\leq n\).
(Mathlib: Ideal.height_le_spanRank_toENat_of_mem_minimal_primes.)
Conversely, if \({\mathfrak {p}}\) is a prime ideal of \(A\) of height \(\leq n\), then there exists an ideal \({\mathfrak {a}}\) of \(A\) generated by \(n\) elements, such that \(\overline{\mathfrak {p}}\) is a minimal prime in \(A/{\mathfrak {a}}\).
(Mathlib: Ideal.exists_spanRank_eq_and_height_eq, Ideal.height_le_iff_exists_minimalPrimes.)
Any height \(1\) prime \({\mathfrak {p}}\) of \(\Lambda \) is principal. Moreover,
(i) If the generator of \({\mathfrak {p}}\) is in \(p{\mathbb {Z}}_p[[T]]\), then we must have \({\mathfrak {p}}=(p)\).
(ii) If the generator of \({\mathfrak {p}}\) is not in \(p{\mathbb {Z}}_p[[T]]\), then by Proposition 4.9 such \({\mathfrak {p}}\) has a unique generator which is a distinguished polynomial.
\(\Lambda \) is a Noetherian regular local ring of Krull dimension \(2\).
(We try to avoid this result but prove its consequences directly, since regular local ring is still WIP in mathlib.)
If \(X\) is a finitely generated torsion \(\Lambda \)-module, then there exists a pseudo-isomorphism
where \(f_1,\cdots ,f_m\) are distinguished polynomials. The characteristic ideal \(\operatorname{char}_\Lambda (X)\) is generated by \(p^{\sum _{j=1}^sn_j}\prod _{i=1}^mf_i^{b_i}\) which is contained in \(p^{\sum _{j=1}^sn_j}{\mathbb {Z}}_p[[T]]\) but not in \(p^{1+\sum _{j=1}^sn_j}{\mathbb {Z}}_p[[T]]\).
Let \(A\) be a ring, \({\mathfrak {a}}\) be an ideal of \(A\). Let \(M,N\) be two \(A\)-modules, and \(\varphi :M\to N\) be an \(A\)-module homomorphism. Then \(\varphi \) is continuous if we endow \(M,N\) with \({\mathfrak {a}}\)-adic topology.
In particular, if \(\varphi \) is an \(A\)-module isomorphism, then it is a homeomorphism of topological spaces if we endow \(M,N\) with \({\mathfrak {a}}\)-adic topology.
For a Noetherian local domain \(A\) of dimension one, the following are equivalent.
\(A\) is integrally closed.
The maximal ideal of \(A\) is principal.
\(A\) is a discrete valuation ring.
\(A\) is a regular local ring.
(Mathlib: IsDiscreteValuationRing.TFAE and tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain.)
Let \(A\) be a Noetherian ring and \(M\) be a finitely generated \(A\)-module. Then there exists a chain of submodules of \(M\)
such that for each \(1\leq i\leq n\), \(M_i/M_{i-1} \cong A/{\mathfrak {p}}_i\) for some prime ideal \({\mathfrak {p}}_i\in {\mathrm{Spec}}(A)\).
Suppose \(K\) is any number field, and \(K_\infty /K\) is any \({\mathbb {Z}}_p\)-extension. Let \(L_\infty \) be the maximal unramified abelian pro-\(p\) extension of \(K_\infty \), let \(X_\infty :={\mathrm{Gal}}(L_\infty /K_\infty )\) which is a \(\Lambda \)-module, where \(\Lambda :={\mathbb {Z}}_p[[\Gamma ]]\), isomorphic to \({\mathbb {Z}}_p[[T]]\) by choosing a topological generator \(\gamma \) of \(\Gamma \), and maps \(T\) to \(\gamma -1\). Then \(X_\infty \) is a finitely generated torsion \(\Lambda \)-module.
Suppose \(\Lambda \cong {\mathbb {Z}}_p[[T]]\), \(X\) is a pro-\(p\) \(\Lambda \)-module, \(x_1,\cdots ,x_t\in X\) such that their images in \(X/TX\) generate \(X/TX\) as a \(\Lambda /(T)\)-module. Then \(x_1,\cdots ,x_t\) generate \(X\) as a \(\Lambda \)-module.
Suppose \(X\) has rank \(r\) as a \(\Lambda \)-module, then we have
as \(n\to \infty \). This is left as an exercise. For example, if \(X=\Lambda \), then \(r=1\), and \(\operatorname{rank}_{{\mathbb {Z}}_p}\big(X/((1+T^{p^n})-1)X\big)=p^n\).
If \(K\) is any number field, \(K_\infty /K\) is any \({\mathbb {Z}}_p\)-extension, and \({\mathfrak {l}}\) is a prime of \(K\) not lying over \(p\). Then \({\mathfrak {l}}\) is unramified in \(K_\infty /K\).
Let \(A\) be a Noetherian ring and let \(M,N\) be finitely generated torsion \(A\)-modules. Let \(\Sigma =\{ {\mathfrak {q}}_1,\cdots ,{\mathfrak {q}}_r\} =\{ {\mathfrak {q}}\in {\mathrm{Supp}}(M)\cup {\mathrm{Supp}}(N)\mid {\mathrm{ht}}({\mathfrak {q}})=1\} \) (by Proposition 3.1 this is a finite set). Let \(S:=A\setminus \bigcup _{i=1}^r{\mathfrak {q}}_i\) which is a multiplicative subset of \(A\). Let \(f:M\to N\) be an \(A\)-module homomorphism. Then \(f\) is a pseudo-isomorphism if and only if \(S^{-1}f:S^{-1}M\to S^{-1}N\) is an isomorphism.
Let \(A\) be a Noetherian ring whose height one localizations are PID (Definition 3.9). Let \(M,N\) be finitely generated torsion \(A\)-modules. Then the followings are equivalent:
There exists a pseudo-isomorphism \(M\to N\).
For any height one prime \({\mathfrak {p}}\) of \(A\), we have \(M_{\mathfrak {p}}\cong N_{\mathfrak {p}}\).
In particular, if there exists a pseudo-isomorphism \(M\to N\), then there also exists a pseudo-isomorphism \(N\to M\).
Let \(A\) be a ring, and let \(f(X)=\sum _{n=0}^\infty a_nX^n\in A[[X]]\) be a formal power series. Then \(f(X)\in A[[X]]^\times \) if and only if \(a_0\in A^\times \).
(Mathlib: PowerSeries.isUnit_iff_constantCoeff)
Let \(A\) be a Noetherian ring.
(i) A finitely generated \(A\)-module \(M\) is called a pseudo-null \(A\)-module, if \(M_{\mathfrak {p}}=0\) for all prime ideals \({\mathfrak {p}}\) of \(A\) of height \(\leq 1\).
(ii) An \(A\)-linear homomorphism \(f:M\to N\) between finitely generated \(A\)-modules is called a pseudo-isomorphism (pis for short), if its kernel and cokernel are pseudo-null \(A\)-modules.
(iii) Two finitely generated \(A\)-modules \(M,N\) are called pseudo-isomorphic (pis for short), denoted by \(M\sim _{\mathrm{pis}}N\) or simply \(M\sim N\), if there exists a pseudo-isomorphism from \(M\) to \(N\).
Let \(A\) be a Noetherian ring, \(M\), \(N\) be finitely generated torsion \(A\)-modules.
(i) If \(M\) is pseudo-null, then \(\operatorname{char}_A(M)=0\).
(ii) If \(M\sim N\), then \(\operatorname{char}_A(M)=\operatorname{char}_A(N)\).
Let \(A\) be a Noetherian ring, \(M\) be a finitely generated \(A\)-module.
(i) If \(A\) is of Krull dimension \(\leq 1\), then \(M\) is pseudo-null if and only if \(M=0\).
(ii) If \(A\) is of Krull dimension \(2\), is a local ring with finite residue field, then \(M\) is pseudo-null if and only if the cardinality of \(M\) is finite.
A regular local ring is a UFD.
(We try to avoid this result since regular local ring is still WIP in mathlib.)
Let \(A\) be a Noetherian ring whose height one localizations are PID (Definition 3.9). Let \(M\) be a finitely generated torsion \(A\)-module. Then there exist height one primes \({\mathfrak {p}}_1,\cdots ,{\mathfrak {p}}_s\) of \(A\) and positive integers \(k_1,\cdots ,k_s\), such that there exists a pseudo-isomorphism \(M\to \bigoplus _{i=1}^s A/{\mathfrak {p}}_i^{k_i}\). Moreover, the sequence \(({\mathfrak {p}}_i^{k_i})_{i=1}^s\) is unique up to ordering.
Let \(A\) be a Noetherian domain. Then \(A\) is a UFD if and only if every prime ideal of height \(1\) is principal (recall that a prime ideal \({\mathfrak {p}}\) is of height \(1\) if \({\mathfrak {p}}\neq 0\) and there is no prime ideal lies in between \(0\) and \({\mathfrak {p}}\)).
(We only need “\(\Rightarrow \)” in our project.)
Let \((A,{\mathfrak {m}},k)\) be a complete local ring, \(g(X)=\sum _{i=0}^\infty a_iX^i\in A[[X]]\setminus {\mathfrak {m}}[[X]]\) be a formal power series such that not all of its coefficients are in \({\mathfrak {m}}\). Let \(n\geq 0\) be the integer such that \(a_n\in A\setminus {\mathfrak {m}}=A^\times \) and \(a_i\in {\mathfrak {m}}\) for all \(0\leq i\leq n-1\). Then for any \(f\in A[[X]]\), there exists a unique formal power series \(q(X)\in A[[X]]\) and a unique polynomial \(r(X)\in A[X]\) of degree \(\leq n-1\) such that \(f=gq+r\).
Let \((A,{\mathfrak {m}},k)\) be a complete local ring. Let \(g(X)\in A[[X]]\setminus {\mathfrak {m}}[[X]]\) be a formal power series such that not all of its coefficients are in \({\mathfrak {m}}\). Then there is a unique distinguished polynomial \(f(X)\in A[X]\) and a unique invertible formal power series \(h(X)\in A[[X]]^\times \) such that \(g=fh\).
(This is incorrect ...) For each \(n\geq 0\) there is an isomorphism \(X_\infty /(\gamma ^{p^n}-1)X_\infty \xrightarrow \sim X_n\).
Let \(K\) be a field, \(p\) be a prime.
(i) An extension \(K_\infty /K\) is called a \({\mathbb {Z}}_p\)-extension, if it is Galois with \(\Gamma ={\mathrm{Gal}}(K_\infty /K)\cong {\mathbb {Z}}_p\) as topological groups.
(ii) If \(K_\infty /K\) is a \({\mathbb {Z}}_p\)-extension, then for any \(n\geq 0\), define \(K_n:=K_\infty ^{\Gamma ^{p^n}}\).
(i) Let \(L_\infty :=\bigcup _{n\geq 0}L_n=\bigcup _{n\geq 0}L_nK_\infty \), then it is an unramified abelian pro-\(p\) extension of \(K_\infty \), because each \(L_nK_\infty /K_\infty \) is finite unramified abelian \(p\)-extension.
(ii) Let \(L_\infty '\) be the maximal unramified abelian pro-\(p\) extension of \(K_\infty \), that is, the compositum of all finite unramified abelian \(p\)-extensions of \(K_\infty \).
(i) For each \(n\geq 0\) let \(L_n\) be the \(p^\infty \)-Hilbert class field of \(K_n\). That is, the maximal unramified abelian extension of \(K_n\) of exponent \(p^\infty \).
(ii) Let \(X_n:={\mathrm{Gal}}(L_n/K_n)\cong {\mathrm{Cl}}(K_n)(p)\), the maximal quotient of the class group \({\mathrm{Cl}}(K_n)\) which is \(p^\infty \)-torsion.