FC09 — Jürgen Neukirch, Algebraic Number Theory (1999)

FC09 — Neukirch, Algebraic Number Theory.

This chapter contains 55 definitions, 13 theorems, 33 propositions, 4 lemmas, 8 corollaries, 2 examples, 13 conventions and 1 other statements.

Of the 129 statements checked against Lean, 11 are formalized somewhere and 118 are not.

Status	Statements	Share	What it means
not formalized	118	91%	A documented search found no Lean statement of it anywhere.
in Mathlib	11	9%	Mathlib states and proves it.
checked in total	129

Which versions of Lean and Mathlib were searched

Canonical source block: FC09 Neukirch Chapter III, FC09-C03-U001–FC09-C03-U129, in canonical source-ID order from Foundational corpus units FC09 Neukirch. The generator retrieves all 129 rows through agent-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). LeanCategories/Lattices/Valued/ArithmeticPlace.lean provides a project sum type of finite and infinite arithmetic places, and LeanCategories/Lattices/Valued/DeterminantLine.lean provides generic-rank, determinant-line, intrinsic-discriminant and Steinitz scaffolding. Neither supplies Neukirch’s valuation-equivalence-class place object or the replete/Arakelov/metrized structures required by the corresponding C03 bundles, so C03 has no project-existing route.
Pinned Mathlib is P=db584cd6d46c92f209a44c0f1c829460d327499d, Lean 4.33.0, Apache-2.0. Native source-complete coverage in C03 is concentrated in the global product formula/class group, trace-dual/different theory, Kähler differentials, Hermite–Minkowski discriminant theorems, the no-unramified-extension theorem for ℚ, and the abstract projective-module lifting criterion.
Current Mathlib was checked at H=71a80585ee495fc24472fd0eaffc89d94e4fd8d6. Targeted current-tree searches found no Arakelov, replete ideal, Euler-Minkowski, or Grothendieck-Riemann-Roch layer. The current different file still has no Kähler-differential bridge identifying the different with the annihilator of Ω, and no first-class relative discriminantIdeal was found. Targeted open-PR title searches on 2026-09-07 likewise found no relevant arithmetic-metric or different/Kähler owner; the returned Kähler and Hermite hits concern refactors or Hermite polynomials, not these source units.
Strict bundle semantics was enforced. In particular, ordinary finite/infinite place representations do not earn U001–U005 where Neukirch packages valuation classes and a nonstandard convention declaring C/R unramified; generic divisor/Picard infrastructure does not earn replete/Arakelov ideals; transitivity of the different alone does not earn U028’s localization-and-completion bundle; derivative membership does not earn U032’s generation theorem; the prime-divides-different criterion does not earn U033’s tame/wild exponent formulas; Kähler infrastructure does not earn U036 without the annihilator equality; and absolute discriminant identities do not earn U038–U043’s relative discriminant-ideal package.
The arithmetic-metric half of the chapter is treated just as strictly. The project determinant-line API does not earn metrized determinant sequences; generic tensor/Hermitian/projective/Picard APIs do not earn the metrized-module category; and ordinary Grothendieck/homological APIs do not earn arithmetic K₀, arithmetic Chern character, Grothendieck–Riemann–Roch, or Euler–Minkowski statements.
Short derivations are credited only from exact pinned ingredients: U031 collapses the conductor in conductor_mul_differentIdeal under the monogenic hypothesis; U045 derives Neukirch’s weaker uniform discriminant bound from Mathlib’s sharper signature-dependent bound using r+2s=n; U047 specializes Hermite finiteness to a fixed algebraic closure; and U083 uses the standard equivalence between Hom-exactness and lifting against surjections.
All mathlib targets were path/token validated against P; current-head negative checks were validated against H.
Route totals for C03: mathlib 11, project-existing 0, package-import 0, reference-port 0, unmatched 118.

Definition (1.1)

FC09-C03-U001 · Chapter III, §1, source L7574 · not formalized

(1.1) Definition. A prime (or place) p of an algebraic number field K is a class of equivalent valuations of K. The nonarchimedean equivalence classes are called finite primes and the archimedean ones infinite primes.

Not formalized. Pinned/current Mathlib has finite/infinite place, product-formula, class-group, scheme, and ordinary divisor infrastructure, while the project has an arithmetic-place sum type; this source row contains a valuation-class, replete/Arakelov ideal, compactness, or arithmetic-divisor bundle not exported as one compatible owner.

Convention / notation

FC09-C03-U002 · Chapter III, §1, source L7578 · not formalized

In the case of a finite prime, the letter p has a multiple meaning: it also stands for the prime ideal of the ring o of integers of K, or for the maximal ideal of the associated valuation ring, or even for the maximal ideal of the completion. However, this will nowhere create any risk of confusion. We write \(p|p\) if p is the characteristic of the residue field \(\kappa(\mathfrak{p})\) of the finite prime p. For an infinite prime we adopt the convention that the completion \(K_{p}\) also serves as its own “residue field,” i.e., we put \[ \kappa (\mathfrak {p}) := K _ {\mathfrak {p}}, \quad \text { when } \mathfrak {p} | \infty . \]

Definition / construction

FC09-C03-U003 · Chapter III, §1, source L7584 · not formalized

To each prime \(\mathfrak{p}\) of \(K\) we now associate a canonical homomorphism \[ v _ {\mathfrak {p}}: K ^ {*} \to \mathbb {R} \] from the multiplicative group \(K^{*}\) of K. If p is finite, then \(v_{p}\) is the p-adic exponential valuation which is normalized by the condition \(v_{\mathfrak{p}}(K^{*}) = \mathbb{Z}\) . If p is infinite, then \(v_{p}\) is given by \[ v _ {\mathfrak {p}} (a) = - \log | \tau a |, \] where \(\tau: K \to \mathbb{C}\) is an embedding which defines \(\mathfrak{p}\) .

Convention / notation

FC09-C03-U004 · Chapter III, §1, source L7598 · not formalized

For an arbitrary prime \(\mathfrak{p}|p\) ( \(p\) prime number or \(p = \infty\) ) we put furthermore \[ f _ {\mathfrak {p}} = \left[ \kappa (\mathfrak {p}): \kappa (p) \right], \] so that \(f_{\mathfrak{p}} = [K_{\mathfrak{p}}:\mathbb{R}]\) if \(\mathfrak{p}|\infty\) , and \[ \mathfrak {N} (\mathfrak {p}) = \left\{ \begin{array}{l l} p ^ {f _ {\mathfrak {p}}}, & \text { if } \mathfrak {p} \nmid \infty , \\ e ^ {f _ {\mathfrak {p}}}, & \text { if } \mathfrak {p} \mid \infty . \end{array} \right. \] This convention suggests that we consider e as being an infinite prime number, and the extension \(C|R\) as being unramified with inertia degree 2. We define the absolute value \(|_{p}:K\to R\) by \[ | a | _ {\mathfrak {p}} = \mathfrak {N} (\mathfrak {p}) ^ {- v _ {\mathfrak {p}} (a)} \] for \(a \neq 0\) and \(|0|_{\mathfrak{p}} = 0\) . If \(\mathfrak{p}\) is the infinite prime associated to the embedding \(\tau : K \to \mathbb{C}\) , then one finds \[ | a | _ {\mathfrak {p}} = | \tau a |, \quad \text { resp. } \quad | a | _ {\mathfrak {p}} = | \tau a | ^ {2}, \] if \(\mathfrak{p}\) is real, resp. complex. If \(L|K\) is a finite extension of \(K\) , then we denote the primes of \(L\) by \(\mathfrak{P}\) and write \(\mathfrak{P}| \mathfrak{p}\) to signify that the valuations in the class \(\mathfrak{P}\) , when restricted to \(K\) , give those of \(\mathfrak{p}\) . In the case of an infinite prime \(\mathfrak{P}\) , we define the inertia degree, resp. the ramification index, by \[ f _ {\mathfrak {P} | \mathfrak {p}} = [ L _ {\mathfrak {P}}: K _ {\mathfrak {p}} ], \quad \text { resp. } e _ {\mathfrak {P} | \mathfrak {p}} = 1. \]

Proposition (1.2)

FC09-C03-U005 · Chapter III, §1, source L7632 · not formalized

(1.2) Proposition. (i) \(\sum_{\mathfrak{P}|\mathfrak{p}}e_{\mathfrak{P}|\mathfrak{p}}f_{\mathfrak{P}|\mathfrak{p}} = \sum_{\mathfrak{P}|\mathfrak{p}}[L_{\mathfrak{P}}:K_{\mathfrak{p}}] = [L:K],\) \[ \mathfrak {N} (\mathfrak {P}) = \mathfrak {N} (\mathfrak {p}) ^ {f _ {\mathfrak {P} | \mathfrak {p}}}, \tag {ii} \] \[ \text {(iii)} v _ {\mathfrak {P}} (a) = e _ {\mathfrak {P} | \mathfrak {p}} v _ {\mathfrak {p}} (a) \quad \text { for } a \in K ^ {*}, \] \[ \left(\mathrm{iv}\right) v _ {\mathfrak {p}} \left(N _ {L _ {\mathfrak {P} | K _ {\mathfrak {p}}} (a)}\right) = f _ {\mathfrak {P} | \mathfrak {p}} v _ {\mathfrak {P}} (a) \quad \text { for } a \in L ^ {*}, \] \[ (\mathrm{v}) | a | _ {\mathfrak {P}} = \left| N _ {L _ {\mathfrak {P}} \mid K _ {\mathfrak {p}}} (a) \right| _ {\mathfrak {p}} \quad \text { for } a \in L. \]

Proposition (1.3)

FC09-C03-U006 · Chapter III, §1, source L7652 · in Mathlib

(1.3) Proposition. Given any \(a \in K^*\) , one has \(|a|_{\mathfrak{p}} = 1\) for almost all \(\mathfrak{p}\) , and \[ \prod_ {\mathfrak {p}} | a | _ {\mathfrak {p}} = 1. \]

Formalized. Mathlib/NumberTheory/NumberField/ProductFormula.lean::prod_abs_eq_one; Mathlib/NumberTheory/NumberField/Completion/FinitePlace.lean::hasFiniteMulSupport — The pinned product formula is exactly the product over normalized finite and infinite absolute values; finite places have finite multiplicative support, giving the “almost all equal 1” clause.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Convention / notation

FC09-C03-U007 · Chapter III, §1, source L7670 · in Mathlib

We denote by \(J(\mathcal{O})\) the group of fractional ideals of K, by \(P(\mathcal{O})\) the subgroup of fractional principal ideals, and by \[ P i c (\mathcal {O}) = J (\mathcal {O}) / P (\mathcal {O}) \] the ideal class group \(Cl_K\) of \(K\) .

Formalized. Mathlib/RingTheory/ClassGroup/Basic.lean::toPrincipalIdeal, def ClassGroup, ClassGroup.equiv; Mathlib/RingTheory/PicardGroup.lean::ClassGroup.equivPic — ClassGroup is the quotient of nonzero fractional ideals by principal fractional ideals, and ClassGroup.equivPic identifies it with the Picard group, exactly the source convention Pic(O)=J(O)/P(O).

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition (1.4)

FC09-C03-U008 · Chapter III, §1, source L7680 · not formalized

(1.4) Definition. A replete ideal of \(K\) is an element of the group \[ J (\overline {{\mathcal {O}}}) := J (\mathcal {O}) \times \prod_ {\mathfrak {p} | \infty} \mathbb {R} _ {+} ^ {*}, \] where \(R_{+}^{*}\) denotes the multiplicative group of positive real numbers.

Definition / construction

FC09-C03-U009 · Chapter III, §1, source L7688 · not formalized

In order to unify notation, we put, for any infinite prime \(\mathfrak{p}\) and any real number \(\nu \in \mathbb{R}\) , \[ \mathfrak {p} ^ {\nu} := e ^ {\nu} \in \mathbb {R} _ {+} ^ {*}. \] Given a system of real numbers \(\nu_{\mathfrak{p}}\) , \(\mathfrak{p}|\infty\) , let \(\prod_{\mathfrak{p}|\infty}\mathfrak{p}^{\nu_{\mathfrak{p}}}\) always denote the vector \[ \prod_ {\mathfrak {p} | \infty} \mathfrak {p} ^ {\nu_ {\mathfrak {p}}} = (\dots , e ^ {\nu_ {\mathfrak {p}}}, \dots) \in \prod_ {\mathfrak {p} | \infty} \mathbb {R} _ {+} ^ {*}, \] and not the product of the quantities \(e^{\nu_{\mathfrak{p}}}\) in \(\mathbb{R}\) . Then every replete ideal \(\mathfrak{a} \in J(\overline{\mathcal{O}})\) admits the unique product representation \[ \mathfrak {a} = \prod_ {\mathfrak {p} \nmid \infty} \mathfrak {p} ^ {\nu_ {\mathfrak {p}}} \times \prod_ {\mathfrak {p} \mid \infty} \mathfrak {p} ^ {\nu_ {\mathfrak {p}}} =: \prod_ {\mathfrak {p}} \mathfrak {p} ^ {\nu_ {\mathfrak {p}}}, \] where \(\nu_{\mathfrak{p}} \in \mathbb{Z}\) for \(\mathfrak{p} \nmid \infty\) , and \(\nu_{\mathfrak{p}} \in \mathbb{R}\) for \(\mathfrak{p} | \infty\) . Put \[ \mathfrak {a} _ {\mathrm{f}} = \prod_ {\mathfrak {p} \nmid \infty} \mathfrak {p} ^ {\nu_ {\mathfrak {p}}} \quad \text { and } \quad \mathfrak {a} _ {\infty} = \prod_ {\mathfrak {p} \mid \infty} \mathfrak {p} ^ {\nu_ {\mathfrak {p}}}, \] so that \(\mathfrak{a} = \mathfrak{a}_{\mathrm{f}} \times \mathfrak{a}_{\infty}\) . \(\mathfrak{a}_{\mathrm{f}}\) is a fractional ideal of \(K\) , and \(\mathfrak{a}_{\infty}\) is an element of \(\prod_{\mathfrak{p}|\infty} \mathbb{R}_{+}^{*}\) . At the same time, we view \(\mathfrak{a}_{\mathrm{f}}\) , resp. \(\mathfrak{a}_{\infty}\) , as replete ideals \[ \mathfrak {a} _ {\mathrm{f}} \times \prod_ {\mathfrak {p} | \infty} 1, \quad \text { resp. } (1) \times \mathfrak {a} _ {\infty}. \] Thus for all elements of \(J(\bar{\mathcal{O}})\) the decomposition \[ \mathfrak {a} = \mathfrak {a} _ {\mathrm{f}} \cdot \mathfrak {a} _ {\infty} \] applies. To \(a \in K^{*}\) we associate the replete principal ideal \[ [ a ] = \prod_ {\mathfrak {p}} \mathfrak {p} ^ {v _ {\mathfrak {p}} (a)} = (a) \times \prod_ {\mathfrak {p} | \infty} \mathfrak {p} ^ {v _ {\mathfrak {p}} (a)}. \] These replete ideals form a subgroup \(P(\overline{\mathcal{O}})\) of \(J(\overline{\mathcal{O}})\) . The factor group \[ P i c (\overline {{{\mathcal {O}}}}) = J (\overline {{{\mathcal {O}}}}) / P (\overline {{{\mathcal {O}}}}) \] is called the replete ideal class group, or replete Picard group.

Definition (1.5)

FC09-C03-U010 · Chapter III, §1, source L7738 · not formalized

(1.5) Definition. The absolute norm of a replete ideal \(\mathfrak{a} = \prod_{\mathfrak{p}} \mathfrak{p}^{\nu_{\mathfrak{p}}}\) is defined to be the positive real number \[ \mathfrak {N} (\mathfrak {a}) = \prod_ {\mathfrak {p}} \mathfrak {N} (\mathfrak {p}) ^ {\nu_ {\mathfrak {p}}}. \]

Definition / construction

FC09-C03-U011 · Chapter III, §1, source L7766 · not formalized

The relations between the replete ideals of a number field K and those of an extension field L are afforded by the two homomorphisms \[ J (\overline {{\mathcal {O}}} _ {K}) \xrightarrow [ N _ {L | K} ]{i _ {L | K}} J (\overline {{\mathcal {O}}} _ {L}), \] which are defined by \[ i _ {L | K} \left(\prod_ {\mathfrak {p}} \mathfrak {p} ^ {\nu_ {\mathfrak {p}}}\right) = \prod_ {\mathfrak {p}} \prod_ {\mathfrak {P} | \mathfrak {p}} \mathfrak {P} ^ {e _ {\mathfrak {P} | \mathfrak {p}} \nu_ {\mathfrak {p}}}, \] \[ N _ {L | K} \left(\prod_ {\mathfrak {P}} \mathfrak {P} ^ {\nu_ {\mathfrak {P}}}\right) = \prod_ {\mathfrak {p}} \prod_ {\mathfrak {P} | \mathfrak {p}} \mathfrak {p} ^ {f _ {\mathfrak {P} | \mathfrak {p}} \nu_ {\mathfrak {P}}}. \] Here the various product signs have to be read according to our convention. These homomorphisms satisfy the functoriality of proposition (1.6): \(N_{M|K} = N_{L|K} \circ N_{M|L}\) and \(i_{M|K} = i_{M|L} \circ i_{L|K}\) for a chain \(K \subseteq L \subseteq M\); \(N_{L|K}(i_{L|K}\mathfrak{a}) = \mathfrak{a}^{[L:K]}\); \(\mathfrak{N}(N_{L|K}(\mathfrak{A})) = \mathfrak{N}(\mathfrak{A})\); and, for \(L|K\) Galois with group \(G\), \(N_{L|K}(\mathfrak{P})\mathcal{O}_{L} = \prod_{\sigma \in G} \sigma\mathfrak{P}\).

Proposition (1.6)

FC09-C03-U012 · Chapter III, §1, source L7784 · not formalized

(1.6) Proposition. (i) For a chain of fields \(K \subseteq L \subseteq M\) , one has \(N_{M|K} = N_{L|K} \circ N_{M|L}\) and \(i_{M|K} = i_{M|L} \circ i_{L|K}\) . (ii) \(N_{L|K}(i_{L|K}\mathfrak{a})=\mathfrak{a}^{[L:K]}\) for \(\mathfrak{a}\in J(\overline{\mathcal{O}}_{K})\) . (iii) \(\mathfrak{N}(N_{L|K}(\mathfrak{A})) = \mathfrak{N}(\mathfrak{A})\) for \(\mathfrak{A} \in J(\bar{\mathcal{O}}_L)\) . (iv) If \(L|K\) is Galois with Galois group \(G\) , then for every prime ideal \(\mathfrak{P}\) of \(\mathcal{O}_L\) , one has \(N_{L|K}(\mathfrak{P})\mathcal{O}_L = \prod_{\sigma \in G} \sigma \mathfrak{P}\) . (v) For any replete principal ideal [a] of K, resp. L, one has \[ i _ {L \mid K} ([ a ]) = [ a ], \quad \text { resp. } N _ {L \mid K} ([ a ]) = [ N _ {L \mid K} (a) ]. \] (vi) \(N_{L|K}(\mathfrak{A}_{\mathrm{f}}) = N_{L|K}(\mathfrak{A})_{\mathrm{f}}\) is the ideal of \(K\) generated by the norms \(N_{L|K}(a)\) of all \(a \in \mathfrak{A}_{\mathrm{f}}\) .

Proposition (1.7)

FC09-C03-U013 · Chapter III, §1, source L7838 · not formalized

(1.7) Proposition. For every finite extension \(L|K\) , the following two diagrams are commutative: \[ \begin{array}{c} P i c (\overline {{\mathcal {O}}} _ {L}) \xrightarrow {\mathfrak {N}} \mathbb {R} _ {+} ^ {*} \\ i _ {L | K} \Biggl \updownarrow N _ {L | K} \qquad [ L: K ] \Biggl \updownarrow \text {id} \\ P i c (\overline {{\mathcal {O}}} _ {K}) \xrightarrow {\mathfrak {N}} \mathbb {R} _ {+} ^ {*}. \end{array} \]

Definition (1.8)

FC09-C03-U014 · Chapter III, §1, source L7858 · not formalized

(1.8) Definition. A replete divisor (or Arakelov divisor) of \(K\) is a formal sum \[ D = \sum_ {\mathfrak {p}} \nu_ {\mathfrak {p}} \mathfrak {p}, \] where \(\nu_{\mathfrak{p}} \in \mathbb{Z}\) for \(\mathfrak{p} \nmid \infty\) , \(\nu_{\mathfrak{p}} \in \mathbb{R}\) for \(\mathfrak{p} | \infty\) , and \(\nu_{\mathfrak{p}} = 0\) for almost all \(\mathfrak{p}\) .

Convention / notation

FC09-C03-U015 · Chapter III, §1, source L7866 · not formalized

The replete divisors form a group, which is denoted by \(Div(\overline{\mathcal{O}})\) . It admits a decomposition \[ D i v (\bar {\mathcal {O}}) \cong D i v (\mathcal {O}) \times \bigoplus_ {\mathfrak {p} | \infty} \mathbb {R} \mathfrak {p}. \] On the right-hand side, the second factor is endowed with the canonical topology, the first one with the discrete topology. On the product we have the product topology, which makes \(Div(\bar{\mathcal{O}})\) into a locally compact topological group.

Definition / construction

FC09-C03-U016 · Chapter III, §1, source L7880 · not formalized

The elements of the form \(\text{div}(f)\) are called replete principal divisors.

Proposition (1.9)

FC09-C03-U017 · Chapter III, §1, source L7896 · not formalized

(1.9) Proposition. The kernel of div: \(K^{*} \to Div(\overline{\mathcal{O}})\) is the group \(\mu(K)\) of roots of unity in K, and its image \(\mathcal{P}(\overline{\mathcal{O}})\) is a discrete subgroup of \(Div(\overline{\mathcal{O}})\) .

Definition (1.10)

FC09-C03-U018 · Chapter III, §1, source L7906 · not formalized

(1.10) Definition. The factor group \[ C H ^ {1} (\bar {\mathcal {O}}) = D i v (\bar {\mathcal {O}}) / \mathcal {P} (\bar {\mathcal {O}}) \] is called the replete divisor class group (or Arakelov class group) of K.

Definition / construction

FC09-C03-U019 · Chapter III, §1, source L7914 · after FC09-C01-U004, FC09-C03-U006 · not formalized

As \(\mathcal{P}(\overline{\mathcal{O}})\) is discrete in \(Div(\overline{\mathcal{O}})\) , and is therefore in particular closed, \(CH^{1}(\overline{\mathcal{O}})\) becomes a locally compact Hausdorff topological group with respect to the quotient topology. It is the correct analogue of the divisor class group of a function field (see chap. I, §14). For the latter we introduced the degree map onto the group Z; for \(CH^{1}(\overline{\mathcal{O}})\) we obtain a degree map onto the group R. It is induced by the continuous homomorphism \[ \deg : D i v (\bar {\mathcal {O}}) \longrightarrow \mathbb {R} \] which sends a replete divisor \(D = \sum_{\mathfrak{p}} \nu_{\mathfrak{p}} \mathfrak{p}\) to the real number \[ \deg (D) = \sum_ {\mathfrak {p}} \nu_ {\mathfrak {p}} \log \mathfrak {N} (\mathfrak {p}) = \log \left(\prod_ {\mathfrak {p}} \mathfrak {N} (\mathfrak {p}) ^ {\nu_ {\mathfrak {p}}}\right). \] From the product formula (1.3), we find for any replete principal divisor \(\mathrm{div}(f_i) \in \mathcal{P}(\overline{\mathcal{O}})\) that \[ \deg \left(\operatorname{div} (f)\right) = \sum_ {\mathfrak {p}} \log \mathfrak {N} (\mathfrak {p}) ^ {v _ {\mathfrak {p}} (f)} = \log \left(\prod_ {\mathfrak {p}} | f | _ {\mathfrak {p}} ^ {- 1}\right) = 0. \] Thus we obtain a well-defined continuous homomorphism \[ \deg : C H ^ {1} (\bar {\mathcal {O}}) \longrightarrow \mathbb {R}. \] The kernel \(CH^{1}(\bar{\mathcal{O}})^{0}\) of this map is made up from the unit group \(O^{*}\) and the ideal class group \(Cl_{K} \cong CH^{1}(\mathcal{O})\) of K as follows.

Proposition (1.11)

FC09-C03-U020 · Chapter III, §1, source L7940 · not formalized

(1.11) Proposition. Let \(\Gamma = \lambda (\mathcal{O}^*)\) denote the complete lattice of units in trace-zero space \(H = \{(x_{\mathfrak{p}})\in \prod_{\mathfrak{p}|\infty}\mathbb{R}\mid \sum_{\mathfrak{p}|\infty}x_{\mathfrak{p}} = 0\}\) . There is an exact sequence \[ 0 \longrightarrow H / \Gamma \longrightarrow C H ^ {1} (\bar {\mathcal {O}}) ^ {0} \longrightarrow C H ^ {1} (\mathcal {O}) \longrightarrow 0. \]

Theorem (1.12)

FC09-C03-U021 · Chapter III, §1, source L7966 · not formalized

(1.12) Theorem. The group \(CH^{1}(\overline{\mathcal{O}})^{0}\) is compact.

Definition / construction

FC09-C03-U022 · Chapter III, §1, source L7976 · after FC09-C01-U118, FC09-C03-U017 · not formalized

The correspondence between replete ideals and replete divisors is given by the two mutually inverse mappings \[ \begin{array}{c c} \operatorname{div}: J (\overline {{\mathcal {O}}}) \longrightarrow D i v (\overline {{\mathcal {O}}}), & \quad \operatorname{div} (\prod_ {\mathfrak {p}} \mathfrak {p} ^ {\nu_ {\mathfrak {p}}}) = \sum_ {\mathfrak {p}} - \nu_ {\mathfrak {p}} \mathfrak {p}, \\ D i v (\overline {{\mathcal {O}}}) \longrightarrow J (\overline {{\mathcal {O}}}), & \quad \sum_ {\mathfrak {p}} \nu_ {\mathfrak {p}} \mathfrak {p} \longmapsto \prod_ {\mathfrak {p}} \mathfrak {p} ^ {- \nu_ {\mathfrak {p}}}. \end{array} \] These are topological isomorphisms once we equip \[ J (\overline {{\mathcal {O}}}) = J (\mathcal {O}) \times \prod_ {\mathfrak {p} | \infty} \mathbb {R} _ {+} ^ {*} \] with the product topology of the discrete topology on \(J(\mathcal{O})\) and the canonical topology on \(\prod_{\mathfrak{p}|\infty}\mathbb{R}_{+}^{*}\) . The image of a divisor \(D = \sum_{\mathfrak{p}}\nu_{\mathfrak{p}}\mathfrak{p}\) is also written as \[ \mathcal {O} (D) = \prod_ {\mathfrak {p}} \mathfrak {p} ^ {- \nu_ {\mathfrak {p}}}. \] The minus sign here is motivated by classical usage in function theory. Replete principal ideals correspond to replete principal divisors in such a way that \(P(\bar{\mathcal{O}})\) becomes a discrete subgroup of \(J(\bar{\mathcal{O}})\) by (1.9), and \(Pic(\bar{\mathcal{O}}) = J(\bar{\mathcal{O}})/P(\bar{\mathcal{O}})\) is a locally compact Hausdorff topological group. We obtain the following extension of chap. I, (12.14).

Proposition (1.13)

FC09-C03-U023 · Chapter III, §1, source L7996 · not formalized

(1.13) Proposition. The mapping div : \(J(\bar{\mathcal{O}}) \stackrel{\sim}{\longrightarrow} Div(\bar{\mathcal{O}})\) induces a topological isomorphism \[ \operatorname{div}: P i c (\bar {\mathcal {O}}) \stackrel {{\sim}} {{\longrightarrow}} C H ^ {1} (\bar {\mathcal {O}}). \]

Corollary (1.14)

FC09-C03-U024 · Chapter III, §1, source L8016 · not formalized

(1.14) Corollary. The group \[ P i c (\bar {\mathcal {O}}) ^ {0} = \left\{\left[ a \right] \in P i c (\bar {\mathcal {O}}) \mid \mathfrak {N} (a) = 1 \right\} \] is compact.

Definition / construction

FC09-C03-U025 · Chapter III, §1, source L8024 · not formalized

There, on an algebraic \(\mathbb{Z}\) -scheme \(X\) , one studies on the one hand the totality of all vector bundles, and on the other, that of all irreducible subschemes of \(X\) . From the first, one constructs a series of groups \(K_{i}(X)\) which constitute the subject of algebraic \(K\) -theory. From the second is constructed a series of groups \(CH^{i}(X)\) , the subject of Chow theory. Vector bundles are by definition locally free \(\mathcal{O}_X\) -modules. In the special case \(X = \operatorname{Spec}(\mathcal{O})\) this includes the fractional ideals. The irreducible subschemes and their formal linear combinations, i.e., the cycles of \(X\) , are to be considered as generalizations of the primes and divisors. The isomorphism between divisor class group and ideal class group extends to the general setting as a homomorphic relation between the groups \(CH^{i}(X)\) and \(K_{i}(X)\) . Thus the initial controversy has been resolved into a seminal mathematical theory (for further reading, see [13]).

Definition (2.1)

FC09-C03-U026 · Chapter III, §2, source L8100 · in Mathlib

(2.1) Definition. The fractional ideal \[ \mathfrak {C} _ {\mathcal {O} | \mathcal {O}} = ^ {*} \mathcal {O} = \left\{x \in L \mid T r (x \mathcal {O}) \subseteq \mathcal {O} \right\} \] is called Dedekind’s complementary module, or the inverse different. Its inverse, \[ \mathfrak {D} _ {\mathcal {O} | \mathcal {O}} = \mathfrak {C} _ {\mathcal {O} | \mathcal {O}} ^ {- 1}, \] is called the different of \(\mathcal{O}|\mathcal{O}\) .

Formalized. Mathlib/RingTheory/DedekindDomain/Different.lean::Submodule.traceDual, FractionalIdeal.dual, def differentIdeal, coeIdeal_differentIdeal — traceDual/FractionalIdeal.dual is the complementary module {x | Tr(xO)⊆A}, and differentIdeal is its inverse, matching Definition 2.1.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Convention / notation

FC09-C03-U027 · Chapter III, §2, source L8114 · in Mathlib

As \(\mathfrak{C}_{\mathcal{O}|\mathcal{O}} \supseteq \mathcal{O}\) , the ideal \(\mathfrak{D}_{\mathcal{O}|\mathcal{O}} \subseteq \mathcal{O}\) is actually an integral ideal of \(L\) . We will frequently denote it by \(\mathfrak{D}_{L|K}\) , provided the intended subrings \(\mathcal{O}, \mathcal{O}\) are evident from the context. In the same way, we write \(\mathfrak{C}_{L|K}\) instead of \(\mathfrak{C}_{\mathcal{O}|\mathcal{O}}\) . The different behaves in the following manner under change of rings \(\mathcal{O}\) and \(\mathcal{O}\) .

Formalized. Mathlib/RingTheory/DedekindDomain/Different.lean::one_le_dual_one, def differentIdeal, coeIdeal_differentIdeal — one_le_dual_one is O⊆C and differentIdeal is defined as an Ideal of the integral closure, so its inverse trace dual is represented by an integral ideal exactly as in the source convention.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Proposition (2.2)

FC09-C03-U028 · Chapter III, §2, source L8116 · not formalized

(2.2) Proposition. (i) For a tower of fields \(K \subseteq L \subseteq M\) , one has \(\mathfrak{D}_{M|K} = \mathfrak{D}_{M|L}\mathfrak{D}_{L|K}\) . (ii) For any multiplicative subset \(S\) of \(\mathcal{O}\) , one has \(\mathfrak{D}_{S^{-1}\mathcal{O}|S^{-1}\mathcal{O}} = S^{-1}\mathfrak{D}_{\mathcal{O}|\mathcal{O}}\) . (iii) If \(\mathfrak{P}|\mathfrak{p}\) are prime ideals of \(\mathcal{O}\) , resp. \(\mathcal{O}\) , and \(\mathcal{O}_{\mathfrak{P}}|\mathcal{O}_{\mathfrak{p}}\) are the associated completions, then \[ \mathfrak {D} _ {\mathcal {O} | \mathcal {O}} \mathcal {O} _ {\mathfrak {P}} = \mathfrak {D} _ {\mathcal {O} _ {\mathfrak {P}} | \mathcal {O} _ {\mathfrak {p}}}. \]

Not formalized. Pinned/current Mathlib has substantial different, discriminant, Kähler-differential, unramified, and Minkowski infrastructure, but this full source row contains an additional relative-ideal, localization/completion, annihilator, ramification-exponent, or all-embeddings measure clause not closed by a checked compatible route.

Corollary (2.3)

FC09-C03-U029 · Chapter III, §2, source L8174 · not formalized

(2.3) Corollary. \(\mathfrak{D} = \prod_{\mathfrak{P}}\mathfrak{D}_{\mathfrak{P}}\)

Definition / construction

FC09-C03-U030 · Chapter III, §2, source L8176 · not formalized

The name “different” is explained by the following explicit description, which was Dedekind’s original way to define it. Let \(\alpha \in O\) and let \(f(X) \in \mathcal{O}[X]\) be the minimal polynomial of \(\alpha\) . We define the different of the element \(\alpha\) by \[ \delta_ {L | K} (\alpha) = \left\{ \begin{array}{l l} f ^ {\prime} (\alpha) & \text {if} L = K (\alpha), \\ 0 & \text {if} L \neq K (\alpha). \end{array} \right. \] In the special case where \(\mathcal{O} = \mathcal{O}[\alpha]\) we then obtain:

Proposition (2.4)

FC09-C03-U031 · Chapter III, §2, source L8184 · in Mathlib

(2.4) Proposition. If \(O = \mathcal{O}[\alpha]\) , then the different is the principal ideal \[ \mathfrak {D} _ {L | K} = \left(\delta_ {L | K} (\alpha)\right). \]

Formalized. Mathlib/RingTheory/DedekindDomain/Different.lean::conductor_mul_differentIdeal; Mathlib/RingTheory/Conductor.lean::conductor_eq_top_of_adjoin_eq_top, conductor_eq_top_iff_adjoin_eq_top — conductor_mul_differentIdeal gives c(α)D=(f’(α)); under O=A[α], the conductor is the unit ideal by conductor_eq_top_of_adjoin_eq_top, yielding D=(f’(α)).

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Theorem (2.5)

FC09-C03-U032 · Chapter III, §2, source L8248 · not formalized

(2.5) Theorem. The different \(D_{L|K}\) is the ideal generated by all differents of elements \(\delta_{L|K}(\alpha)\) for \(\alpha \in O\) .

Theorem (2.6)

FC09-C03-U033 · Chapter III, §2, source L8302 · not formalized

(2.6) Theorem. A prime ideal \(\mathfrak{P}\) of \(L\) is ramified over \(K\) if and only if \(\mathfrak{P}|\mathfrak{D}_{L|K}\) . Let \(\mathfrak{P}^s\) be the maximal power of \(\mathfrak{P}\) dividing \(\mathfrak{D}_{L|K}\) , and let \(e\) be the ramification index of \(\mathfrak{P}\) over \(K\) . Then one has \[ s = e - 1, \quad \text { if } \mathfrak {P} \text { is tamely ramified, } \] \[ e \leq s \leq e - 1 + v _ {\mathfrak {P}} (e), \quad i f \mathfrak {P} i s w i l d l y r a m i f i e d. \]

Definition / construction

FC09-C03-U034 · Chapter III, §2, source L8342 · in Mathlib

The geometric significance of the different, and thus also the way it fits into higher dimensional algebraic geometry, is brought out by the following characterization, which is due to \(E. K\ddot{A}HLER\) . For an arbitrary extension \(B|A\) of commutative rings, consider the homomorphism \[ \mu : B \otimes_ {A} B \longrightarrow B, \quad x \otimes y \longmapsto x y, \] whose kernel we denote by I. Then \[ \Omega_ {B | A} ^ {1} := I / I ^ {2} = I \otimes_ {B \otimes B} B \] is a \(B \otimes B\) -module, and hence in particular also a B-module, via the embedding \(B \to B \otimes B\) , \(b \mapsto b \otimes 1\) . It is called the module of differentials of \(B|A\) , and its elements are called Kähler differentials. If we put \[ d x = x \otimes 1 - 1 \otimes x \bmod I ^ {2}, \] then we obtain a mapping \[ d: B \longrightarrow \Omega_ {B | A} ^ {1} \] satisfying \[ d (x y) = x d y + y d x, \] \[ d a = 0 \quad \text { for } \quad a \in A. \]

Formalized. Mathlib/RingTheory/Kaehler/Basic.lean::KaehlerDifferential.ideal, def KaehlerDifferential, KaehlerDifferential.D, KaehlerDifferential.D_apply — Mathlib defines Ω[B/A] as the cotangent module I/I² for the multiplication kernel. Its universal derivation uses 1⊗x−x⊗1, the negative of Neukirch’s displayed convention x⊗1−1⊗x; this harmless sign change gives the same Kähler module and derivation theory.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition / construction

FC09-C03-U035 · Chapter III, §2, source L8376 · in Mathlib

Such a map is called a derivation of \(B|A\) . One can show that d is universal among all derivations of \(B|A\) with values in B-modules. \(\Omega_{B|A}^{1}\) consists of the linear combinations \(\sum y_{i} dx_{i}\) . The link with the different is now this.

Formalized. Mathlib/RingTheory/Kaehler/Basic.lean::KaehlerDifferential.span_range_derivation, Derivation.liftKaehlerDifferential, Derivation.liftKaehlerDifferential_unique, KaehlerDifferential.linearMapEquivDerivation — linearMapEquivDerivation is the universal property Hom_B(Ω,M)≃Der_A(B,M), and span_range_derivation says Ω is generated by the dx, exactly the source unit.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Proposition (2.7)

FC09-C03-U036 · Chapter III, §2, source L8378 · not formalized

(2.7) Proposition. The different \(\mathfrak{D}_{\mathcal{O}|\circ}\) is the annihilator of the \(\mathcal{O}\) -module \(\Omega_{\mathcal{O}|\circ}^{1}\) , i.e., \[ \mathfrak {D} _ {\mathcal {O} | \mathcal {O}} = \left\{x \in \mathcal {O} \mid x d y = 0 \quad \text {for all} \quad y \in \mathcal {O} \right\}. \]

Definition / construction

FC09-C03-U037 · Chapter III, §2, source L8386 · not formalized

A most intimate connection holds between the different and the discriminant of \(O|O\) . The latter is defined as follows.

Definition (2.8)

FC09-C03-U038 · Chapter III, §2, source L8388 · not formalized

(2.8) Definition. The discriminant \(d_{O|O}\) is the ideal of O which is generated by the discriminants \(d(\alpha_{1},\ldots,\alpha_{n})\) of all the bases \(\alpha_{1},\ldots,\alpha_{n}\) of L|K which are contained in O.

Theorem (2.9)

FC09-C03-U039 · Chapter III, §2, source L8392 · not formalized

(2.9) Theorem. The following relation exists between the discriminant and the different: \[ \mathfrak {d} _ {L | K} = N _ {L | K} (\mathfrak {D} _ {L | K}). \]

Corollary (2.10)

FC09-C03-U040 · Chapter III, §2, source L8412 · not formalized

(2.10) Corollary. For a tower of fields \(K \subseteq L \subseteq M\) , one has \[ \mathfrak {d} _ {M | K} = \mathfrak {d} _ {L | K} ^ {[ M: L ]} N _ {L | K} (\mathfrak {d} _ {M | L}). \]

Corollary (2.11)

FC09-C03-U041 · Chapter III, §2, source L8426 · not formalized

(2.11) Corollary. \(\mathfrak{d} = \prod_{\mathfrak{P}}\mathfrak{d}_{\mathfrak{P}}\)

Definition / construction

FC09-C03-U042 · Chapter III, §2, source L8428 · not formalized

The extension \(L|K\) is called unramified if all prime ideals \(\mathfrak{p}\) of \(K\) are unramified. This amounts to requiring that all primes of \(K\) be unramified. In fact, the infinite primes are always to be regarded as unramified because \(e_{\mathfrak{P}| \mathfrak{p}} = 1\) .

Corollary (2.12)

FC09-C03-U043 · Chapter III, §2, source L8430 · not formalized

(2.12) Corollary. A prime ideal \(\mathfrak{p}\) of \(K\) is ramified in \(L\) if and only if \(\mathfrak{p}|\mathfrak{d}\) . In particular, the extension \(L|K\) is unramified if the discriminant \(\mathfrak{d} = (1)\) .

Theorem (2.13)

FC09-C03-U044 · Chapter III, §2, source L8434 · not formalized

(2.13) Theorem. Let K be an algebraic number field and let S be a finite set of primes of K. Then there exist only finitely many extensions \(L|K\) of given degree n which are unramified outside of S.

Proposition (2.14)

FC09-C03-U045 · Chapter III, §2, source L8466 · in Mathlib

(2.14) Proposition. The discriminant of an algebraic number field \(K\) of degree \(n\) satisfies \[ \left| d _ {K} \right| ^ {1 / 2} \geq \frac {n ^ {n}}{n !} \left(\frac {\pi}{4}\right) ^ {n / 2}. \]

Formalized. Mathlib/NumberTheory/NumberField/Discriminant/Basic.lean::abs_discr_ge'; Mathlib/NumberTheory/NumberField/InfinitePlace/Basic.lean::card_add_two_mul_card_eq_rank — abs_discr_ge' proves the stronger bound |d_K| ≥ n^(2n)/((4/π)(2s)(n!)²). Since r+2s=n, 2s≤n; taking square roots gives Neukirch’s stated √|d_K| ≥ n^n/n!·(π/4)(n/2).

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Lemma (2.15)

FC09-C03-U046 · Chapter III, §2, source L8510 · not formalized

(2.15) Lemma. In Minkowski space \(K_{\mathbb{R}} = \left[\prod_{\tau} \mathbb{C}\right]^+\) , the domain \[ X _ {t} = \left\{\left(z _ {\tau}\right) \in K _ {\mathbb {R}} \mid \sum_ {\tau} | z _ {\tau} | < t \right\} \] has volume \[ \operatorname{vol} (X _ {t}) = 2 ^ {r} \pi^ {s} \frac {t ^ {n}}{n !} \cdot \]

Hermite’s Theorem (2.16)

FC09-C03-U047 · Chapter III, §2, source L8608 · in Mathlib

(2.16) Hermite’s Theorem. There exist only finitely many number fields with bounded discriminant.

Formalized. Mathlib/NumberTheory/NumberField/Discriminant/Basic.lean::NumberField.finite_of_discr_bdd — The pinned Hermite theorem gives finiteness of number fields of bounded discriminant inside a fixed algebraic closure; every number field embeds there, yielding the source finiteness up to isomorphism.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Theorem (2.18)

FC09-C03-U048 · Chapter III, §2, source L8620 · in Mathlib

(2.18) Theorem. The field \(\mathbb{Q}\) does not admit any unramified extensions.

Formalized. Mathlib/NumberTheory/NumberField/ExistsRamified.lean::NumberField.finrank_eq_one_of_unramified, bijective_algebraMap_int_of_finite_of_unramified — A number field whose ring of integers is unramified over ℤ has degree one (indeed the integer algebra map is bijective), so there is no nontrivial unramified extension of ℚ in Neukirch’s convention.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition / construction

FC09-C03-U049 · Chapter III, §2, source L8622 · not formalized

If \(\mathfrak{p}\) is a prime ideal of \(K\) , then for any such curve \(X\) , one may define the “reduction mod \(\mathfrak{p}\)”. This is a curve defined over the residue class field of \(\mathfrak{p}\) . One says that \(X\) has good reduction at the prime \(\mathfrak{p}\) if its reduction mod \(\mathfrak{p}\) is again a smooth curve.

Definition / construction

FC09-C03-U050 · Chapter III, §3, source L8710 · not formalized

In order to mimic this state of affairs in number theory, let us recall the explanations of chap. I, §14 and chap. III, §1. We endow the places p of an algebraic number field K with the rôle of points of a space X which should be conceived of as the analogue of a compact Riemann surface. The elements \(f \in K^{*}\) will be given the rôle of “meromorphic functions” on this space X. The order of the pole, resp. zero of f at the point \(p \in X\) , for \(p \nmid \infty\) , is defined to be the integer \(v_{\mathfrak{p}}(f)\) , and for \(p|_{\infty}\) it is the real number \(v_{\mathfrak{p}}(f) = -\log |\tau f|\) . In this way we associate to each \(f \in K^{*}\) the replete divisor \[ \operatorname{div} (f) = \sum_ {\mathfrak {p}} v _ {\mathfrak {p}} (f) \mathfrak {p} \in D i v (\bar {\mathcal {O}}). \] More precisely, for a given divisor \(D = \sum_{\mathfrak{p}} \nu_{\mathfrak{p}} \mathfrak{p}\) , we are interested in the replete ideal \[ \mathcal {O} (D) = \prod_ {\mathfrak {p}} \mathfrak {p} ^ {- \nu_ {\mathfrak {p}}} \] and the set \[ \begin{array}{r l} H ^ {0} (\mathcal {O} (D)) & = \left\{f \in K ^ {*} \big | \operatorname{div} (f) \geq - D \right\} \\ & = \left\{f \in \mathcal {O} (D) _ {\mathrm{f}} \big | 0 \neq | f | _ {\mathfrak {p}} \leq \mathfrak {N} (\mathfrak {p}) ^ {\nu_ {\mathfrak {p}}} \text {for} \mathfrak {p} | \infty \right\}, \end{array} \] where the relation \(D' \geq D\) between divisors \(D' = \sum_{p} v_{p}' p\) and \(D = \sum_{p} v_{p} p\) is simply defined to mean \(v_{p}' \geq v_{p}\) for all p. Note that \(H^{0}(\mathcal{O}(D))\) is no longer a vector space. An analogue of \(H^{1}(X, \mathcal{O}(D))\) is completely missing. Instead of attacking directly the problem of measuring the size of \(H^{0}(\mathcal{O}(D))\) , we proceed as in the function-theoretic model by looking at the “Euler-Poincaré characteristic” of the replete ideal \(\mathcal{O}(D)\) . Before defining this, we want to establish the relation between the Minkowski space \(K_{R} = \left[\prod_{\tau} C\right]^{+}\) , \(\tau \in \operatorname{Hom}(K, \mathbb{C})\) , and the product \(\prod_{p| \infty} K_{p}\) . The reader will allow us to explain this simple situation in the following sketch.

Not formalized. Pinned/current Mathlib has ordinary ideals, cohomological primitives, trace duality, and number-field lattice theory, but no replete/Arakelov divisor or arithmetic Riemann–Roch package closes this source unit.

Definition / construction

FC09-C03-U051 · Chapter III, §3, source L8730 · after FC09-C02-U099 · not formalized

We have the correspondences \[ \rho \colon K \to \mathbb {R} \quad \longmapsto \quad \mathfrak {p} \quad \text { real prime }, \rho = \rho_ {\mathfrak {p}}: K _ {\mathfrak {p}} \stackrel {{\sim}} {{\longrightarrow}} \mathbb {R}, \] \(\sigma, \overline{\sigma}: K \to \mathbb{C} \quad \longmapsto \quad \mathfrak{p} \quad \text{complex prime}, \sigma = \sigma_{\mathfrak{p}}: K_{\mathfrak{p}} \stackrel{\sim}{\longrightarrow} \mathbb{C}\) . There are the following isomorphisms \[ K \otimes_ {\mathbb {Q}} \mathbb {R} \stackrel {{\sim}} {{\longrightarrow}} K _ {\mathbb {R}}, \quad a \otimes x \longmapsto ((\tau a) x) _ {\tau}, \] \[ K \otimes_ {\mathbb {Q}} \mathbb {R} \stackrel {{\sim}} {{\longrightarrow}} \prod_ {\mathfrak {p} | \infty} K _ {\mathfrak {p}}, \quad a \otimes x \longmapsto ((\tau_ {\mathfrak {p}} a) x) _ {\mathfrak {p} | \infty}, \] \(\tau_{p}\) being the canonical embedding \(K \rightarrow K_{p}\) (see chap. II, (8.3)). They fit into the commutative diagram \[ \begin{array}{r c l r c l} K \otimes \mathbb {R} & \cong & K _ {\mathbb {R}} & = & \prod_ {\rho} \mathbb {R} & \times & \prod_ {\sigma} [ \mathbb {C} \times \mathbb {C} ] ^ {+} \\ \Big \| & & \uparrow & & \uparrow \Pi_ {\rho_ {\mathfrak {p}}} & & \uparrow \Pi_ {[ \sigma_ {\mathfrak {p}} \times \overline {{\sigma}} _ {\mathfrak {p}} ]} \\ K \otimes \mathbb {R} & \cong & \prod_ {\mathfrak {p} | \infty} K _ {\mathfrak {p}}. = & & \prod_ {\mathfrak {p} \text {real}} K _ {\mathfrak {p}} & \times & \prod_ {\mathfrak {p} \text {complex}}, \end{array} \] where the arrow on the right is given by \(a \mapsto (\sigma a, \overline{\sigma} a)\) . Via this isomorphism, we identify \(K_{\mathbb{R}}\) with \(\prod_{\mathfrak{p}|\infty} K_{\mathfrak{p}}\) : \[ K _ {\mathbb {R}} = \prod_ {\mathfrak {p} | \infty} K _ {\mathfrak {p}}. \] The scalar product \(\langle x, y \rangle = \sum_{\tau} x_{\tau} \bar{y}_{\tau}\) on \(K_{\mathbb{R}}\) is then transformed into \[ \langle x, y \rangle = \sum_ {\mathfrak {p} \text {real}} x _ {\mathfrak {p}} y _ {\mathfrak {p}} + \sum_ {\mathfrak {p} \text {complex}} (x _ {\mathfrak {p}} \bar {y} _ {\mathfrak {p}} + \bar {x} _ {\mathfrak {p}} y _ {\mathfrak {p}}). \] The Haar measure \(\mu\) on \(K_{\mathbb{R}}\) which is determined by \(\langle x, y \rangle\) becomes the product measure \[ \mu = \prod_ {\mathfrak {p} | \infty} \mu_ {\mathfrak {p}}, \] where \[ \begin{array}{l} \mu_ {\mathfrak {p}} = \text { Lebesgue measure on } K _ {\mathfrak {p}} = \mathbb {R}, \text { if } \mathfrak {p} \text { real }, \\ \mu_ {\mathfrak {p}} = 2 \text { Lebesgue measure on } K _ {\mathfrak {p}} = \mathbb {C}, \text { if } \mathfrak {p} \text { complex }. \end{array} \] Indeed, the system \(1 / \sqrt{2}\) , \(i / \sqrt{2}\) is an orthonormal basis with respect to the scalar product \(x\overline{y} + \overline{x}y\) on \(K_{\mathfrak{p}} = \mathbb{C}\) . Hence the square \(Q = \{z = x + iy \mid 0 \leq x, y \leq 1 / \sqrt{2}\}\) has volume \(\mu_{\mathfrak{p}}(Q) = 1\) , but Lebesgue volume \(1/2\) . Finally, the logarithm map \[ \ell : \left[ \prod_ {\tau} \mathbb {C} ^ {*} \right] ^ {+} \longrightarrow \left[ \prod_ {\tau} \mathbb {R} \right] ^ {+}, \quad x \longmapsto (\log | x _ {\tau} |) _ {\tau} \] studied in Minkowski theory is transformed into the mapping \[ \ell : \prod_ {\mathfrak {p} | \infty} K _ {\mathfrak {p}} ^ {*} \longrightarrow \prod_ {\mathfrak {p} | \infty} \mathbb {R}, \quad x \longmapsto \left(\log | x _ {\mathfrak {p}} | _ {\mathfrak {p}}\right), \] for one has the commutative diagram \[ \begin{array}{c c c} K _ {\mathbb {R}} ^ {*} & \xrightarrow {\ell} & [ \prod_ {\tau} \mathbb {R} ] ^ {+} \\ \Big \downarrow & & \Big \downarrow \\ \prod_ {\mathfrak {p} | \infty} K _ {\mathfrak {p}} ^ {*} & \xrightarrow {\ell} & \prod_ {\mathfrak {p} | \infty} \mathbb {R}, \end{array} \] where the arrow on the right, \[ \left[ \prod_ {\tau} \mathbb {R} \right] ^ {+} = \prod_ {\rho} \mathbb {R} \times \prod_ {\sigma} [ \mathbb {R} \times \mathbb {R} ] ^ {+} \longrightarrow \prod_ {\mathfrak {p} | \infty} \mathbb {R}, \] is defined by \(x \mapsto x\) for \(\rho \leftrightarrow p\) , and by \((x, x) \mapsto 2x\) for \(\sigma \leftrightarrow p\) . This isomorphism takes the trace map \(x \mapsto \sum_{\tau} x_{\tau}\) on \(\left[\prod_{\tau} R\right]^{+}\) into the trace map \(x \mapsto \sum_{p \mid \infty} x_{p}\) on \(\prod_{p \mid \infty} R\) , and hence the trace-zero space \(H = \left\{ x \in \left[\prod_{\tau} R\right]^+ \mid \sum_{\tau} x_{\tau} = 0 \right\}\) into the trace-zero space \[ H = \left\{x \in \prod_ {\mathfrak {p} | \infty} \mathbb {R} \mid \sum_ {\mathfrak {p} | \infty} x _ {\mathfrak {p}} = 0 \right\}. \] In this way we have translated all necessary invariants of the Minkowski space \(K_{R}\) to the product \(\prod_{p|\infty} K_{p}\) .

Definition / construction

FC09-C03-U052 · Chapter III, §3, source L8812 · not formalized

To a given replete ideal \[ \mathfrak {a} = \mathfrak {a} _ {\mathrm{f}} \cdot \mathfrak {a} _ {\infty} = \prod_ {\mathfrak {p} \nmid \infty} \mathfrak {p} ^ {\nu_ {\mathfrak {p}}} \times \prod_ {\mathfrak {p} \mid \infty} \mathfrak {p} ^ {\nu_ {\mathfrak {p}}} \] we now associate the following complete lattice \(ja\) in \(K_{\mathbb{R}}\) . The fractional ideal \(\mathfrak{a}_{\mathrm{f}} \subseteq K\) is mapped by the embedding \(j: K \to K_{\mathbb{R}}\) onto a complete lattice \(j\mathfrak{a}_{\mathrm{f}}\) of \(K_{\mathbb{R}} = \prod_{\mathfrak{p}|\infty}K_{\mathfrak{p}}\) . By componentwise multiplication, \(\mathfrak{a}_{\infty} = \prod_{\mathfrak{p}|\infty}\mathfrak{p}^{\nu_{\mathfrak{p}}} = (\dots ,e^{\nu_{\mathfrak{p}}},\dots)_{\mathfrak{p}|\infty}\) yields an isomorphism \[ \mathfrak {a} _ {\infty}: K _ {\mathbb {R}} \to K _ {\mathbb {R}}, (x _ {\mathfrak {p}}) _ {\mathfrak {p} | \infty} \mapsto (e ^ {\nu_ {\mathfrak {p}}} x _ {\mathfrak {p}}) _ {\mathfrak {p} | \infty}, \] with determinant \[ \det \left(a _ {\infty}\right) = \prod_ {p \mid \infty} e ^ {\nu_ {p} f _ {p}} = \prod_ {p \mid \infty} \mathfrak {N} (p) ^ {\nu_ {p}} = \mathfrak {N} \left(a _ {\infty}\right).\tag{*} \] The image of the lattice \(ja_{f}\) under this map is a complete lattice \[ j \mathfrak {a} := \mathfrak {a} _ {\infty} j \mathfrak {a} _ {\mathrm{f}}. \] Let \(\text{vol}(\mathfrak{a})\) denote the volume of a fundamental mesh of \(j\mathfrak{a}\) with respect to the canonical measure. By (*), we then have \[ \operatorname{vol} (a) = \mathfrak {N} (a _ {\infty}) \operatorname{vol} (a _ {f}). \]

Definition (3.1)

FC09-C03-U053 · Chapter III, §3, source L8842 · not formalized

(3.1) Definition. If \(\mathfrak{a}\) is a replete ideal of \(K\) , then the real number \[ \chi (\mathfrak {a}) = - \log \operatorname{vol} (\mathfrak {a}) \] will be called the Euler-Minkowski characteristic of a.

Proposition (3.2)

FC09-C03-U054 · Chapter III, §3, source L8852 · not formalized

(3.2) Proposition. The Euler-Minkowski characteristic \(\chi(\mathfrak{a})\) only depends on the class of \(\mathfrak{a}\) in \(Pic(\overline{\mathcal{O}}) = J(\overline{\mathcal{O}})/P(\overline{\mathcal{O}})\) .

Proposition (3.3)

FC09-C03-U055 · Chapter III, §3, source L8882 · not formalized

(3.3) Proposition. For every replete ideal \(\mathfrak{a}\) of \(K\) one has \[ \operatorname{vol} (\mathfrak {a}) = \sqrt {| d _ {K} |} \mathfrak {N} (\mathfrak {a}). \]

Proposition (3.4)

FC09-C03-U056 · Chapter III, §3, source L8914 · not formalized

(3.4) Proposition. For every replete ideal of K we have the formula \[ \chi (\mathfrak {a}) = \deg (\mathfrak {a}) + \chi (\mathcal {O}). \]

Definition / construction

FC09-C03-U057 · Chapter III, §3, source L8926 · not formalized

There is no immediate analogue of \(H^{1}(X,\mathcal{O}_{X})\) in arithmetic. However, there is an analogue of \(H^{0}(X,\mathcal{O}_{X})\) . For each replete ideal \(a=\prod_{p}p^{\nu_{p}}\) of the number field K, we define \[ H ^ {0} (\mathfrak {a}) = \left\{f \in K ^ {*} \mid v _ {\mathfrak {p}} (f) \geq v _ {\mathfrak {p}} \text { for all } \mathfrak {p} \right\}. \] This is a finite set because \(jH^0(\mathfrak{a})\) lies in the part of the lattice \(j\mathfrak{a}_{\mathfrak{f}} \subseteq K_{\mathbb{R}}\) which is bounded by the conditions \(|f|_{\mathfrak{p}} \leq e^{-\nu_{\mathfrak{p}}f_{\mathfrak{p}}}\) , \(\mathfrak{p}|\infty\) . As the analogue of the dimension, we put \(\ell(\mathfrak{a}) = 0\) if \(H^0(\mathfrak{a}) = \emptyset\) , and in all other cases \[ \ell (\mathfrak {a}) := \log \frac {\# H ^ {0} (\mathfrak {a})}{\operatorname{vol} (W)}, \] where the normalizing factor \(\operatorname{vol}(W)\) is the volume of the set \[ W = \left\{\left(z _ {\tau}\right) \in K _ {\mathbb {R}} = \left[ \prod_ {\tau} \mathbb {C} \right] ^ {+} \mid | z _ {\tau} | \leq 1 \right\}. \] This volume is given explicitly by \[ \operatorname{vol}(W) = 2^{r}(2\pi)^{s}, \] where \(r\), resp. \(s\), is the number of real, resp. complex, primes of \(K\).

Definition (3.5)

FC09-C03-U058 · Chapter III, §3, source L8958 · not formalized

(3.5) Definition. The genus of a number field \(K\) is defined to be the real number \(\| x(K) - \sqrt{1 - x}\) \[ g = \ell (\mathcal {O}) - \chi (\mathcal {O}) = \log \frac {\# \mu (K) \sqrt {| d _ {K} |}}{2 ^ {r} (2 \pi) ^ {s}}. \]

Proposition (3.6)

FC09-C03-U059 · Chapter III, §3, source L8966 · not formalized

(3.6) Proposition. For every replete ideal \(\mathfrak{a}\) of \(K\) one has \[ \chi (\mathfrak {a}) = \deg (\mathfrak {a}) + \ell (\mathcal {O}) - g. \]

Theorem (3.7)

FC09-C03-U060 · Chapter III, §3, source L8980 · not formalized

(3.7) Theorem (S. LANG). For replete ideals \(\mathfrak{a} = \prod_{\mathfrak{p}} \mathfrak{p}^{\nu_{\mathfrak{p}}} \in J(\overline{\mathcal{O}})\) , one has \[ \# H ^ {0} (\mathfrak {a} ^ {- 1}) = \frac {2 ^ {r} (2 \pi) ^ {s}}{\sqrt {| d _ {K} |}} \mathfrak {N} (\mathfrak {a}) + O \left(\mathfrak {N} (\mathfrak {a}) ^ {1 - \frac {1}{n}}\right) \] if \(\mathfrak{N}(\mathfrak{a})\to \infty\) . Here, as usual, \(O(t)\) denotes a function such that \(O(t) / t\) remains bounded as \(t\to \infty\) .

Lemma (3.8)

FC09-C03-U061 · Chapter III, §3, source L8990 · not formalized

(3.8) Lemma. Let \(\mathfrak{a}_1, \ldots, \mathfrak{a}_h\) be fractional ideals representing the classes of the finite ideal class group \(Pic(\mathcal{O})\) . Let \(c\) be a positive constant and \[ \mathfrak {A} _ {i} = \left\{\mathfrak {a} = \prod_ {\mathfrak {p}} \mathfrak {p} ^ {\nu_ {\mathfrak {p}}} \mid \mathfrak {a} _ {\mathrm{f}} = \mathfrak {a} _ {i}, \mathfrak {N} (\mathfrak {p}) ^ {\nu_ {\mathfrak {p}}} \leq c \mathfrak {N} (\mathfrak {a}) ^ {f _ {\mathfrak {p}} / n} f o r \mathfrak {p} | \infty \right\}. \] Then the constant \(c\) can be chosen in such a way that \[ J (\overline {{\mathcal {O}}}) = \bigcup_ {i = 1} ^ {h} \mathfrak {A} _ {i} P (\overline {{\mathcal {O}}}). \]

Definition / construction

FC09-C03-U062 · Chapter III, §3, source L9168 · not formalized

The number \[ i(D) = \ell(D) - \chi(D) \] is called the index of specialty of \(D\); with it one obtains the Riemann–Roch theorem (3.9) for replete divisors \(D \in \operatorname{Div}(\overline{\mathcal{O}})\).

Theorem (3.9)

FC09-C03-U063 · Chapter III, §3, source L9176 · not formalized

(3.9) Theorem (Riemann-Roch). For every replete divisor \(D \in Div(\overline{\mathcal{O}})\) we have the formula \[ \ell (D) = \deg (D) + \ell (\mathcal {O}) - g + i (D). \] The index of specialty \(i(D)\) satisfies \[ i (D) = O \left(e ^ {- \frac {1}{n} \deg (D)}\right), \] in particular, \(i(D)\to 0\) for \(\deg (D)\to \infty\)

Definition (3.10)

FC09-C03-U064 · Chapter III, §3, source L9212 · not formalized

(3.10) Definition. The fractional ideal \[ \omega_ {K} = \mathfrak {C} _ {K | \mathbb {Q}} \cong \operatorname{Hom} _ {\mathbb {Z}} (\mathcal {O}, \mathbb {Z}) \] is called the canonical module of the number field K.

Proposition (3.11)

FC09-C03-U065 · Chapter III, §3, source L9222 · not formalized

(3.11) Proposition. The canonical modules of L and K satisfy the relation \[ \omega_ {L} = \mathfrak {C} _ {L | K} \omega_ {K}. \]

Proposition (3.12)

FC09-C03-U066 · Chapter III, §3, source L9234 · not formalized

(3.12) Proposition. \(\deg \omega_K = -2\chi (\mathcal{O}) = 2g - 2\ell (\mathcal{O}).\)

Proposition (3.13)

FC09-C03-U067 · Chapter III, §3, source L9248 · not formalized

(3.13) Proposition. Let \(L|K\) be a finite extension and \(g_{L}\) , resp. \(g_{K}\) , the genus of \(L\) , resp. \(K\) . Then one has \[ g _ {L} - \ell (\mathcal {O} _ {L}) = [ L: K ] \big (g _ {K} - \ell (\mathcal {O} _ {K}) \big) + \frac {1}{2} \deg \mathfrak {C} _ {L | K}. \] In particular, in the case of an unramified extension \(L|K\) : \[ \chi (\mathcal {O} _ {L}) = [ L: K ] \chi (\mathcal {O} _ {K}). \]

Convention / notation

FC09-C03-U068 · Chapter III, §3, source L9300 · after FC09-C03-U067 · not formalized

Distinguishing the invariants of Riemann-Roch theory with respect to the Minkowski measure by a tilde, we get the relations \[ \widetilde {\chi} (\mathfrak {a}) = \chi (\mathfrak {a}) + \log 2 ^ {s}, \quad \widetilde {\ell} (\mathfrak {a}) = \ell (\mathfrak {a}) + \log 2 ^ {s} \] (the latter in case that \(H^0(\mathfrak{a}) \neq \emptyset\) ), whereas the genus remains unchanged. Substituting this into the Riemann-Hurwitz formula (3.13) preserves its shape only if one enriches \(\mathfrak{C}_{L|K}\) into a replete ideal in which all infinite primes \(\mathfrak{P}\) such that \(L_{\mathfrak{P}} \neq K_{\mathfrak{p}}\) occur. This forces us to consider the extension \(\mathbb{C}|\mathbb{R}\) as ramified, to put \(\tilde{e}_{\mathfrak{P}| \mathfrak{p}} = [L_{\mathfrak{P}} : K_{\mathfrak{p}}]\) , \(\widetilde{f}_{\mathfrak{P}| \mathfrak{p}} = 1\) , and in particular \[ \tilde {e} _ {\mathfrak {p}} = \left[ K _ {\mathfrak {p}}: \mathbb {R} \right], \quad \widetilde {f} _ {\mathfrak {p}} = 1. \] The following modifications ensue from this. For an infinite prime \(\mathfrak{p}\) one has to define \[ \tilde {v} _ {\mathfrak {p}} (a) = - \tilde {e} _ {\mathfrak {p}} \log | \tau a |, \quad \mathfrak {p} ^ {\nu} = e ^ {\nu / \tilde {e} _ {\mathfrak {p}}}, \quad \widetilde {\mathfrak {N}} (\mathfrak {p}) = e. \] The absolute norm as well as the degree of a replete ideal a remain unaltered: \[ \widetilde {\mathfrak {N}} (\mathfrak {a}) = \mathfrak {N} (\mathfrak {a}), \quad \widetilde {\deg} (\mathfrak {a}) = - \log \widetilde {\mathfrak {N}} (\mathfrak {a}) = \deg (\mathfrak {a}). \] The canonical module \(\omega_{K}\) however has to be changed: \[ \tilde {\omega} _ {K} = \omega_ {K} \prod_ {\mathfrak {p} \text { complex }} \mathfrak {p} ^ {2 \log 2}, \] in order for the equation \[ \deg \tilde {\omega} _ {K} = - 2 \widetilde {\chi} (\mathcal {O}) = 2 g - 2 \tilde {\ell} (\mathcal {O}) \] to hold. By the same token, the ideal \(\mathfrak{C}_{L|K}\) has to be replaced by the replete ideal \[ \tilde{\mathfrak{C}}_{L|K} = \mathfrak{C}_{L|K}\prod_{\substack{\widetilde{\mathfrak{P}}|\infty \\ e_{\widetilde{\mathfrak{P}}|\widetilde{\mathfrak{p}}}\neq 1}}\mathfrak{P}^{2\log 2} \] so that \[ \tilde {\omega} _ {L} = \tilde {\mathfrak {C}} _ {L | K} i _ {L | K} (\tilde {\omega} _ {K}). \] In the same way as in (3.13), this yields the Riemann-Hurwitz formula \[ g _ {L} - \tilde {\ell} (\mathcal {O} _ {L}) = [ L: K ] \big (g _ {K} - \tilde {\ell} (\mathcal {O} _ {K}) \big) + \frac {1}{2} \deg \tilde {\mathfrak {C}} _ {L | K}. \]

Definition / construction

FC09-C03-U069 · Chapter III, §3, source L9354 · not formalized

In view of this sensitivity to the chosen metric on Minkowski space \(K_{R}\) , the mathematician UWE JANNSEN proposes as analogues of the function fields not just number fields K by themselves but number fields equipped with a metric of the type \[ \langle x, y \rangle_ {K} = \sum_ {\tau} \alpha_ {\tau} x _ {\tau} \overline {{{{y}}}} _ {\tau}, \] \(\alpha_{\tau}>0,\alpha_{\tau}=\alpha_{\overline{\tau}}\) , on \(K_{R}\) . Let these new objects be called metrized number fields. This idea does indeed do justice to the situation in question in a very precise manner, and it is of fundamental importance for algebraic number theory. We denote metrized number fields \((K,\langle,\rangle_{K})\) as \(\tilde{K}\) and attach to them the following invariants. Let \[ \langle x, y \rangle_ {K} = \sum_ {\tau} \alpha_ {\tau} x _ {\tau} \overline {{{{y}}}} _ {\tau}. \] Let \(\mathfrak{p} = \mathfrak{p}_{\tau}\) be the infinite prime corresponding to \(\tau: K \to \mathbb{C}\) . We then put \(\alpha_{\mathfrak{p}} = \alpha_{\tau}\) . At the same time, we also use the letter \(\mathfrak{p}\) for the positive real number \[ \mathfrak {p} = e ^ {\alpha_ {\mathfrak {p}}} \in \mathbb {R} _ {+} ^ {*}, \] which we interpret as the replete ideal \((1) \times (1, \cdots, 1, e^{\alpha_{\mathfrak{p}}}, 1, \cdots, 1) \in J(\mathcal{O}) \times \prod_{\mathfrak{p} | \infty} \mathbb{R}_{+}^{*}\) . We put \[ e _ {\mathfrak {p}} = 1 / \alpha_ {\mathfrak {p}} \quad \text { and } \quad f _ {\mathfrak {p}} = \alpha_ {\mathfrak {p}} [ K _ {\mathfrak {p}}: \mathbb {R} ], \] and we define the valuation \(v_{\mathfrak{p}}\) of \(K^{*}\) associated to \(\mathfrak{p}\) by \[ v _ {\mathfrak {p}} (a) = - e _ {\mathfrak {p}} \log | \tau a |. \] Further, we put \[ \mathfrak {N} (\mathfrak {p}) = e ^ {f _ {\mathfrak {p}}} \quad \text { and } \quad | a | _ {\mathfrak {p}} = \mathfrak {N} (\mathfrak {p}) ^ {- v _ {\mathfrak {p}} (a)}, \] so that again \(|a|_{\mathfrak{p}} = |\tau a|\) if \(\mathfrak{p}\) is real, and \(|a|_{\mathfrak{p}} = |\tau a|^2\) if \(\mathfrak{p}\) is complex. For every replete ideal \(\mathfrak{a}\) of \(K\) , there is a unique representation \(\mathfrak{a} = \prod_{\mathfrak{p}} \mathfrak{p}^{\nu_{\mathfrak{p}}}\) , which gives the absolute norm \(\mathfrak{N}(\mathfrak{a}) = \prod_{\mathfrak{p}} \mathfrak{N}(\mathfrak{p})^{\nu_{\mathfrak{p}}}\) , and the degree \[ \deg_ {\tilde {K}} (\mathfrak {a}) = - \log \mathfrak {N} (\mathfrak {a}). \]

Definition / construction

FC09-C03-U070 · Chapter III, §3, source L9396 · not formalized

The canonical module of \(\widetilde{K}\) is defined to be the replete ideal \[ \omega_ {\tilde {K}} = \omega_ {K} \cdot \omega_ {\infty} \in J (\overline {{\mathcal {O}}}) = J (\mathcal {O}) \times \prod_ {\mathfrak {p} | \infty} \mathbb {R} _ {+} ^ {*}, \] where \(\omega_{K}\) is the inverse of the different \(\mathfrak{D}_{K|\mathbb{Q}}\) of \(K|\mathbb{Q}\) , and \[ \omega_ {\infty} = \left(\alpha_ {\mathfrak {p}} ^ {- 1}\right) _ {\mathfrak {p} | \infty} \in \prod_ {\mathfrak {p} | \infty} \mathbb {R} _ {+} ^ {*}. \]

Proposition (3.14)

FC09-C03-U071 · Chapter III, §3, source L9434 · not formalized

(3.14) Proposition. The metrized fields \((\mathbb{Q}, \alpha xy)\) are the only metrized number fields of genus 0.

Definition / construction

FC09-C03-U072 · Chapter III, §3, source L9454 · not formalized

An extension of metrized number fields is a pair \(\widetilde{K} = (K, \langle , \rangle_K)\) , \(\widetilde{L} = (L, \langle , \rangle_L)\) , such that \(K \subseteq L\) and the metrics \[ \langle x, y \rangle_ {K} = \sum_ {\tau} \alpha_ {\tau} x _ {\tau} \overline {{{y}}} _ {\tau}, \quad \langle x, y \rangle_ {L} = \sum_ {\sigma} \beta_ {\sigma} x _ {\sigma} \overline {{{y}}} _ {\sigma} \] satisfy the relation \(\alpha_{\tau} \geq \beta_{\sigma}\) whenever \(\tau = \sigma|_K\) . If \(\mathfrak{P}| \mathfrak{p}\) are infinite primes of \(L|K\) , \(\mathfrak{P}\) belonging to \(\sigma\) and \(\mathfrak{p}\) to \(\tau = \sigma|_K\) , we define the ramification index and inertia degree by \[ e _ {\mathfrak {P} | \mathfrak {p}} = \alpha_ {\tau} / \beta_ {\sigma} \quad \text { and } \quad f _ {\mathfrak {P} | \mathfrak {p}} = \beta_ {\sigma} / \alpha_ {\tau} [ L _ {\mathfrak {P}}: K _ {\mathfrak {p}} ]. \] Thus the fundamental identity \[ \sum_ {\mathfrak {P} | \mathfrak {p}} e _ {\mathfrak {P} | \mathfrak {p}} f _ {\mathfrak {P} | \mathfrak {p}} = [ L: K ] \] is preserved. Also P is unramified if and only if \(\alpha_{\tau} = \beta_{\sigma}\) . For “replete prime ideals” \(p = e^{\alpha_{\tau}}\) , \(P = e^{\beta_{\sigma}}\) , we put \[ i _ {L | K} (\mathfrak {p}) = \prod_ {\mathfrak {P} | \mathfrak {p}} \mathfrak {P} ^ {e _ {\mathfrak {P} | \mathfrak {p}}}, \quad N _ {L | K} (\mathfrak {P}) = \mathfrak {p} ^ {f _ {\mathfrak {P} | \mathfrak {p}}}. \]

Definition / construction

FC09-C03-U073 · Chapter III, §3, source L9478 · not formalized

Finally we define the different of \(\widetilde{L}|\widetilde{K}\) to be the replete ideal \[ \mathfrak {D} _ {\tilde {L} | \tilde {K}} = \mathfrak {D} _ {L | K} \cdot \mathfrak {D} _ {\infty} \in J (\overline {{\mathcal {O}}} _ {L}) = J (\mathcal {O} _ {L}) \times \prod_ {\mathfrak {P} | \infty} \mathbb {R} _ {+} ^ {*}, \] where \(\mathfrak{D}_{L|K}\) is the different of \(L|K\) and \[ \mathfrak {D} _ {\infty} = (\beta_ {\mathfrak {P}} / \alpha_ {\mathfrak {p}}) _ {\mathfrak {P} | \infty} \in \prod_ {\mathfrak {P} | \infty} \mathbb {R} _ {+} ^ {*}, \] where \(\beta_{\mathfrak{P}} = \beta_{\sigma}\) and \(\alpha_{\mathfrak{p}} = \alpha_{\tau}\) ( \(\mathfrak{P}\) belongs to \(\sigma\) and \(\mathfrak{p}\) to \(\tau = \sigma|_K\) ). With this convention, we obtain the general Riemann-Hurwitz formula \[ g_{\widetilde{L}} - \ell_{\widetilde{L}}(\mathcal{O}_{L}) = [L:K]\big(g_{\widetilde{K}} - \ell_{\widetilde{K}}(\mathcal{O}_{K})\big) - \tfrac{1}{2}\deg \mathfrak{D}_{\widetilde{L}|\widetilde{K}}. \]

Convention / notation

FC09-C03-U074 · Chapter III, §4, source L9526 · not formalized

The field \(K\) is embedded in \(K_{\mathbb{C}}\) via \[ K \longrightarrow K \otimes_ {\mathbb {Q}} \mathbb {C}, \quad a \longmapsto a \otimes 1, \] and we identify it with its image. In the interpretation (2), the image of \(a \in K\) appears as the tuple \(\bigoplus_{\sigma} \sigma a\) of conjugates of a, and in the interpretation (3) as the function \(x(\sigma) = \sigma a\) .

Not formalized. Pinned/current Mathlib has tensor products, complex embeddings, Hermitian/inner-product spaces, projective modules, Picard groups, ranks and determinant algebra, while the project has determinant-line scaffolding; this source row contains a metrized-module, full Dedekind-module classification, or arithmetic determinant bundle not exported compatibly.

Convention / notation

FC09-C03-U075 · Chapter III, §4, source L9534 · not formalized

We denote the generator of the Galois group \(G(\mathbb{C}|\mathbb{R})\) by \(F_{\infty}\) , or simply by \(F\) . This underlines the fact that it has a position analogous to the Frobenius automorphism \(F_{p} \in G(\overline{\mathbb{F}}_{p}|\mathbb{F}_{p})\) , in accordance with our decision of §1 to view the extension \(\mathbb{C}|\mathbb{R}\) as unramified. \(F\) induces an involution \(F\) on \(K_{\mathbb{C}}\) which, in the representation \(K_{\mathbb{C}} = \operatorname{Hom}(X(\mathbb{C}), \mathbb{C})\) for \(x: X(\mathbb{C}) \to \mathbb{C}\) , is given by \[ (F x) (\sigma) = \overline {{x (\overline {{\sigma}})}}. \] F is an automorphism of the R-algebra \(K_{C}\) . It is called the Frobenius correspondence. Sometimes we also consider, besides F, the involution \(z \mapsto \bar{z}\) on \(K_{C}\) which is given by \[ \bar {z} (\sigma) = \overline {{z (\sigma)}}. \] We call it the conjugation. Finally, we call an element \(x \in K_{C}\) , that is, a function \(x : X(\mathbb{C}) \to \mathbb{C}\) , positive (written x > 0) if it takes real values, and if \(x(\sigma) > 0\) for all \(\sigma \in X(\mathbb{C})\) .

Convention / notation

FC09-C03-U076 · Chapter III, §4, source L9548 · not formalized

By convention every O-module considered in the sequel will be supposed to be finitely generated. For every such O-module M, we put \[ M _ {\mathbb {C}} = M \otimes_ {\mathbb {Z}} \mathbb {C}. \] This is a module over the ring \(K_{C} = O \otimes_{Z} C\) , and viewing O as a subring of \(K_{C}\) – as we agreed above – we may also write \[ M _ {\mathbb {C}} = M \otimes_ {\mathcal {O}} K _ {\mathbb {C}} \] as \(M\otimes_{\mathbb{Z}}\mathbb{C} = M\otimes_{\mathcal{O}}(\mathcal{O}\otimes_{\mathbb{Z}}\mathbb{C})\) . The involution \(x\mapsto Fx\) on \(K_{\mathbb{C}}\) induces the involution \[ F(a \otimes x) = a \otimes Fx \] on \(M_{\mathbb{C}}\); in the representation \(M_{\mathbb{C}} = M \otimes_{\mathbb{Z}} \mathbb{C}\) this is \(F(a \otimes z) = a \otimes \bar{z}\).

Definition (4.1)

FC09-C03-U077 · Chapter III, §4, source L9572 · not formalized

(4.1) Definition. A hermitian metric on the \(K_{\mathbb{C}}\) -module \(M_{\mathbb{C}}\) is a sesquilinear mapping \[ \langle , \rangle_ {M}: M _ {\mathbb {C}} \times M _ {\mathbb {C}} \longrightarrow K _ {\mathbb {C}}, \] i.e., a \(K_{\mathbb{C}}\) -linear form \(\langle x, y \rangle_M\) in the first variable satisfying \[ \overline {{\langle x , y \rangle}} _ {M} = \langle y, x \rangle_ {M}, \] such that one has \(\langle x, x \rangle_M > 0\) for \(x \neq 0\) .

Definition / construction

FC09-C03-U078 · Chapter III, §4, source L9586 · not formalized

The metric \(\langle ,\rangle_{M}\) is called \(F\) -invariant if we have furthermore \[ F \langle x, y \rangle_ {M} = \langle F x, F y \rangle_ {M}. \] This notion may be immediately reduced to the usual notion of a hermitian metric if we view the \(K_{C}\) -module \(M_{C}\) , by means of the decomposition \(K_{C} = \bigoplus_{\sigma} C\) , as a direct sum \[ M _ {\mathbb {C}} = M \otimes_ {\mathcal {O}} K _ {\mathbb {C}} = \bigoplus_ {\sigma \in X (\mathbb {C})} M _ {\sigma} \] of \(\mathbb{C}\) -vector spaces \[ M _ {\sigma} = M \otimes_ {\mathcal {O}, \sigma} \mathbb {C}. \] The hermitian metric \(\langle\ ,\rangle_{M}\) then splits into the direct sum \[ \langle x,y \rangle_{M} = \bigoplus_{\sigma \in X(\mathbb{C})} \langle x_{\sigma}, y_{\sigma} \rangle_{M_{\sigma}} \] of hermitian scalar products on the summands \(M_{\sigma}\).

Definition (4.2)

FC09-C03-U079 · Chapter III, §4, source L9616 · not formalized

(4.2) Definition. A metrized O-module is a finitely generated O-module M with an F -invariant hermitian metric on \(M_{C}\) .

Example / comparison

FC09-C03-U080 · Chapter III, §4, source L9618 · not formalized

Example 1: Every fractional ideal \(\mathfrak{a} \subseteq K\) of \(\mathcal{O}\) , in particular \(\mathcal{O}\) itself, may be equipped with the trivial metric \[ \langle x, y \rangle = x \overline {{y}} = \bigoplus_ {\sigma \in X (\mathbb {C})} x _ {\sigma} \overline {{y}} _ {\sigma} \] on \(\mathfrak{a} \otimes_{\mathbb{Z}} \mathbb{C} = K \otimes_{\mathbb{Q}} \mathbb{C} = K_{\mathbb{C}}\) . All the \(F\) -invariant hermitian metrics on \(\mathfrak{a}\) are obtained as \[ \alpha \langle x, y \rangle = \alpha x \overline {{{y}}} = \bigoplus_ {\sigma} \alpha (\sigma) x _ {\sigma} \overline {{{y}}} _ {\sigma}, \] where \(\alpha \in K_{\mathbb{C}}\) varies over the functions \(\alpha : X(\mathbb{C}) \to \mathbb{R}_{+}^{*}\) such that \(\alpha(\overline{\sigma}) = \alpha(\sigma)\) .

Example / comparison

FC09-C03-U081 · Chapter III, §4, source L9632 · not formalized

Example 2: Let \(L|K\) be a finite extension and \(\mathfrak{A}\) a fractional ideal of \(L\) , which we view as an \(\mathcal{O}\) -module \(M\) . If \(Y(\mathbb{C}) = \operatorname{Hom}(L, \mathbb{C})\) , we have the restriction map \(Y(\mathbb{C}) \to X(\mathbb{C})\) , \(\tau \mapsto \tau|_K\) , and we write \(\tau|\sigma\) if \(\sigma = \tau|_K\) . For the complexification \(M_{\mathbb{C}} = \mathfrak{A} \otimes_{\mathbb{Z}} \mathbb{C} = L_{\mathbb{C}}\) , we obtain the decomposition \[ M _ {\mathbb {C}} = \bigoplus_ {\tau \in Y (\mathbb {C})} \mathbb {C} = \bigoplus_ {\sigma \in X (\mathbb {C})} M _ {\sigma}, \] where \(M_{\sigma} = \bigoplus_{\tau|_{\sigma}} C\) . M is turned into a metrized O-module by fixing the standard metrics \[ \langle x, y \rangle_ {M _ {\sigma}} = \sum_ {\tau | \sigma} x _ {\tau} \overline {{{{y}}}} _ {\tau} \] on the \([L:K]\) -dimensional \(\mathbb{C}\) -vector spaces \(M_{\sigma}\) .

Definition / construction

FC09-C03-U082 · Chapter III, §4, source L9646 · not formalized

If \(M\) and \(M'\) are metrized \(\mathcal{O}\) -modules, then so is their direct sum \(M \oplus M'\) , the tensor product \(M \otimes M'\) , the dual \(\check{M} = \operatorname{Hom}_{\mathcal{O}}(M, \mathcal{O})\) and the \(n\) -th exterior power \(\bigwedge^{n} M\) . In fact, we have that \[ (M \oplus M ^ {\prime}) _ {\mathbb {C}} = M _ {\mathbb {C}} \oplus M _ {\mathbb {C}} ^ {\prime}, (M \otimes_ {\mathcal {O}} M ^ {\prime}) _ {\mathbb {C}} = M _ {\mathbb {C}} \otimes_ {K _ {\mathbb {C}}} M _ {\mathbb {C}} ^ {\prime}, \] \[ \check {M} _ {\mathbb {C}} = \operatorname{Hom} _ {K _ {\mathbb {C}}} (M _ {\mathbb {C}}, K _ {\mathbb {C}}), \quad (\bigwedge^ {n} M) _ {\mathbb {C}} = \bigwedge_ {K _ {\mathbb {C}}} ^ {n} M _ {\mathbb {C}}, \] and the metrics on these \(K_{\mathbb{C}}\) -modules are given by \[ \langle x \oplus x ^ {\prime}, y \oplus y ^ {\prime} \rangle_ {M \oplus M ^ {\prime}} = \langle x, y \rangle_ {M} + \langle x ^ {\prime}, y ^ {\prime} \rangle_ {M ^ {\prime}}, \quad \text {resp.} \] \[ \langle x \otimes x ^ {\prime}, y \otimes y ^ {\prime} \rangle_ {M \otimes M ^ {\prime}} = \langle x, y \rangle_ {M} \cdot \langle x ^ {\prime}, y ^ {\prime} \rangle_ {M ^ {\prime}}, \quad \text {resp.} \] \[ \langle \check {x}, \check {y} \rangle_ {\check {M}} = \overline {{\langle x , y \rangle}} _ {M}, \qquad \mathrm{resp.} \] \[ \left\langle x _ {1} \wedge \dots \wedge x _ {n}, y _ {1} \wedge \dots \wedge y _ {n} \right\rangle_ {\wedge^ {n} M} = \det \bigl (\langle x _ {i}, y _ {j} \rangle_ {M} \bigr). \] Here \(\check{x}\) , in the case of the module \(\check{M}_{\mathbb{C}}\) , denotes the homomorphism \(\check{x} = \langle ,x\rangle_{M}:M_{\mathbb{C}}\to K_{\mathbb{C}}\) .

Definition / construction

FC09-C03-U083 · Chapter III, §4, source L9676 · in Mathlib

Among all \(\mathcal{O}\) -modules \(M\) the projective ones play a special rôle. They are defined by the condition that for every exact sequence of \(\mathcal{O}\) -modules \(F' \to F \to F''\) the sequence \[ \operatorname{Hom} _ {\mathcal {O}} (M, F ^ {\prime}) \longrightarrow \operatorname{Hom} _ {\mathcal {O}} (M, F) \longrightarrow \operatorname{Hom} _ {\mathcal {O}} (M, F ^ {\prime \prime}) \] is also exact. This is equivalent to any of the following conditions (the last two, because o is a Dedekind domain). For the proof, we refer the reader to standard textbooks of commutative algebra (see for instance [90], chap. IV, §3, or [16], chap. 7, §4).

Formalized. Mathlib/Algebra/Module/Projective.lean::Projective, projective_lifting_property, Projective.of_lifting_property — Mathlib packages projectivity in an equivalent splitting model and proves exactly the lifting property against every surjection. Since Hom(M,−) is always left exact, surjectivity of Hom(M,F)→Hom(M,F″) for every short exact sequence is equivalent to this lifting property, matching Neukirch’s definition.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Proposition (4.3)

FC09-C03-U084 · Chapter III, §4, source L9684 · not formalized

(4.3) Proposition. For any finitely generated \(\mathcal{O}\) -module \(M\) the following conditions are equivalent: (i) \(M\) is projective, (ii) \(M\) is a direct summand of a finitely generated free \(\mathcal{O}\) -module, (iii) \(M\) is locally free, i.e., \(M \otimes_{\mathcal{O}} \mathcal{O}_{\mathfrak{p}}\) is a free \(\mathcal{O}_{\mathfrak{p}}\) -module for any prime ideal \(\mathfrak{p}\) , (iv) \(M\) is torsion free, i.e., the map \(M \to M\) , \(x \mapsto ax\) , is injective for all nonzero \(a \in \mathcal{O}\) , (v) \(M \cong \mathfrak{a} \oplus \mathcal{O}^n\) for some ideal \(\mathfrak{a}\) of \(\mathcal{O}\) and some integer \(n \geq 0\) .

Definition / construction

FC09-C03-U085 · Chapter III, §4, source L9696 · after FC09-C03-U084 · not formalized

In order to distinguish them from projective O-modules, we will henceforth call arbitrary finitely generated O-modules coherent. The rank of a coherent O-module M is defined to be the dimension \[ \operatorname{rk} (M) = \dim_ {K} (M \otimes_ {\mathcal {O}} K). \] The projective \(\mathcal{O}\) -modules \(L\) of rank 1 are called invertible \(\mathcal{O}\) -modules, because for them \(L \otimes_{\mathcal{O}} \check{L} \to \mathcal{O}\) , \(a \otimes \check{a} \mapsto \check{a}(a)\) , is an isomorphism. The invertible \(\mathcal{O}\) -modules are either fractional ideals of \(K\) , or isomorphic to a fractional ideal as \(\mathcal{O}\) -modules. Indeed, if \(L\) is projective of rank 1 and \(\alpha \in L\) , \(\alpha \neq 0\) , then, by (4.3), (iv), mapping \[ L \longrightarrow L \otimes_ {\mathcal {O}} K = K (\alpha \otimes 1), \quad x \longmapsto f (x) (\alpha \otimes 1), \] gives an injective \(\mathcal{O}\) -module homomorphism \(L \to K\) , \(x \mapsto f(x)\) , onto a fractional ideal \(\mathfrak{a} \subseteq K\) .

Definition / construction

FC09-C03-U086 · Chapter III, §4, source L9710 · not formalized

To see the connection with the Riemann-Roch theory of the last section, which we are about to generalize, we observe that every replete ideal \[ \mathfrak {a} = \prod_ {\mathfrak {p} \nmid \infty} \mathfrak {p} ^ {\nu_ {\mathfrak {p}}} \prod_ {\mathfrak {p} | \infty} \mathfrak {p} ^ {\nu_ {\mathfrak {p}}} = \mathfrak {a} _ {\mathrm{f}} \mathfrak {a} _ {\infty} \] of \(K\) defines an invertible, metrized \(\mathcal{O}\) -module. In fact, the identity \(\mathfrak{a}_{\infty} = \prod_{\mathfrak{p}|\infty} \mathfrak{p}^{\nu_{\mathfrak{p}}}\) yields the function \[ \alpha : X (\mathbb {C}) \longrightarrow \mathbb {R} _ {+}, \quad \alpha (\sigma) = e ^ {2 \nu_ {\mathfrak {p} \sigma}}, \] where \(p_{\sigma}\) denotes as before the infinite place defined by \(\sigma: K \to C\) . Since \(p_{\overline{\sigma}} = p_{\sigma}\) , one has \(\alpha(\overline{\sigma}) = \alpha(\sigma)\) , and we obtain on the complexification \[ \mathfrak {a} _ {\mathrm{fC}} = \mathfrak {a} _ {\mathrm{f}} \otimes_ {\mathbb {Z}} \mathbb {C} = K _ {\mathbb {C}} \] the F-invariant hermitian metric \[ \langle x, y \rangle_ {a} = \alpha x \overline {{y}} = \bigoplus_ {\sigma \in X (\mathbb {C})} e ^ {2 \nu_ {\mathfrak {p} \sigma}} x _ {\sigma} \overline {{y}} _ {\sigma} \] (see example 1, p. 227). We denote the metrized \(\mathcal{O}\) -module thus obtained by \(L(\mathfrak{a})\) . The ordinary fractional ideals, i.e., the replete ideals \(\mathfrak{a}\) such that \(\mathfrak{a}_{\infty} = 1\) , and in particular \(\mathcal{O}\) itself, are thus equipped with the trivial metric \(\langle x, y \rangle_{\mathfrak{a}} = \langle x, y \rangle = x\overline{y}\) .

Definition (4.4)

FC09-C03-U087 · Chapter III, §4, source L9738 · not formalized

(4.4) Definition. Two metrized \(\mathcal{O}\) -modules \(M\) and \(M'\) are called isometric if there exists an isomorphism \[ f: M \longrightarrow M ^ {\prime} \] of \(\mathcal{O}\) -modules which induces an isometry \(f_{\mathbb{C}}: M_{\mathbb{C}} \to M_{\mathbb{C}}'\) .

Proposition (4.5)

FC09-C03-U088 · Chapter III, §4, source L9746 · not formalized

(4.5) Proposition. (i) Two replete ideals \(\mathfrak{a}\) and \(\mathfrak{b}\) define isometric metrized \(\mathcal{O}\) -modules \(L(\mathfrak{a})\) and \(L(\mathfrak{b})\) if and only if they differ by a replete principal ideal \([a]\) : \(\mathfrak{a} = \mathfrak{b}[a]\) . (ii) Every invertible metrized \(\mathcal{O}\) -module is isometric to an \(\mathcal{O}\) -module \(L(\mathfrak{a})\) . (iii) \(L(\mathfrak{ab}) \cong L(\mathfrak{a}) \otimes_{\mathcal{O}} L(\mathfrak{b}), L(\mathfrak{a}^{-1}) = \check{L}(\mathfrak{a})\) .

Definition (4.6)

FC09-C03-U089 · Chapter III, §4, source L9836 · not formalized

(4.6) Definition. A short exact sequence \[ 0 \longrightarrow M ^ {\prime} \stackrel {\alpha} {\longrightarrow} M \stackrel {\beta} {\longrightarrow} M ^ {\prime \prime} \longrightarrow 0 \] of metrized O-modules is by definition a short exact sequence of the underlying O-modules which splits isometrically, i.e., in the sequence \[ 0 \longrightarrow M _ {\mathbb {C}} ^ {\prime} \stackrel {\alpha_ {\mathbb {C}}} {\longrightarrow} M _ {\mathbb {C}} \stackrel {\beta_ {\mathbb {C}}} {\longrightarrow} M _ {\mathbb {C}} ^ {\prime \prime} \longrightarrow 0, \] \(M_{\mathbb{C}}^{\prime}\) is mapped isometrically onto \(\alpha_{\mathbb{C}}M_{\mathbb{C}}^{\prime}\) , and the orthogonal complement \((\alpha_{\mathbb{C}}M_{\mathbb{C}}^{\prime})^{\perp}\) is mapped isometrically onto \(M_{\mathbb{C}}^{\prime\prime}\) .

Definition / construction

FC09-C03-U090 · Chapter III, §4, source L9850 · not formalized

The homomorphisms \(\alpha\) , \(\beta\) in a short exact sequence of metrized O-modules are called an admissible monomorphism, resp. epimorphism.

Proposition (4.7)

FC09-C03-U091 · Chapter III, §4, source L9858 · not formalized

(4.7) Proposition. If \(0 \to M' \xrightarrow{\alpha} M \xrightarrow{\beta} M'' \to 0\) is a short exact sequence of projective metrized \(\mathcal{O}\) -modules, we have a canonical isometry \[ \det M ^ {\prime} \otimes_ {\mathcal {O}} \det M ^ {\prime \prime} \cong \det M. \]

Convention / notation

FC09-C03-U092 · Chapter III, §5, source L9932 · not formalized

We will now manufacture two abelian groups from the collection of all metrized O-modules, resp. the collection of all projective metrized O-modules. We denote by \(\{M\}\) the isometry class of a metrized O-module M and form the free abelian group \[ F _ {0} (\bar {\mathcal {O}}) = \bigoplus_ {\{M \}} \mathbb {Z} \{M \}, \quad \text {resp.} \quad F ^ {0} (\bar {\mathcal {O}}) = \bigoplus_ {\{M \}} \mathbb {Z} \{M \}, \] on the isometry classes of projective, resp. coherent, metrized o-modules. In this group, we consider the subgroup \[ R _ {0} (\overline {{\mathcal {O}}}) \subseteq F _ {0} (\overline {{\mathcal {O}}}), \quad \text { resp. } \quad R ^ {0} (\overline {{\mathcal {O}}}) \subseteq F ^ {0} (\overline {{\mathcal {O}}}), \] generated by all elements \(\{M'\} - \{M\} + \{M''\}\) which arise from a short exact sequence \[ 0 \longrightarrow M ^ {\prime} \longrightarrow M \longrightarrow M ^ {\prime \prime} \longrightarrow 0 \] of projective, resp. coherent, metrized O-modules.

Not formalized. Pinned/current Mathlib has ordinary Grothendieck/homological and characteristic-class ingredients in various settings, but no metrized Grothendieck group, arithmetic Chern character, arithmetic Grothendieck–Riemann–Roch, or Euler–Minkowski package closes this source unit.

Definition (5.1)

FC09-C03-U093 · Chapter III, §5, source L9952 · not formalized

(5.1) Definition. The quotient groups \[ K _ {0} (\bar {\mathcal {O}}) = F _ {0} (\bar {\mathcal {O}}) / R _ {0} (\bar {\mathcal {O}}), \quad r e s p. \quad K ^ {0} (\bar {\mathcal {O}}) = F ^ {0} (\bar {\mathcal {O}}) / R ^ {0} (\bar {\mathcal {O}}) \] are called the replete (or compactified) Grothendieck groups of \(\mathcal{O}\) . If \(M\) is a metrized \(\mathcal{O}\) -module, then \([M]\) denotes the class it defines in \(K_0(\overline{\mathcal{O}})\) , resp. \(K^0 (\overline{\mathcal{O}})\) .

Convention / notation

FC09-C03-U094 · Chapter III, §5, source L10004 · not formalized

Associating to the class \([M]\) of a projective O-module M in \(K_{0}(\overline{\mathcal{O}})\) its class in \(K^{0}(\overline{\mathcal{O}})\) (which again is denoted by \([M]\) ), defines a homomorphism \[ K _ {0} (\overline {{{\mathcal {O}}}}) \longrightarrow K ^ {0} (\overline {{{\mathcal {O}}}}). \] It is called the Poincaré homomorphism. We will show next that the Poincaré homomorphism is an isomorphism. The proof is based on the following two lemmas.

Lemma (5.2)

FC09-C03-U095 · Chapter III, §5, source L10012 · not formalized

(5.2) Lemma. All coherent metrized O-modules M admit a “metrized projective resolution”, i.e., a short exact sequence \[ 0 \longrightarrow E \longrightarrow F \longrightarrow M \longrightarrow 0 \] of metrized O-modules in which E and F are projective.

Definition / construction

FC09-C03-U096 · Chapter III, §5, source L10034 · not formalized

In a diagram of metrized projective resolutions of M \[ \begin{array}{c c c c c c} 0 \longrightarrow & E & \longrightarrow & F & \longrightarrow & M \\ & \Big \downarrow & & \Big \downarrow & & \Big \| \\ 0 \longrightarrow & E ^ {\prime} & \longrightarrow & F ^ {\prime} & \longrightarrow & M \\ \end{array} \longrightarrow 0 \] the resolution in the top line will be called dominant if the vertical arrows are admissible epimorphisms.

Lemma (5.3)

FC09-C03-U097 · Chapter III, §5, source L10042 · not formalized

(5.3) Lemma. Let \[ 0 \longrightarrow E ^ {\prime} \longrightarrow F ^ {\prime} \stackrel {f ^ {\prime}} {\longrightarrow} M \longrightarrow 0, \quad 0 \longrightarrow E ^ {\prime \prime} \longrightarrow F ^ {\prime \prime} \stackrel {f ^ {\prime \prime}} {\longrightarrow} M \longrightarrow 0 \] be two metrized projective resolutions of the metrized O-module M. Then, taking the O-module \[ F = F ^ {\prime} \times_ {M} F ^ {\prime \prime} = \left\{(x ^ {\prime}, x ^ {\prime \prime}) \in F ^ {\prime} \times F ^ {\prime \prime} \mid f ^ {\prime} (x ^ {\prime}) = f ^ {\prime \prime} (x ^ {\prime \prime}) \right\} \] and the mapping \(f: F \to M, (x', x'') \mapsto f'(x') = f''(x'')\) , one obtains a third metrized projective resolution \[ 0 \longrightarrow E \longrightarrow F \longrightarrow M \longrightarrow 0 \] with kernel \(E = E' \times E''\) which dominates both given ones.

Theorem (5.4)

FC09-C03-U098 · Chapter III, §5, source L10128 · not formalized

(5.4) Theorem. The Poincaré homomorphism \[ K _ {0} (\overline {{{\mathcal {O}}}}) \longrightarrow K ^ {0} (\overline {{{\mathcal {O}}}}) \] is an isomorphism.

Proposition (5.5)

FC09-C03-U099 · Chapter III, §5, source L10202 · not formalized

(5.5) Proposition. Associating to a replete ideal \(\mathfrak{a}\) of \(K\) the metrized \(\mathcal{O}\) -module \(L(\mathfrak{a})\) yields a homomorphism \[ P i c (\overline {{{\mathcal {O}}}}) \longrightarrow K _ {0} (\overline {{{\mathcal {O}}}}) ^ {*}, \quad [ \mathfrak {a} ] \longmapsto [ L (\mathfrak {a}) ], \] into the unit group of the ring \(K_0(\overline{\mathcal{O}})\) .

Proposition (5.6)

FC09-C03-U100 · Chapter III, §5, source L10218 · not formalized

(5.6) Proposition. \(K_{0}(\overline{\mathcal{O}})\) is generated as an additive group by the elements [a].

Proposition (5.7)

FC09-C03-U101 · Chapter III, §5, source L10234 · not formalized

(5.7) Proposition. For any two replete ideals \(\mathfrak{a}\) and \(\mathfrak{b}\) of \(K\) we have in \(K_0(\overline{\mathcal{O}})\) the equation \[ ([ a ] - 1) ([ b ] - 1) = 0. \]

Definition / construction

FC09-C03-U102 · Chapter III, §6, source L10412 · not formalized

The Grothendieck ring \(K_{0}(\overline{\mathcal{O}})\) is equipped with a canonical surjective homomorphism \[ \operatorname{rk}: K _ {0} (\bar {\mathcal {O}}) \longrightarrow \mathbb {Z}. \] Indeed, the rule which associates to every isometry class \(\{M\}\) of projective metrized O-modules the rank \[ \operatorname{rk} \{M \} = \dim_ {K} (M \otimes_ {\mathcal {O}} K) \] extends by linearity to a ring homomorphism \(F_0(\overline{\mathcal{O}}) \to \mathbb{Z}\) . For a short exact sequence \(0 \to M' \to M \to M'' \to 0\) of metrized \(\mathcal{O}\) -modules one has \(\operatorname{rk}(M) = \operatorname{rk}(M') + \operatorname{rk}(M'')\) , and so \(\operatorname{rk}(\{M'\} - \{M\} + \{M''\}) = 0\) . Thus \(\operatorname{rk}\) is zero on the ideal \(R_0(\overline{\mathcal{O}})\) and induces therefore a homomorphism \(K_0(\overline{\mathcal{O}}) \to \mathbb{Z}\) . It is called the augmentation of \(K_0(\overline{\mathcal{O}})\) and its kernel \(I = \ker(\operatorname{rk})\) is called the augmentation ideal.

Proposition (6.1)

FC09-C03-U103 · Chapter III, §6, source L10426 · not formalized

(6.1) Proposition. The ideal I, resp. \(I^{2}\) , is generated as an additive group by the elements \([a]-1\) , resp. \(([a]-1)([b]-1)\) , where a, b vary over the replete ideals of K.

Corollary (6.2)

FC09-C03-U104 · Chapter III, §6, source L10450 · not formalized

(6.2) Corollary. \(I^2 = 0\) .

Definition / construction

FC09-C03-U105 · Chapter III, §6, source L10452 · not formalized

We now define \[ \operatorname{gr} K _ {0} (\overline {{{{\mathcal {O}}}}}) = \mathbb {Z} \oplus I \] and turn this additive group into a ring by putting \(xy = 0\) for \(x, y \in I\) .

Definition (6.3)

FC09-C03-U106 · Chapter III, §6, source L10460 · not formalized

(6.3) Definition. The additive homomorphism \[ c _ {1}: K _ {0} (\bar {\mathcal {O}}) \longrightarrow I, \quad c _ {1} (\xi) = \xi - \mathrm{rk} (\xi) \] is called the first Chern class. The mapping \[ \operatorname{ch}: K _ {0} (\bar {\mathcal {O}}) \to \operatorname{gr} K _ {0} (\bar {\mathcal {O}}), \quad \operatorname{ch} (\xi) = \operatorname{rk} (\xi) + c _ {1} (\xi), \] is called the Chern character of \(K_{0}(\bar{\mathcal{O}})\) .

Proposition (6.4)

FC09-C03-U107 · Chapter III, §6, source L10474 · not formalized

(6.4) Proposition. The Chern character \[ \operatorname{ch}: K _ {0} (\overline {{{{\mathcal {O}}}}}) \longrightarrow \operatorname{gr} K _ {0} (\overline {{{{\mathcal {O}}}}}) \] is an isomorphism of rings.

Definition / construction

FC09-C03-U108 · Chapter III, §6, source L10496 · after FC09-C03-U091 · not formalized

We obtain a complete and explicit description of the Chern character by taking into account another homomorphism, as well as the homomorphism \(\operatorname{rk}: K_{0}(\bar{\mathcal{O}}) \to \mathbb{Z}\) , namely \[ \det: K _ {0} (\overline {{{\mathcal {O}}}}) \longrightarrow P i c (\overline {{{\mathcal {O}}}}) \] which is induced by taking determinants det M of projective o-modules M as follows (see §4). det M is an invertible metrized o-module, and therefore of the form \(L(\mathfrak{a})\) for some replete ideal a, which is well determined up to isomorphism. Denoting by [det M] the class of a in \(Pic(\overline{\mathcal{O}})\) , the linear extension of the map \(\{M\}\mapsto[\det M]\) gives a homomorphism \[ \det: F _ {0} (\overline {{{\mathcal {O}}}}) \longrightarrow P i c (\overline {{{\mathcal {O}}}}). \] It maps the subgroup \(R_{0}(\bar{\mathcal{O}})\) to 1, because it is generated by the elements \(\{M'\}-\{M\}+\{M''\}\) which arise from short exact sequences \[ 0 \longrightarrow M ^ {\prime} \longrightarrow M \longrightarrow M ^ {\prime \prime} \longrightarrow 0 \] of projective metrized o-modules and which, by (4.7), satisfy \[ \begin{array}{c} \det \{M \} = [ \det M ] = [ \det M ^ {\prime} \otimes \det M ^ {\prime \prime} ] \\ = [ \det M ^ {\prime} ] [ \det M ^ {\prime \prime} ] = \det \{M ^ {\prime} \} \det \{M ^ {\prime \prime} \}. \end{array} \] Thus we get an induced homomorphism \(\det: K_{0}(\overline{\mathcal{O}}) \to \text{Pic}(\overline{\mathcal{O}})\) . It satisfies the following proposition.

Proposition (6.5)

FC09-C03-U109 · Chapter III, §6, source L10522 · not formalized

(6.5) Proposition. (i) The canonical homomorphism \[ P i c (\overline {{{\mathcal {O}}}}) \longrightarrow K _ {0} (\overline {{{\mathcal {O}}}}) ^ {*} \] is injective. (ii) The restriction of det to \(I\) , \[ \det: I \longrightarrow P i c (\overline {{{\mathcal {O}}}}), \] is an isomorphism.

Definition / construction

FC09-C03-U110 · Chapter III, §6, source L10554 · not formalized

From the isomorphism \(\det: I \xrightarrow{\sim} \operatorname{Pic}(\overline{\mathcal{O}})\) , we now obtain an isomorphism \[ \operatorname{gr} K _ {0} (\overline {{\mathcal {O}}}) \stackrel {\sim} {\longrightarrow} \mathbb {Z} \oplus P i c (\overline {{\mathcal {O}}}) \] and the composite \[ K _ {0} (\overline {{{\mathcal {O}}}}) \xrightarrow {\mathrm{ch}} \operatorname{gr} K _ {0} (\overline {{{\mathcal {O}}}}) \xrightarrow {\mathrm{id} \oplus \det} \mathbb {Z} \oplus P i c (\overline {{{\mathcal {O}}}}) \] will again be called the Chern character of \(K_{0}(\bar{\mathcal{O}})\) . Observing that \(\det(c_{1}(\xi)) = \det(\xi - \mathrm{rk}(\xi) \cdot 1) = \det(\xi)\) , this yields the explicit description of the Grothendieck group \(K_{0}(\bar{\mathcal{O}})\) :

Theorem (6.6)

FC09-C03-U111 · Chapter III, §6, source L10568 · not formalized

(6.6) Theorem. The Chern character gives an isomorphism \[ \operatorname{ch}: K _ {0} (\bar {\mathcal {O}}) \stackrel {{\sim}} {{\longrightarrow}} \mathbb {Z} \oplus P i c (\bar {\mathcal {O}}), \quad \operatorname{ch} (\xi) = \operatorname{rk} (\xi) \oplus \det (\xi). \]

Definition / construction

FC09-C03-U112 · Chapter III, §7, source L10578 · not formalized

We now consider a finite extension \(L|K\) of algebraic number fields and study the relations between the Grothendieck groups of \(L\) and \(K\) . Let \(\mathcal{O}\) , resp. \(\mathcal{O}\) , be the ring of integers of \(K\) , resp. \(L\) , and write \(X(\mathbb{C}) = \operatorname{Hom}(K, \mathbb{C})\) , \(Y(\mathbb{C}) = \operatorname{Hom}(L, \mathbb{C})\) . The inclusion \(i: \mathcal{O} \to \mathcal{O}\) and the surjection \(Y(\mathbb{C}) \to X(\mathbb{C})\) , \(\sigma \mapsto \sigma|_K\) , give two canonical homomorphisms \[ i ^ {*}: K _ {0} (\overline {{{\mathcal {O}}}}) \longrightarrow K _ {0} (\overline {{{\mathcal {O}}}}) \quad \text { and } \quad i _ {*}: K _ {0} (\overline {{{\mathcal {O}}}}) \longrightarrow K _ {0} (\overline {{{\mathcal {O}}}}), \] defined as follows. If \(M\) is a projective metrized \(\mathcal{O}\) -module, then \(M \otimes_{\mathcal{O}} \mathcal{O}\) is a projective \(\mathcal{O}\) -module. As \[ (M \otimes_ {\mathcal {O}} \mathcal {O}) _ {\mathbb {C}} = M \otimes_ {\mathcal {O}} \mathcal {O} \otimes_ {\mathbb {Z}} \mathbb {C} = M _ {\mathbb {C}} \otimes_ {K _ {\mathbb {C}}} L _ {\mathbb {C}}, \] the hermitian metric on the \(K_{C}\) -module \(M_{C}\) extends canonically to an F-invariant metric of the \(L_{C}\) -module \((M \otimes_{\circ} O)_{\mathbb{C}}\) . Therefore \(M \otimes_{\circ} O\) is automatically a metrized O-module, which we denote by \(i^{*}M\) . If \[ 0 \longrightarrow M ^ {\prime} \longrightarrow M \longrightarrow M ^ {\prime \prime} \longrightarrow 0 \] is a short exact sequence of projective metrized O-modules, then \[ 0 \longrightarrow M ^ {\prime} \otimes_ {\mathcal {O}} \mathcal {O} \longrightarrow M \otimes_ {\mathcal {O}} \mathcal {O} \longrightarrow M ^ {\prime \prime} \otimes_ {\mathcal {O}} \mathcal {O} \longrightarrow 0 \] is a short exact sequence of metrized O-modules, because O is a projective O-module and the metrics in the sequence \[ 0 \longrightarrow M _ {\mathbb {C}} ^ {\prime} \longrightarrow M _ {\mathbb {C}} \longrightarrow M _ {\mathbb {C}} ^ {\prime \prime} \longrightarrow 0 \] simply extend \(L_{C}\) -sesquilinearly to metrics in the sequence of \(L_{C}\) -modules \[ 0 \longrightarrow M _ {\mathbb {C}} ^ {\prime} \otimes_ {K _ {\mathbb {C}}} L _ {\mathbb {C}} \longrightarrow M _ {\mathbb {C}} \otimes_ {K _ {\mathbb {C}}} L _ {\mathbb {C}} \longrightarrow M _ {\mathbb {C}} ^ {\prime \prime} \otimes_ {K _ {\mathbb {C}}} L _ {\mathbb {C}} \longrightarrow 0. \] This is why mapping, in the usual way (i.e., via the representation \(K_{0}(\overline{\mathcal{O}})=F_{0}(\overline{\mathcal{O}})/R_{0}(\overline{\mathcal{O}})\) ), \[ M \longmapsto [ i ^ {*} M ] = [ M \otimes_ {\mathcal {O}} \mathcal {O} ] \] gives a well-defined homomorphism \[ i ^ {*}: K _ {0} (\overline {{\mathcal {O}}}) \longrightarrow K _ {0} (\overline {{\mathcal {O}}}). \] The reader may verify for himself that this is in fact a ring homomorphism.

Definition / construction

FC09-C03-U113 · Chapter III, §7, source L10630 · not formalized

On the other hand, if M is a projective metrized O-module, then M is automatically also a projective O-module. For the complexification \(M_{C} = M \otimes_{Z} C\) we have the decomposition \[ M _ {\mathbb {C}} = \bigoplus_ {\tau \in Y (\mathbb {C})} M _ {\tau} = \bigoplus_ {\sigma \in X (\mathbb {C})} \bigoplus_ {\tau | \sigma} M _ {\tau} = \bigoplus_ {\sigma \in X (\mathbb {C})} M _ {\sigma}, \] where \(M_{\tau} = M\otimes_{\mathcal{O},\tau}\mathbb{C}\) and \[ M _ {\sigma} = M \otimes_ {\mathcal {O}, \sigma} \mathbb {C} = \bigoplus_ {\tau | \sigma} M _ {\tau}. \] The C-vector spaces \(M_{\tau}\) carry hermitian metrics \(\langle, \rangle_{M_{\tau}}\) , and we define the metric \(\langle, \rangle_{M_{\sigma}}\) on the C-vector space \(M_{\sigma}\) to be the orthogonal sum \[ \langle x, y \rangle_ {M _ {\sigma}} = \sum_ {\tau | \sigma} \langle x _ {\tau}, y _ {\tau} \rangle_ {M _ {\tau}}. \] This gives a hermitian metric on the \(K_{C}\) -module \(M_{C}\) , whose F-invariance is clearly guaranteed by the F-invariance of the original metric \(\langle,\rangle_{M}\) . We denote the metrized O-module M thus constructed by \(i_{*}M\) . If \(0 \rightarrow M' \rightarrow M \rightarrow M'' \rightarrow 0\) is a short exact sequence of projective metrized O-modules, then \[ 0 \longrightarrow i _ {*} M ^ {\prime} \longrightarrow i _ {*} M \longrightarrow i _ {*} M ^ {\prime \prime} \longrightarrow 0 \] is clearly an exact sequence of projective metrized O-modules. As before, this is why the correspondence \[ M \longmapsto [ i _ {*} M ] \] gives us a well-defined (additive) homomorphism \[ i _ {*}: K _ {0} (\overline {{\mathcal {O}}}) \longrightarrow K _ {0} (\overline {{\mathcal {O}}}). \]

Proposition (7.1)

FC09-C03-U114 · Chapter III, §7, source L10668 · not formalized

(7.1) Proposition (Projection Formula). The diagram \[ \begin{array}{c c c c c} K _ {0} (\overline {{\mathcal {O}}}) & \times & K _ {0} (\overline {{\mathcal {O}}}) & \longrightarrow & K _ {0} (\overline {{\mathcal {O}}}) \\ i _ {*} \Big \downarrow & & \Big \uparrow i ^ {*} & & \Big \downarrow i _ {*} \\ K _ {0} (\overline {{\mathcal {O}}}) & \times & K _ {0} (\overline {{\mathcal {O}}}) & \longrightarrow & K _ {0} (\overline {{\mathcal {O}}}) \end{array} \] is commutative, where the horizontal arrows are multiplication.

Definition / construction

FC09-C03-U115 · Chapter III, §7, source L10702 · after FC09-C03-U111, FC09-C03-U088 · not formalized

The Riemann-Roch problem in Grothendieck’s perspective is the task of computing the Chern character \(\operatorname{ch}(i_*M)\) for a projective metrized \(\mathcal{O}\) -module \(M\) in terms of \(\operatorname{ch}(M)\) . By (6.6), this amounts to computing \(\det(i_*M)\) in terms of \(\det M\) . But \(\det M\) is an invertible metrized \(\mathcal{O}\) -module and is therefore isometric by (4.5) to the metrized \(\mathcal{O}\) -module \(L(\mathfrak{A})\) of a replete ideal \(\mathfrak{A}\) of \(L\) . \(N_{L|K}(\mathfrak{A})\) is then a replete ideal of \(K\) , and we put \[ N _ {L | K} (\det M) := L \left(N _ {L | K} (\mathfrak {A})\right). \] This is an invertible metrized O-module which is well determined by M up to isometry. With this notation we first establish the following theorem.

Theorem (7.2)

FC09-C03-U116 · Chapter III, §7, source L10710 · not formalized

(7.2) Theorem. For any projective metrized O-module M one has: \[ \operatorname{rk} (i _ {*} M) = \operatorname{rk} (M) \operatorname{rk} (\mathcal {O}), \] \[ \det (i _ {*} M) \cong N _ {L | K} (\det M) \otimes_ {\mathcal {O}} (\det i _ {*} \mathcal {O}) ^ {\operatorname{rk} (M)}. \] Here we have \(\operatorname{rk}(\mathcal{O}) = [L:K]\) .

Corollary (7.3)

FC09-C03-U117 · Chapter III, §7, source L10818 · not formalized

(7.3) Corollary. For every class \(\xi \in K_0(\overline{\mathcal{O}})\) , one has the formulas \[ \operatorname{rk} (i _ {*} \xi) = [ L: K ] \operatorname{rk} (\xi), \] \[ \det (i _ {*} \xi) = [ \det i _ {*} \mathcal {O} ] ^ {\mathrm{rk} (\xi)} N _ {L | K} (\det \xi). \]

Proposition (7.4)

FC09-C03-U118 · Chapter III, §7, source L10830 · not formalized

(7.4) Proposition. There is a canonical isomorphism \[ (\det i _ {*} \mathcal {O}) ^ {\otimes 2} \cong \mathfrak {d} _ {L | K} \] of metrized o-modules.

Definition / construction

FC09-C03-U119 · Chapter III, §7, source L10926 · after FC09-C03-U116, FC09-C03-U118, FC09-C03-U117 · not formalized

We now set out to rewrite the results obtained in (7.2) and (7.4) in the language of GROTHENDIECK’s general formalism. For the homomorphism \(i_{*}\) there is the commutative diagram \[ \begin{array}{c c c} K _ {0} (\overline {{\mathcal {O}}}) & \xrightarrow {\mathrm{rk}} & \mathbb {Z} \\ i _ {*} \Big \downarrow & & \Big \downarrow_ {[ L: K ]} \\ K _ {0} (\overline {{\mathcal {O}}}) & \xrightarrow {\mathrm{rk}} & \mathbb {Z}, \end{array} \] because \([L:K]\) times the rank of an O-module M is its rank as O-module. Therefore \(i_{*}\) induces a homomorphism \[ i _ {*}: I (\overline {{\mathcal {O}}}) \longrightarrow I (\overline {{\mathcal {O}}}) \] between the kernels of both rank homomorphisms, so that there is a homomorphism \[ i _ {*}: \operatorname{gr} K _ {0} (\overline {{\mathcal {O}}}) \longrightarrow \operatorname{gr} K _ {0} (\overline {{\mathcal {O}}}). \] It is called the Gysin map. (7.3) immediately gives the following explicit description of it.

Corollary (7.5)

FC09-C03-U120 · Chapter III, §7, source L10946 · not formalized

(7.5) Corollary. The diagram \[ \begin{array}{c c c} \operatorname{gr} K _ {0} (\overline {{\mathcal {O}}}) & \xrightarrow [ \sim ]{\operatorname{id} \oplus \det} & \mathbb {Z} \oplus P i c (\overline {{\mathcal {O}}}) \\ i _ {*} \Big \downarrow & & \Big \downarrow_ {[ L: K ] \oplus N _ {L | K}} \\ \operatorname{gr} K _ {0} (\overline {{\mathcal {O}}}) & \xrightarrow [ \sim ]{\operatorname{id} \oplus \det} & \mathbb {Z} \oplus P i c (\overline {{\mathcal {O}}}) \end{array} \] is commutative.

Definition (7.6)

FC09-C03-U121 · Chapter III, §7, source L10970 · not formalized

(7.6) Definition. The Todd class of \(O|O\) is defined to be the element \[ \operatorname{Td} (\mathcal {O} | \mathcal {O}) = 1 - \frac {1}{2} c _ {1} \left(\left[ \Omega_ {\mathcal {O} | \mathcal {O}} ^ {1} \right]\right) = 1 - \frac {1}{2} \left[ \Omega_ {\mathcal {O} | \mathcal {O}} ^ {1} \right] \in \operatorname{gr} K _ {0} (\overline {{\mathcal {O}}}) \otimes \mathbb {Z} \left[ \frac {1}{2} \right]. \]

Theorem (7.7)

FC09-C03-U122 · Chapter III, §7, source L10990 · not formalized

(7.7) Theorem (Grothendieck-Riemann-Roch). The diagram \[ \begin{array}{c c c} K _ {0} (\overline {{\mathcal {O}}}) & \xrightarrow {\operatorname{Td} (\mathcal {O} | \mathcal {O}) \mathrm{ch}} & \operatorname{gr} K _ {0} (\overline {{\mathcal {O}}}) \\ i _ {*} \Big \downarrow & & \Big \downarrow i _ {*} \\ K _ {0} (\overline {{\mathcal {O}}}) & \xrightarrow {\mathrm{ch}} & \operatorname{gr} K _ {0} (\overline {{\mathcal {O}}}) \end{array} \] is commutative.

Proposition (8.1)

FC09-C03-U123 · Chapter III, §8, source L11058 · not formalized

(8.1) Proposition. The degree map \[ \deg_ {K}: P i c (\bar {\mathcal {O}}) \longrightarrow \mathbb {R}, \quad \deg_ {K} ([ \mathfrak {a} ]) = - \log \mathfrak {N} (\mathfrak {a}), \] extends uniquely to a homomorphism \[ \chi_ {K}: K _ {0} (\overline {{{{\mathcal {O}}}}}) \longrightarrow \mathbb {R} \] on \(K_0(\overline{\mathcal{O}})\) , and thereby on \(K^0 (\overline{\mathcal{O}})\) . It is given by \[ \chi_ {K} = \deg \circ \det \] and called the Euler-Minkowski characteristic over \(K\) .

Convention / notation

FC09-C03-U124 · Chapter III, §8, source L11086 · after FC09-C03-U123, FC09-C03-U116 · not formalized

Via the Poincaré isomorphism \(K_0(\overline{\mathcal{O}}) \xrightarrow{\sim} K^0(\overline{\mathcal{O}})\) , we transfer the maps det and \(\chi_K\) to the Grothendieck group \(K^0(\overline{\mathcal{O}})\) of coherent metrized \(\mathcal{O}\) -modules. Then proposition (8.1) is equally valid for \(K^0(\overline{\mathcal{O}})\) as for \(K_0(\overline{\mathcal{O}})\) . We define in what follows \(\chi_K(M) = \chi_K([M])\) for a metrized \(\mathcal{O}\) -module \(M\) . If \(L|K\) is an extension of algebraic number fields and \(i: \mathcal{O} \to \mathcal{O}\) the inclusion of the maximal orders of \(K\) , resp. \(L\) , then applying \(\deg_K\) to the formula (7.2) and using \[ \deg_ {L} (\mathfrak {A}) = - \log \mathfrak {N} (\mathfrak {A}) = - \log \mathfrak {N} \left(N _ {L | K} (\mathfrak {A})\right) = \deg_ {K} \left(N _ {L | K} (\mathfrak {A})\right) \]

Theorem (8.2)

FC09-C03-U125 · Chapter III, §8, source L11094 · not formalized

(8.2) Theorem. For every coherent \(\mathcal{O}\) -module \(M\) , the Riemann-Roch formula \[ \chi_ {K} (i _ {*} M) = \deg_ {L} (\det M) + \operatorname{rk} (M) \chi_ {K} (i _ {*} \mathcal {O}) \] is valid, and in particular, for an invertible metrized O-module M, we have \[ \chi_ {K} (i _ {*} M) = \deg_ {L} (M) + \chi_ {K} (i _ {*} \mathcal {O}). \]

Convention / notation

FC09-C03-U126 · Chapter III, §8, source L11126 · not formalized

It will be denoted by \(\operatorname{vol}(M)\) for short. It does not depend on the choice of Z-basis \(\alpha_{1},\ldots,\alpha_{n}\) because a different choice is linked to the original one by a matrix with integer coefficients which also has an inverse with integer coefficients, hence has determinant of absolute value 1.

Definition / construction

FC09-C03-U127 · Chapter III, §8, source L11134 · not formalized

In the present case, where the base field is Q, the degree map \[ \deg : P i c (\overline {{\mathbb {Z}}}) \longrightarrow \mathbb {R} \] is an isomorphism (see § 1, exercise 3), and we call the unique homomorphism arising from this, \[ \chi = \deg \circ \det: K ^ {0} (\overline {{\mathbb {Z}}}) \longrightarrow \mathbb {R}, \] the Euler-Minkowski characteristic. It is computed explicitly as follows.

Proposition (8.3)

FC09-C03-U128 · Chapter III, §8, source L11148 · not formalized

(8.3) Proposition. For a coherent metrized \(\mathbb{Z}\) -module \(M\) , one has \[ \chi (M) = \log \# M _ {\mathrm{tor}} - \log \operatorname{vol} (M / M _ {\mathrm{tor}}). \] In this formula \(M_{tor}\) denotes the torsion subgroup of M and \(M/M_{tor}\) the projective metrized Z-module which receives its metric from M via \(M \otimes R = M/M_{tor} \otimes R\) .

Proposition (8.4)

FC09-C03-U129 · Chapter III, §8, source L11206 · not formalized

(8.4) Proposition. \(\chi(a) = \chi(i_*L(a)).\)