FC09 — Jürgen Neukirch, Algebraic Number Theory (1999)
FC09 — Neukirch, Algebraic Number Theory.
This chapter contains 56 definitions, 10 theorems, 44 propositions, 8 lemmas, 6 corollaries, 3 examples, 6 conventions and 2 other statements.
Of the 135 statements checked against Lean, 65 are formalized somewhere and 70 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 70 | 52% | A documented search found no Lean statement of it anywhere. |
| in Mathlib | 64 | 47% | Mathlib states and proves it. |
| in another Lean project | 1 | 1% | Some other Lean development has it; using it means porting that code. |
| checked in total | 135 |
- Canonical source block: FC09 Neukirch Chapter I,
FC09-C01-U001–FC09-C01-U135, in canonical source-ID order from Foundational corpus units FC09 Neukirch. The generator retrieves all 135 rows throughagent-memory, asserts exact order/uniqueness, and assigns exactly one route to every unit. - Project-first inspection used
A=3b2239e161592472b34e02ad3b7da308f9ce7280(Lean 4.33.0, Apache-2.0). Project-owned arithmetic code was searched first, includingLeanCategories/Algebra/FractionalIdeals.lean; that wrapper re-exposes the class-group map/kernel/surjectivity pieces but does not close a C01 bundle beyond the pinned Mathlib owners recorded here, so C01 has noproject-existingroute. - Pinned Mathlib is
P=db584cd6d46c92f209a44c0f1c829460d327499d, Lean 4.33.0, Apache-2.0. Native coverage is extensive in Gaussian integers, number fields/integrality, trace/norm/discriminants, Dedekind and fractional ideals, Minkowski/class-number/Dirichlet-unit theory, ramification/Hilbert/cyclotomic theory, localization/DVRs, affine schemes, and rational-function valuations. - Current Mathlib was checked at
H=71a80585ee495fc24472fd0eaffc89d94e4fd8d6(2026-09-07 00:03:14 UTC). Targeted current-tree symbol/file searches and targeted open-PR searches were run for the unresolved bundles. Current H contains neither the #40848 localization declarations nor the #40791 S-unit theorem module. Open PR #40848 at2c91fb2be280d3a396f0f7de2d7d0df5bf2a8243proves that the valuation-defined S-integer ring is the required localization and a Dedekind domain; this changes U096 to a revision-specificreference-port. Open PR #40791 at6c4013931e7a0c11d5696f2bcf76628d6fcdf565proves finite generation and the rank formula for S-units, but no checked source-complete route here identifies its torsion factor withμ(K)and packages Neukirch U097’s full direct-product isomorphism, so U097 remains unmatched. - Strict bundle semantics was enforced throughout. In particular, the Gaussian infrastructure does not earn U006’s complete prime classification or U007’s
ℤ[i]=𝓞_{ℚ(i)}identification; the pinned embedding formulas do not earn U015 without its characteristic-polynomial factorization; the standard mixed-space convention is not silently identified with Neukirch’s all-embeddings metric/measure in U045–U048; the weaker exported Minkowski class bound does not earn U053’s sharp(2/π)^sconstant; the deleted-coordinate regulator convention does not earn U060’s√(r+s)covolume statement; and partial Hilbert-theory APIs do not earn the full U081 inertia-field bundle. - The late chapter is treated the same way: local/scheme order-of-vanishing APIs do not earn U115’s global divisor/principal-divisor/rational-equivalence bundle; a generic presheaf does not earn U124 because Neukirch also imposes
F(∅)=0; and the rational-function Ostrowski theorem does not earn U132 because that unit also asserts finiteness of the valuations outside the chosen affine model. Spec/Zariski/residue fields, sheaf/stalk/structure-sheaf, and full faithfulness of affine Spec are credited only where they close their complete source units. - All pinned targets listed as
mathlibwere path/token validated against P. The U096 target was validated bygit showat the exact #40848 head revision, and the cited #40791 finite-generation/rank declarations were likewise checked at its exact head. - Route totals for C01:
mathlib64,project-existing0,package-import0,reference-port1,unmatched70.
Theorem (1.1)
(1.1) Theorem. For all prime numbers \(p \neq 2\) , one has: \[ p = a ^ {2} + b ^ {2} \quad (a, b \in \mathbb {Z}) \quad \Longleftrightarrow \quad p \equiv 1 \bmod 4. \]
Formalized. Mathlib/NumberTheory/SumTwoSquares.lean::Nat.Prime.sq_add_sq; Mathlib/NumberTheory/LegendreSymbol/Basic.lean::mod_four_ne_three_of_sq_eq_neg_one — The pinned two-squares theorem and the mod-4 obstruction give the stated iff for odd primes.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition (1.2)
(1.2) Proposition. The ring \(\mathbb{Z}[i]\) is euclidean, therefore in particular factorial.
Formalized. Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean::EuclideanDomain — GaussianInt carries the Euclidean-domain instance used for factoriality.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
The norm of \(z = x + iy\) is defined by \[ N (x + i y) = (x + i y) (x - i y) = x ^ {2} + y ^ {2}, \] i.e., by \(N(z) = |z|^{2}\) . It is multiplicative, so that one has \[ p ^ {2} = N (\alpha) \cdot N (\beta). \] Since \(\alpha\) and \(\beta\) are not units, it follows that \(N(\alpha), N(\beta) \neq 1\) (see exercise 1), and therefore \(p = N(\alpha) = a^2 + b^2\) , where we put \(\alpha = a + bi\) .
Formalized. Mathlib/NumberTheory/Zsqrtd/Basic.lean::norm, norm_def, norm_mul, norm_eq_mul_conj, norm_eq_one_iff' — For d=-1, norm_def is x²+y², norm_eq_mul_conj is N(z)=zar z, and norm_mul is multiplicativity; norm_eq_one_iff' identifies norm-one elements with units, supplying the nonunit step used in the source argument.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition (1.3)
(1.3) Proposition. The group of units of the ring \(\mathbb{Z}[i]\) consists of the fourth roots of unity, \[ \mathbb {Z} [ i ] ^ {*} = \{1, - 1, i, - i \}. \]
Not formalized. Pinned/current Mathlib has substantial Gaussian-integer infrastructure, but no checked declaration or derivation closes this entire source unit with its stated classification/identification clauses.
Definition / construction
In order to answer the question for primes, i.e., irreducible elements of the ring Z[i], we first recall that two elements \(\alpha, \beta\) in a ring are called associated, symbolically \(\alpha \sim \beta\) , if they differ only by a unit factor, and that every element associated to an irreducible element \(\pi\) is also irreducible. Using theorem (1.1) we obtain the following precise list of all prime numbers of Z[i].
Formalized. Mathlib/Algebra/GroupWithZero/Associated.lean::Associated, Associated.irreducible — Associated elements are exactly unit multiples, and Associated.irreducible transports irreducibility.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Theorem (1.4)
(1.4) Theorem. The prime elements \(\pi\) of \(\mathbb{Z}[i]\) , up to associated elements, are given as follows. (1) \(\pi = 1 + i\) (2) \(\pi = a + bi\) with \(a^2 + b^2 = p\) , \(p \equiv 1 \mod 4\) , \(a > |b| > 0\) , (3) \(\pi = p, \quad p \equiv 3 \bmod 4\) . Here, \(p\) denotes a prime number of \(\mathbb{Z}\) .
Not formalized. Pinned/current Mathlib has substantial Gaussian-integer infrastructure, but no checked declaration or derivation closes this entire source unit with its stated classification/identification clauses.
Proposition (1.5)
(1.5) Proposition. \(\mathbb{Z}[i]\) consists precisely of those elements of the extension field \(\mathbb{Q}(i)\) of \(\mathbb{Q}\) which satisfy a monic polynomial equation \[ x ^ {2} + a x + b = 0 \] with coefficients \(a, b \in \mathbb{Z}\) .
Not formalized. Pinned/current Mathlib has substantial Gaussian-integer infrastructure, but no checked declaration or derivation closes this entire source unit with its stated classification/identification clauses.
Definition / construction
An algebraic number field is a finite field extension K of Q. The elements of K are called algebraic numbers. An algebraic number is called integral, or an algebraic integer, if it is a zero of a monic polynomial \(f(x) \in \mathbb{Z}[x]\) . This notion of integrality applies not only to algebraic numbers, but occurs in many different contexts and therefore has to be treated in full generality.
Formalized. Mathlib/NumberTheory/NumberField/Basic.lean::NumberField, RingOfIntegers; Mathlib/RingTheory/IntegralClosure/IsIntegral/Defs.lean::IsIntegral — A NumberField is finite-dimensional over ℚ; IsIntegral ℤ x is exactly satisfaction of a monic polynomial over ℤ, and RingOfIntegers is the resulting integral closure.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition (2.1)
(2.1) Definition. Let \(A \subseteq B\) be an extension of rings. An element \(b \in B\) is called integral over \(A\) , if it satisfies a monic equation \[ x ^ {n} + a _ {1} x ^ {n - 1} + \dots + a _ {n} = 0, \quad n \geq 1, \] with coefficients \(a_{i} \in A\) . The ring B is called integral over A if all elements \(b \in B\) are integral over A.
Formalized. Mathlib/RingTheory/IntegralClosure/IsIntegral/Defs.lean::IsIntegral, Algebra.IsIntegral — Integrality is defined by a monic polynomial equation, with algebra integrality meaning every element is integral.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition (2.2)
(2.2) Proposition. Finitely many elements \(b_{1}, \ldots, b_{n} \in B\) are all integral over A if and only if the ring \(A[b_{1}, \ldots, b_{n}]\) viewed as an A-module is finitely generated.
Formalized. Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean::IsIntegral.fg_adjoin_singleton, Algebra.finite_adjoin_of_finite_of_isIntegral; Mathlib/RingTheory/IntegralClosure/Algebra/Basic.lean::IsIntegral.of_finite — The pinned finite-adjoin theorem gives the forward implication and module-finite implies integrality for the converse.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition (2.3)
(2.3) Proposition (Row-Column Expansion). Let \(A = (a_{ij})\) be an \((r \times r)\) -matrix with entries in an arbitrary ring, and let \(A^{*} = (a_{ij}^{*})\) be the adjoint matrix, i.e., \(a_{ij}^{*} = (-1)^{i+j} \det(A_{ij})\) , where the matrix \(A_{ij}\) is obtained from A by deleting the i-th column and the j-th row. Then one has \[ A A ^ {*} = A ^ {*} A = \det (A) E, \] where \(E\) denotes the unit matrix of rank \(r\) . For any vector \(x = (x_{1},\ldots ,x_{r})\) , this yields the implication \[ A x = 0 \implies (\det A) x = 0. \]
Formalized. Mathlib/LinearAlgebra/Matrix/Adjugate.lean::mul_adjugate, adjugate_mul — The two adjugate identities are AA=AA=det(A)I and immediately give the vector consequence.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition (2.4)
(2.4) Proposition. Let \(A \subseteq B \subseteq C\) be two ring extensions. If \(C\) is integral over \(B\) and \(B\) is integral over \(A\) , then \(C\) is integral over \(A\) .
Formalized. Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean::Algebra.IsIntegral.tower_top, isIntegral_trans — Pinned integrality is transitive in algebra towers, exactly Proposition 2.4.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
From what we have proven, the set of all elements \[ \bar {A} = \left\{b \in B \mid b \text { integral over } A \right\} \] in a ring extension \(A \subseteq B\) forms a ring. It is called the integral closure of A in B. A is said to be integrally closed in B if \(A = \overline{A}\) . It is immediate from (2.4) that the integral closure \(\overline{A}\) is itself integrally closed in B. If A is an integral domain with field of fractions K, then the integral closure \(\overline{A}\) of A in K is called the normalization of A, and A is simply called integrally closed if \(A = \overline{A}\) . For instance, every factorial ring is integrally closed.
Formalized. Mathlib/RingTheory/IntegralClosure/Algebra/Basic.lean::integralClosure, mem_integralClosure_iff; Mathlib/RingTheory/IntegralClosure/IntegrallyClosed.lean::IsIntegrallyClosedIn (integralClosure R A) A, integralClosure_eq_bot_iff; Mathlib/RingTheory/Polynomial/RationalRoot.lean::instIsIntegrallyClosed — The integral closure is the subring of integral elements and is itself integrally closed in the ambient algebra; fraction-ring closure is normalization, and the pinned UFD instance supplies the source factorial-ring example.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition (2.5)
(2.5) Definition. The trace and norm of an element \(x \in L\) are defined to be the trace and determinant, respectively, of the endomorphism \[ T _ {x}: L \rightarrow L, \quad T _ {x} (\alpha) = x \alpha , \] of the \(K\) -vector space \(L\) : \[ T r _ {L | K} (x) = T r \left(T _ {x}\right), \quad N _ {L | K} (x) = \det \left(T _ {x}\right). \]
Formalized. Mathlib/RingTheory/Trace/Defs.lean::Algebra.trace; Mathlib/RingTheory/Norm/Defs.lean::Algebra.norm — Pinned trace and norm are defined from the multiplication endomorphism exactly as in the source.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition (2.6)
(2.6) Proposition. If \(L|K\) is a separable extension and \(\sigma : L \to \overline{K}\) varies over the different \(K\) -embeddings of \(L\) into an algebraic closure \(\overline{K}\) of \(K\) , then we have \[ f _ {x} (t) = \prod_ {\sigma} (t - \sigma x),\tag{i} \] (ii) \(Tr_{L|K}(x) = \sum_{\sigma}\sigma x,\) \[ N _ {L | K} (x) = \prod_ {\sigma} \sigma x.\tag{iii} \]
Not formalized. Pinned/current Mathlib has the surrounding number-field, integrality, trace/norm, basis and discriminant APIs, but no checked source-complete theorem closes this stronger basis/index/compositum unit.
Corollary (2.7)
(2.7) Corollary. In a tower of finite field extensions \(K \subseteq L \subseteq M\) , one has \[ T r _ {L | K} \circ T r _ {M | L} = T r _ {M | K}, \quad N _ {L | K} \circ N _ {M | L} = N _ {M | K}. \]
Formalized. Mathlib/RingTheory/Trace/Defs.lean::trace_trace; Mathlib/RingTheory/Norm/Transitivity.lean::Algebra.norm_norm — These are exactly Tr_{M/K}=Tr_{L/K}∘Tr_{M/L} and N_{M/K}=N_{L/K}∘N_{M/L}.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
The discriminant of a basis \(\alpha_{1},\ldots ,\alpha_{n}\) of a separable extension \(L|K\) is defined by \[ d (\alpha_ {1}, \dots , \alpha_ {n}) = \det ((\sigma_ {i} \alpha_ {j})) ^ {2}, \] where \(\sigma_{i}, i = 1, \ldots, n\) , varies over the \(K\) -embeddings \(L \to \overline{K}\) . Because of the relation \[ T r _ {L | K} (\alpha_ {i} \alpha_ {j}) = \sum_ {k} (\sigma_ {k} \alpha_ {i}) (\sigma_ {k} \alpha_ {j}), \] the matrix \((Tr_{L|K}(\alpha_i\alpha_j))\) is the product of the matrices \((\sigma_k\alpha_i)^t\) and \((\sigma_k\alpha_j)\) . Thus one may also write \[ d \left(\alpha_ {1}, \dots , \alpha_ {n}\right) = \det \left(T r _ {L | K} \left(\alpha_ {i} \alpha_ {j}\right)\right). \] In the special case of a basis of type \(1, \theta, \ldots, \theta^{n-1}\) one gets \[ d(1,\theta,\dots,\theta^{n-1}) = \prod_{i<j} (\theta_{i}-\theta_{j})^{2}, \] where \(\theta_{i} = \sigma_{i}\theta\).
Formalized. Mathlib/RingTheory/Discriminant.lean::Algebra.discr, discr_def, discr_eq_det_embeddingsMatrixReindex_pow_two — Mathlib defines the discriminant as the determinant of the trace matrix and proves the separable embedding-matrix determinant-square formula used for Neukirch’s first definition.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition (2.8)
(2.8) Proposition. If \(L|K\) is separable and \(\alpha_{1},\ldots ,\alpha_{n}\) is a basis, then the discriminant \[ d (\alpha_ {1}, \dots , \alpha_ {n}) \neq 0, \] and \[ (x, y) = T r _ {L | K} (x y) \] is a nondegenerate bilinear form on the \(K\) -vector space \(L\) .
Formalized. Mathlib/RingTheory/Discriminant.lean::discr_not_zero_of_basis; Mathlib/RingTheory/Trace/Basic.lean::traceForm_nondegenerate — For a finite separable field extension the pinned theorems give both nonzero discriminant for every basis and nondegeneracy of (x,y)↦Tr(xy).
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Lemma (2.9)
(2.9) Lemma. Let \(\alpha_{1},\ldots ,\alpha_{n}\) be a basis of \(L|K\) which is contained in \(B\) , of discriminant \(d = d(\alpha_1,\dots ,\alpha_n)\) . Then one has \[ d B \subseteq A \alpha_ {1} + \dots + A \alpha_ {n}. \]
Not formalized. Pinned/current Mathlib has the surrounding number-field, integrality, trace/norm, basis and discriminant APIs, but no checked source-complete theorem closes this stronger basis/index/compositum unit.
Definition / construction
A system of elements \(\omega_1, \ldots, \omega_n \in B\) such that each \(b \in B\) can be written uniquely as a linear combination \[ b = a _ {1} \omega_ {1} + \dots + a _ {n} \omega_ {n} \] with coefficients \(a_{i} \in A\) , is called an integral basis of B over A (or: an A-basis of B). Since such an integral basis is automatically a basis of L|K, its length n always equals the degree \([L : K]\) of the field extension. The existence of an integral basis signifies that B is a free A-module of rank \(n = [L : K]\) . In general, such an integral basis does not exist. If, however, A is a principal ideal domain, then one has the following more general result, proposition (2.10): if \(L|K\) is separable and \(A\) is a principal ideal domain, then every finitely generated \(B\)-submodule \(M \neq 0\) of \(L\) is a free \(A\)-module of rank \([L:K]\).
Not formalized. Pinned/current Mathlib has the surrounding number-field, integrality, trace/norm, basis and discriminant APIs, but no checked source-complete theorem closes this stronger basis/index/compositum unit.
Proposition (2.10)
(2.10) Proposition. If \(L|K\) is separable and \(A\) is a principal ideal domain, then every finitely generated \(B\) -submodule \(M \neq 0\) of \(L\) is a free \(A\) -module of rank \([L:K]\) . In particular, \(B\) admits an integral basis over \(A\) .
Not formalized. Pinned/current Mathlib has the surrounding number-field, integrality, trace/norm, basis and discriminant APIs, but no checked source-complete theorem closes this stronger basis/index/compositum unit.
Proposition (2.11)
(2.11) Proposition. Let \(L|K\) and \(L'|K\) be two Galois extensions of degree \(n\) , resp. \(n'\) , such that \(L \cap L' = K\) . Let \(\omega_1, \ldots, \omega_n\) , resp. \(\omega_1', \ldots, \omega_{n'}'\) , be an integral basis of \(L|K\) , resp. \(L'|K\) , with discriminant \(d\) , resp. \(d'\) . Suppose that \(d\) and \(d'\) are relatively prime in the sense that \(xd + x'd' = 1\) , for suitable \(x, x' \in A\) . Then \(\omega_i \omega_j'\) is an integral basis of \(LL'\) , of discriminant \(d^{n'}d'^n\) .
Not formalized. Pinned/current Mathlib has the surrounding number-field, integrality, trace/norm, basis and discriminant APIs, but no checked source-complete theorem closes this stronger basis/index/compositum unit.
Proposition (2.12)
(2.12) Proposition. If \(\mathfrak{a} \subseteq \mathfrak{a}'\) are two nonzero finitely generated \(\mathcal{O}_K\) -submodules of \(K\) , then the index \((\mathfrak{a}' : \mathfrak{a})\) is finite and satisfies \[ d (\mathfrak {a}) = \left(\mathfrak {a} ^ {\prime}: \mathfrak {a}\right) ^ {2} d \left(\mathfrak {a} ^ {\prime}\right). \]
Not formalized. Pinned/current Mathlib has the surrounding number-field, integrality, trace/norm, basis and discriminant APIs, but no checked source-complete theorem closes this stronger basis/index/compositum unit.
Example / comparison
Example: The ring of integers of the field \(K = \mathbb{Q}(\sqrt{-5})\) is given by §2, exercise 4, as \(o_{K} = Z + Z\sqrt{-5}\) . In this ring, the rational integer 21 can be decomposed in two ways, \[ 2 1 = 3 \cdot 7 = (1 + 2 \sqrt {- 5}) \cdot (1 - 2 \sqrt {- 5}). \] All factors occurring here are irreducible in \(O_{K}\) . For if one had, for instance, \(3 = \alpha\beta\) , with \(\alpha, \beta\) non-units, then \(9 = N_{K|\mathbb{Q}}(\alpha) N_{K|\mathbb{Q}}(\beta)\) would imply \(N_{K|\mathbb{Q}}(\alpha) = \pm3\) . But the equation \[ N _ {K | \mathbb {Q}} (x + y \sqrt {- 5}) = x ^ {2} + 5 y ^ {2} = \pm 3 \] has no solutions in \(\mathbb{Z}\) . In the same way it is seen that \(7, 1 + 2\sqrt{-5}\) , and \(1 - 2\sqrt{-5}\) are irreducible. As the fractions \[ \frac {1 \pm 2 \sqrt {- 5}}{3}, \quad \frac {1 \pm 2 \sqrt {- 5}}{7} \] do not belong to \(O_{K}\) , the numbers 3 and 7 are not associated to \(1 + 2\sqrt{-5}\) or \(1 - 2\sqrt{-5}\) . The two prime factorizations of 21 are therefore essentially different. Realizing the failure of unique factorization in general has led to one of the grand events in the history of number theory, the discovery of ideal theory by \(E_{DUARD}\) KUMMER. Inspired by the discovery of complex numbers, Kummer’s idea was that the integers of K would have to admit an embedding into a bigger domain of “ideal numbers” where unique factorization into “ideal prime numbers” would hold. For instance, in the example of \[ 2 1 = 3 \cdot 7 = (1 + 2 \sqrt {- 5}) (1 - 2 \sqrt {- 5}), \] the factors on the right would be composed of ideal prime numbers \(p_{1}, p_{2}, p_{3}, p_{4}\) , subject to the rules \[ 3 = \mathfrak {p} _ {1} \mathfrak {p} _ {2}, \quad 7 = \mathfrak {p} _ {3} \mathfrak {p} _ {4}, \quad 1 + 2 \sqrt {- 5} = \mathfrak {p} _ {1} \mathfrak {p} _ {3}, \quad 1 - 2 \sqrt {- 5} = \mathfrak {p} _ {2} \mathfrak {p} _ {4}. \] This would resolve the above non-uniqueness into the wonderfully unique factorization \[ 2 1 = \left(\mathfrak {p} _ {1} \mathfrak {p} _ {2}\right) \left(\mathfrak {p} _ {3} \mathfrak {p} _ {4}\right) = \left(\mathfrak {p} _ {1} \mathfrak {p} _ {3}\right) \left(\mathfrak {p} _ {2} \mathfrak {p} _ {4}\right). \] Kummer’s concept of “ideal numbers” was later replaced by that of ideals of the ring \(\mathcal{O}_K\) . The reason for this is easily seen: whatever an ideal number \(a\) should be defined to be, it ought to be linked to certain numbers \(a \in \mathcal{O}_K\) by a divisibility relation \(a|a\) satisfying the following rules, for \(a, b, \lambda \in \mathcal{O}_K\) , \[ \mathfrak {a} | a \text { and } \mathfrak {a} | b \Rightarrow \mathfrak {a} | a \pm b; \quad \mathfrak {a} | a \Rightarrow \mathfrak {a} | \lambda a. \] And an ideal number \(\mathfrak{a}\) should be determined by the totality of its divisors in \(\mathcal{O}_K\) \[ \underline {{{{\mathfrak {a}}}}} = \left\{a \in \mathcal {O} _ {K} \mid \mathfrak {a} | a \right\}. \] But in view of the rules for divisibility, this set is an ideal of \(\mathcal{O}_K\) . This is the reason why \(RICHARD \ DEDEKIND\) re-introduced Kummer’s “ideal numbers” as being the ideals of \(\mathcal{O}_K\) . Once this is done, the divisibility relation \(\mathfrak{a} \mid a\) can simply be defined by the inclusion \(a \in \mathfrak{a}\) , and more generally the divisibility relation \(\mathfrak{a} \mid \mathfrak{b}\) between two ideals by \(\mathfrak{b} \subseteq \mathfrak{a}\) . In what follows, we will study this notion of divisibility more closely. The basic theorem here is the following.
Not formalized. Pinned/current Mathlib has Dedekind, fractional-ideal and class-group infrastructure, but this source unit contains a stronger example or exact presentation not exported as a complete compatible theorem.
Theorem (3.1)
(3.1) Theorem. The ring \(O_{K}\) is noetherian, integrally closed, and every prime ideal \(p \neq 0\) is a maximal ideal.
Formalized. Mathlib/NumberTheory/NumberField/Basic.lean::IsDedekindDomain — The ring of integers of every number field has the pinned IsDedekindDomain instance.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition (3.2)
(3.2) Definition. A noetherian, integrally closed integral domain in which every nonzero prime ideal is maximal is called a Dedekind domain.
Formalized. Mathlib/RingTheory/DedekindDomain/Basic.lean::isDedekindDomain_iff — The pinned characterization is Noetherian + integrally closed + dimension one, equivalent to nonzero primes maximal.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
Instead of the ring \(O_{K}\) we will now consider an arbitrary Dedekind domain o, and we denote by K the field of fractions of o. Given two ideals a and b of o (or more generally of an arbitrary ring), the divisibility relation \(a|b\) is defined by \(b \subseteq a\) , and the sum of the ideals by \[ \mathfrak {a} + \mathfrak {b} = \left\{a + b \mid a \in \mathfrak {a}, b \in \mathfrak {b} \right\}. \] This is the smallest ideal containing a as well as b, in other words, it is the greatest common divisor \(\gcd(a,b)\) of a and b. By the same token the intersection \(a \cap b\) is the lcm (least common multiple) of a and b. We define the product of a and b by \[ \mathfrak {a b} = \left\{\sum_ {i} a _ {i} b _ {i} \mid a _ {i} \in \mathfrak {a}, b _ {i} \in \mathfrak {b} \right\}. \] With respect to this multiplication the ideals of o will grant us what the elements alone may refuse to provide: the unique prime factorization.
Formalized. Mathlib/RingTheory/DedekindDomain/Ideal/Basic.lean::Ideal.dvd_iff_le; Mathlib/RingTheory/Ideal/Operations.lean::Ideal.add_eq_sup, mul_mem_mul, span_mul_span — Pinned ideal order gives a|b iff b⊆a in a Dedekind domain; ideal addition is lattice supremum (hence the smallest containing ideal), infimum is intersection, and ideal multiplication is the span of finite products.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Theorem (3.3)
(3.3) Theorem. Every ideal \(\mathfrak{a}\) of \(\mathcal{O}\) different from (0) and (1) admits a factorization \[ \mathfrak {a} = \mathfrak {p} _ {1} \dots \mathfrak {p} _ {r} \] into nonzero prime ideals \(p_{i}\) of O which is unique up to the order of the factors.
Formalized. Mathlib/RingTheory/DedekindDomain/Factorization.lean::finprod_heightOneSpectrum_factorization; Mathlib/RingTheory/DedekindDomain/Ideal/Basic.lean::Ideal.uniqueFactorizationMonoid — Nonzero ideals form a unique-factorization monoid and the height-one factorization theorem gives the explicit prime product.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Lemma (3.4)
(3.4) Lemma. For every ideal \(\mathfrak{a} \neq 0\) of \(\mathcal{O}\) there exist nonzero prime ideals \(\mathfrak{p}_1, \mathfrak{p}_2, \ldots, \mathfrak{p}_r\) such that \[ \mathfrak {a} \supseteq \mathfrak {p} _ {1} \mathfrak {p} _ {2} \dots \mathfrak {p} _ {r}. \]
Formalized. Mathlib/RingTheory/DedekindDomain/Factorization.lean::finprod_heightOneSpectrum_factorization; Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean::prod_normalizedFactors_eq_self — The canonical finite prime factorization supplies the required product of nonzero primes contained in the ideal.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Lemma (3.5)
(3.5) Lemma. Let \(\mathfrak{p}\) be a prime ideal of \(\mathcal{O}\) and define \[ \mathfrak {p} ^ {- 1} = \left\{x \in K \mid x \mathfrak {p} \subseteq \mathcal {O} \right\}. \] Then one has \(\mathfrak{a}\mathfrak{p}^{-1}:=\{\sum_{i}a_{i}x_{i}\mid a_{i}\in\mathfrak{a},x_{i}\in\mathfrak{p}^{-1}\}\neq\mathfrak{a}\) , for every ideal \(\mathfrak{a}\neq0\) .
Formalized. Mathlib/RingTheory/FractionalIdeal/Inverse.lean::mem_inv_iff; Mathlib/RingTheory/DedekindDomain/Ideal/Basic.lean::not_inv_le_one_of_ne_bot, coe_ideal_mul_inv, FractionalIdeal.semifield — For nonzero p, mem_inv_iff is exactly p⁻¹={x | xp⊆O}; a nonzero proper prime has p⁻¹⊄O, and cancellation in the pinned fractional-ideal semifield gives a·p⁻¹≠a for every nonzero a.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Convention / notation
In the sequel such an identity will be automatically understood to signify that the \(p_{i}\) are pairwise distinct. If in particular a is a principal ideal (a), then – following the tradition which tends to attribute to the ideals the rôle of “ideal numbers” – we will write with a slight abuse of notation \[ a = \mathfrak {p} _ {1} ^ {\nu_ {1}} \dots \mathfrak {p} _ {r} ^ {\nu_ {r}}. \] Similarly, the notation \(a|a\) is often used instead of \(\mathfrak{a}|(a)\) and \((\mathfrak{a},\mathfrak{b})=1\) is written for two relatively prime ideals, instead of the correct formula \((\mathfrak{a},\mathfrak{b})=\mathfrak{a}+\mathfrak{b}=\mathcal{O}\) . For a product \(a=a_{1}\cdots a_{n}\) of relatively prime ideals \(a_{1},\ldots,a_{n}\) , one has an analogue of the well-known “Chinese Remainder Theorem” from elementary number theory. We may formulate this result for an arbitrary ring taking into account that \[ \mathfrak{a} = \bigcap_{i=1}^{n} \mathfrak{a}_{i}. \]
Not formalized. Pinned/current Mathlib has Dedekind, fractional-ideal and class-group infrastructure, but this source unit contains a stronger example or exact presentation not exported as a complete compatible theorem.
Chinese Remainder Theorem (3.6)
(3.6) Chinese Remainder Theorem. Let \(\mathfrak{a}_1, \ldots, \mathfrak{a}_n\) be ideals in a ring \(\mathcal{O}\) such that \(\mathfrak{a}_i + \mathfrak{a}_j = \mathcal{O}\) for \(i \neq j\) . Then, if \(\mathfrak{a} = \bigcap_{i=1}^{n} \mathfrak{a}_i\) , one has \[ \mathcal {O} / \mathfrak {a} \cong \bigoplus_ {i = 1} ^ {n} \mathcal {O} / \mathfrak {a} _ {i}. \]
Formalized. Mathlib/RingTheory/Ideal/Quotient/Operations.lean::quotientInfRingEquivPiQuotient; Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean::quotientEquivPiOfProdEq — The pinned quotient-product equivalences give the pairwise-coprime CRT decomposition.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition (3.7)
(3.7) Definition. A fractional ideal of \(K\) is a finitely generated \(\mathcal{O}\) -submodule \(\mathfrak{a} \neq 0\) of \(K\) .
Formalized. Mathlib/RingTheory/FractionalIdeal/Basic.lean::IsFractional, FractionalIdeal, fg_of_isNoetherianRing; Mathlib/RingTheory/FractionalIdeal/Operations.lean::isFractional_of_fg — Mathlib uses the equivalent common-denominator model; over the Noetherian Dedekind domain, fg_of_isNoetherianRing and isFractional_of_fg prove equivalence with finite generation. Neukirch’s J_K is the nonzero subtype of this type.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
For instance, an element \(a \in K^{*}\) defines the fractional “principal ideal” (a) = aO. Obviously, since O is noetherian, an O-submodule \(a \neq 0\) of K is a fractional ideal if and only if there exists \(c \in O\) , \(c \neq 0\) , such that \(ca \subseteq O\) is an ideal of the ring O. Fractional ideals are multiplied in the same way as ideals in O. For distinction the latter may henceforth be called integral ideals of K.
Formalized. Mathlib/RingTheory/FractionalIdeal/Operations.lean::spanSingleton; Mathlib/RingTheory/FractionalIdeal/Basic.lean::den, den_mul_self_eq_num, fg_of_isNoetherianRing, mul_def; Mathlib/RingTheory/FractionalIdeal/Operations.lean::isFractional_of_fg — Pinned spanSingleton is aO. den_mul_self_eq_num supplies the nonzero common denominator, the finite-generation converses hold over the Noetherian domain, and fractional multiplication is the submodule product.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition (3.8)
(3.8) Proposition. The fractional ideals form an abelian group, the ideal group \(J_{K}\) of K. The identity element is \((1) = \mathcal{O}\) , and the inverse of a is \[ \mathfrak {a} ^ {- 1} = \left\{x \in K \mid x \mathfrak {a} \subseteq \mathcal {O} \right\}. \]
Formalized. Mathlib/RingTheory/FractionalIdeal/Inverse.lean::mem_inv_iff; Mathlib/RingTheory/DedekindDomain/Ideal/Basic.lean::FractionalIdeal.semifield, coe_ideal_mul_inv — The pinned semifield makes the nonzero fractional ideals an abelian group with identity O; mem_inv_iff identifies inversion with {x | xa⊆O}.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Corollary (3.9)
(3.9) Corollary. Every fractional ideal \(\mathfrak{a}\) admits a unique representation as a product \[ \mathfrak {a} = \prod_ {\mathfrak {p}} \mathfrak {p} ^ {\nu_ {\mathfrak {p}}} \] with \(v_{p} \in Z\) and \(v_{p} = 0\) for almost all p. In other words, \(J_{K}\) is the free abelian group on the set of nonzero prime ideals p of O.
Formalized. Mathlib/RingTheory/DedekindDomain/Factorization.lean::finprod_heightOneSpectrum_factorization, count_zpow_self, finite_factors — The finite-support integer exponent function and reconstruction theorem give the unique fractional-ideal factorization.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
The fractional principal ideals \((a) = a\mathcal{O}, a \in K^{*}\) , form a subgroup of the group of ideals \(J_{K}\) , which will be denoted \(P_{K}\) . The quotient group \[ C l _ {K} = J _ {K} / P _ {K} \] is called the ideal class group, or class group for short, of K. Along with the group of units \(\sigma^{*}\) of o, it fits into the exact sequence \[ 1 \longrightarrow \mathcal {O} ^ {*} \longrightarrow K ^ {*} \longrightarrow J _ {K} \longrightarrow C l _ {K} \longrightarrow 1, \] where the arrow in the middle is given by \(a \mapsto (a)\) . So the class group \(Cl_{K}\) measures the expansion that takes place when we pass from numbers to ideals, whereas the unit group \(O^{*}\) measures the contraction in the same process. This immediately raises the problem of understanding these groups \(O^{*}\) and \(Cl_{K}\) more thoroughly. For general Dedekind domains they may turn out to be completely arbitrary groups. For the ring \(O_{K}\) of integers in a number field K, however, one obtains important finiteness theorems, which are fundamental for the further development of number theory. But these results cannot be had for nothing. They will be obtained by viewing the numbers geometrically as lattice points in space. For this we will now prepare the necessary concepts, which all come from linear algebra.
Formalized. Mathlib/RingTheory/ClassGroup/Basic.lean::toPrincipalIdeal, ClassGroup, ClassGroup.mk, ClassGroup.mk_eq_one_iff, ClassGroup.mk0_surjective; Mathlib/Algebra/Algebra/Operations.lean::span_singleton_eq_one_iff — The class group is the quotient of nonzero fractional ideals by the image of Kˣ under toPrincipalIdeal; mk_eq_one_iff and mk0_surjective give the kernel and surjectivity at J_K→Cl_K. Since span_singleton_eq_one_iff says xO=O exactly when x comes from Oˣ, the kernel of Kˣ→J_K is precisely Oˣ, closing the entire exact sequence.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition (4.1)
(4.1) Definition. Let \(V\) be an \(n\) -dimensional \(\mathbb{R}\) -vector space. A lattice in \(V\) is a subgroup of the form \[ \Gamma = \mathbb {Z} v _ {1} + \dots + \mathbb {Z} v _ {m} \] with linearly independent vectors \(v_{1}, \ldots, v_{m}\) of V. The m-tuple \((v_{1}, \ldots, v_{m})\) is called a basis and the set \[ \Phi = \left\{x _ {1} v _ {1} + \dots + x _ {m} v _ {m} \mid x _ {i} \in \mathbb {R}, 0 \leq x _ {i} < 1 \right\} \] a fundamental mesh of the lattice. The lattice is called complete or a Z-structure of V, if m = n.
Not formalized. Pinned/current Mathlib has full-lattice, canonical-embedding, Minkowski, class-number and Dirichlet-unit infrastructure, but this source row is more general or contains an extra finiteness/normalization clause not exported as one complete route.
Proposition (4.2)
(4.2) Proposition. A subgroup \(\Gamma \subseteq V\) is a lattice if and only if it is discrete.
Not formalized. Pinned/current Mathlib has full-lattice, canonical-embedding, Minkowski, class-number and Dirichlet-unit infrastructure, but this source row is more general or contains an extra finiteness/normalization clause not exported as one complete route.
Lemma (4.3)
(4.3) Lemma. A lattice \(\Gamma\) in \(V\) is complete if and only if there exists a bounded subset \(M \subseteq V\) such that the collection of all translates \(M + \gamma, \gamma \in \Gamma\) , covers the entire space \(V\) .
Not formalized. Pinned/current Mathlib has full-lattice, canonical-embedding, Minkowski, class-number and Dirichlet-unit infrastructure, but this source row is more general or contains an extra finiteness/normalization clause not exported as one complete route.
Definition / construction
Now let V be a euclidean vector space, i.e., an R-vector space of finite dimension n equipped with a symmetric, positive definite bilinear form \[ \langle , \rangle : V \times V \longrightarrow \mathbb {R}. \] Then we have on V a notion of volume – more precisely a Haar measure. The cube spanned by an orthonormal basis \(e_{1}, \ldots, e_{n}\) has volume 1, and more generally, the parallelepiped spanned by n linearly independent vectors \(v_{1}, \ldots, v_{n}\) , \[ \Phi = \left\{x _ {1} v _ {1} + \dots + x _ {n} v _ {n} \mid x _ {i} \in \mathbb {R}, 0 \leq x _ {i} < 1 \right\} \] has volume \[ \operatorname{vol} (\Phi) = | \det A |, \] where \(A = (a_{ik})\) is the matrix of the base change from \(e_1, \ldots, e_n\) to \(v_1, \ldots, v_n\) , so that \(v_i = \sum_k a_{ik} e_k\) . Since \[ \left(\langle v _ {i}, v _ {j} \rangle\right) = \left(\sum_ {k, \ell} a _ {i k} a _ {j \ell} \langle e _ {k}, e _ {\ell} \rangle\right) = \left(\sum_ {k} a _ {i k} a _ {j k}\right) = A A ^ {t}, \] we also have the invariant notation \[ \operatorname{vol} (\Phi) = \left| \det (\langle v _ {i}, v _ {j} \rangle) \right| ^ {1 / 2}. \] Let \(\Gamma\) be the lattice spanned by \(v_{1},\ldots ,v_{n}\) . Then \(\Phi\) is a fundamental mesh of \(\Gamma\) , and we write for short \[ \operatorname{vol} (\Gamma) = \operatorname{vol} (\Phi). \] This does not depend on the choice of a basis \(v_{1}, \ldots, v_{n}\) of the lattice because the transition matrix passing to a different basis, as well as its inverse, has integer coefficients, and therefore has determinant \(\pm1\) so that the set \(\Phi\) is transformed into a set of the same volume.
Not formalized. Pinned/current Mathlib has full-lattice, canonical-embedding, Minkowski, class-number and Dirichlet-unit infrastructure, but this source row is more general or contains an extra finiteness/normalization clause not exported as one complete route.
Definition / construction
A subset \(X\) of \(V\) is called centrally symmetric if \(x \in X\) implies \(-x \in X\), and convex if, for any two points \(x, y \in X\), the whole line segment \(\{ty + (1-t)x \mid 0 \leq t \leq 1\}\) joining \(x\) to \(y\) is contained in \(X\). With these definitions one has Minkowski’s lattice point theorem (4.4).
Not formalized. Pinned/current Mathlib has full-lattice, canonical-embedding, Minkowski, class-number and Dirichlet-unit infrastructure, but this source row is more general or contains an extra finiteness/normalization clause not exported as one complete route.
Minkowski’s Lattice Point Theorem (4.4)
(4.4) Minkowski’s Lattice Point Theorem. Let \(\Gamma\) be a complete lattice in the euclidean vector space \(V\) and \(X\) a centrally symmetric, convex subset of \(V\) . Suppose that \[ \operatorname{vol} (X) > 2 ^ {n} \operatorname{vol} (\Gamma). \] Then \(X\) contains at least one nonzero lattice point \(\gamma \in \Gamma\) .
Formalized. Mathlib/MeasureTheory/Group/GeometryOfNumbers.lean::exists_ne_zero_mem_lattice_of_measure_mul_two_pow_lt_measure, exists_ne_zero_mem_lattice_of_measure_mul_two_pow_le_measure — The pinned geometry-of-numbers theorem is Minkowski’s symmetric-convex-body lattice-point criterion.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
The basic idea in Minkowski’s treatment of an algebraic number field \(K|Q\) of degree \(n\) is to interpret its numbers as points in \(n\) -dimensional space. This explains why his theory has been called “Geometry of Numbers.” It seems appropriate, however, to follow the current trend and call it “Minkowski Theory” instead, because in the meantime a geometric approach to number theory has been developed which is quite different in nature and much more comprehensive. We will explain this in §13. In the present section, we consider the canonical mapping \[ j: K \longrightarrow K _ {\mathbb {C}} := \prod_ {\tau} \mathbb {C}, \quad a \longmapsto j a = (\tau a), \] which results from the n complex embeddings \(\tau: K \to C\) . The C-vector space \(K_{C}\) is equipped with the hermitian scalar product \[ \langle x, y \rangle = \sum_ {\tau} x _ {\tau} \overline {{{y}}} _ {\tau}.\tag{*} \] Let us recall that a hermitian scalar product is given by a form \(H(x,y)\) which is linear in the first variable and satisfies \(\overline{H(x,y)} = H(y,x)\) as well as \(H(x,x) > 0\) for \(x \neq 0\) . In the sequel we always view \(K_{C}\) as a hermitian space, with respect to the “standard metric” (*).
Formalized. Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean::NumberField.canonicalEmbedding, apply_at; Mathlib/Analysis/InnerProductSpace/PiL2.lean::EuclideanSpace.equiv, PiLp.inner_apply — The canonical embedding has coordinates τ(a). Transporting it through EuclideanSpace.equiv.symm equips the finite embedding product with the ℓ² Hermitian form; PiLp.inner_apply is the coordinate sum, up to Mathlib’s opposite linear-slot convention.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
We call the euclidean vector space \[ K _ {\mathbb {R}} = \left[ \prod_ {\tau} \mathbb {C} \right] ^ {+} \] the Minkowski space, its scalar product \(\langle ,\rangle\) the canonical metric, and the associated Haar measure (see §4, p. 26) the canonical measure. Since \(Tr\circ F = F\circ Tr\) we have on \(K_{\mathbb{R}}\) the \(\mathbb{R}\) -linear map \[ T r: K _ {\mathbb {R}} \longrightarrow \mathbb {R}, \] and its composite with \(j: K \to K_{\mathbb{R}}\) is again the usual trace of \(K|\mathbb{Q}\) , \[ T r _ {K | \mathbb {Q}} (a) = T r (j a). \] Remark: We mention in passing - it will not be used in the sequel - that the mapping \(j: K \to K_{\mathbb{R}}\) identifies the vector space \(K_{\mathbb{R}}\) with the tensor product \(K \otimes_{\mathbb{Q}} \mathbb{R}\) , \[ K \otimes_{\mathbb{Q}} \mathbb{R} \xrightarrow{\ \sim\ } K_{\mathbb{R}}, \quad a \otimes x \longmapsto (ja)x, \] and likewise for \(K \otimes_{\mathbb{Q}} \mathbb{C}\).
Not formalized. Pinned/current Mathlib has full-lattice, canonical-embedding, Minkowski, class-number and Dirichlet-unit infrastructure, but this source row is more general or contains an extra finiteness/normalization clause not exported as one complete route.
Proposition (5.1)
(5.1) Proposition. There is an isomorphism \[ f: K _ {\mathbb {R}} \longrightarrow \prod_ {\tau} \mathbb {R} = \mathbb {R} ^ {r + 2 s} \] given by the rule \((z_{\tau})\mapsto (x_{\tau})\) where \[ x _ {\rho} = z _ {\rho}, \quad x _ {\sigma} = \operatorname{Re} (z _ {\sigma}), \quad x _ {\overline {{\sigma}}} = \operatorname{Im} (z _ {\sigma}). \] This isomorphism transforms the canonical metric \(\langle\ ,\rangle\) into the scalar product \[ (x, y) = \sum_ {\tau} \alpha_ {\tau} x _ {\tau} y _ {\tau}, \] where \(\alpha_{\tau} = 1\) , resp. \(\alpha_{\tau} = 2\) , if \(\tau\) is real, resp. complex.
Not formalized. Pinned/current Mathlib has full-lattice, canonical-embedding, Minkowski, class-number and Dirichlet-unit infrastructure, but this source row is more general or contains an extra finiteness/normalization clause not exported as one complete route.
Convention / notation
Minkowski himself worked with the Lebesgue measure on \(R^{r+2s}\) , and most textbooks follow suit. The corresponding measure on \(K_{R}\) is the one determined by the scalar product \[ (x, y) = \sum_ {\tau} \frac {1}{\alpha_ {\tau}} x _ {\tau} \overline {{{y}}} _ {\tau}. \] This scalar product may therefore be called the Minkowski metric on \(K_{R}\) . But we will systematically work with the canonical metric, and denote by vol the corresponding canonical measure.
Not formalized. Pinned/current Mathlib has full-lattice, canonical-embedding, Minkowski, class-number and Dirichlet-unit infrastructure, but this source row is more general or contains an extra finiteness/normalization clause not exported as one complete route.
Proposition (5.2)
(5.2) Proposition. If \(a \neq 0\) is an ideal of \(O_{K}\) , then \(\Gamma = j\alpha\) is a complete lattice in \(K_{R}\) . Its fundamental mesh has volume \[ \operatorname{vol} (\Gamma) = \sqrt {| d _ {K} |} \left(\mathcal {O} _ {K}: \mathfrak {a}\right). \]
Not formalized. Pinned/current Mathlib has full-lattice, canonical-embedding, Minkowski, class-number and Dirichlet-unit infrastructure, but this source row is more general or contains an extra finiteness/normalization clause not exported as one complete route.
Theorem (5.3)
(5.3) Theorem. Let \(\mathfrak{a} \neq 0\) be an integral ideal of \(K\) , and let \(c_{\tau} > 0\) , for \(\tau \in \operatorname{Hom}(K, \mathbb{C})\) , be real numbers such that \(c_{\tau} = c_{\overline{\tau}}\) and \[ \prod_ {\tau} c _ {\tau} > A (\mathcal {O} _ {K}: \mathfrak {a}), \] where \(A = \left(\frac{2}{\pi}\right)^s\sqrt{|d_K|}\) . Then there exists \(a \in \mathfrak{a}, a \neq 0\) , such that \[ | \tau a | < c _ {\tau} \quad \text { for all } \quad \tau \in \operatorname{Hom} (K, \mathbb {C}). \]
Formalized. Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean::convexBodyLT, convexBodyLT_volume, minkowskiBound, exists_ne_zero_mem_ideal_lt, volume_fundamentalDomain_fractionalIdealLatticeBasis; Mathlib/NumberTheory/NumberField/Discriminant/Basic.lean::mixedEmbedding.covolume_idealLattice — Writing the conjugation-symmetric c_τ as a function on infinite places, convexBodyLT imposes exactly |τ(a)|<c_τ. Its volume together with the pinned fractional-ideal covolume reduces the Minkowski hypothesis to ∏_τ c_τ>(2/π)^s√|d_K|·N(a), so exists_ne_zero_mem_ideal_lt is Theorem 5.3 in Mathlib’s one-complex-place coordinate convention.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
The R-vector space \(\left[\prod_{\tau}R\right]^{+}\) is explicitly given as follows. Separate as before the embeddings \(\tau:K\to C\) into real ones, \(\rho_{1},\ldots,\rho_{r}\) , and pairs of complex conjugate ones, \(\sigma_{1},\overline{\sigma}_{1},\ldots,\sigma_{s},\overline{\sigma}_{s}\) . We obtain a decomposition which is analogous to the one we saw above for \(\left[\prod_{\tau}C\right]^{+}\) , \[ \left[ \prod_ {\tau} \mathbb {R} \right] ^ {+} = \prod_ {\rho} \mathbb {R} \times \prod_ {\sigma} [ \mathbb {R} \times \mathbb {R} ] ^ {+}. \] The factor \([R \times R]^{+}\) now consists of the points \((x, x)\) , and we identify it with R by the map \((x, x) \mapsto 2x\) . In this way we obtain an isomorphism \[ \left[ \prod_ {\tau} \mathbb {R} \right] ^ {+} \cong \mathbb {R} ^ {r + s}, \] which again transforms the map \(Tr:\left[\prod_{\tau}\mathbb{R}\right]^{+}\to \mathbb{R}\) into the usual map \[ T r: \mathbb {R} ^ {r + s} \longrightarrow \mathbb {R} \] given by the sum of the coordinates. Identifying \(\left[\prod_{\tau} \mathbb{R}\right]^+\) with \(\mathbb{R}^{r+s}\) , the homomorphism \[ \ell : K _ {\mathbb {R}} ^ {*} \longrightarrow \mathbb {R} ^ {r + s} \] is given by \[ \ell (x) = \left(\log | x _ {\rho_ {1}} |, \dots , \log | x _ {\rho_ {r}} |, \log | x _ {\sigma_ {1}} | ^ {2}, \dots , \log | x _ {\sigma_ {s}} | ^ {2}\right), \] where we write \(x \in K_{\mathbb{R}}^{*} \subseteq \prod_{\tau} \mathbb{C}^{*}\) as \(x = (x_{\tau})\) .
Not formalized. Pinned/current Mathlib has full-lattice, canonical-embedding, Minkowski, class-number and Dirichlet-unit infrastructure, but this source row is more general or contains an extra finiteness/normalization clause not exported as one complete route.
Proposition (6.1)
(6.1) Proposition. If \(a = p_{1}^{\nu_{1}} \cdots p_{r}^{\nu_{r}}\) is the prime factorization of an ideal \(a \neq 0\) , then one has \[ \mathfrak {N} (\mathfrak {a}) = \mathfrak {N} (\mathfrak {p} _ {1}) ^ {\nu_ {1}} \dots \mathfrak {N} (\mathfrak {p} _ {r}) ^ {\nu_ {r}}. \]
Formalized. Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean::Ideal.absNorm, map_mul Ideal.absNorm; Mathlib/RingTheory/DedekindDomain/Factorization.lean::Ideal.finprod_heightOneSpectrum_factorization — The absolute ideal norm is a bundled multiplicative homomorphism; applying it to the unique finite prime-ideal factorization gives exactly N(a)=∏N(p_i)^ν_i.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
The proposition immediately implies the multiplicativity \[ \mathfrak {N} (\mathfrak {a b}) = \mathfrak {N} (\mathfrak {a}) \mathfrak {N} (\mathfrak {b}) \] of the absolute norm. It may therefore be extended to a homomorphism \[ \mathfrak {N}: J _ {K} \longrightarrow \mathbb {R} _ {+} ^ {*} \] defined on all fractional ideals \(a = \prod_{p} p^{\nu_{p}}, \nu_{p} \in Z\) . The following lemma, a consequence of (5.3), is crucial for the finiteness of the ideal class group.
Formalized. Mathlib/RingTheory/FractionalIdeal/Norm.lean::FractionalIdeal.absNorm, absNorm_eq_zero_iff, coeIdeal_absNorm — The pinned fractional-ideal absolute norm is multiplicative into ℚ and nonzero exactly on nonzero fractional ideals; restricting to J_K lands in ℚ_{>0}⊂ℝ_{>0} and extends the integral ideal norm.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Lemma (6.2)
(6.2) Lemma. In every ideal \(\mathfrak{a} \neq 0\) of \(\mathcal{O}_K\) there exists an \(a \in \mathfrak{a}\) , \(a \neq 0\) , such that \[ \left| N _ {K | \mathbb {Q}} (a) \right| \leq \left(\frac {2}{\pi}\right) ^ {s} \sqrt {| d _ {K} |} \mathfrak {N} (\mathfrak {a}). \]
Not formalized. Pinned/current Mathlib has full-lattice, canonical-embedding, Minkowski, class-number and Dirichlet-unit infrastructure, but this source row is more general or contains an extra finiteness/normalization clause not exported as one complete route.
Theorem (6.3)
(6.3) Theorem. The ideal class group \(Cl_{K} = J_{K}/P_{K}\) is finite. Its order \[ h _ {K} = (J _ {K}: P _ {K}) \] is called the class number of \(K\) .
Formalized. Mathlib/NumberTheory/NumberField/ClassNumber.lean::instFintypeClassGroup, NumberField.classNumber — The ring-of-integers class group has a pinned Fintype instance, and NumberField.classNumber is its cardinality, exactly h_K.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Convention / notation
From the homomorphisms \[ \mathcal{O}_{K}^{*} \xrightarrow{\ j\ } S \xrightarrow{\ \ell\ } H \] one forms the composite \(\lambda := \ell \circ j \colon \mathcal{O}_{K}^{*} \to H\), whose image is denoted \[ \Gamma = \lambda(\mathcal{O}_{K}^{*}) \subseteq H, \] and this is the setting of proposition (7.1) on the exactness of the resulting sequence.
Formalized. Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean::NumberField.Units.logEmbedding, sum_logEmbedding_component, NumberField.Units.unitLattice — Mathlib records the weighted archimedean logarithms in the equivalent coordinate chart obtained by deleting one hyperplane coordinate; sum_logEmbedding_component reconstructs the omitted coordinate, and unitLattice is precisely the image Γ.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition (7.1)
(7.1) Proposition. The sequence \[ 1 \longrightarrow \mu (K) \longrightarrow \mathcal {O} _ {K} ^ {*} \stackrel {\lambda} {\longrightarrow} \Gamma \longrightarrow 0 \] is exact.
Formalized. Mathlib/NumberTheory/NumberField/Units/Basic.lean::torsion, rootsOfUnity_eq_torsion; Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean::logEmbedding_ker, NumberField.Units.unitLattice — The logarithmic map has kernel exactly the torsion subgroup, identified with μ(K), and unitLattice is its image; hence 1→μ(K)→O_K^*→Γ→0 is exact.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Lemma (7.2)
(7.2) Lemma. Up to multiplication by units there are only finitely many elements \(\alpha \in \mathcal{O}_K\) of given norm \(N_{K|\mathbb{Q}}(\alpha) = a\) .
Not formalized. Pinned/current Mathlib has full-lattice, canonical-embedding, Minkowski, class-number and Dirichlet-unit infrastructure, but this source row is more general or contains an extra finiteness/normalization clause not exported as one complete route.
Theorem (7.3)
(7.3) Theorem. The group \(\Gamma\) is a complete lattice in the \((r + s - 1)\) -dimensional vector space \(H\) , and is therefore isomorphic to \(\mathbb{Z}^{r + s - 1}\) .
Formalized. Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean::instZLattice_unitLattice, unitLattice_rank, NumberField.Units.rank; Mathlib/NumberTheory/NumberField/InfinitePlace/Basic.lean::card_eq_nrRealPlaces_add_nrComplexPlaces — The image Γ is a full ℤ-lattice; its rank is card (InfinitePlace K)-1 = r+s-1, yielding Γ≅ℤ^(r+s-1).
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Theorem (7.4)
(7.4) Theorem. The group of units \(O_{K}^{*}\) of \(O_{K}\) is the direct product of the finite cyclic group \(\mu(K)\) and a free abelian group of rank \(r + s - 1\) .
Formalized. Mathlib/NumberTheory/NumberField/Units/Basic.lean::torsion, instance : Finite (torsion K), IsCyclic (torsion K), rootsOfUnity_eq_torsion; Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean::finrank_modTorsion, exist_unique_eq_mul_prod, NumberField.Units.rank; Mathlib/NumberTheory/NumberField/InfinitePlace/Basic.lean::card_eq_nrRealPlaces_add_nrComplexPlaces — The torsion subgroup is the finite cyclic μ(K), and exist_unique_eq_mul_prod gives a unique torsion element times integral powers of rank K=r+s-1 fundamental units, i.e. the asserted direct product.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition (7.5)
(7.5) Proposition. The volume of the fundamental mesh of the unit lattice \(\lambda (\mathcal{O}_K^*)\) in \(H\) is \(\mathrm{vol}\bigl (\lambda (\mathcal{O}_K^*)\bigr) = \sqrt{r + s} R,\) \[ \operatorname{vol} \left(\lambda \left(\mathcal {O} _ {K} ^ {*}\right)\right) = \sqrt {r + s} R, \] where R is the absolute value of the determinant of an arbitrary minor of rank \(t = r + s - 1\) of the following matrix: \[ \left( \begin{array}{c c c} \lambda_ {1} (\varepsilon_ {1}) & \dots & \lambda_ {1} (\varepsilon_ {t}) \\ \vdots & & \vdots \\ \lambda_ {t + 1} (\varepsilon_ {1}) & \dots & \lambda_ {t + 1} (\varepsilon_ {t}) \end{array} \right). \]
Not formalized. Pinned/current Mathlib has full-lattice, canonical-embedding, Minkowski, class-number and Dirichlet-unit infrastructure, but this source row is more general or contains an extra finiteness/normalization clause not exported as one complete route.
Definition / construction
This absolute value R is called the regulator of the field K.
Formalized. Mathlib/NumberTheory/NumberField/Units/Regulator.lean::regulator, regulator_eq_det, regulator_pos — Mathlib’s regulator is the absolute determinant/covolume invariant in the standard deleted-coordinate logarithmic chart, which is exactly the scalar R named by Neukirch after Proposition 7.5.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition (8.1)
(8.1) Proposition. Let \(\mathcal{O}\) be a Dedekind domain with field of fractions \(K\) , let \(L|K\) be a finite extension of \(K\) and \(\mathcal{O}\) the integral closure of \(\mathcal{O}\) in \(L\) . Then \(\mathcal{O}\) is again a Dedekind domain.
Not formalized. Pinned/current Mathlib has ramification, inertia, Galois and cyclotomic infrastructure, but this full source bundle is either more general than the available hypotheses or contains a decomposition statement not exported as a complete compatible theorem.
Definition / construction
This we also denote for short by \(\mathfrak{P}|\mathfrak{p}\) , and we call \(\mathfrak{P}\) a prime divisor of \(\mathfrak{p}\) . The exponent \(e_i\) is called the ramification index, and the degree of the field extension \[ f _ {i} = \left[ \mathcal {O} / \mathfrak {P} _ {i}: \mathcal {O} / \mathfrak {p} \right] \] is called the inertia degree of \(P_{i}\) over p. If the extension \(L|K\) is separable, the numbers \(e_{i}\) , \(f_{i}\) and the degree \(n = [L : K]\) are connected by the following law.
Formalized. Mathlib/RingTheory/RamificationInertia/Ramification.lean::Ideal.ramificationIdx; Mathlib/RingTheory/RamificationInertia/Inertia.lean::Ideal.inertiaDeg — Pinned ramification index and residue-field inertia degree are exactly the source e(P/p) and f(P/p).
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition (8.2)
(8.2) Proposition. Let \(L|K\) be separable. Then we have the fundamental identity \[ \sum_ {i = 1} ^ {r} e _ {i} f _ {i} = n. \]
Formalized. Mathlib/NumberTheory/RamificationInertia/Basic.lean::Ideal.sum_ramification_inertia — This theorem is exactly Σ_P e(P/p)f(P/p)=[L:K].
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
Suppose now that the separable extension \(L|K\) is given by a primitive element \(\theta \in \mathcal{O}\) with minimal polynomial \[ p (X) \in \mathcal {O} [ X ], \] so that \(L = K(\theta)\) . We may then deduce a result about the nature of the decomposition of p in O which, albeit not complete, does show characteristic phenomena and a striking simplicity. It is incomplete in that a finite number of prime ideals are excluded; only those relatively prime to the conductor of the ring \(\sigma[\theta]\) can be considered. This conductor is defined to be the biggest ideal F of O which is contained in \(\sigma[\theta]\) . In other words \[ \mathfrak {F} = \left\{\alpha \in \mathcal {O} \mid \alpha \mathcal {O} \subseteq \mathcal {O} [ \theta ] \right\}. \] Since \(\mathcal{O}\) is a finitely generated \(\mathcal{O}\) -module (see proof of (8.1)), one has \(\mathfrak{F} \neq 0\) .
Not formalized. Pinned/current Mathlib has ramification, inertia, Galois and cyclotomic infrastructure, but this full source bundle is either more general than the available hypotheses or contains a decomposition statement not exported as a complete compatible theorem.
Proposition (8.3)
(8.3) Proposition. Let \(\mathfrak{p}\) be a prime ideal of \(\mathcal{O}\) which is relatively prime to the conductor \(\mathfrak{F}\) of \(\mathcal{O}[\theta]\) , and let \[ \overline {{{p}}} (X) = \overline {{{p}}} _ {1} (X) ^ {e _ {1}} \dots \overline {{{p}}} _ {r} (X) ^ {e _ {r}} \] be the factorization of the polynomial \(\overline{p}(X) = p(X)\) mod \(\mathfrak{p}\) into irreducibles \(\overline{p}_i(X) = p_i(X)\) mod \(\mathfrak{p}\) over the residue class field \(\mathcal{O} / \mathfrak{p}\) , with all \(p_i(X) \in \mathcal{O}[X]\) monic. Then \[ \mathfrak {P} _ {i} = \mathfrak {p O} + p _ {i} (\theta) \mathcal {O}, \quad i = 1, \dots , r, \] are the different prime ideals of O above p. The inertia degree \(f_{i}\) of \(P_{i}\) is the degree of \(\overline{p}_{i}(X)\) , and one has \[ \mathfrak {p} = \mathfrak {P} _ {1} ^ {e _ {1}} \dots \mathfrak {P} _ {r} ^ {e _ {r}}. \]
Not formalized. Pinned/current Mathlib has ramification, inertia, Galois and cyclotomic infrastructure, but this full source bundle is either more general than the available hypotheses or contains a decomposition statement not exported as a complete compatible theorem.
Definition / construction
The prime ideal \(\mathfrak{p}\) is said to split completely (or to be totally split) in \(L\) , if in the decomposition \[ \mathfrak {p} = \mathfrak {P} _ {1} ^ {e _ {1}} \dots \mathfrak {P} _ {r} ^ {e _ {r}}, \] one has \(r = n = [L : K]\) , so that \(e_i = f_i = 1\) for all \(i = 1, \ldots, r\) . \(\mathfrak{p}\) is called nonsplit, or indecomposed, if \(r = 1\) , i.e., if there is only a single prime ideal of \(L\) over \(\mathfrak{p}\) . From the fundamental identity \[ \sum_ {i = 1} ^ {r} e _ {i} f _ {i} = n \] we now understand the name of inertia degree: the smaller this degree is, the more the ideal p will be tend to factor into different prime ideals.
Not formalized. Pinned/current Mathlib has ramification, inertia, Galois and cyclotomic infrastructure, but this full source bundle is either more general than the available hypotheses or contains a decomposition statement not exported as a complete compatible theorem.
Definition / construction
The prime ideal \(P_{i}\) in the decomposition \(p = \prod_{i=1}^{r} P_{i}^{e_{i}}\) is called unramified over O (or over K) if \(e_{i} = 1\) and if the residue class field extension \(O/P_{i}|O/p\) is separable. If not, it is called ramified, and totally ramified if furthermore \(f_{i} = 1\) . The prime ideal p is called unramified if all \(P_{i}\) are unramified, otherwise it is called ramified. The extension \(L|K\) itself is called unramified if all prime ideals p of K are unramified in L.
Not formalized. Pinned/current Mathlib has ramification, inertia, Galois and cyclotomic infrastructure, but this full source bundle is either more general than the available hypotheses or contains a decomposition statement not exported as a complete compatible theorem.
Proposition (8.4)
(8.4) Proposition. If \(L \mid K\) is separable, then there are only finitely many prime ideals of K which are ramified in L.
Not formalized. Pinned/current Mathlib has ramification, inertia, Galois and cyclotomic infrastructure, but this full source bundle is either more general than the available hypotheses or contains a decomposition statement not exported as a complete compatible theorem.
Definition / construction
The precise description of the ramified prime ideals is given by the discriminant of \(O|O\) . It is defined to be the ideal d of o which is generated by the discriminants \(d(\omega_{1},\ldots,\omega_{n})\) of all bases \(\omega_{1},\ldots,\omega_{n}\) of L|K contained in O. We will show in chapter III, §2 that the prime divisors of 0 are exactly the prime ideals which ramify in L.
Not formalized. Pinned/current Mathlib has ramification, inertia, Galois and cyclotomic infrastructure, but this full source bundle is either more general than the available hypotheses or contains a decomposition statement not exported as a complete compatible theorem.
Example / comparison
The law of decomposition of a prime \(p\) in a quadratic number field \(\mathbb{Q}(\sqrt{a})\) is intimately related to Gauss’s quadratic reciprocity law, which concerns the integer solutions of \(x^{2} + by = a\) with \(a, b \in \mathbb{Z}\) and reduces to the case of an odd prime \(b = p\) with \((a,p) = 1\), that is, to whether \(a\) is a quadratic residue \(\bmod p\). The conductor of \(\mathbb{Z}[\sqrt{a}]\) in the ring of integers of \(\mathbb{Q}(\sqrt{a})\) divides \(2\), so proposition (8.3) applies and yields the decomposition criterion (8.5), from which Gauss’s reciprocity law (8.6) follows.
Not formalized. Pinned/current Mathlib has ramification, inertia, Galois and cyclotomic infrastructure, but this full source bundle is either more general than the available hypotheses or contains a decomposition statement not exported as a complete compatible theorem.
Proposition (8.5)
(8.5) Proposition. For squarefree \(a\) and \((p, 2a) = 1\) , we have the equivalence \[ \left(\frac {a}{p}\right) = 1 \iff p \text { is totally split in } \mathbb {Q} (\sqrt {a}) . \]
Not formalized. Pinned/current Mathlib has ramification, inertia, Galois and cyclotomic infrastructure, but this full source bundle is either more general than the available hypotheses or contains a decomposition statement not exported as a complete compatible theorem.
Theorem (8.6)
(8.6) Theorem (Gauss’s Reciprocity Law). For two distinct odd prime numbers \(\ell\) and \(p\) , the following identity holds: \[ \left(\frac {\ell}{p}\right) \left(\frac {p}{\ell}\right) = (- 1) ^ {\frac {\ell - 1}{2} \frac {p - 1}{2}}. \] One also has the two “supplementary theorems” \[ \left(\frac {- 1}{p}\right) = (- 1) ^ {\frac {p - 1}{2}}, \quad \left(\frac {2}{p}\right) = (- 1) ^ {\frac {p ^ {2} - 1}{8}}. \]
Formalized. Mathlib/NumberTheory/LegendreSymbol/QuadraticReciprocity.lean::quadratic_reciprocity, at_two; Mathlib/NumberTheory/LegendreSymbol/Basic.lean::legendreSym.at_neg_one — These declarations are Gauss reciprocity and the -1/2 supplementary laws in Legendre-symbol form.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
The ideals \(\sigma\mathfrak{P}\) , for \(\sigma\in G\) , are called the prime ideals conjugate to \(\mathfrak{P}\) .
Formalized. Mathlib/NumberTheory/RamificationInertia/Galois.lean::coe_smul_primesOver, exists_smul_eq_of_isGaloisGroup — The Galois action on primes-over is explicit; σ•P is exactly the conjugate prime ideal.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition (9.1)
(9.1) Proposition. The Galois group G acts transitively on the set of all prime ideals P of O lying above p, i.e., these prime ideals are all conjugates of each other.
Formalized. Mathlib/NumberTheory/RamificationInertia/Galois.lean::exists_smul_eq_of_isGaloisGroup — For any two primes above p the pinned theorem produces σ with σP=Q.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition (9.2)
(9.2) Definition. If \(\mathfrak{P}\) is a prime ideal of \(\mathcal{O}\) , then the subgroup \[ G _ {\mathfrak {P}} = \left\{\sigma \in G \mid \sigma \mathfrak {P} = \mathfrak {P} \right\} \] is called the decomposition group of \(\mathfrak{P}\) over \(K\) . The fixed field \[ Z _ {\mathfrak {P}} = \left\{x \in L \mid \sigma x = x \quad f o r a l l \sigma \in G _ {\mathfrak {P}} \right\} \] is called the decomposition field of \(\mathfrak{P}\) over \(K\) .
Formalized. Mathlib/RingTheory/Ideal/Over.lean::MulAction.stabilizer; Mathlib/NumberTheory/RamificationInertia/HilbertTheory.lean::IsDecompositionField — The decomposition group is the stabilizer of P and the decomposition field is its fixed field, exactly the source definition.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
Remark: The decomposition group regulates the prime decomposition also in the case of a non-Galois extension. For subgroups U and V of a group G, consider the equivalence relation in G defined by \[ \sigma \sim \sigma^ {\prime} \iff \sigma^ {\prime} = u \sigma v \quad \text { for } u \in U, v \in V. \] The corresponding equivalence classes \[ U \sigma V = \left\{u \sigma v \mid u \in U, v \in V \right\} \] are called the double cosets of \(G\) modd \(U, V\) . The set of these double cosets, which form a partition of \(G\) , is denoted \(U \backslash G / V\) . Now let \(L|K\) be an arbitrary separable extension, and embed it into a Galois extension \(N|K\) with Galois group \(G\) . In \(G\) , consider the subgroup \(H = G(N|L)\) . Let \(\mathfrak{p}\) be a prime ideal of \(K\) and \(P_{\mathfrak{p}}\) the set of prime ideals of \(L\) above \(\mathfrak{p}\) . If \(\mathfrak{P}\) is a prime ideal of \(N\) above \(\mathfrak{p}\) , then the rule \[ H \backslash G / G _ {\mathfrak {P}} \longrightarrow P _ {\mathfrak {p}}, \quad H \sigma G _ {\mathfrak {P}} \longmapsto \sigma \mathfrak {P} \cap L, \] gives a well-defined bijection. The proof is left to the reader.
Not formalized. Pinned/current Mathlib has ramification, inertia, Galois and cyclotomic infrastructure, but this full source bundle is either more general than the available hypotheses or contains a decomposition statement not exported as a complete compatible theorem.
Proposition (9.3)
(9.3) Proposition. Let \(\mathfrak{P}_Z = \mathfrak{P} \cap Z_{\mathfrak{P}}\) be the prime ideal of \(Z_{\mathfrak{P}}\) below \(\mathfrak{P}\) . Then we have: (i) \(\mathfrak{P}_Z\) is nonsplit in \(L\) , i.e., \(\mathfrak{P}\) is the only prime ideal of \(L\) above \(\mathfrak{P}_Z\) . (ii) \(\mathfrak{P}\) over \(Z_{\mathfrak{P}}\) has ramification index \(e\) and inertia degree \(f\) . (iii) The ramification index and the inertia degree of \(\mathfrak{P}_Z\) over \(K\) both equal 1.
Formalized. Mathlib/NumberTheory/RamificationInertia/HilbertTheory.lean::primesOver_eq_singleton, ramificationIdxIn_eq, inertiaDegIn_eq, ramificationIdx_eq, inertiaDeg_eq — The pinned Hilbert-theory theorems give the unique prime above P_Z and the stated e/f values on both sides of the decomposition field.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition (9.4)
(9.4) Proposition. The extension \(\kappa (\mathfrak{P})|\kappa (\mathfrak{p})\) is normal and admits a surjective homomorphism \[ G _ {\mathfrak {P}} \longrightarrow G (\kappa (\mathfrak {P}) | \kappa (\mathfrak {p})). \]
Formalized. Mathlib/RingTheory/Invariant/Basic.lean::IsFractionRing.stabilizerQuotientInertiaEquiv; Mathlib/NumberTheory/RamificationInertia/Galois.lean::Ideal.IsFractionRing.normal, Ideal.IsFractionRing.finite_of_isInvariant — The residue extension is normal/finite and the stabilizer modulo inertia is equivalent to its automorphism group, yielding the source surjection.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition (9.5)
(9.5) Definition. The kernel \(I_{\mathfrak{P}} \subseteq G_{\mathfrak{P}}\) of the homomorphism \[ G _ {\mathfrak {P}} \longrightarrow G \big (\kappa (\mathfrak {P}) | \kappa (\mathfrak {p}) \big) \] is called the inertia group of \(\mathfrak{P}\) over \(K\) . The fixed field \[ T _ {\mathfrak {P}} = \left\{x \in L \mid \sigma x = x \quad \text { for all } \sigma \in I _ {\mathfrak {P}} \right\} \] is called the inertia field of \(\mathfrak{P}\) over \(K\) .
Formalized. Mathlib/RingTheory/Ideal/Over.lean::stabilizerHom, ker_stabilizerHom; Mathlib/RingTheory/Ideal/Defs.lean::abbrev inertia; Mathlib/NumberTheory/RamificationInertia/HilbertTheory.lean::class IsInertiaField, FixedPoints.intermediateField (inertia Gal(L/K) P) — Pinned inertia is exactly the kernel of the decomposition-group residue action, and the canonical IsInertiaField instance is the fixed field of that subgroup.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition (9.6)
(9.6) Proposition. The extension \(T_{\mathfrak{P}}|Z_{\mathfrak{P}}\) is normal, and one has \[ G (T _ {\mathfrak {P}} | Z _ {\mathfrak {P}}) \cong G \big (\kappa (\mathfrak {P}) | \kappa (\mathfrak {p}) \big), \quad G (L | T _ {\mathfrak {P}}) = I _ {\mathfrak {P}}. \] If the residue field extension \(\kappa (\mathfrak{P})|\kappa (\mathfrak{p})\) is separable, then one has \[ \# I _ {\mathfrak {P}} = [ L: T _ {\mathfrak {P}} ] = e, \quad (G _ {\mathfrak {P}}: I _ {\mathfrak {P}}) = [ T _ {\mathfrak {P}}: Z _ {\mathfrak {P}} ] = f. \] In this case one finds for the prime ideal \(\mathfrak{P}_T\) of \(T_{\mathfrak{P}}\) below \(\mathfrak{P}\) : (i) The ramification index of \(\mathfrak{P}\) over \(\mathfrak{P}_T\) is \(e\) and the inertia degree is 1. (ii) The ramification index of \(\mathfrak{P}_T\) over \(\mathfrak{P}_Z\) is 1, and the inertia degree is \(f\) .
Not formalized. Pinned/current Mathlib has ramification, inertia, Galois and cyclotomic infrastructure, but this full source bundle is either more general than the available hypotheses or contains a decomposition statement not exported as a complete compatible theorem.
Lemma (10.1)
(10.1) Lemma. Let n be a prime power \(\ell^{\nu}\) and put \(\lambda = 1 - \zeta\) . Then the principal ideal ( \(\lambda\) ) in the ring O of integers of \(\mathbb{Q}(\zeta)\) is a prime ideal of degree 1, and we have \[ \ell \mathcal {O} = (\lambda) ^ {d}, \quad \text { where } \quad d = \varphi (\ell^ {\nu}) = [ \mathbb {Q} (\zeta): \mathbb {Q} ]. \] Furthermore, the basis \(1, \zeta, \ldots, \zeta^{d-1}\) of \(\mathbb{Q}(\zeta)|\mathbb{Q}\) has the discriminant \[ d (1, \zeta , \ldots , \zeta^ {d - 1}) = \pm \ell^ {s}, \quad s = \ell^ {\nu - 1} (\nu \ell - \nu - 1). \]
Formalized. Mathlib/NumberTheory/NumberField/Cyclotomic/Ideal.lean::map_eq_span_zeta_sub_one_pow, inertiaDeg_span_zeta_sub_one, ramificationIdx_span_zeta_sub_one; Mathlib/NumberTheory/NumberField/Cyclotomic/Basic.lean::integralPowerBasisOfPrimePow, discr_prime_pow — For n=p^ν the zeta-minus-one ideal is prime of inertia degree one and pO is its φ(n)-th power; the integral power basis is 1,ζ,… and discr_prime_pow gives the exact signed p-power discriminant exponent.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition (10.2)
(10.2) Proposition. A Z-basis of the ring O of integers of \(\mathbb{Q}(\zeta)\) is given by \(1, \zeta, \ldots, \zeta^{d-1}\) , with \(d = \varphi(n)\) , in other words, \[ \mathcal {O} = \mathbb {Z} + \mathbb {Z} \zeta + \dots + \mathbb {Z} \zeta^ {d - 1} = \mathbb {Z} [ \zeta ]. \]
Formalized. Mathlib/NumberTheory/NumberField/Cyclotomic/Basic.lean::adjoinEquivRingOfIntegers, integralPowerBasis — The pinned algebra equivalence identifies the ring of integers with ℤ[ζ], and integralPowerBasis has powers of ζ as basis.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition (10.3)
(10.3) Proposition. Let \(n = \prod_{p} p^{\nu_{p}}\) be the prime factorization of n and, for every prime number p, let \(f_{p}\) be the smallest positive integer such that \[ p ^ {f _ {p}} \equiv 1 \bmod n / p ^ {\nu_ {p}}. \] Then one has in \(\mathbb{Q}(\zeta)\) the factorization \[ p = \left(\mathfrak {p} _ {1} \dots \mathfrak {p} _ {r}\right) ^ {\varphi \left(p ^ {\nu p}\right)}, \] where \(\mathfrak{p}_1, \ldots, \mathfrak{p}_r\) are distinct prime ideals, all of degree \(f_p\) .
Formalized. Mathlib/NumberTheory/NumberField/Cyclotomic/Ideal.lean::inertiaDegIn_eq, ramificationIdxIn_eq; Mathlib/NumberTheory/RamificationInertia/Galois.lean::ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn — The public cyclotomic formulas give residue degree ord_{n/p^ν}(p), ramification φ(p^ν), and the Galois fundamental identity determines the number of distinct primes.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Corollary (10.4)
(10.4) Corollary. A prime number \(p\) is ramified in \(\mathbb{Q}(\zeta)\) if and only if \[ n \equiv 0 \bmod p, \] except in the case where \(p = 2 = (4, n)\) . A prime number \(p \neq 2\) is totally split in \(\mathbb{Q}(\zeta)\) if and only if \[ p \equiv 1 \bmod n. \]
Not formalized. Pinned/current Mathlib has ramification, inertia, Galois and cyclotomic infrastructure, but this full source bundle is either more general than the available hypotheses or contains a decomposition statement not exported as a complete compatible theorem.
Proposition (10.5)
(10.5) Proposition. Let \(\ell\) and \(p\) be odd prime numbers, \(\ell^{*} = (-1)^{\frac{\ell - 1}{2}}\ell\) , and \(\zeta\) a primitive \(\ell\) -th root of unity. Then one has: \[ \begin{array}{l} p \text {is totally split in} \mathbb {Q} \big (\sqrt {\ell^ {*}} \big) \iff p \text {splits in} \mathbb {Q} (\zeta) \text {into an even} \\ \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \text {number of prime ideals.} \end{array} \]
Not formalized. Pinned/current Mathlib has ramification, inertia, Galois and cyclotomic infrastructure, but this full source bundle is either more general than the available hypotheses or contains a decomposition statement not exported as a complete compatible theorem.
Proposition (11.1)
(11.1) Proposition. The mappings \[ \mathfrak {q} \longmapsto \mathfrak {q} S ^ {- 1} \quad a n d \quad \mathfrak {Q} \longmapsto \mathfrak {Q} \cap A \] are mutually inverse 1–1-correspondences between the prime ideals \(\mathfrak{q} \subseteq A \setminus S\) of \(A\) and the prime ideals \(\mathfrak{Q}\) of \(AS^{-1}\) .
Formalized. Mathlib/RingTheory/Localization/Ideal.lean::orderIsoOfPrime, map_under — Pinned localization gives the extension/contraction order equivalence between primes disjoint from S and primes of S⁻¹A.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Corollary (11.2)
(11.2) Corollary. If \(\mathfrak{p}\) is a prime ideal of \(A\) , then \(A_{\mathfrak{p}}\) is a local ring, i.e., \(A_{\mathfrak{p}}\) has a unique maximal ideal, namely \(\mathfrak{m}_{\mathfrak{p}} = \mathfrak{p}A_{\mathfrak{p}}\) . There is a canonical embedding \[ A / \mathfrak {p} \hookrightarrow A _ {\mathfrak {p}} / \mathfrak {m} _ {\mathfrak {p}}, \] identifying \(A_{p}/m_{p}\) with the field of fractions of A/p. In particular, if p is a maximal ideal of A, then one has \[ A / \mathfrak {p} ^ {n} \cong A _ {\mathfrak {p}} / \mathfrak {m} _ {\mathfrak {p}} ^ {n} \quad f o r n \geq 1. \]
Formalized. Mathlib/RingTheory/Localization/AtPrime/Basic.lean::AtPrime.isLocalRing, map_eq_maximalIdeal, equivQuotMaximalIdealPow; Mathlib/RingTheory/LocalRing/ResidueField/Ideal.lean::abbrev Ideal.ResidueField, injective_algebraMap_quotient_residueField, IsFractionRing (R ⧸ I) I.ResidueField — The at-prime localization is local with maximal ideal pA_p; Ideal.ResidueField is its residue field and an IsFractionRing of A/p, and equivQuotMaximalIdealPow gives A/p^n ≃ A_p/m_p^n when p is maximal.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition (11.3)
(11.3) Definition. A discrete valuation ring is a principal ideal domain \(\mathcal{O}\) with a unique maximal ideal \(\mathfrak{p} \neq 0\) .
Formalized. Mathlib/RingTheory/DiscreteValuationRing/Basic.lean::class IsDiscreteValuationRing, not_a_field — The pinned DVR class is exactly a local PID whose unique maximal ideal is nonzero, which is the source definition.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
The exponent n is called the valuation of a. It is denoted \(v(a)\) , and it is obviously characterized by the equation \[ (a) = \mathfrak {p} ^ {v (a)}. \] The valuation is a function \[ v: K ^ {*} \longrightarrow \mathbb {Z}. \] Extending it to K by the convention \(v(0) = \infty\) , a simple calculation shows that it satisfies the conditions \[ v (a b) = v (a) + v (b), \quad v (a + b) \geq \min \left\{v (a), v (b) \right\}. \] This innocuous looking function gives rise to a theory which will occupy all of the next chapter.
Formalized. Mathlib/RingTheory/Valuation/Discrete/IsDiscreteValuationRing.lean::def maximalIdeal, isRankOneDiscrete; Mathlib/RingTheory/DedekindDomain/AdicValuation.lean::def valuation, intValuation_eq_exp_neg_multiplicity, valuation_of_mk; Mathlib/RingTheory/DedekindDomain/Factorization.lean::FractionalIdeal.count — The maximal height-one prime of a DVR induces a rank-one discrete valuation on its fraction field. Under the standard multiplicative encoding exp(-v), intValuation_eq_exp_neg_multiplicity identifies v with the exponent of the principal ideal; valuation multiplication/addition laws give the source v(ab) and ultrametric inequality.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition (11.4)
(11.4) Proposition. If \(\mathcal{O}\) is a Dedekind domain, and \(S \subseteq \mathcal{O} \setminus \{0\}\) is a multiplicative subset, then \(\mathcal{O} S^{-1}\) is also a Dedekind domain.
Formalized. Mathlib/RingTheory/DedekindDomain/Dvr.lean::IsLocalization.isDedekindDomain — Pinned Dedekind localization is exactly Proposition 11.4.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition (11.5)
(11.5) Proposition. Let \(\mathcal{O}\) be a noetherian integral domain. \(\mathcal{O}\) is a Dedekind domain if and only if, for all prime ideals \(\mathfrak{p} \neq 0\) , the localizations \(\mathcal{O}_{\mathfrak{p}}\) are discrete valuation rings.
Formalized. Mathlib/RingTheory/DedekindDomain/Dvr.lean::class IsDedekindDomainDvr, IsDedekindDomain.isDedekindDomainDvr, IsDedekindDomainDvr.isDedekindDomain — The IsDedekindDomainDvr class is Noetherian plus DVR localizations at every nonzero prime, and the two conversion instances prove its equivalence with IsDedekindDomain.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
The maximal ideal \(p\mathbb{Z}_{(p)}\) consists of all fractions a/b satisfying \(p \mid a, p \nmid b\) , and the group of units consists of all fractions a/b satisfying \(p \nmid ab\) . The valuation associated to \(\mathbb{Z}_{(p)}\) , \[ v _ {p}: \mathbb {Q} \longrightarrow \mathbb {Z} \cup \{\infty \}, \] is called the \(p\) -adic valuation of \(\mathbb{Q}\) . The valuation \(v_{p}(x)\) of an element \(x \in \mathbb{Q}^{*}\) is given by \[ v _ {p} (x) = \nu , \] where \(x = p^{\nu}a/b\) with integers a, b relatively prime to p.
Formalized. Mathlib/NumberTheory/Padics/PadicVal/Basic.lean::padicValRat, padicValRat_def, padicValRat.multiplicity_sub_multiplicity; Mathlib/RingTheory/Localization/AtPrime/Basic.lean::isUnit_mk'_iff, mk'_mem_maximal_iff — For p prime, padicValRat is numerator p-multiplicity minus denominator p-multiplicity. The at-prime localization criteria say a/b is a unit exactly when the numerator avoids (p), and lies in the maximal ideal exactly when the numerator lies in (p), yielding the source descriptions of ℤ_(p).
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Convention / notation
Write \(Cl(\mathcal{O})\), resp. \(Cl(\mathcal{O}(X))\), for the ideal class groups of \(\mathcal{O}\), resp. \(\mathcal{O}(X)\). These, together with the unit groups \(\mathcal{O}^{*}\) and \(\mathcal{O}(X)^{*}\), are related by the canonical exact sequence of proposition (11.6).
Formalized. Mathlib/RingTheory/ClassGroup/Basic.lean::ClassGroup — ClassGroup R is the ideal class group for each Dedekind ring R; together with the standard unit group Rˣ, this directly supplies the notation Cl(O), Cl(O(X)), O* and O(X)*.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition (11.6)
(11.6) Proposition. There is a canonical exact sequence \[ 1 \longrightarrow \mathcal {O} ^ {*} \longrightarrow \mathcal {O} (X) ^ {*} \longrightarrow \bigoplus_ {\mathfrak {p} \notin X} K ^ {*} / \mathcal {O} _ {\mathfrak {p}} ^ {*} \longrightarrow C l (\mathcal {O}) \longrightarrow C l (\mathcal {O} (X)) \longrightarrow 1, \] and one has \(K^{*} / \mathcal{O}_{\mathfrak{p}}^{*}\cong \mathbb{Z}\)
Not formalized. Pinned/current Mathlib has localization, DVR and S-integer primitives; targeted open-PR search also checked the S-integer/S-unit developments, but this full exact-sequence/finiteness/decomposition row is not closed by a compatible source.
Definition / construction
For the ring of integers \(O_{K}\) of an algebraic number field K, the proposition yields the following results. Let S denote a finite set of prime ideals of \(O_{K}\) (not any more a multiplicative subset), and let X be the set of all prime ideals that do not belong to S. We put \[ \mathcal {O} _ {K} ^ {S} = \mathcal {O} _ {K} (X). \] The units of this ring are called the S-units, and the group \(Cl_{K}^{S} = Cl(\mathcal{O}_{K}^{S})\) the S-class group of K.
Formalized. Mathlib/RingTheory/DedekindDomain/SInteger.lean::IsDedekindDomain.IsLocalizationSInteger, IsDedekindDomain.isDedekindDomainSInteger — PR #40848 proves the valuation-defined S-integer ring is precisely the relevant localization and a Dedekind domain, so its units and ClassGroup implement Neukirch’s S-units and S-class group. This is post-pin and therefore a revision-specific port.
Searched: mathlib4 PR #40848 head 2c91fb2be280d3a396f0f7de2d7d0df5bf2a8243; Apache-2.0; Lean 4.34-era
Corollary (11.7)
(11.7) Corollary. For the group \(K^S = (\mathcal{O}_K^S)^*\) of \(S\) -units of \(K\) there is an isomorphism \[ K ^ {S} \cong \mu (K) \times \mathbb {Z} ^ {\# S + r + s - 1}, \] where \(r\) and \(s\) are defined as in §5, p. 30.
Not formalized. Pinned/current Mathlib has localization, DVR and S-integer primitives; targeted open-PR search also checked the S-integer/S-unit developments, but this full exact-sequence/finiteness/decomposition row is not closed by a compatible source.
Corollary (11.8)
(11.8) Corollary. The \(S\) -class group \(Cl_K^S = Cl(\mathcal{O}_K^S)\) is finite.
Not formalized. Pinned/current Mathlib has localization, DVR and S-integer primitives; targeted open-PR search also checked the S-integer/S-unit developments, but this full exact-sequence/finiteness/decomposition row is not closed by a compatible source.
Definition (12.1)
(12.1) Definition. Let \(K |Q\) be an algebraic number field of degree n. An order of K is a subring O of \(O_{K}\) which contains an integral basis of length n. The ring \(O_{K}\) is called the maximal order of K.
Not formalized. Pinned/current Mathlib has Picard, conductor, localization and order-of-vanishing primitives, but no first-class number-field order/Chow-group package closes this complete one-dimensional-order statement.
Proposition (12.2)
(12.2) Proposition. An order \(\mathcal{O}\) of \(K\) is a one-dimensional noetherian integral domain.
Not formalized. Pinned/current Mathlib has Picard, conductor, localization and order-of-vanishing primitives, but no first-class number-field order/Chow-group package closes this complete one-dimensional-order statement.
Convention / notation
In what follows, we always let O be a one-dimensional noetherian integral domain and K its field of fractions. We set out by proving the following stronger version of the Chinese remainder theorem.
Not formalized. Pinned/current Mathlib has Picard, conductor, localization and order-of-vanishing primitives, but no first-class number-field order/Chow-group package closes this complete one-dimensional-order statement.
Proposition (12.3)
(12.3) Proposition. If \(\mathfrak{a} \neq 0\) is an ideal of \(\mathcal{O}\) , then \[ \mathcal {O} / \mathfrak {a} \cong \bigoplus_ {\mathfrak {p}} \mathcal {O} _ {\mathfrak {p}} / \mathfrak {a} \mathcal {O} _ {\mathfrak {p}} = \bigoplus_ {\mathfrak {p} \supseteq \mathfrak {a}} \mathcal {O} _ {\mathfrak {p}} / \mathfrak {a} \mathcal {O} _ {\mathfrak {p}}. \]
Not formalized. Pinned/current Mathlib has Picard, conductor, localization and order-of-vanishing primitives, but no first-class number-field order/Chow-group package closes this complete one-dimensional-order statement.
Proposition (12.4)
(12.4) Proposition. A fractional ideal \(\mathfrak{a}\) of \(\mathcal{O}\) is invertible if and only if, for every prime ideal \(\mathfrak{p} \neq 0\) , \[ \mathfrak {a} _ {\mathfrak {p}} = \mathfrak {a} \mathcal {O} _ {\mathfrak {p}} \] is a fractional principal ideal of \(\mathcal{O}_{\mathfrak{p}}\) .
Not formalized. Pinned/current Mathlib has Picard, conductor, localization and order-of-vanishing primitives, but no first-class number-field order/Chow-group package closes this complete one-dimensional-order statement.
Convention / notation
We denote the group of invertible ideals of \(\mathcal{O}\) by \(J(\mathcal{O})\) . It contains the group \(P(\mathcal{O})\) of fractional principal ideals \(a\mathcal{O}, a \in K^{*}\) .
Not formalized. Pinned/current Mathlib has Picard, conductor, localization and order-of-vanishing primitives, but no first-class number-field order/Chow-group package closes this complete one-dimensional-order statement.
Definition (12.5)
(12.5) Definition. The quotient group \[ P i c (\mathcal {O}) = J (\mathcal {O}) / P (\mathcal {O}) \] is called the Picard group of the ring \(\mathcal{O}\) .
Not formalized. Pinned/current Mathlib has Picard, conductor, localization and order-of-vanishing primitives, but no first-class number-field order/Chow-group package closes this complete one-dimensional-order statement.
Proposition (12.6)
(12.6) Proposition. The correspondence \(\mathfrak{a} \mapsto (\mathfrak{a}_{\mathfrak{p}}) = (\mathfrak{a}\mathcal{O}_{\mathfrak{p}})\) yields an isomorphism \[ J (\mathcal {O}) \cong \bigoplus_ {\mathfrak {p}} P (\mathcal {O} _ {\mathfrak {p}}). \] Identifying the subgroup \(P(\mathcal{O})\) with its image in the direct sum one gets \[ P i c (\mathcal {O}) \cong \left(\bigoplus_ {\mathfrak {p}} P (\mathcal {O} _ {\mathfrak {p}})\right) / P (\mathcal {O}). \]
Not formalized. Pinned/current Mathlib has Picard, conductor, localization and order-of-vanishing primitives, but no first-class number-field order/Chow-group package closes this complete one-dimensional-order statement.
Lemma (12.7)
(12.7) Lemma. Let \(\mathcal{O}\) be a one-dimensional noetherian integral domain and \(\tilde{\mathcal{O}}\) its normalization. Then, for each ideal \(\mathfrak{a} \neq 0\) of \(\mathcal{O}\) , the quotient \(\tilde{\mathcal{O}} / \mathfrak{a}\tilde{\mathcal{O}}\) is a finitely generated \(\mathcal{O}\) -module.
Not formalized. Pinned/current Mathlib has Picard, conductor, localization and order-of-vanishing primitives, but no first-class number-field order/Chow-group package closes this complete one-dimensional-order statement.
Proposition (12.8)
(12.8) Proposition ( \(KRULL-AKIZUKI\) ). Let O be a one-dimensional noetherian integral domain with field of fractions K. Let \(L|K\) be a finite extension and O the integral closure of O in L. Then O is a Dedekind domain.
Not formalized. Pinned/current Mathlib has Picard, conductor, localization and order-of-vanishing primitives, but no first-class number-field order/Chow-group package closes this complete one-dimensional-order statement.
Proposition (12.9)
(12.9) Proposition. One has the canonical exact sequence \[ 1 \longrightarrow \mathcal {O} ^ {*} \longrightarrow \tilde {\mathcal {O}} ^ {*} \longrightarrow \bigoplus_ {\mathfrak {p}} \tilde {\mathcal {O}} _ {\mathfrak {p}} ^ {*} / \mathcal {O} _ {\mathfrak {p}} ^ {*} \longrightarrow P i c (\mathcal {O}) \longrightarrow P i c (\tilde {\mathcal {O}}) \longrightarrow 1. \] In the sum, \(\mathfrak{p}\) varies over the prime ideals \(\neq 0\) of \(\mathcal{O}\) and \(\tilde{\mathcal{O}}_{\mathfrak{p}}\) denotes the integral closure of \(\mathcal{O}_{\mathfrak{p}}\) in \(K\) .
Not formalized. Pinned/current Mathlib has Picard, conductor, localization and order-of-vanishing primitives, but no first-class number-field order/Chow-group package closes this complete one-dimensional-order statement.
Definition / construction
A prime ideal \(p \neq 0\) of o is called regular if \(o_{p}\) is integrally closed, and thus a discrete valuation ring. For the regular prime ideals, the summands \(\tilde{o}_{p}^{*}/\tilde{o}_{p}^{*}\) in (12.9) are trivial. There are only finitely many non-regular prime ideals of o, namely the divisors of the conductor of o. This is by definition the biggest ideal of \(\tilde{o}\) which is contained in o, in other words, \[ f = \left\{a \in \tilde {\mathcal {O}} \mid a \tilde {\mathcal {O}} \subseteq \mathcal {O} \right\}. \] Since \(\tilde{\mathcal{O}}\) is a finitely generated \(\mathcal{O}\) -module, we have \(f \neq 0\) .
Not formalized. Pinned/current Mathlib has Picard, conductor, localization and order-of-vanishing primitives, but no first-class number-field order/Chow-group package closes this complete one-dimensional-order statement.
Proposition (12.10)
(12.10) Proposition. For any prime ideal \(\mathfrak{p} \neq 0\) of \(\mathcal{O}\) one has \[ \mathfrak {p} \nmid f \iff \mathfrak {p} \text { is regular. } \] If this is the case, then \(\tilde{\mathfrak{p}} = \mathfrak{p}\tilde{\mathcal{O}}\) is a prime ideal of \(\tilde{\mathcal{O}}\) and \(\mathcal{O}_{\mathfrak{p}} = \tilde{\mathcal{O}}_{\tilde{\mathfrak{p}}}\) .
Not formalized. Pinned/current Mathlib has Picard, conductor, localization and order-of-vanishing primitives, but no first-class number-field order/Chow-group package closes this complete one-dimensional-order statement.
Proposition (12.11)
(12.11) Proposition. \(\bigoplus_{\mathfrak{p}}\tilde{\mathcal{O}}_{\mathfrak{p}}^{*} / \mathcal{O}_{\mathfrak{p}}^{*}\cong (\tilde{\mathcal{O}} /\mathfrak{f})^{*} / (\mathcal{O} / \mathfrak{f})^{*}\) .
Not formalized. Pinned/current Mathlib has Picard, conductor, localization and order-of-vanishing primitives, but no first-class number-field order/Chow-group package closes this complete one-dimensional-order statement.
Theorem (12.12)
(12.12) Theorem. Let \(\mathcal{O}\) be an order in an algebraic number field \(K\) , \(\mathcal{O}_K\) the maximal order, and \(\mathfrak{f}\) the conductor of \(\mathcal{O}\) . Then the groups \(\mathcal{O}_K^* / \mathcal{O}^*\) and \(Pic(\mathcal{O})\) are finite and one has \[ \# P i c (\mathcal {O}) = \frac {h _ {K}}{(\mathcal {O} _ {K} ^ {*} : \mathcal {O} ^ {*})} \frac {\# (\mathcal {O} _ {K} / \mathfrak {f}) ^ {*}}{\# (\mathcal {O} / \mathfrak {f}) ^ {*}}, \] where \(h_K\) is the class number of \(K\) . In particular, one has that \[ \operatorname{rank} \left(\mathcal {O} ^ {*}\right) = \operatorname{rank} \left(\mathcal {O} _ {K} ^ {*}\right) = r + s - 1. \]
Not formalized. Pinned/current Mathlib has Picard, conductor, localization and order-of-vanishing primitives, but no first-class number-field order/Chow-group package closes this complete one-dimensional-order statement.
Definition / construction
The definition of the Picard group of a one-dimensional noetherian integral domain \(\mathcal{O}\) avoids the problem of the uniqueness of prime ideal decomposition by restricting attention to the invertible ideals, and thus leaving aside the information carried by noninvertibles. But there is another important generalization of the ideal class group which does take into account all prime ideals of \(\mathcal{O}\) . It is based on an artificial re-introduction of the uniqueness of prime decomposition. This group is called the divisor class group, or Chow group of \(\mathcal{O}\) . Its definition starts from the free abelian group \[ D i v (\mathcal {O}) = \bigoplus_ {\mathfrak {p}} \mathbb {Z} \mathfrak {p} \] on the set of all maximal ideals \(\mathfrak{p}\) of \(\mathcal{O}\) (i.e., the set of all prime ideals \(\neq 0\) ). This group is called the divisor group of \(\mathcal{O}\) . Its elements are formal sums \[ D = \sum_ {\mathfrak {p}} n _ {\mathfrak {p}} \mathfrak {p} \] with \(n_{p} \in Z\) and \(n_{p} = 0\) for almost all p, called divisors (or 0-cycles). Corollary (3.9) simply says that, in the case of a Dedekind domain, the divisor group \(Div(\mathcal{O})\) and the group of ideals are canonically isomorphic. The additive notation and the name of the group stem from function theory where divisors for analytic functions play the same rôle as ideals do for algebraic numbers (see chap. III, §3).
Not formalized. Pinned/current Mathlib has Picard, conductor, localization and order-of-vanishing primitives, but no first-class number-field order/Chow-group package closes this complete one-dimensional-order statement.
Definition / construction
In order to define the divisor class group we have to associate to every \(f \in K^{*}\) a “principal divisor” \(\text{div}(f)\) . We use the case of a Dedekind domain to guide us. There the principal ideal (f) was given by \[ (f) = \prod_ {\mathfrak {p}} \mathfrak {p} ^ {v _ {\mathfrak {p}} (f)}, \] where \(v_{p}: K^{*} \to Z\) is the p-adic exponential valuation associated to the valuation ring \(O_{p}\) . In general, \(O_{p}\) is not anymore a discrete valuation ring. Nevertheless, \(O_{p}\) defines a homomorphism \[ \operatorname{ord} _ {\mathfrak {p}}: K ^ {*} \to \mathbb {Z} \] which generalizes the valuation function. If \(f = a / b \in K^*\) , with \(a, b \in \mathcal{O}\) , then we put \[ \operatorname{ord} _ {\mathfrak {p}} (f) = \ell_ {\mathcal {O} _ {\mathfrak {p}}} (\mathcal {O} _ {\mathfrak {p}} / a \mathcal {O} _ {\mathfrak {p}}) - \ell_ {\mathcal {O} _ {\mathfrak {p}}} (\mathcal {O} _ {\mathfrak {p}} / b \mathcal {O} _ {\mathfrak {p}}), \] where \(\ell_{\mathcal{O}_{\mathfrak{p}}}(M)\) denotes the length of an \(\mathcal{O}_{\mathfrak{p}}\) -module \(M\) , i.e., the maximal length of a strictly decreasing chain \[ M = M _ {0} \supsetneqq M _ {1} \supsetneqq \dots \supsetneqq M _ {\ell} = 0 \] of \(\mathcal{O}_{\mathfrak{p}}\) -submodules. In the special case where \(\mathcal{O}_{\mathfrak{p}}\) is a discrete valuation ring with maximal ideal \(\mathfrak{m}\) , the value \(\nu = v_{\mathfrak{p}}(a)\) of \(a \in \mathcal{O}_{\mathfrak{p}}\) , for \(a \neq 0\) , is given by the equation \[ a \mathcal {O} _ {\mathfrak {p}} = \mathfrak {m} ^ {\nu}. \] It is equal to the length of the \(O_{p}\) -module \(O_{p}/m^{\nu}\) , because the longest chain of submodules is \[ \mathcal {O} _ {\mathfrak {p}} / \mathfrak {m} ^ {\nu} \supset \mathfrak {m} / \mathfrak {m} ^ {\nu} \supset \dots \supset \mathfrak {m} ^ {\nu} / \mathfrak {m} ^ {\nu} = (0). \] Thus the function \(ord_{p}\) agrees with the exponential valuation \(v_{p}\) in this case. The property of the function \(ord_{p}\) to be a homomorphism follows from the fact (which is easily proved) that the length function \(\ell_{O_{p}}\) is multiplicative on short exact sequences of \(O_{p}\) -modules. Using the functions \(ord_{p}: K^{*} \to Z\) , we can now associate to every element \(f \in K^{*}\) the divisor \[ \operatorname{div} (f) = \sum_ {\mathfrak {p}} \operatorname{ord} _ {\mathfrak {p}} (f) \mathfrak {p}, \] and thus obtain a canonical homomorphism \[ \operatorname{div}: K ^ {*} \longrightarrow D i v (\mathcal {O}). \] The elements \(\text{div}(f)\) are called principal divisors. They form a subgroup \(\mathcal{P}(\mathcal{O})\) of \(\text{Div}(\mathcal{O})\) . Two divisors D and \(D'\) which differ only by a principal divisor are called rationally equivalent.
Not formalized. Pinned/current Mathlib has Picard, conductor, localization and order-of-vanishing primitives, but no first-class number-field order/Chow-group package closes this complete one-dimensional-order statement.
Definition (12.13)
(12.13) Definition. The quotient group \[ C H ^ {1} (\mathcal {O}) = D i v (\mathcal {O}) / \mathcal {P} (\mathcal {O}) \] is called the divisor class group or Chow group of \(\mathcal{O}\) .
Not formalized. Pinned/current Mathlib has Picard, conductor, localization and order-of-vanishing primitives, but no first-class number-field order/Chow-group package closes this complete one-dimensional-order statement.
Definition / construction
The Chow group is related to the Picard group by a canonical homomorphism \[ \operatorname{div}: P i c (\mathcal {O}) \longrightarrow C H ^ {1} (\mathcal {O}) \] which is defined as follows. If a is an invertible ideal, then, by (12.4), \(aO_{p}\) , for any prime ideal \(p \neq 0\) , is a principal ideal \(a_{p}O_{p}, a_{p} \in K^{*}\) , and we put \[ \operatorname{div} (\mathfrak {a}) = \sum_ {\mathfrak {p}} - \operatorname{ord} _ {\mathfrak {p}} (a _ {\mathfrak {p}}) \mathfrak {p}. \] This gives us a homomorphism \[ \operatorname{div}: J (\mathcal {O}) \longrightarrow D i v (\mathcal {O}) \] of the ideal group \(J(\mathcal{O})\) which takes principal ideals into principal divisors, and therefore induces a homomorphism \[ \operatorname{div}: P i c (\mathcal {O}) \longrightarrow C H ^ {1} (\mathcal {O}). \] In the special case of a Dedekind domain we obtain:
Not formalized. Pinned/current Mathlib has Picard, conductor, localization and order-of-vanishing primitives, but no first-class number-field order/Chow-group package closes this complete one-dimensional-order statement.
Proposition (12.14)
(12.14) Proposition. If \(\mathcal{O}\) is a Dedekind domain, then \[ \operatorname{div}: P i c (\mathcal {O}) \longrightarrow C H ^ {1} (\mathcal {O}) \] is an isomorphism.
Not formalized. Pinned/current Mathlib has Picard, conductor, localization and order-of-vanishing primitives, but no first-class number-field order/Chow-group package closes this complete one-dimensional-order statement.
Definition / construction
In order to explain this, let us start from polynomials \[ f (x) = a _ {n} x ^ {n} + \dots + a _ {0} \] with complex coefficients \(a_{i} \in C\) , which may be immediately interpreted as functions on the complex plane. This property may be formulated in a purely algebraic way as follows. Let \(a \in C\) be a point in the complex plane. The set of all functions \(f(x)\) in the polynomial ring C[x] which vanish at the point a forms the maximal ideal \(\mathfrak{p} = (x - a)\) of C[x]. In this way the points of the complex plane correspond 1-1 to the maximal ideals of C[x]. We denote the set of all these maximal ideals by \[ M = \operatorname{Max} (\mathbb {C} [ x ]). \] We may view M as a new kind of space and may interpret the elements \(f(x)\) of the ring C[x] as functions on M as follows. For every point \(\mathfrak{p} = (x - a)\) of M we have the canonical isomorphism \[ \mathbb {C} [ x ] / \mathfrak {p} \stackrel {\sim} {\longrightarrow} \mathbb {C}, \] which sends the residue class \(f(x) \mod \mathfrak{p}\) to \(f(a)\) . We may thus view this residue class \[ f (\mathfrak {p}) := f (x) \bmod \mathfrak {p} \in \kappa (\mathfrak {p}) \] in the residue class field \(\kappa(\mathfrak{p}) = \mathbb{C}[x]/\mathfrak{p}\) as the “value” of f at the point \(p \in M\) . The topology on C cannot be transferred to M by algebraic means. All that can be salvaged algebraically are the point sets defined by equations of the form \[ f (x) = 0 \] (i.e., only the finite sets and \(M\) itself). These sets are defined to be the closed subsets. In the new formulation they are the sets \[ V (f) = \left\{\mathfrak {p} \in M \mid f (\mathfrak {p}) = 0 \right\} = \left\{\mathfrak {p} \in M \mid \mathfrak {p} \supseteq (f (x)) \right\}. \]
Not formalized. Pinned/current Mathlib has Spec, structure-sheaf, stalk and affine-scheme infrastructure, but this full example/global divisor/function-field statement is not exported as a complete compatible theorem.
Definition / construction
The algebraic interpretation of functions given above leads to the following geometric perception of completely general rings. For an arbitrary ring O, one introduces the spectrum \[ X = \operatorname{Spec} (\mathcal {O}) \] as being the set of all prime ideals \(\mathfrak{p}\) of \(\mathcal{O}\) . The Zariski topology on \(X\) is defined by stipulating that the sets \[ V (a) = \left\{\mathfrak {p} \mid \mathfrak {p} \supseteq a \right\} \] be the closed sets, where a varies over the ideals of o. This does make X into a topological space (observe that \(V(\mathfrak{a}) \cup V(\mathfrak{b}) = V(\mathfrak{ab})\) ) which, however, is usually not Hausdorff. The closed points correspond to the maximal ideals of o.
Formalized. Mathlib/RingTheory/Spectrum/Prime/Basic.lean::PrimeSpectrum; Mathlib/RingTheory/Spectrum/Prime/Topology.lean::PrimeSpectrum.isClosed_singleton_iff_isMaximal — Pinned PrimeSpectrum is Spec with Zariski topology; singleton closed points are exactly maximal ideals.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
The elements \(f \in O\) now play the rôle of functions on the topological space X: the “value” of f at the point p is defined to be \[ f (\mathfrak {p}) := f \bmod {\mathfrak {p}} \] and is an element of the residue class field \(\kappa(\mathfrak{p})\) , i.e., in the field of fractions of \(\sigma/\mathfrak{p}\) . So the values of f do not in general lie in a single field.
Formalized. Mathlib/RingTheory/LocalRing/ResidueField/Ideal.lean::abbrev Ideal.ResidueField, algebraMap_quotient_residueField_mk, IsFractionRing (R ⧸ I) I.ResidueField — For a prime ideal p, p.ResidueField is the residue field of A_p and an IsFractionRing of A/p; the algebra map sends the quotient class of f to its value in κ(p).
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Example / comparison
Example: The space \(X = \text{Spec}(\mathbb{Z})\) may be represented by a line.| 2 | 3 | 5 | 7 | 11 | generic point |
For every prime number one has a closed point, and there is also the generic point (0), the closure of which is the total space X. The nonempty open sets in X are obtained by throwing out finitely many prime numbers \(p_{1}, \ldots, p_{n}\) . The integers \(a \in Z\) are viewed as functions on X by defining the value of a at the point (p) to be the residue class \[ a (p) = a \bmod p \in \mathbb {Z} / p \mathbb {Z}. \] The fields of values are then \[ \mathbb {Z} / 2 \mathbb {Z}, \mathbb {Z} / 3 \mathbb {Z}, \mathbb {Z} / 5 \mathbb {Z}, \mathbb {Z} / 7 \mathbb {Z}, \mathbb {Z} / 1 1 \mathbb {Z}, \dots , \mathbb {Q}. \] Thus every prime field occurs exactly once. An important refinement of the geometric interpretation of elements of the ring \(\mathcal{O}\) as functions on the space \(X = \operatorname{Spec}(\mathcal{O})\) is obtained by forming the structure sheaf \(\mathcal{O}_X\) . This means the following. Let \(U \neq \emptyset\) be an open subset of \(X\) . If \(\mathcal{O}\) is a one-dimensional integral domain, then the ring of “regular functions” on \(U\) is given by \[ \mathcal {O} (U) = \left\{\frac {f}{g} \mid g (\mathfrak {p}) \neq 0 \quad \text { for all } \mathfrak {p} \in U \right\}, \] in other words, it is the localization of \(\mathcal{O}\) with respect to the multiplicative set \(S = \mathcal{O} \setminus \bigcup_{\mathfrak{p} \in U} \mathfrak{p}\) (see §11). In the general case, \(\mathcal{O}(U)\) is defined to consist of all elements \[ s = (s _ {\mathfrak {p}}) \in \prod_ {\mathfrak {p} \in U} \mathcal {O} _ {\mathfrak {p}} \] which locally are quotients of two elements of \(\mathcal{O}\) . More precisely, this means that for every \(\mathfrak{p} \in U\) , there exists a neighbourhood \(V \subseteq U\) of \(\mathfrak{p}\) , and elements \(f, g \in \mathcal{O}\) such that, for each \(\mathfrak{q} \in V\) , one has \(g(\mathfrak{q}) \neq 0\) and \(s_{\mathfrak{q}} = f / g\) in \(\mathcal{O}_{\mathfrak{q}}\) . These quotients have to be understood in the more general sense of commutative algebra (see §11, exercise 1). We leave it to the reader to check that one gets back the above definition in the case of a one-dimensional integral domain \(\mathcal{O}\) . If \(V \subseteq U\) are two open sets of \(X\) , then the projection \[ \prod_ {\mathfrak {p} \in U} \mathcal {O} _ {\mathfrak {p}} \longrightarrow \prod_ {\mathfrak {p} \in V} \mathcal {O} _ {\mathfrak {p}} \] induces a homomorphism \[ \rho_ {U V}: \mathcal {O} (U) \longrightarrow \mathcal {O} (V), \] called the restriction from U to V. The system of rings \(\mathcal{O}(U)\) and mappings \(\rho_{UV}\) is a sheaf on X. This notion means the following.
Not formalized. Pinned/current Mathlib has Spec, structure-sheaf, stalk and affine-scheme infrastructure, but this full example/global divisor/function-field statement is not exported as a complete compatible theorem.
Definition (13.1)
(13.1) Definition. Let X be a topological space. A presheaf F of abelian groups (rings, etc.) consists of the following data. (1) For every open set \(U\) , an abelian group (a ring, etc.) \(\mathcal{F}(U)\) is given. (2) For every inclusion \(U \subseteq V\) , a homomorphism \(\rho_{UV} : \mathcal{F}(U) \to \mathcal{F}(V)\) is given, which is called restriction. These data are subject to the following conditions: (a) \(\mathcal{F}(\emptyset)=0,\) (b) \(\rho_{UU}\) is the identity id: \(\mathcal{F}(U)\to \mathcal{F}(U)\) , (c) \(\rho_{UW} = \rho_{VW} \circ \rho_{UV}\) , for open sets \(W \subseteq V \subseteq U\) .
Not formalized. Pinned/current Mathlib has Spec, structure-sheaf, stalk and affine-scheme infrastructure, but this full example/global divisor/function-field statement is not exported as a complete compatible theorem.
Definition / construction
The elements \(s \in \mathcal{F}(U)\) are called the sections of the presheaf F over U. If \(V \subseteq U\) , then one usually writes \(\rho_{UV}(s) = s|_{V}\) . The definition of a presheaf can be reformulated most concisely in the language of categories. The open sets of the topological space X form a category \(X_{top}\) in which only inclusions are admitted as morphisms. A presheaf of abelian groups (rings) is then simply a contravariant functor \[ \mathcal {F}: X _ {\text { top }} \longrightarrow (a b), (r i n g s) \] into the category of abelian groups (resp. rings) such that \(\mathcal{F}(\emptyset)=0\) .
Not formalized. Pinned/current Mathlib has Spec, structure-sheaf, stalk and affine-scheme infrastructure, but this full example/global divisor/function-field statement is not exported as a complete compatible theorem.
Definition (13.2)
(13.2) Definition. A presheaf \(\mathcal{F}\) on the topological space \(X\) is called a sheaf if, for all open coverings \(\{U_i\}\) of the open sets \(U\) , one has: (i) If \(s, s' \in \mathcal{F}(U)\) are two sections such that \(s|_{U_i} = s'|_{U_i}\) for all \(i\) , then \(s = s'\) . (ii) If \(s_i \in \mathcal{F}(U_i)\) is a family of sections such that \[ s _ {i} \mid_ {U _ {i} \cap U _ {j}} = s _ {j} \mid_ {U _ {i} \cap U _ {j}} \] for all \(i, j\) , then there exists a section \(s \in \mathcal{F}(U)\) such that \(s|_{U_i} = s_i\) for all \(i\) .
Formalized. Mathlib/Topology/Sheaves/SheafCondition/UniqueGluing.lean::IsCompatible, IsSheafUniqueGluing, isSheaf_iff_isSheafUniqueGluing — Pinned IsSheafUniqueGluing says every compatible family over a cover has a unique gluing, and is equivalent to the sheaf predicate.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
The stalk of the sheaf \(\mathcal{F}\) at the point \(x \in X\) is defined to be the direct limit (see chap. IV, §2) \[ \mathcal {F} _ {x} = \varinjlim_ {U \ni x} \mathcal {F} (U), \] where U varies over all open neighbourhoods of x. In other words, two sections \(s_{U} \in \mathcal{F}(U)\) and \(s_{V} \in \mathcal{F}(V)\) are called equivalent in the disjoint union \(\bigcup_{U \ni x} \mathcal{F}(U)\) if there exists a neighbourhood \(W \subseteq U \cap V\) of x such that \(s_{U}|_{W} = s_{V}|_{W}\) . The equivalence classes are called germs of sections at x. They are the elements of \(F_{x}\) .
Formalized. Mathlib/Topology/Sheaves/Stalks.lean::def stalk, def germ, exists_germ_eq, theorem germ_eq — The stalk is defined as the colimit over neighborhoods; germ, exists_germ_eq, and germ_eq give the source germ representatives and local-equivalence criterion.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Proposition (13.3)
(13.3) Proposition. The rings \(\mathcal{O}(U)\) , together with the restriction mappings \(\rho_{UV}\) , form a sheaf on \(X\) . It is denoted by \(\mathcal{O}_X\) and called the structure sheaf on \(X\) . The stalk of \(\mathcal{O}_X\) at the point \(\mathfrak{p} \in X\) is the localization \(\mathcal{O}_{\mathfrak{p}}\) , i.e., \(\mathcal{O}_{X,\mathfrak{p}} \cong \mathcal{O}_{\mathfrak{p}}\) .
Formalized. Mathlib/AlgebraicGeometry/StructureSheaf.lean::Spec.structureSheaf, stalkIso, IsLocalization.to_stalk — The pinned structure sheaf on Spec has stalk canonically isomorphic to the localization A_p.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
The proof of this proposition follows immediately from the definitions. The couple \((X,\mathcal{O}_{X})\) is called an affine scheme. Usually, however, the structure sheaf \(O_{X}\) is dropped from the notation. Now let \[ \varphi : \mathcal {O} \longrightarrow \mathcal {O} ^ {\prime} \] be a homomorphism of rings and \(X = \operatorname{Spec}(\mathcal{O})\) , \(X' = \operatorname{Spec}(\mathcal{O}')\) . Then \(\varphi\) induces a continuous map \[ f: X ^ {\prime} \longrightarrow X, f (\mathfrak {p} ^ {\prime}) := \varphi^ {- 1} (\mathfrak {p} ^ {\prime}), \] and, for every open subset U of X, a homomorphism \[ f _ {U} ^ {*}: \mathcal {O} (U) \longrightarrow \mathcal {O} (U ^ {\prime}), \quad s \longmapsto s \circ f | _ {U ^ {\prime}}, \] where \(U' = f^{-1}(U)\) . The maps \(f_U^*\) have the following two properties.
Formalized. Mathlib/AlgebraicGeometry/Scheme.lean::def Spec, Spec.map; Mathlib/AlgebraicGeometry/AffineScheme.lean::IsAffine — Pinned Spec and Spec.map turn ring maps contravariantly into morphisms of affine schemes.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
A continuous map \(f: X' \to X\) together with a family of homomorphisms \(f_U^*: \mathcal{O}(U) \to \mathcal{O}(U')\) which satisfy conditions a) and b) is called a morphism from the scheme \(X'\) to the scheme \(X\) . When referring to such a morphism, the maps \(f_U^*\) are usually not written explicitly. One can show that every morphism between two affine schemes \(X' = \operatorname{Spec}(\mathcal{O}')\) and \(X = \operatorname{Spec}(\mathcal{O})\) is induced in the way described above by a ring homomorphism \(\varphi: \mathcal{O} \to \mathcal{O}'\) .
Formalized. Mathlib/AlgebraicGeometry/Scheme.lean::structure Hom; Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean::Spec.fullyFaithful, Spec.map_surjective, Spec.homEquiv — Scheme.Hom packages the underlying locally ringed-space morphism; full faithfulness/surjectivity of Spec.map says every affine-scheme morphism is induced uniquely by the opposite ring homomorphism.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition / construction
If \(L|K\) is Galois with Galois group \(G = G(L|K)\) , then every automorphism \(\sigma \in G\) induces via \(\sigma : \mathcal{O} \to \mathcal{O}\) an automorphism of schemes \(\sigma : X \to X\) . Since the ring \(\mathcal{O}\) is fixed, the diagram \[ \begin{array}{c} X \xrightarrow {\sigma} X \\ f \searrow_ {Y} \swarrow_ {f} \end{array} \] is commutative. Such an automorphism is called a covering transformation of the ramified covering X/Y. The group of covering transformations is denoted by \(\operatorname{Aut}_{Y}(X)\) . We thus have a canonical isomorphism \[ G (L | K) \cong \operatorname{Aut} _ {Y} (X). \]
Not formalized. Pinned/current Mathlib has Spec, structure-sheaf, stalk and affine-scheme infrastructure, but this full example/global divisor/function-field statement is not exported as a complete compatible theorem.
Definition / construction
In chap. II, §7, we will see that the composite of two unramified extensions of \(K\) is again unramified. The composite \(\widetilde{K}\) , taken inside some algebraic closure \(\overline{K}\) of \(K\) , of all unramified extensions \(L|K\) is called the maximal unramified extension of \(K\) . The integral closure \(\tilde{\mathcal{O}}\) of \(\mathcal{O}\) in \(\widetilde{K}\) is still a one-dimensional integral domain, but in general no longer noetherian, and, as a rule, there will be infinitely many prime ideals lying above a given prime ideal \(\mathfrak{p} \neq 0\) of \(\mathcal{O}\) . The scheme \(\widetilde{Y} = \operatorname{Spec}(\tilde{\mathcal{O}})\) with the morphism \[ f: \widetilde {Y} \longrightarrow Y \] is called the universal covering of Y. It plays the same rôle for schemes that the universal covering space \(\widetilde{X} \to X\) of a topological space plays in topology. There the group of covering transformations \(\operatorname{Aut}_{X}(\widetilde{X})\) is canonically isomorphic to the fundamental group \(\pi_{1}(X)\) . Therefore we define in our present context the fundamental group of the scheme Y by \[ \pi_ {1} (Y) = \operatorname{Aut} _ {Y} (\widetilde {Y}) = G (\widetilde {K} | K). \]
Not formalized. Pinned/current Mathlib has Spec, structure-sheaf, stalk and affine-scheme infrastructure, but this full example/global divisor/function-field statement is not exported as a complete compatible theorem.
Definition / construction
The definition of a discrete valuation of K does not require the subring O to be given in advance, and in fact, aside from those arising from O, there are finitely many other discrete valuations of K. In the case of the field \(\mathbb{F}_{p}(t)\) there is one more valuation, besides the ones associated to the prime ideals \(\mathfrak{p} = (p(t))\) of \(\mathbb{F}_{p}[t]\) , namely, the degree valuation \(v_{\infty}\) . For \(\frac{f}{g} \in \mathbb{F}_{p}(t)\) , \(f, g \in \mathbb{F}_{p}[t]\) , it is defined by \[ v _ {\infty} \left(\frac {f}{g}\right) = \deg (g) - \deg (f). \] It is associated to the prime ideal \(\mathfrak{p} = y\mathbb{F}_p[y]\) of the ring \(\mathbb{F}_p[y]\) , where \(y = 1 / t\) . One can show that this exhausts all normalized valuations of the field \(\mathbb{F}_p(t)\) .
Not formalized. Pinned/current Mathlib has Spec, structure-sheaf, stalk and affine-scheme infrastructure, but this full example/global divisor/function-field statement is not exported as a complete compatible theorem.
Definition / construction
For an arbitrary finite extension K of \(\mathbb{F}_{p}(t)\) , instead of restricting attention to prime ideals, one now considers all normalized discrete valuations \(v_{p}\) of K in the above sense, where the index p has kept only a symbolic value. As an analogue of the ideal group we form the “divisor group”, i.e., the free abelian group generated by these symbols, \[ D i v (K) = \left\{\sum_ {\mathfrak {p}} n _ {\mathfrak {p}} \mathfrak {p} \mid n _ {\mathfrak {p}} \in \mathbb {Z}, n _ {\mathfrak {p}} = 0 \text { for almost all } \mathfrak {p} \right\}. \]
Not formalized. Pinned/current Mathlib has Spec, structure-sheaf, stalk and affine-scheme infrastructure, but this full example/global divisor/function-field statement is not exported as a complete compatible theorem.
Definition / construction
We consider the mapping \[ \operatorname{div}: K ^ {*} \longrightarrow D i v (K), \quad \operatorname{div} (f) = \sum_ {\mathfrak {p}} v _ {\mathfrak {p}} (f) \mathfrak {p}, \] the image of which is written \(\mathcal{P}(K)\) , and we define the divisor class group of \(K\) by \[ C l (K) = D i v (K) / \mathcal {P} (K). \] Unlike the ideal class group of an algebraic number field, this group is not finite. Rather, one has the canonical homomorphism \[ \deg : C l (K) \longrightarrow \mathbb {Z}, \] which associates to the class of p the degree \(\deg(\mathfrak{p}) = [\kappa(\mathfrak{p}) : \mathbb{F}_{p}]\) of the residue class field of the valuation ring of p, and which associates to the class of an arbitrary divisor \(a = \sum_{p} n_{p} p\) the sum \[ \deg (\mathfrak {a}) = \sum_ {\mathfrak {p}} n _ {\mathfrak {p}} \deg (\mathfrak {p}). \] For a principal divisor \(\text{div}(f)\) , \(f \in K^{*}\) , we find by an easy calculation that \(\deg(\text{div}(f)) = 0\) , so that the mapping deg is indeed well-defined. As an analogue of the finiteness of the class number of an algebraic number field, one obtains here the fact that, if not \(Cl(K)\) itself, the kernel \(Cl^{0}(K)\) of deg is finite. The infinitude of the class group of function fields must not be considered as strange. On the contrary, it is rather the finiteness in the number field case that should be regarded as a deficiency which calls for correction. The adequate appreciation of this situation and its amendment will be explained in chap. III, §1.
Not formalized. Pinned/current Mathlib has Spec, structure-sheaf, stalk and affine-scheme infrastructure, but this full example/global divisor/function-field statement is not exported as a complete compatible theorem.
Definition / construction
The pair \((X, \mathcal{O}_X)\) is the scheme corresponding to the field \(\mathbb{F}_p(t)\) . It is called the projective line over \(\mathbb{F}_p\) and denoted \(\mathbb{P}_{\mathbb{F}_p}^1\) .
Not formalized. Pinned/current Mathlib has Spec, structure-sheaf, stalk and affine-scheme infrastructure, but this full example/global divisor/function-field statement is not exported as a complete compatible theorem.