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

FC09 — Neukirch, Algebraic Number Theory.

This chapter contains 54 definitions, 5 theorems, 53 propositions, 2 lemmas, 8 corollaries, 4 examples, 6 conventions and 3 other statements.

Of the 135 statements checked against Lean, 32 are formalized somewhere and 103 are not.

Status	Statements	Share	What it means
not formalized	103	76%	A documented search found no Lean statement of it anywhere.
in Mathlib	31	23%	Mathlib states and proves it.
in lean-categories	1	1%	This repository states and proves it.
checked in total	135

Which versions of Lean and Mathlib were searched

Canonical source block: FC09 Neukirch Chapter II, FC09-C02-U001–FC09-C02-U135, in canonical source-ID order from Foundational corpus units FC09 Neukirch. The generator retrieves all 135 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/ForMathlib/DenseIntegralCompletion.lean is a material project-owned owner: its compatible quotient-power equivalences and inverse-limit/completed-valuation-ring comparison, specialized through the pinned rational height-one-prime/PadicInt equivalence, close U025 as project-existing. Other project p-adic/local-global wrappers do not close an additional C02 bundle beyond the pinned owners recorded here.
Pinned Mathlib is P=db584cd6d46c92f209a44c0f1c829460d327499d, Lean 4.33.0, Apache-2.0. Native coverage is strongest for the Cauchy construction of ℚ_p, p-adic valuations and ℤ_p ideals, absolute-value equivalence/weak approximation/Ostrowski, valuation rings and DVRs, generic completion, finite-dimensional topology and spectral norms, nonarchimedean local fields, the p-adic factorial formula, Krull topology/infinite Galois correspondence, fixed fields, and the valuation-subring inertia kernel.
Current Mathlib was checked at H=71a80585ee495fc24472fd0eaffc89d94e4fd8d6. Targeted current-tree and open-work searches were run for the unresolved Newton-polygon, henselian-extension, local-field classification, valuation-extension, ramification, and higher-ramification bundles. The current Mathlib/RingTheory/Valuation/RamificationGroup.lean still explicitly says TODO: Define higher ramification groups in lower numbering; no compatible current/open route was found for U125–U135.
Strict bundle semantics was enforced. In particular, the infinity valuation on k(t) does not earn U015 without its product formula; p-adic residue maps do not earn formal digit/power-series presentations; principal-unit infrastructure does not earn the all-level quotients U041–U042; generic adic-completion infrastructure does not earn U049 because that row also asserts the units inverse limit; simple-root Hensel APIs do not earn the factorization and henselian-characterization rows; ideal-theoretic ramification APIs do not earn the henselian/unramified/tame valued-field bundles; and decomposition/inertia definitions do not earn any source row that also asserts a ramification group, exact sequence, completion isomorphism, or higher ramification theorem.
Short derivations are credited only when all ingredients are exact pinned owners: U024 uses the kernel of toZModPow plus its elementary surjectivity by natural representatives; U033 converts a uniform integer bound to |n|≤1 by applying the bound to powers; U054 combines the spectral-norm uniqueness/constant-term formula with field-norm transitivity. These are direct theorem-level derivations, not partial semantic matches.
All mathlib targets were path/token validated against P, every project-existing target against project baseline A, and the higher-ramification negative check against H.
Route totals for C02: mathlib 31, project-existing 1, package-import 0, reference-port 0, unmatched 103.

Definition / construction

FC09-C02-U001 · Chapter II, §1, source L4146 · not formalized

This point of view suggests the further question: whether not only the “value” of the integer \(f \in Z\) at p, but also the higher derivatives of f can be reasonably defined. In the case of the polynomials \(f(z) \in \mathbb{C}[z]\) , the higher derivatives at the point z = a are given by the coefficients of the expansion \[ f (z) = a _ {0} + a _ {1} (z - a) + \dots + a _ {n} (z - a) ^ {n}, \] and more generally, for rational functions \(f(z) = \frac{g(z)}{h(z)} \in \mathbb{C}(z)\) , with \(g, h \in \mathbb{C}[z]\) , they are defined by the Taylor expansion \[ f (z) = \sum_ {\nu = 0} ^ {\infty} a _ {\nu} (z - a) ^ {\nu}, \] provided there is no pole at z = a, i.e., as long as \((z - a) \nmid h(z)\) . The fact that such an expansion can also be written down, relative to a prime number p in Z, for any rational number \(f \in Q\) as long as it lies in the local ring \[ \mathbb {Z} _ {(p)} = \left\{\frac {g}{h} \mid g, h \in \mathbb {Z}, p \nmid h \right\}, \] leads us to the notion of p-adic number. First, every positive integer \(f \in N\) admits a p-adic expansion \[ f = a _ {0} + a _ {1} p + \dots + a _ {n} p ^ {n}, \] with coefficients \(a_{i}\) in \(\{0,1,\ldots,p-1\}\) , i.e., in a fixed system of representatives of the “field of values” \(\kappa(p)=\mathbb{F}_{p}\) . This representation is clearly unique. It is computed explicitly by successively dividing by p, forming the following system of equations:

Not formalized. Pinned/current Mathlib has the p-adic completion, PadicInt, residue maps and projective-limit universal-property APIs, but this source row uses a stronger formal-digit/power-series model or a bundled quotient/solvability identification not closed by one checked compatible route.

Definition (1.1)

FC09-C02-U002 · Chapter II, §1, source L4194 · not formalized

(1.1) Definition. Fix a prime number \(p\) . A \(p\) -adic integer is a formal infinite series \[ a _ {0} + a _ {1} p + a _ {2} p ^ {2} + \dots , \] where \(0 \leq a_{i} < p\) , for all \(i = 0,1,2,\ldots\) . The set of all \(p\) -adic integers is denoted by \(\mathbb{Z}_{p}\) .

Proposition (1.2)

FC09-C02-U003 · Chapter II, §1, source L4204 · not formalized

(1.2) Proposition. The residue classes \(a \mod p^n \in \mathbb{Z} / p^n\mathbb{Z}\) can be uniquely represented in the form \[ a \equiv a _ {0} + a _ {1} p + a _ {2} p ^ {2} + \dots + a _ {n - 1} p ^ {n - 1} \bmod p ^ {n} \] where \(0 \leq a_{i} < p\) for \(i = 0, \ldots, n - 1\) .

Definition / construction

FC09-C02-U004 · Chapter II, §1, source L4244 · not formalized

We call it the \(p\) -adic expansion of \(f\) .

Definition / construction

FC09-C02-U005 · Chapter II, §1, source L4246 · not formalized

In analogy with the Laurent series \(f(z) = \sum_{\nu = -m}^{\infty} a_{\nu}(z - a)^{\nu}\) , we now extend the domain of \(p\) -adic integers into that of the formal series \[ \sum_ {\nu = - m} ^ {\infty} a _ {\nu} p ^ {\nu} = a _ {- m} p ^ {- m} + \dots + a _ {- 1} p ^ {- 1} + a _ {0} + a _ {1} p + \dots , \] where \(m \in Z\) and \(0 \leq a_{\nu} < p\) . Such series we call simply p-adic numbers and we write \(Q_{p}\) for the set of all these p-adic numbers. If \(f \in Q\) is any rational number, then we write \[ f = \frac {g}{h} p ^ {- m} \quad \text { where } g, h \in \mathbb {Z}, (g h, p) = 1, \] and if \[ a _ {0} + a _ {1} p + a _ {2} p ^ {2} + \dots \] is the \(p\) -adic expansion of \(\frac{g}{h}\) , then we attach to \(f\) the \(p\) -adic number \[ a _ {0} p ^ {- m} + a _ {1} p ^ {- m + 1} + \dots + a _ {m} + a _ {m + 1} p + \dots \in \mathbb {Q} _ {p} \] as its \(p\) -adic expansion. In this way we obtain a canonical mapping \[ \mathbb {Q} \longrightarrow \mathbb {Q} _ {p}, \] which takes \(\mathbb{Z}\) into \(\mathbb{Z}_p\) and is injective. For if \(a, b \in \mathbb{Z}\) have the same \(p\) -adic expansion, then \(a - b\) is divisible by \(p^n\) for every \(n\) , and hence \(a = b\) . We now identify \(\mathbb{Q}\) with its image in \(\mathbb{Q}_p\) , so that we may write \(\mathbb{Q} \subseteq \mathbb{Q}_p\) and \(\mathbb{Z} \subseteq \mathbb{Z}_p\) . Thus, for every rational number \(f \in \mathbb{Q}\) , we obtain an identity \[ f = \sum_ {\nu = - m} ^ {\infty} a _ {\nu} p ^ {\nu}. \]

Example / comparison

FC09-C02-U006 · Chapter II, §1, source L4286 · not formalized

Examples: a) \(-1 = (p - 1) + (p - 1)p + (p - 1)p^{2} + \cdots\) . In fact, we have \[ - 1 = (p - 1) + (p - 1) p + \dots + (p - 1) p ^ {n - 1} - p ^ {n}, \] hence \(-1 \equiv (p - 1) + (p - 1)p + \cdots + (p - 1)p^{n-1} \mod p^n\) . b) \(\frac{1}{1-p}=1+p+p^{2}+\cdots.\) In fact, hence \[ \begin{array}{c} 1 = (1 + p + \dots + p ^ {n - 1}) (1 - p) + p ^ {n}, \\ \frac {1}{1 - p} \equiv 1 + p + \dots + p ^ {n - 1} \bmod p ^ {n}. \end{array} \]

Definition / construction

FC09-C02-U007 · Chapter II, §1, source L4342 · not formalized

This set is called the projective limit of the rings \(\mathbb{Z} / p^n\mathbb{Z}\) and is denoted by \(\varprojlim_{n}\mathbb{Z} / p^n\mathbb{Z}\) . In other words, we have \[ \varprojlim_ {n} \mathbb {Z} / p ^ {n} \mathbb {Z} = \left\{(x _ {n}) _ {n \in \mathbb {N}} \in \prod_ {n = 1} ^ {\infty} \mathbb {Z} / p ^ {n} \mathbb {Z} \middle | \lambda_ {n} (x _ {n + 1}) = x _ {n}, n = 1, 2, \ldots \right\}. \]

Proposition (1.3)

FC09-C02-U008 · Chapter II, §1, source L4350 · not formalized

(1.3) Proposition. Associating to every \(p\) -adic integer \[ f = \sum_ {\nu = 0} ^ {\infty} a _ {\nu} p ^ {\nu} \] the sequence \((\overline{s}_n)_{n\in \mathbb{N}}\) of residue classes \[ \bar {s} _ {n} = \sum_ {\nu = 0} ^ {n - 1} a _ {\nu} p ^ {\nu} \bmod p ^ {n} \in \mathbb {Z} / p ^ {n} \mathbb {Z}, \] yields a bijection \[ \mathbb {Z} _ {p} \stackrel {{\sim}} {{\longrightarrow}} \varprojlim_ {n} \mathbb {Z} / p ^ {n} \mathbb {Z}. \]

Definition / construction

FC09-C02-U009 · Chapter II, §1, source L4368 · after FC09-C02-U003 · not formalized

The proof is an immediate consequence of proposition (1.2). The projective limit \(\varprojlim Z/p^{n}Z\) offers the advantage of being clearly a ring. In fact, it is a subring of the direct product \(\prod_{n=1}^{\infty}Z/p^{n}Z\) where addition and multiplication are defined componentwise. We identify \(Z_{p}\) with \(\varprojlim Z/p^{n}Z\) and obtain the ring of p-adic integers \(Z_{p}\) . Since every element \(f \in \mathbb{Q}_p\) admits a representation \[ f = p ^ {- m} g \] with \(g \in Z_{p}\) , addition and multiplication extend from \(Z_{p}\) to \(Q_{p}\) and \(Q_{p}\) becomes the field of fractions of \(Z_{p}\) .

Proposition (1.4)

FC09-C02-U010 · Chapter II, §1, source L4416 · not formalized

(1.4) Proposition. Let \(F(x_{1},\ldots ,x_{n})\) be a polynomial with integer coefficients, and fix a prime number \(p\) . The congruence \[ F (x _ {1}, \dots , x _ {n}) \equiv 0 \bmod p ^ {\nu} \] is solvable for arbitrary \(\nu \geq 1\) if and only if the equation \[ F (x _ {1}, \dots , x _ {n}) = 0 \] is solvable in \(p\) -adic integers.

Definition / construction

FC09-C02-U011 · Chapter II, §2, source L4524 · in Mathlib

The \(p\) -adic absolute value \(|_{p}\) is defined as follows. Let \(a = \frac{b}{c}\) , \(b, c \in \mathbb{Z}\) be a nonzero rational number. We extract from \(b\) and from \(c\) as high a power of the prime number \(p\) as possible, \[ a = p ^ {m} \frac {b ^ {\prime}}{c ^ {\prime}}, (b ^ {\prime} c ^ {\prime}, p) = 1,\tag{2} \] and we put \[ | a | _ {p} = \frac {1}{p ^ {m}}. \]

Formalized. Mathlib/NumberTheory/Padics/PadicNorm.lean::padicNorm, padicNorm_p_of_prime — padicNorm is the p-adic absolute value on ℚ, normalized by |p|_p=p⁻¹.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition / construction

FC09-C02-U012 · Chapter II, §2, source L4540 · in Mathlib

The exponent \(m\) in the representation (2) of the number \(a\) is denoted by \(v_{p}(a)\) , and one puts formally \(v_{p}(0) = \infty\) . This gives the function \[ v _ {p}: \mathbb {Q} \longrightarrow \mathbb {Z} \cup \{\infty \}, \] which is easily checked to satisfy the properties \[ 1) v _ {p} (a) = \infty \Longleftrightarrow a = 0, \] \[ 2) v _ {p} (a b) = v _ {p} (a) + v _ {p} (b), \] \[ 3) \quad v _ {p} (a + b) \geq \min \{v _ {p} (a), v _ {p} (b) \}, \] where \(x + \infty = \infty\) , \(\infty + \infty = \infty\) and \(\infty > x\) , for all \(x \in Z\) . The function \(v_{p}\) is called the p-adic exponential valuation of Q. The p-adic absolute value is given by \[ | \mathbf {\Omega} | _ {p}: \mathbb {Q} \longrightarrow \mathbb {R}, a \longmapsto | a | _ {p} = p ^ {- v _ {p} (a)}. \]

Formalized. Mathlib/NumberTheory/Padics/PadicVal/Basic.lean::padicValRat, padicValRat.mul; Mathlib/NumberTheory/Padics/PadicNorm.lean::padicNorm — The rational p-adic valuation has the additive valuation laws, and padicNorm is its multiplicative p^{-v_p} encoding.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Proposition (2.1)

FC09-C02-U013 · Chapter II, §2, source L4576 · in Mathlib

(2.1) Proposition. For every rational number \(a \neq 0\) , one has \[ \prod_ {p} | a | _ {p} = 1, \] where p varies over all prime numbers as well as the symbol \(\infty\) .

Formalized. Mathlib/NumberTheory/NumberField/ProductFormula.lean::NumberField.prod_abs_eq_one; Mathlib/NumberTheory/Padics/HeightOneSpectrum.lean::valuation_equiv_padicValuation, primesEquiv — Specializing the number-field product formula to ℚ and identifying its finite height-one places with p-adic valuations gives the finite-prime factors together with the archimedean factor.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition / construction

FC09-C02-U014 · Chapter II, §2, source L4598 · not formalized

The notation \(||_{\infty}\) for the ordinary absolute value is motivated by the analogy of the field of rational numbers Q with the rational function field \(k(t)\) over a finite field k, with which we started our considerations. Instead of Z, we have inside \(k(t)\) the polynomial ring k[t], the prime ideals \(p \neq 0\) of which are given by the monic irreducible polynomials \(p(t) \in k[t]\) . For every such p, one defines an absolute value \[ \mid \mid_ {\mathfrak {p}}: k (t) \longrightarrow \mathbb {R} \] as follows. Let \(f(t) = \frac{g(t)}{h(t)}\) , \(g(t), h(t) \in k[t]\) be a nonzero rational function. We extract from \(g(t)\) and \(h(t)\) the highest possible power of the irreducible polynomial \(p(t)\) , \[ f (t) = p (t) ^ {m} \frac {\tilde {g} (t)}{\tilde {h} (t)}, (\tilde {g} \tilde {h}, p) = 1, \] and put \[ v _ {\mathfrak {p}} (f) = m, \quad | f | _ {\mathfrak {p}} = q _ {\mathfrak {p}} ^ {- v _ {\mathfrak {p}} (f)}, \] where \(q_{p} = q^{d_{p}}\) , \(d_{p}\) being the degree of the residue class field of p over k and q a fixed real number > 1. Furthermore we put \(v_{\mathfrak{p}}(0) = \infty\) and \(|0|_{\mathfrak{p}} = 0\) , and obtain for \(v_{\mathfrak{p}}\) and \(| \mid_{\mathfrak{p}}\) the same conditions 1), 2), 3) as for \(v_{p}\) and \(| \mid_{p}\) above. In the case \(\mathfrak{p} = (t - a)\) for \(a \in k\) , the valuation \(v_{\mathfrak{p}}(f)\) is clearly the order of the zero, resp. pole, of the function \(f = f(t)\) at t = a.

Definition / construction

FC09-C02-U015 · Chapter II, §2, source L4618 · after FC09-C02-U013 · not formalized

But for the function field \(k(t)\) , there is one more exponential valuation \[ v _ {\infty}: k (t) \longrightarrow \mathbb {Z} \cup \{\infty \}, \] namely \[ v _ {\infty} (f) = \deg (h) - \deg (g), \] where \(f = \frac{g}{h} \neq 0\) , \(g, h \in k[t]\) . It describes the order of zero, resp. pole, of \(f(t)\) at the point at infinity \(\infty\) , i.e., the order of zero, resp. pole, of the function \(f(1/t)\) at the point t = 0. It is associated to the prime ideal \(\mathfrak{p} = (1/t)\) of the ring \(k[1/t] \subseteq k(t)\) in the same way as the exponential valuations \(v_{\mathfrak{p}}\) are associated to the prime ideals \(\mathfrak{p}\) of \(k[t]\) . Putting \[ | f | _ {\infty} = q ^ {- v _ {\infty} (f)}, \] the unique factorization in \(k(t)\) yields, as in (2.1) above, the formula \[ \prod_ {\mathfrak {p}} | f | _ {\mathfrak {p}} = 1, \] where p varies over the prime ideals of \(k[t]\) as well as the symbol \(\infty\) , which now denotes the point at infinity (see chap. I, §14, p. 95).

Definition / construction

FC09-C02-U016 · Chapter II, §2, source L4648 · in Mathlib

A Cauchy sequence with respect to \(| \mid_{p}\) is by definition a sequence \(\{x_{n}\}\) of rational numbers such that for every \(\varepsilon > 0\) , there exists a positive integer \(n_{0}\) satisfying \[ \left| x _ {n} - x _ {m} \right| _ {p} < \varepsilon \quad \text {for all} \quad n, m \geq n _ {0}. \]

Formalized. Mathlib/Topology/UniformSpace/Cauchy.lean::def CauchySeq, cauchySeq_iff — Mathlib’s CauchySeq is the standard uniform/metric Cauchy condition used in the source.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Example / comparison

FC09-C02-U017 · Chapter II, §2, source L4654 · not formalized

Example: Every formal series \[ \sum_ {\nu = 0} ^ {\infty} a _ {\nu} p ^ {\nu}, \quad 0 \leq a _ {\nu} < p, \] provides a Cauchy sequence via its partial sums \[ x _ {n} = \sum_ {\nu = 0} ^ {n - 1} a _ {\nu} p ^ {\nu}, \] because for \(n > m\) one has \[ \left| x _ {n} - x _ {m} \right| _ {p} = \left| \sum_ {\nu = m} ^ {n - 1} a _ {\nu} p ^ {\nu} \right| _ {p} \leq \max _ {m \leq \nu < n} \left\{\left| a _ {\nu} p ^ {\nu} \right| _ {p} \right\} \leq \frac {1}{p ^ {m}}. \]

Definition / construction

FC09-C02-U018 · Chapter II, §2, source L4672 · not formalized

A sequence \(\{x_{n}\}\) in Q is called a nullsequence with respect to \(|_{p}\) if \(|x_{n}|_{p}\) is a sequence converging to 0 in the usual sense.

Example / comparison

FC09-C02-U019 · Chapter II, §2, source L4674 · not formalized

Example: 1, \(p, p^2, p^3, \ldots\)

Definition / construction

FC09-C02-U020 · Chapter II, §2, source L4676 · in Mathlib

The Cauchy sequences form a ring R, the nullsequences form a maximal ideal m, and we define afresh the field of p-adic numbers to be the residue class field \[ \mathbb {Q} _ {p} := R / \mathfrak {m}. \] We embed \(\mathbb{Q}\) in \(\mathbb{Q}_p\) by associating to every element \(a \in \mathbb{Q}\) the residue class of the constant sequence \((a, a, a, \ldots)\) . The \(p\) -adic absolute value \(| \mid_{p}\) on \(\mathbb{Q}\) is extended to \(\mathbb{Q}_p\) by giving the element \(x = \{x_n\} \mod \mathfrak{m} \in R / \mathfrak{m}\) the absolute value \[ | x | _ {p} := \lim _ {n \rightarrow \infty} | x _ {n} | _ {p} \in \mathbb {R}. \] This limit exists because \(\{|x_n|_p\}\) is a Cauchy sequence in \(\mathbb{R}\) , and it is independent of the choice of the sequence \(\{x_n\}\) within its class mod \(\mathfrak{m}\) because any \(p\) -adic nullsequence \(\{y_n\} \in \mathfrak{m}\) satisfies of course \(\lim_{n\to \infty}|y_n|_p = 0\) .

Formalized. Mathlib/NumberTheory/Padics/PadicNumbers.lean::def Padic, def mk, coe_inj, padicNormE — Padic is defined as the quotient Cauchy completion of ℚ for padicNorm; mk is the quotient map, rational coercion is injective, and padicNormE is the extended absolute value.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition / construction

FC09-C02-U021 · Chapter II, §2, source L4690 · in Mathlib

The \(p\) -adic exponential valuation \(\nu_{p}\) on \(\mathbb{Q}\) extends to an exponential valuation \[ v _ {p}: \mathbb {Q} _ {p} \longrightarrow \mathbb {Z} \cup \{\infty \}. \] In fact, if \(x \in \mathbb{Q}_p\) is the class of the Cauchy sequence \(\{x_n\}\) where \(x_n \neq 0\) , then \[ v _ {p} (x _ {n}) = - \log_ {p} | x _ {n} | _ {p} \] either diverges to \(\infty\) or is a Cauchy sequence in \(\mathbb{Z}\) which eventually must become constant for large \(n\) because \(\mathbb{Z}\) is discrete. We put \[ v _ {p} (x) = \lim _ {n \rightarrow \infty} v _ {p} (x _ {n}) = v _ {p} (x _ {n}) \quad \text { for } n \geq n _ {0}. \] Again we find for all \(x \in \mathbb{Q}_p\) that \[ | x | _ {p} = p ^ {- v _ {p} (x)}. \]

Formalized. Mathlib/NumberTheory/Padics/PadicNumbers.lean::def valuation, valuation_ratCast, norm_eq_zpow_neg_valuation, def addValuation, def mulValuation, comap_mulValuation_eq_padicValuation — The pinned p-adic valuation extends the rational one, has bundled additive/multiplicative forms, and norm_eq_zpow_neg_valuation is exactly the norm relation.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Proposition (2.2)

FC09-C02-U022 · Chapter II, §2, source L4716 · in Mathlib

(2.2) Proposition. The field \(\mathbb{Q}_p\) of \(p\) -adic numbers is complete with respect to the absolute value \(|\cdot|_p\) , i.e., every Cauchy sequence in \(\mathbb{Q}_p\) converges with respect to \(|\cdot|_p\) .

Formalized. Mathlib/NumberTheory/Padics/PadicNumbers.lean::instance : CompleteSpace ℚ_[p] — ℚ_[p] carries the pinned CompleteSpace instance.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Proposition (2.3)

FC09-C02-U023 · Chapter II, §2, source L4732 · in Mathlib

(2.3) Proposition. The set \[ \mathbb {Z} _ {p} := \left\{x \in \mathbb {Q} _ {p} \mid | x | _ {p} \leq 1 \right\} \] is a subring of \(\mathbb{Q}_p\) . It is the closure with respect to \(|\cdot|_p\) of the ring \(\mathbb{Z}\) in the field \(\mathbb{Q}_p\) .

Formalized. Mathlib/NumberTheory/Padics/PadicIntegers.lean::def PadicInt, def subring, mem_subring_iff, completeSpace; Mathlib/NumberTheory/Padics/RingHoms.lean::denseRange_intCast — PadicInt is exactly the norm-≤1 subring of ℚ_p, is complete (hence closed in the Hausdorff ambient field), and the integer cast has dense range.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Proposition (2.4)

FC09-C02-U024 · Chapter II, §2, source L4762 · in Mathlib

(2.4) Proposition. The nonzero ideals of the ring \(Z_{p}\) are the principal ideals \[ p ^ {n} \mathbb {Z} _ {p} = \left\{x \in \mathbb {Q} _ {p} \mid v _ {p} (x) \geq n \right\}, \] with \(n\geq 0\) , and one has \[ \mathbb {Z} _ {p} / p ^ {n} \mathbb {Z} _ {p} \cong \mathbb {Z} / p ^ {n} \mathbb {Z}. \]

Formalized. Mathlib/NumberTheory/Padics/PadicIntegers.lean::ideal_eq_span_pow_p, maximalIdeal_eq_span_p; Mathlib/NumberTheory/Padics/RingHoms.lean::toZModPow, ker_toZModPow — Every nonzero ideal is generated by p^n. toZModPow has kernel (p^n); surjectivity follows by lifting a residue class via its natural-number representative, so the first isomorphism theorem gives ℤ_p/(p^n) ≃ ZMod(p^n).

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Proposition (2.5)

FC09-C02-U025 · Chapter II, §2, source L4836 · in lean-categories

(2.5) Proposition. The homomorphism \[ \mathbb {Z} _ {p} \longrightarrow \varprojlim_ {n} \mathbb {Z} / p ^ {n} \mathbb {Z} \] is an isomorphism.

Formalized. LeanCategories/ForMathlib/DenseIntegralCompletion.lean::quotientPowEquivAdicCompletionIntegers, adicCompletionEquivAdicCompletionIntegers, adicCompletionHomeomorphAdicCompletionIntegers; Mathlib/NumberTheory/Padics/HeightOneSpectrum.lean::adicCompletionIntegers.padicIntEquiv, primesEquiv — The project proves that a height-one adic inverse-limit completion is the completed valuation ring and identifies all quotient powers compatibly; specializing R=ℤ,K=ℚ and composing with the pinned PadicInt equivalence gives Neukirch’s ℤ_p ≃ lim_n ℤ/p^nℤ.

Searched: A=3b2239e161592472b34e02ad3b7da308f9ce7280; P=db584cd6d46c92f209a44c0f1c829460d327499d

Convention / notation

FC09-C02-U026 · Chapter II, §2, source L4884 · not formalized

Another way to introduce the \(p\)-adic numbers: let \(\mathbb{Z}X\) be the ring of formal power series \(\sum_{i=0}^{\infty} a_{i}X^{i}\) with integer coefficients. Then one has the canonical isomorphism of proposition (2.6), \[ \mathbb{Z}_{p} \cong \mathbb{Z}X/(X-p). \]

Proposition (2.6)

FC09-C02-U027 · Chapter II, §2, source L4886 · not formalized

(2.6) Proposition. There is a canonical isomorphism \[ \mathbb {Z} _ {p} \cong \mathbb {Z} [ [ X ] ] / (X - p). \]

Definition (3.1)

FC09-C02-U028 · Chapter II, §3, source L4974 · in Mathlib

(3.1) Definition. A valuation of a field \(K\) is a function \[ | \quad |: K \to \mathbb {R} \] enjoying the properties (i) \(|x|\geq 0\) , and \(|x| = 0\Longleftrightarrow x = 0,\) (ii) \(|xy| = |x||y|\) , (iii) \(|x + y| \leq |x| + |y|\) “triangle inequality”.

Formalized. Mathlib/Algebra/Order/AbsoluteValue/Basic.lean::structure AbsoluteValue — AbsoluteValue packages multiplicativity, the triangle inequality and positivity exactly as the source multiplicative valuation.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition / construction

FC09-C02-U029 · Chapter II, §3, source L4988 · in Mathlib

We tacitly exclude in the sequel the case where \(| \mid |\) is the trivial valuation of \(K\) which satisfies \(|x| = 1\) for all \(x \neq 0\) . Defining the distance between two points \(x, y \in K\) by \[ d (x, y) = | x - y | \] makes K into a metric space, and hence in particular a topological space.

Formalized. Mathlib/Analysis/Normed/Field/WithAbs.lean::WithAbs, normedField; Mathlib/Analysis/AbsoluteValue/Equivalence.lean::IsNontrivial — AbsoluteValue.IsNontrivial expresses nontriviality and WithAbs v equips the field with the norm/metric induced by v.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition (3.2)

FC09-C02-U030 · Chapter II, §3, source L4996 · in Mathlib

(3.2) Definition. Two valuations of \(K\) are called equivalent if they define the same topology on \(K\) .

Formalized. Mathlib/Analysis/AbsoluteValue/Equivalence.lean::isEquiv_iff_isHomeomorph — isEquiv_iff_isHomeomorph identifies equivalence of absolute values with equality of their induced topologies via the identity homeomorphism.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Proposition (3.3)

FC09-C02-U031 · Chapter II, §3, source L4998 · in Mathlib

(3.3) Proposition. Two valuations \(|_{1}\) and \(|_{2}\) on \(K\) are equivalent if and only if there exists a real number \(s > 0\) such that one has \[ | x | _ {1} = | x | _ {2} ^ {s} \] for all \(x \in K\) .

Formalized. Mathlib/Analysis/AbsoluteValue/Equivalence.lean::isEquiv_iff_exists_rpow_eq — This is the pinned exact characterization v∼w iff w(x)=v(x)^c for some c>0.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Approximation Theorem (3.4)

FC09-C02-U032 · Chapter II, §3, source L5034 · in Mathlib

(3.4) Approximation Theorem. Let \(|_{1}, \ldots, |_{n}\) be pairwise inequivalent valuations of the field \(K\) and let \(a_1, \ldots, a_n \in K\) be given elements. Then for every \(\varepsilon > 0\) there exists an \(x \in K\) such that \[ \left| x - a _ {i} \right| _ {i} < \varepsilon \quad \text { for all } i = 1, \dots , n. \]

Formalized. Mathlib/Analysis/AbsoluteValue/Equivalence.lean::denseRange_algebraMap_pi — The diagonal map into a finite product of pairwise inequivalent nontrivial valued fields has dense range, which is the weak approximation theorem in the source.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition (3.5)

FC09-C02-U033 · Chapter II, §3, source L5064 · in Mathlib

(3.5) Definition. The valuation | | is called nonarchimedean if \(|n|\) stays bounded, for all \(n \in N\) . Otherwise it is called archimedean.

Formalized. Mathlib/Analysis/Normed/Field/Ultra.lean::isUltrametricDist_iff_forall_norm_natCast_le_one — The pinned criterion says nonarchimedean/ultrametric is equivalent to |n|≤1 for every natural n. Neukirch’s apparently weaker boundedness condition is equivalent by applying a uniform bound to n^k and taking kth powers.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Proposition (3.6)

FC09-C02-U034 · Chapter II, §3, source L5066 · in Mathlib

(3.6) Proposition. The valuation \(|\) is nonarchimedean if and only if it satisfies the strong triangle inequality \[ | x + y | \leq \max \left\{| x |, | y | \right\}. \]

Formalized. Mathlib/Analysis/Normed/Group/Ultra.lean::isUltrametricDist_iff_isNonarchimedean_norm — The pinned equivalence is exactly the ultrametric inequality |x+y|≤max(|x|,|y|).

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Proposition (3.7)

FC09-C02-U035 · Chapter II, §3, source L5108 · in Mathlib

(3.7) Proposition. Every valuation of \(\mathbb{Q}\) is equivalent to one of the valuations \(| |_{p}\) or \(| |_{\infty}\) .

Formalized. Mathlib/NumberTheory/Ostrowski.lean::equiv_real_or_padic — Every nontrivial absolute value on ℚ is equivalent to the real absolute value or a p-adic one.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition / construction

FC09-C02-U036 · Chapter II, §3, source L5182 · after FC09-C02-U028 · not formalized

A function v on K with these properties is called an exponential valuation of K. We exclude the case of the trivial function \(v(x) = 0\) for \(x \neq 0\) , \(v(0) = \infty\) . Two exponential valuations \(v_{1}\) and \(v_{2}\) of K are called equivalent if \(v_{1} = sv_{2}\) , for some real number s > 0. For every exponential valuation v we obtain a valuation in the sense of (3.1) by putting \[ | x | = q ^ {- v (x)}, \] for some fixed real number q > 1. To distinguish it from v, we call | | an associated multiplicative valuation, or absolute value. Replacing v by an equivalent valuation sv (i.e., replacing q by \(q' = q^{s}\) ) changes | | into the equivalent multiplicative valuation | \(|^{s}\) . The conditions (i), (ii), (iii) immediately imply the proposition (3.8) on the subset of elements of absolute value at most one.

Not formalized. Pinned/current Mathlib has absolute values, valuation subrings, DVRs and completion infrastructure, but this row contains a stronger classification, graded-quotient, higher-unit, residue-preservation, Laurent-series, or simultaneous inverse-limit statement not exported as a source-complete route.

Proposition (3.8)

FC09-C02-U037 · Chapter II, §3, source L5190 · in Mathlib

(3.8) Proposition. The subset \[ \mathcal {O} = \left\{x \in K \mid v (x) \geq 0 \right\} = \left\{x \in K \mid | x | \leq 1 \right\} \] is a ring with group of units \[ \mathcal {O} ^ {*} = \left\{x \in K \mid v (x) = 0 \right\} = \left\{x \in K \mid | x | = 1 \right\} \] and the unique maximal ideal \[ \mathfrak {p} = \left\{x \in K \mid v (x) > 0 \right\} = \left\{x \in K \mid | x | < 1 \right\}. \] \(\mathcal{O}\) is an integral domain with field of fractions \(K\) and has the property that, for every \(x \in K\) , either \(x \in \mathcal{O}\) or \(x^{-1} \in \mathcal{O}\) .

Formalized. Mathlib/RingTheory/Valuation/ValuationSubring.lean::mem_or_inv_mem, valuation_le_one_iff, valuation_eq_one_iff, valuation_lt_one_iff, IsFractionRing A K — A valuation subring is exactly {v≤1}; its units are valuation-one elements, its maximal ideal is v<1, every x or x⁻¹ lies in it, and its fraction field is K. This is the multiplicative encoding of Neukirch’s v≥0/v=0/v>0 clauses.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition / construction

FC09-C02-U038 · Chapter II, §3, source L5208 · in Mathlib

Such a ring is called a valuation ring. Its only maximal ideal is \(\mathfrak{p} = \{x \in \mathcal{O} \mid x^{-1} \notin \mathcal{O}\}\) . The field \(\mathcal{O} / \mathfrak{p}\) is called the residue class field of \(\mathcal{O}\) . A valuation ring is always integrally closed. For if \(x \in K\) is integral over \(\mathcal{O}\) , then there is an equation \[ x ^ {n} + a _ {1} x ^ {n - 1} + \dots + a _ {n} = 0 \] with \(a_{i} \in O\) and the hypothesis \(x \notin O\) , so that \(x^{-1} \in O\) , would imply the contradiction \(x = -a_{1} - a_{2}x^{-1} - \cdots - a_{n}(x^{-1})^{n-1} \in O\) .

Formalized. Mathlib/RingTheory/Valuation/ValuationSubring.lean::ValuationSubring, mem_or_inv_mem; Mathlib/RingTheory/Valuation/LocalSubring.lean::IsIntegrallyClosed V — The valuation-subring interface supplies the unique local maximal ideal/residue-field structure and the pinned integrally-closed instance.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition / construction

FC09-C02-U039 · Chapter II, §3, source L5216 · in Mathlib

An exponential valuation \(v\) is called discrete if it admits a smallest positive value \(s\) . In this case, one finds \[ v (K ^ {*}) = s \mathbb {Z}. \] It is called normalized if s = 1. Dividing by s we may always pass to a normalized valuation without changing the invariants \(O, O^{*}, p\) . Having done so, an element \[ \pi \in \mathcal {O} \quad \text { such that } \quad v (\pi) = 1 \] is a prime element, and every element \(x \in K^{*}\) admits a unique representation \[ x = u \pi^ {m} \] with \(m \in \mathbb{Z}\) and \(u \in \mathcal{O}^*\) . For if \(v(x) = m\) , then \(v(x\pi^{-m}) = 0\) , hence \(u = x\pi^{-m} \in \mathcal{O}^*\) .

Formalized. Mathlib/RingTheory/Valuation/Discrete/Basic.lean::class IsRankOneDiscrete, def IsUniformizer, structure Uniformizer; Mathlib/RingTheory/DiscreteValuationRing/Basic.lean::exists_units_eq_smul_zpow_of_irreducible — Rank-one discrete valuations and uniformizers are first-class; in the fraction field of the resulting DVR every nonzero element is uniquely controlled by an integral uniformizer exponent, with the exported existence normal form x=u·π^n and uniqueness supplied by the valuation.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Proposition (3.9)

FC09-C02-U040 · Chapter II, §3, source L5236 · not formalized

(3.9) Proposition. If \(v\) is a discrete exponential valuation of \(K\) , then \[ \mathcal {O} = \left\{x \in K \mid v (x) \geq 0 \right\} \] is a principal ideal domain, hence a discrete valuation ring (see I, (11.3)). Suppose v is normalized. Then the nonzero ideals of \(\sigma\) are given by \[ \mathfrak {p} ^ {n} = \pi^ {n} \mathcal {O} = \left\{x \in K \mid v (x) \geq n \right\}, \quad n \geq 0, \] where \(\pi\) is a prime element, i.e., \(v(\pi) = 1\) . One has \[ \mathfrak {p} ^ {n} / \mathfrak {p} ^ {n + 1} \cong \mathcal {O} / \mathfrak {p}. \]

Definition / construction

FC09-C02-U041 · Chapter II, §3, source L5264 · not formalized

In a discretely valued field \(K\) the chain \[ \mathcal {O} \supseteq \mathfrak {p} \supseteq \mathfrak {p} ^ {2} \supseteq \mathfrak {p} ^ {3} \supseteq \dots \] consisting of the ideals of the valuation ring \(\mathcal{O}\) forms a basis of neighbourhoods of the zero element. Indeed, if \(v\) is a normalized exponential valuation and \(| = q^{-v} (q > 1)\) an associated multiplicative valuation, then \[ \mathfrak {p} ^ {n} = \left\{x \in K \mid | x | < \frac {1}{q ^ {n - 1}} \right\}. \] As a basis of neighbourhoods of the element 1 of \(K^*\) , we obtain in the same way the descending chain \[ \mathcal {O} ^ {*} = U ^ {(0)} \supseteq U ^ {(1)} \supseteq U ^ {(2)} \supseteq \dots \] of subgroups \[ U ^ {(n)} = 1 + \mathfrak {p} ^ {n} = \left\{x \in K ^ {*} \mid | 1 - x | < \frac {1}{q ^ {n - 1}} \right\}, \quad n > 0, \] of \(\mathcal{O}^*\) . (Observe that \(1 + \mathfrak{p}^n\) is closed under multiplication and that, if \(x \in U^{(n)}\) , then so is \(x^{-1}\) because \(|1 - x^{-1}| = |x|^{-1}|x - 1| = |1 - x| < \frac{1}{q^{n-1}}\) .) \(U^{(n)}\) is called the n-th higher unit group and \(U^{(1)}\) the group of principal units. Regarding the successive quotients of the chain of higher unit groups, we have the proposition (3.10): \(\mathcal{O}^{*}/U^{(n)} \cong (\mathcal{O}/\mathfrak{p}^{n})^{*}\) and \(U^{(n)}/U^{(n+1)} \cong \mathcal{O}/\mathfrak{p}\) for \(n \geq 1\).

Proposition (3.10)

FC09-C02-U042 · Chapter II, §3, source L5292 · not formalized

(3.10) Proposition. \(\mathcal{O}^{*} / U^{(n)} \cong (\mathcal{O} / \mathfrak{p}^{n})^{*}\) and \(U^{(n)} / U^{(n + 1)} \cong \mathcal{O} / \mathfrak{p}\) , for \(n \geq 1\) .

Definition (4.1)

FC09-C02-U043 · Chapter II, §4, source L5334 · in Mathlib

(4.1) Definition. A valued field \((K, | |)\) is called complete if every Cauchy sequence \(\{a_{n}\}_{n\in\mathbb{N}}\) in K converges to an element \(a \in K\) , i.e., \[ \lim _ {n \to \infty} | a _ {n} - a | = 0. \] Here, as usual, we call \(\{a_n\}_{n\in \mathbb{N}}\) a Cauchy sequence if for every \(\varepsilon >0\) there exists \(N\in \mathbb{N}\) such that \[ \left| a _ {n} - a _ {m} \right| < \varepsilon \quad \text {for all} \quad n, m \geq N. \]

Formalized. Mathlib/Topology/UniformSpace/Cauchy.lean::class CompleteSpace, CauchySeq.tendsto_limUnder — CompleteSpace says every Cauchy filter converges; the sequence theorem gives the source metric formulation.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition / construction

FC09-C02-U044 · Chapter II, §4, source L5346 · in Mathlib

From any valued field \((K, | |)\) we get a complete valued field \((\widehat{K}, | |)\) by the process of completion. This completion is obtained in the same way as the field of real numbers is constructed from the field of rational numbers. Take the ring \(R\) of all Cauchy sequences of \((K, | |)\) , consider therein the maximal ideal \(\mathfrak{m}\) of all nullsequences with respect to \(| |\) , and define \[ \widehat {K} = R / \mathfrak {m}. \] One embeds the field \(K\) into \(\widehat{K}\) by sending every \(a \in K\) to the class of the constant Cauchy sequence \((a, a, a, \ldots)\) . The valuation \(| \mid |\) is extended from \(K\) to \(\widehat{K}\) by giving the element \(a \in \widehat{K}\) which is represented by the Cauchy sequence \(\{a_n\}_{n \in \mathbb{N}}\) the absolute value \[ | a | = \lim _ {n \rightarrow \infty} | a _ {n} |. \] This limit exists because \(|a_n| - |a_m| \leq |a_n - a_m|\) implies that \(|a_n|\) is a Cauchy sequence of real numbers. As in the case of the field of real numbers, one proves that \(\widehat{K}\) is complete with respect to the extended \(|\) , and that each \(a \in \widehat{K}\) is a limit of a sequence \(\{a_n\}\) in \(K\) . Finally one proves the uniqueness of the completion \((\widehat{K}, | \mid)\) : if \((\widehat{K}', | \mid')\) is another complete valued field that contains \((K, | \mid)\) as a dense subfield, then mapping \[ | | - \lim _ {n \rightarrow \infty} a _ {n} \quad \longmapsto \quad | | ^ {\prime} - \lim _ {n \rightarrow \infty} a _ {n} \] gives a \(K\) -isomorphism \(\sigma : \widehat{K} \to \widehat{K}'\) such that \(|a| = |\sigma a|^{\prime}\) .

Formalized. Mathlib/Analysis/Normed/Field/WithAbs.lean::abbrev Completion, normedField; Mathlib/Topology/UniformSpace/Completion.lean::completeSpace, denseRange_coe, extension_coe, extension_unique — AbsoluteValue.Completion is the Hausdorff completion of the induced normed field; it is complete, the canonical map is dense, and uniformly continuous maps extend uniquely, giving the source uniqueness statement and extension of the absolute value/field operations.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Theorem (4.2)

FC09-C02-U045 · Chapter II, §4, source L5370 · not formalized

(4.2) Theorem (OSTROWSKI). Let K be a field which is complete with respect to an archimedean valuation | |. Then there is an isomorphism \(\sigma\) from K onto R or C satisfying \[ | a | = | \sigma a | ^ {s} \quad \text { for all } \quad a \in K, \] for some fixed \(s \in (0,1]\) .

Proposition (4.3)

FC09-C02-U046 · Chapter II, §4, source L5458 · not formalized

(4.3) Proposition. If \(\mathcal{O} \subseteq K\) , resp. \(\widehat{\mathcal{O}} \subseteq \widehat{K}\) , is the valuation ring of \(v\) , resp. of \(\hat{v}\) , and \(\mathfrak{p}\) , resp. \(\widehat{\mathfrak{p}}\) , is the maximal ideal, then one has \[ \widehat {\mathcal {O}} / \widehat {\mathfrak {p}} \cong \mathcal {O} / \mathfrak {p} \] and, if \(v\) is discrete, one has furthermore \[ \widehat {\mathcal {O}} / \widehat {\mathfrak {p}} ^ {n} \cong \mathcal {O} / \mathfrak {p} ^ {n} \quad f o r \quad n \geq 1. \]

Proposition (4.4)

FC09-C02-U047 · Chapter II, §4, source L5472 · not formalized

(4.4) Proposition. Let \(R \subseteq \mathcal{O}\) be a system of representatives for \(\kappa = \mathcal{O} / \mathfrak{p}\) such that \(0 \in R\) , and let \(\pi \in \mathcal{O}\) be a prime element. Then every \(x \neq 0\) in \(K\) admits a unique representation as a convergent series \[ x = \pi^ {m} (a _ {0} + a _ {1} \pi + a _ {2} \pi^ {2} + \dots) \] where \(a_{i} \in R, a_{0} \neq 0, m \in \mathbb{Z}\) .

Definition / construction

FC09-C02-U048 · Chapter II, §4, source L5502 · not formalized

In the case of the rational function field \(k(t)\) and the valuation \(v_{p}\) attached to a prime ideal \(\mathfrak{p} = (t - a)\) of \(k[t]\) (see §2), we may take as a system of representatives R the field of coefficients k itself. The completion then turns out to be the field of formal power series \(k((x))\) , x = t - a, consisting of all formal Laurent series \[ f (t) = (t - a) ^ {m} (a _ {0} + a _ {1} (t - a) + a _ {2} (t - a) ^ {2} + \dots), \] with \(a_{i} \in k\) and \(m \in Z\) .

Proposition (4.5)

FC09-C02-U049 · Chapter II, §4, source L5536 · not formalized

(4.5) Proposition. The canonical mapping \[ \mathcal {O} \longrightarrow \varprojlim_ {n} \mathcal {O} / \mathfrak {p} ^ {n} \] is an isomorphism and a homeomorphism. The same is true for the mapping \[ \mathcal {O} ^ {*} \longrightarrow \varprojlim_ {n} \mathcal {O} ^ {*} / U ^ {(n)}. \]

Definition / construction

FC09-C02-U050 · Chapter II, §4, source L5580 · not formalized

Let \(K\) again be a field which is complete with respect to a nonarchimedean valuation \(|\cdot|\) . Let \(\mathcal{O}\) be the corresponding valuation ring with maximal ideal \(\mathfrak{p}\) and residue class field \(\kappa = \mathcal{O} / \mathfrak{p}\) . We call a polynomial \(f(x) = a_0 + a_1x + \dots + a_nx^n \in \mathcal{O}[x]\) primitive if \(f(x) \not\equiv 0 \mod \mathfrak{p}\) , i.e., if \[ | f | = \max \left\{\left| a _ {0} \right|, \dots , \left| a _ {n} \right| \right\} = 1. \]

Not formalized. Pinned/current Mathlib has Hensel, spectral-norm, finite-dimensional and local-field infrastructure, but this complete source bundle contains a stronger root/factorization, logarithm-exponential, classification, Newton-polygon, or henselian-extension assertion not exported compatibly.

Hensel’s Lemma (4.6)

FC09-C02-U051 · Chapter II, §4, source L5586 · not formalized

(4.6) Hensel’s Lemma. If a primitive polynomial \(f(x) \in \mathcal{O}[x]\) admits modulo \(\mathfrak{p}\) a factorization \[ f (x) \equiv \overline {{{{g}}}} (x) \overline {{{{h}}}} (x) \bmod {\mathfrak {p}} \] into relatively prime polynomials \(\overline{g},\overline{h}\in \kappa [x]\) , then \(f(x)\) admits a factorization \[ f (x) = g (x) h (x) \] into polynomials \(g, h \in \mathcal{O}[x]\) such that \(\deg(g) = \deg(\overline{g})\) and \[ g (x) \equiv \overline {{g}} (x) \bmod {\mathfrak {p}} \quad a n d \quad h (x) \equiv \overline {{h}} (x) \bmod {\mathfrak {p}}. \]

Example / comparison

FC09-C02-U052 · Chapter II, §4, source L5670 · not formalized

Example: The polynomial \(x^{p-1}-1\in\mathbb{Z}_{p}[x]\) splits over the residue class field \(Z_{p}/pZ_{p}=F_{p}\) into distinct linear factors. Applying (repeatedly) Hensel’s lemma, we see that it also splits into linear factors over \(Z_{p}\) . We thus obtain the astonishing result that the field \(Q_{p}\) of p-adic numbers contains the \((p-1)\) -th roots of unity. These, together with 0, even form a system of representatives for the residue class field, which is closed under multiplication.

Corollary (4.7)

FC09-C02-U053 · Chapter II, §4, source L5672 · not formalized

(4.7) Corollary. Let the field K be complete with respect to the nonarchimedean valuation \(\mid\mid\) . Then, for every irreducible polynomial \(f(x)=a_{0}+a_{1}x+\cdots+a_{n}x^{n}\in K[x]\) such that \(a_{0}a_{n}\neq0\) , one has \[ | f | = \max \left\{\left| a _ {0} \right|, \left| a _ {n} \right| \right\}. \] In particular, \(a_{n} = 1\) and \(a_0 \in \mathcal{O}\) imply that \(f \in \mathcal{O}[x]\) .

Theorem (4.8)

FC09-C02-U054 · Chapter II, §4, source L5690 · in Mathlib

(4.8) Theorem. Let \(K\) be complete with respect to the valuation \(| \cdot |\) . Then \(| \cdot |\) may be extended in a unique way to a valuation of any given algebraic extension \(L|K\) . This extension is given by the formula \[ | \alpha | = \sqrt [ n ]{\left| N _ {L | K} (\alpha) \right|}, \] when \(L|K\) has finite degree \(n\) . In this case \(L\) is again complete.

Formalized. Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean::spectralNorm_unique_field_norm_ext, spectralNorm_eq_norm_coeff_zero_rpow, instance (priority := 100) completeSpace; Mathlib/RingTheory/Norm/Transitivity.lean::norm_eq_norm_adjoin — The spectral norm is the unique multiplicative absolute value extending a complete nonarchimedean base norm and finite extensions are complete. Combining its minimal-polynomial constant-term formula with transitivity of the field norm yields |x|L=|N{L/K}(x)|_K^(1/[L:K]).

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Proposition (4.9)

FC09-C02-U055 · Chapter II, §4, source L5738 · in Mathlib

(4.9) Proposition. Let \(K\) be complete with respect to the valuation \(| \cdot |\) and let \(V\) be an \(n\) -dimensional normed vector space over \(K\) . Then, for any basis \(v_1, \ldots, v_n\) of \(V\) the maximum norm \[ \left\| x _ {1} v _ {1} + \dots + x _ {n} v _ {n} \right\| = \max \left\{\left| x _ {1} \right|, \dots , \left| x _ {n} \right| \right\} \] is equivalent to the given norm on \(V\) . In particular, \(V\) is complete and the isomorphism \[ K ^ {n} \longrightarrow V, \quad (x _ {1}, \dots , x _ {n}) \longmapsto x _ {1} v _ {1} + \dots + x _ {n} v _ {n}, \] is a homeomorphism.

Formalized. Mathlib/Topology/Algebra/Module/FiniteDimension.lean::def equivFunL, theorem FiniteDimensional.complete; Mathlib/Analysis/Normed/Module/FiniteDimension.lean::continuous_of_finiteDimensional — A finite basis gives a continuous linear equivalence with coordinate space; every linear map between finite-dimensional normed spaces is continuous, giving equivalence of norms, and finite-dimensional spaces over a complete field are complete.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Definition / construction

FC09-C02-U056 · Chapter II, §5, source L5836 · in Mathlib

Among all complete (nonarchimedean) valued fields, those arising as completions of a global field, i.e., of a finite extension of either Q or \(\mathbb{F}_{p}(t)\) , have the most eminent relevance for number theory. The valuation on such a completion is discrete and has a finite residue class field, as we shall see shortly. In contrast to the global fields, all fields which are complete with respect to a discrete valuation and have a finite residue class field are called local fields. For such a local field, the normalized exponential valuation is denoted by \(v_{p}\) , and \(|I_{p}\) denotes the absolute value normalized by \[ | x | _ {\mathfrak {p}} = q ^ {- v _ {\mathfrak {p}} (x)}, \] where q is the cardinality of the residue class field.

Formalized. Mathlib/NumberTheory/LocalField/Basic.lean::class IsNonarchimedeanLocalField, IsDiscreteValuationRing 𝒪[K], Finite 𝓀[K], CompleteSpace K; Mathlib/Topology/Algebra/Valued/LocallyCompact.lean::compactSpace_iff_completeSpace_and_isDiscreteValuationRing_and_finite_residueField — Mathlib’s local-field class is the equivalent locally compact nontrivial valuative formulation and proves exactly that the valuation ring is a complete DVR with finite residue field; the compactness characterization gives the converse DVR/complete/finite-residue package.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Proposition (5.1)

FC09-C02-U057 · Chapter II, §5, source L5844 · in Mathlib

(5.1) Proposition. A local field \(K\) is locally compact. Its valuation ring \(\mathcal{O}\) is compact.

Formalized. Mathlib/NumberTheory/LocalField/Basic.lean::LocallyCompactSpace K, isCompact_closedBall, CompactSpace 𝒪[K] — A nonarchimedean local field is locally compact and its closed unit ball/valuation ring is compact.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Proposition (5.2)

FC09-C02-U058 · Chapter II, §5, source L5850 · not formalized

(5.2) Proposition. The local fields are precisely the finite extensions of the fields \(\mathbb{Q}_p\) and \(\mathbb{F}_p((t))\) .

Definition / construction

FC09-C02-U059 · Chapter II, §5, source L5858 · not formalized

We have just seen that the local fields of characteristic p are the power series fields \(\mathbb{F}_{q}((t))\) , with \(q = p^{f}\) . The local fields of characteristic 0, i.e., the finite extensions \(K|\mathbb{Q}_{p}\) of the fields of p-adic numbers \(Q_{p}\) , are called p-adic number fields. For them one has an exponential function and a logarithm function. In contrast to the real and complex case, however, the former is not defined on all of K, whereas the latter is given on the whole multiplicative group \(K^{*}\) . For the definition of the logarithm we make use of the following fact.

Proposition (5.3)

FC09-C02-U060 · Chapter II, §5, source L5860 · not formalized

(5.3) Proposition. The multiplicative group of a local field \(K\) admits the decomposition \[ K ^ {*} = (\pi) \times \mu_ {q - 1} \times U ^ {(1)}. \] Here \(\pi\) is a prime element, \((\pi) = \{\pi^k \mid k \in \mathbb{Z}\}\) , \(q = \# \kappa\) is the number of elements in the residue class field \(\kappa = \mathcal{O} / \mathfrak{p}\) , and \(U^{(1)} = 1 + \mathfrak{p}\) is the group of principal units.

Proposition (5.4)

FC09-C02-U061 · Chapter II, §5, source L5870 · not formalized

(5.4) Proposition. For a p-adic number field K there is a uniquely determined continuous homomorphism \[ \log : K ^ {*} \to K \] such that \(\log p = 0\) which on principal units \((1 + x) \in U^{(1)}\) is given by the series \[ \log (1 + x) = x - \frac {x ^ {2}}{2} + \frac {x ^ {3}}{3} - \dots . \]

Definition / construction

FC09-C02-U062 · Chapter II, §5, source L5896 · not formalized

For every \(\alpha \in K^{*}\) , choosing a prime element \(\pi\) , we have a unique representation \[ \alpha = \pi^ {v _ {\mathfrak {p}} (\alpha)} \omega (\alpha) \langle \alpha \rangle , \] where \(v_{p} = ev_{p}\) is the normalized valuation of \(K, \omega(\alpha) \in \mu_{q-1}, \langle\alpha\rangle \in U^{(1)}\) . As suggested by the equation \(p = \pi^{e}\omega(p)\langle p\rangle\) , we define \(\log \pi = -\frac{1}{e}\log \langle p\rangle\) and thus obtain the homomorphism \(\log: K^{*} \to K\) by \[ \log \alpha = v _ {\mathfrak {p}} (\alpha) \log \pi + \log \langle \alpha \rangle . \] It is obviously continuous and has the property that \(\log p = 0\) . If \(\lambda : K^* \to K\) is any continuation of \(\log : U^{(1)} \to K\) such that \(\lambda(p) = 0\) , then we find that \(\lambda(\xi) = \frac{1}{q-1} \lambda(\xi^{q-1}) = 0\) for each \(\xi \in \mu_{q-1}\) . It follows that \(0 = e\lambda(\pi) + \lambda(\langle p \rangle) = e\lambda(\pi) + \log \langle p \rangle\) , so that \(\lambda(\pi) = \log \pi\) , and thus \(\lambda(\alpha) = v_{\mathfrak{p}}(\alpha)\lambda(\pi) + \lambda(\langle \alpha \rangle) = v_{\mathfrak{p}}(\alpha)\log \pi + \log \langle \alpha \rangle = \log \alpha\) , for all \(\alpha \in K^*\) . log is therefore uniquely determined and independent of the choice of \(\pi\) .

Proposition (5.5)

FC09-C02-U063 · Chapter II, §5, source L5910 · not formalized

(5.5) Proposition. Let \(K|\mathbb{Q}_p\) be a \(\mathfrak{p}\) -adic number field with valuation ring \(\mathcal{O}\) and maximal ideal \(\mathfrak{p}\) , and let \(p\mathcal{O} = \mathfrak{p}^e\) . Then the power series \(\exp (x) = 1 + x + \frac{x^2}{2!} +\frac{x^3}{3!} +\dots \quad\) and \(\log (1 + z) = z - \frac{z^2}{2} +\frac{z^3}{3} -\dots ,\) yield, for \(n > \frac{e}{p - 1}\) , two mutually inverse isomorphisms (and homeomorphisms) \[ \mathfrak {p} ^ {n} \xrightarrow [ \text {log} ]{\exp} U ^ {(n)}. \]

Lemma (5.6)

FC09-C02-U064 · Chapter II, §5, source L5920 · in Mathlib

(5.6) Lemma. Let \(\nu = \sum_{i=0}^{r} a_i p^i\) , \(0 \leq a_i < p\) , be the \(p\) -adic expansion of the natural number \(\nu \in \mathbb{N}\) . Then \[ v _ {p} (\nu !) = \frac {1}{p - 1} \sum_ {i = 0} ^ {r} a _ {i} (p ^ {i} - 1). \]

Formalized. Mathlib/NumberTheory/Padics/PadicVal/Basic.lean::sub_one_mul_padicValNat_factorial, padicValNat_factorial — The pinned digit-sum formula (p-1)v_p(n!) = n - sum(digits_p n) is precisely Neukirch’s formula.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Proposition (5.7)

FC09-C02-U065 · Chapter II, §5, source L6018 · not formalized

(5.7) Proposition. Let \(K\) be a local field and \(q = p^f\) the number of elements in the residue class field. Then the following hold. (i) If \(K\) has characteristic 0, then one has (both algebraically and topologically) \[ K ^ {*} \cong \mathbb {Z} \oplus \mathbb {Z} / (q - 1) \mathbb {Z} \oplus \mathbb {Z} / p ^ {a} \mathbb {Z} \oplus \mathbb {Z} _ {p} ^ {d}, \] where \(a \geq 0\) and \(d = [K : \mathbb{Q}_p]\) . (ii) If \(K\) has characteristic \(p\) , then one has (both algebraically and topologically) \[ K ^ {*} \cong \mathbb {Z} \oplus \mathbb {Z} / (q - 1) \mathbb {Z} \oplus \mathbb {Z} _ {p} ^ {\mathbb {N}}. \]

Corollary (5.8)

FC09-C02-U066 · Chapter II, §5, source L6124 · not formalized

(5.8) Corollary. If the natural number n is not divisible by the characteristic of K, then one finds the following indices for the subgroups of n-th powers \(K^{*n}\) and \(U^{n}\) in the multiplicative group \(K^{*}\) and in the unit group U: \[ (K ^ {*}: K ^ {* n}) = n (U: U ^ {n}) = \frac {n}{| n | _ {\mathfrak {p}}} \# \mu_ {n} (K). \]

Definition / construction

FC09-C02-U067 · Chapter II, §6, source L6180 · after FC09-C02-U046, FC09-C02-U051 · not formalized

Most results on complete valued fields can be derived from Hensel’s lemma alone, without the full strength of completeness. This lemma is valid in a much bigger class of nonarchimedean valued fields than the complete ones. For example, let \((K, v)\) be a nonarchimedean valued field and \((\widehat{K}, \widehat{v})\) its completion. Let O, resp. \(\widehat{O}\) , be the valuation rings of K, resp. \(\widehat{K}\) . We then consider the separable closure \(K_v\) of K in \(\widehat{K}\) , and the valuation ring \(o_v \subseteq K_v\) with maximal ideal \(p_v\) , which is associated to the restriction of \(\widehat{v}\) to \(K_v\) , \[ K \subseteq K _ {v} \subseteq \widehat {K}, \quad \mathcal {O} \subseteq \mathcal {O} _ {v} \subseteq \widehat {\mathcal {O}}. \] Then Hensel’s lemma holds in the ring \(\mathcal{O}_v\) as well as in the ring \(\widehat{\mathcal{O}}\) even though \(K_v\) will not, as a rule, be complete. When \(K_v\) is algebraically closed in \(\widehat{K} -\) hence in particular \(\mathrm{char}(K) = 0 -\) this is immediately obvious (otherwise it follows from (6.6) and §6, exercise 3 below). Indeed, by (4.3) we have \[ \mathcal {O} / \mathfrak {p} = \mathcal {O} _ {v} / \mathfrak {p} _ {v} = \widehat {\mathcal {O}} / \widehat {\mathfrak {p}}, \] and if a primitive polynomial \(f(x) \in \mathcal{O}_v[x]\) splits over \(\mathcal{O}_v / \mathfrak{p}_v\) into relatively prime factors \(\overline{g}(x), \overline{h}(x)\) , then we have by Hensel’s lemma (4.6) a factorization in \(\widehat{\mathcal{O}}\) \[ f (x) = g (x) h (x) \] such that \(g \equiv \overline{g} \mod \widehat{p}, h \equiv \overline{h} \mod \widehat{p}, \deg(g) = \deg(\overline{g})\) . But this factorization already takes place over \(O_{v}\) once the highest coefficient of g is chosen to be in \(O_{v}^{*}\) , because the coefficients of f, and therefore also those of g and h are algebraic over K. The valued field \(K_{v}\) is called the henselization of the field K with respect to v. It enjoys all the relevant algebraic properties of the completion \(\widehat{K}\) , but offers the advantage of being itself an algebraic extension of K which can also be obtained in a purely algebraic manner, without the analytic recourse to the completion (see §9, exercise 4). The consequence is that taking the henselization of an infinite algebraic extension \(L|K\) is possible within the category of algebraic extensions. Let us define in general:

Definition (6.1)

FC09-C02-U068 · Chapter II, §6, source L6202 · after FC09-C02-U051 · not formalized

(6.1) Definition. A henselian field is a field with a nonarchimedean valuation v whose valuation ring o satisfies Hensel’s lemma in the sense of (4.6). One also calls the valuation v or the valuation ring o henselian.

Theorem (6.2)

FC09-C02-U069 · Chapter II, §6, source L6204 · not formalized

(6.2) Theorem. Let \(K\) be a henselian field with respect to the valuation \(| \cdot |\) . Then \(| \cdot |\) admits one and only one extension to any given algebraic extension \(L|K\) . It is given by \[ | \alpha | = \sqrt [ n ]{\left| N _ {L | K} (\alpha) \right|}, \] if \(L|K\) has finite degree n. In any case, the valuation ring of the extended valuation is the integral closure of the valuation ring of K in L.

Definition / construction

FC09-C02-U070 · Chapter II, §6, source L6214 · not formalized

Let v be an arbitrary exponential valuation of the field K and let \[ f (x) = a _ {0} + a _ {1} x + \dots + a _ {n} x ^ {n} \in K [ x ] \] be a polynomial satisfying \(a_{0}a_{n} \neq 0\) . To each term \(a_{i}x^{i}\) we associate a point \((i, v(a_{i})) \in \mathbb{R}^{2}\) , ignoring however the point \((i, \infty)\) if \(a_{i} = 0\) . We now take the lower convex envelope of the set of points \[ \left\{(0, v (a _ {0})), (1, v (a _ {1})), \dots , (n, v (a _ {n})) \right\}. \] This produces a polygonal chain which is called the Newton polygon of \(f(x)\) .

Proposition (6.3)

FC09-C02-U071 · Chapter II, §6, source L6232 · not formalized

(6.3) Proposition. Let \(f(x) = a_{0} + a_{1}x + \cdots + a_{n}x^{n}, a_{0}a_{n} \neq 0\) , be a polynomial over the field K, v an exponential valuation of K, and w an extension to the splitting field L of f. If \((r, v(a_{r})) \leftrightarrow (s, v(a_{s}))\) is a line segment of slope -m occurring in the Newton polygon of f, then \(f(x)\) has precisely s - r roots \(\alpha_{1}, \ldots, \alpha_{s-r}\) of value \[ w (\alpha_ {1}) = \dots = w (\alpha_ {s - r}) = m. \]

Proposition (6.4)

FC09-C02-U072 · Chapter II, §6, source L6292 · not formalized

(6.4) Proposition. If the valuation v admits a unique extension w to the splitting field L of f, then the factorization \[ f (x) = a _ {n} \prod_ {j = 1} ^ {r} f _ {j} (x) \] is defined already over \(K\) , i.e., \(f_{j}(x) = \prod_{w(\alpha_{i}) = m_{j}}(x - \alpha_{i}) \in K[x]\) .

Corollary (6.5)

FC09-C02-U073 · Chapter II, §6, source L6312 · not formalized

(6.5) Corollary. Let \(f(x) = a_{0} + a_{1}x + \cdots + a_{n}x^{n} \in K[x]\) be an irreducible polynomial with \(a_{n} \neq 0\) . Then, if \(| \mid |\) is a nonarchimedean valuation of K with a unique extension to the splitting field, one has \[ | f | = \max \left\{\left| a _ {0} \right|, \left| a _ {n} \right| \right\}. \]

Theorem (6.6)

FC09-C02-U074 · Chapter II, §6, source L6320 · not formalized

(6.6) Theorem. A nonarchimedean valued field \((K, | \mid)\) is henselian if and only if the valuation \(| \mid\) can be uniquely extended to any algebraic extension.

Proposition (6.7)

FC09-C02-U075 · Chapter II, §6, source L6364 · not formalized

(6.7) Proposition. A nonarchimedean field \((K, v)\) is henselian if any monic polynomial \(f(x) \in \mathcal{O}[x]\) which splits over the residue class field \(\kappa = \mathcal{O} / \mathfrak{p}\) as \[ f (x) \equiv \overline {{g}} (x) \overline {{h}} (x) \bmod {\mathfrak {p}} \] with relatively prime monic factors \(\overline{g}(x),\overline{h} (x)\in \kappa [x]\) , admits itself a splitting \[ f (x) = g (x) h (x) \] into monic factors \(g(x), h(x) \in \mathcal{O}[x]\) such that \[ g (x) \equiv \bar {g} (x) \bmod \mathfrak {p} \quad a n d \quad h (x) \equiv \bar {h} (x) \bmod \mathfrak {p}. \]

Definition / construction

FC09-C02-U076 · Chapter II, §6, source L6410 · not formalized

The index \[ e = e (w \mid v) = \left(w \left(L ^ {*}\right): v \left(K ^ {*}\right)\right) \] is called the ramification index of the extension \(L|K\) and the degree \[ f = f (w \mid v) = [ \lambda : \kappa ] \] is called the inertia degree. If v, and hence \(w = \frac{1}{n}v \circ N_{L|K}\) , is discrete and if \(o, p, \pi\) , resp. O, P, \(\Pi\) , are the valuation ring, the maximal ideal and a prime element of K, resp. L, then one has \[ e = \left(w (\Pi) \mathbb {Z}: v (\pi) \mathbb {Z}\right), \] so that \(v(\pi) = ew(\Pi)\) , and we find \[ \pi = \varepsilon \Pi^ {e}, \] for some unit \(\varepsilon\in\mathcal{O}^{*}\) . From this one deduces the familiar (see chap. I) interpretation of the ramification index: \(\mathfrak{p}\;\mathcal{O}=\pi\;\mathcal{O}=\Pi^{e}\mathcal{O}=\mathfrak{P}^{e}\) , or \[ \mathfrak{p} = \mathfrak{P}^{e}. \]

Not formalized. Pinned/current Mathlib has ramification/inertia and valued-extension primitives, but no checked route closes Neukirch’s full henselian/unramified/tame/extension-of-valuations statement at this level of generality.

Proposition (6.8)

FC09-C02-U077 · Chapter II, §6, source L6440 · not formalized

(6.8) Proposition. One has \([L:K] \geq ef\) and the fundamental identity \[ [ L: K ] = e f, \] if \(v\) is discrete and \(L|K\) is separable.

Definition / construction

FC09-C02-U078 · Chapter II, §7, source L6540 · not formalized

In this section we fix a base field K which is henselian with respect to a nonarchimedean valuation v or | . As before, we denote the valuation ring, the maximal ideal and the residue class field by \(O, p, \kappa\) , respectively. If \(L|K\) is an algebraic extension, then the corresponding invariants are labelled w, O, P, \(\lambda\) , respectively. An especially important rôle among these extensions is played by the unramified extensions, which are defined as follows.

Definition (7.1)

FC09-C02-U079 · Chapter II, §7, source L6542 · not formalized

(7.1) Definition. A finite extension \(L|K\) is called unramified if the extension \(\lambda|\kappa\) of the residue class field is separable and one has \[ [ L: K ] = [ \lambda : \kappa ]. \] An arbitrary algebraic extension \(L|K\) is called unramified if it is a union of finite unramified subextensions.

Proposition (7.2)

FC09-C02-U080 · Chapter II, §7, source L6552 · not formalized

(7.2) Proposition. Let \(L|K\) and \(K'|K\) be two extensions inside an algebraic closure \(\overline{K}|K\) and let \(L' = LK'\) . Then one has \[ L \mid K \text { unramified } \quad \Longrightarrow \quad L ^ {\prime} \mid K ^ {\prime} \text { unramified. } \] Each subextension of an unramified extension is unramified.

Corollary (7.3)

FC09-C02-U081 · Chapter II, §7, source L6578 · not formalized

(7.3) Corollary. The composite of two unramified extensions of \(K\) is again unramified.

Definition (7.4)

FC09-C02-U082 · Chapter II, §7, source L6582 · not formalized

(7.4) Definition. Let \(L|K\) be an algebraic extension. Then the composite \(T|K\) of all unramified subextensions is called the maximal unramified subextension of \(L|K\) .

Proposition (7.5)

FC09-C02-U083 · Chapter II, §7, source L6584 · not formalized

(7.5) Proposition. The residue class field of T is the separable closure \(\lambda_{s}\) of \(\kappa\) in the residue class field extension \(\lambda|\kappa\) of L|K, whereas the value group of T equals that of K.

Definition (7.6)

FC09-C02-U084 · Chapter II, §7, source L6598 · not formalized

(7.6) Definition. An algebraic extension \(L|K\) is called tamely ramified if the extension \(\lambda|\kappa\) of the residue class fields is separable and one has \(([L:T], p) = 1\) . In the infinite case this latter condition is taken to mean that the degree of each finite subextension of \(L|T\) is prime to \(p\) .

Proposition (7.7)

FC09-C02-U085 · Chapter II, §7, source L6602 · not formalized

(7.7) Proposition. A finite extension \(L|K\) is tamely ramified if and only if the extension \(L|T\) is generated by radicals \[ L = T \left(\sqrt [ m _ {1} ]{a _ {1}}, \dots , \sqrt [ m _ {r} ]{a _ {r}}\right) \] such that \((m_i, p) = 1\) . In this case the fundamental identity always holds: \[ [ L: K ] = e f. \]

Corollary (7.8)

FC09-C02-U086 · Chapter II, §7, source L6656 · not formalized

(7.8) Corollary. Let \(L|K\) and \(K'|K\) be two extensions inside the algebraic closure \(\overline{K}|K\) , and \(L' = LK'\) . Then we have: \[ L \mid K \text { tamely ramified } \implies L ^ {\prime} \mid K ^ {\prime} \text { tamely ramified }. \] Every subextension of a tamely ramified extension is tamely ramified.

Corollary (7.9)

FC09-C02-U087 · Chapter II, §7, source L6672 · not formalized

(7.9) Corollary. The composite of tamely ramified extensions is tamely ramified.

Definition (7.10)

FC09-C02-U088 · Chapter II, §7, source L6676 · not formalized

(7.10) Definition. Let \(L|K\) be an algebraic extension. Then the composite \(V|K\) of all tamely ramified subextensions is called the maximal tamely ramified subextension of \(L|K\) .

Convention / notation

FC09-C02-U089 · Chapter II, §7, source L6678 · not formalized

Let \(w(L^{*})^{(p)}\) denote the subgroup of all elements \(\omega \in w(L^{*})\) such that \(m\omega \in v(K^{*})\) for some \(m\) satisfying \((m, p) = 1\) . The quotient group \(w(L^{*})^{(p)} / v(K^{*})\) then consists of all elements of \(w(L^{*}) / v(K^{*})\) whose order is prime to \(p\) .

Proposition (7.11)

FC09-C02-U090 · Chapter II, §7, source L6680 · not formalized

(7.11) Proposition. The maximal tamely ramified subextension \(V|K\) of \(L|K\) has value group \(w(V^{*}) = w(L^{*})^{(p)}\) and residue class field equal to the separable closure \(\lambda_{s}\) of \(\kappa\) in \(\lambda|\kappa\) .

Definition / construction

FC09-C02-U091 · Chapter II, §7, source L6690 · not formalized

If \(L|K\) is finite and \(e = e'p^a\) where \((e', p) = 1\) , then \([V : T] = e'\) . The extension \(L|K\) is called totally (or purely) ramified if \(T = K\) , and wildly ramified if it is not tamely ramified, i.e., if \(V \neq L\) .

Proposition (7.12)

FC09-C02-U092 · Chapter II, §7, source L6694 · not formalized

(7.12) Proposition. Let \(L = K(\zeta)\) , and let \(O|O\) , resp. \(\lambda|\kappa\) , be the extension of valuation rings, resp. residue class fields, of \(L|K\) . Suppose that \((n, p) = 1\) . Then one has: (i) The extension \(L|K\) is unramified of degree \(f\) , where \(f\) is the smallest natural number such that \(q^f \equiv 1 \mod n\) . (ii) The Galois group \(G(L|K)\) is canonically isomorphic to \(G(\lambda|\kappa)\) and is generated by the automorphism \(\varphi:\zeta\mapsto\zeta^{q}\) . (iii) \(\mathcal{O} = \mathcal{O}[\zeta]\) .

Proposition (7.13)

FC09-C02-U093 · Chapter II, §7, source L6706 · not formalized

(7.13) Proposition. Let \(\zeta\) be a primitive \(p^m\) -th root of unity. Then one has: (i) \(\mathbb{Q}_p(\zeta)|\mathbb{Q}_p\) is totally ramified of degree \(\varphi(p^m) = (p - 1)p^{m - 1}\) . (ii) \(G(\mathbb{Q}_p(\zeta)|\mathbb{Q}_p)\cong (\mathbb{Z} / p^m\mathbb{Z})^*\) . (iii) \(\mathbb{Z}_p[\zeta]\) is the valuation ring of \(\mathbb{Q}_p(\zeta)\) . (iv) \(1 - \zeta\) is a prime element of \(\mathbb{Z}_p[\zeta]\) with norm \(p\) .

Convention / notation

FC09-C02-U094 · Chapter II, §8, source L6744 · not formalized

Having seen that the henselian valuations extend uniquely to algebraic extensions we will now study the question of how a valuation v of a field K extends to an algebraic extension in general. So let v be an arbitrary archimedean or nonarchimedean valuation. There is a little discrepancy in notation here, because archimedean valuations manifest themselves only as absolute values while the letter v has hitherto been used for nonarchimedean exponential valuations. In spite of this, it will prove advantageous, and agrees with current usage, to employ the letter v simultaneously for both types of valuations, to denote the corresponding multiplicative valuation in both cases by \(| \mid_{v}\) and the completion by \(K_{v}\) . Where confusion lurks, we will supply clarifying remarks. For every valuation v of K we consider the completion \(K_{v}\) and an algebraic closure \(\overline{K}_{v}\) of \(K_{v}\) . The canonical extension of v to \(K_{v}\) is again denoted by v and the unique extension of this latter valuation to \(\overline{K}_{v}\) by \(\overline{v}\) .

Definition / construction

FC09-C02-U095 · Chapter II, §8, source L6748 · not formalized

Let \(L|K\) be an algebraic extension. Choosing a K-embedding \[ \tau : L \longrightarrow \overline {{K}} _ {v}, \] we obtain by restriction of \(\bar{v}\) to \(\tau L\) an extension \[ w = \overline {{v}} \circ \tau \] of the valuation v to L. In other words, if v, resp. \(\overline{v}\) , are given by the absolute values \(|_{v}\) , resp. \(|_{\overline{v}}\) , on K, \(K_{v}\) , resp. \(\overline{K}_{v}\) , where \(|_{\overline{v}}\) extends precisely the absolute value \(|_{v}\) of \(K_{v}\) , then we obtain on L the multiplicative valuation \[ | x | _ {w} = | \tau x | _ {\overline {{v}}}. \] The mapping \(\tau : L \to \overline{K}_v\) is obviously continuous with respect to this valuation. It extends in a unique way to a continuous \(K\) -embedding \[ \tau : L _ {w} \longrightarrow \overline {{{K}}} _ {v}, \] where, in the case of an infinite extension \(L|K\) , \(L_{w}\) does not mean the completion of L with respect to w, but the union \(L_{w} = \bigcup_{i} L_{iw}\) of the completions \(L_{iw}\) of all finite subextensions \(L_{i}|K\) of \(L|K\) . This union will be henceforth called the localization of L with respect to w. When \([L:K] < \infty\) , \(\tau\) is given by the rule \[ x = w \underset {n \rightarrow \infty} {- \lim} x _ {n} \quad \longmapsto \quad \tau x := \bar {v} \underset {n \rightarrow \infty} {- \lim} \tau x _ {n}, \] where \(\{x_{n}\}_{n\in \mathbb{N}}\) is a \(w\) -Cauchy sequence in \(L\) , and hence \(\{\tau x_n\}_{n\in \mathbb{N}}\) a \(\overline{v}\) -Cauchy sequence in \(\overline{K}_v\) . Note here that the sequence \(\tau x_{n}\) converges in the finite complete extension \(\tau L\cdot K_v\) of \(K_{v}\) . We consider the diagram of fields (*) of fields relating \(L\), \(K_{v}\) and \(L_{w}\): the canonical extension of \(w\) from \(L\) to \(L_{w}\) is the unique extension of the valuation of \(K_{v}\) to the finite extension \(\tau L \cdot K_{v}\).

Extension Theorem (8.1)

FC09-C02-U096 · Chapter II, §8, source L6806 · not formalized

(8.1) Extension Theorem. Let \(L|K\) be an algebraic field extension and \(v\) a valuation of \(K\) . Then one has: (i) Every extension \(w\) of the valuation \(v\) arises as the composite \(w = \overline{v} \circ \tau\) for some \(K\) -embedding \(\tau : L \to \overline{K}_v\) . (ii) Two extensions \(\overline{v} \circ \tau\) and \(\overline{v} \circ \tau'\) are equal if and only if \(\tau\) and \(\tau'\) are conjugate over \(K_{v}\) .

Proposition (8.2)

FC09-C02-U097 · Chapter II, §8, source L6852 · not formalized

(8.2) Proposition. Suppose the extension \(L|K\) is generated by the zero \(\alpha\) of the irreducible polynomial \(f(X) \in K[X]\) . Then the valuations \(w_1, \ldots, w_r\) extending \(v\) to \(L\) correspond 1-1 to the irreducible factors \(f_1, \ldots, f_r\) in the decomposition \[ f (X) = f _ {1} (X) ^ {m _ {1}} \dots f _ {r} (X) ^ {m _ {r}} \] of \(f\) over the completion \(K_v\) . The extended valuation \(w_{i}\) is explicitly obtained from the factor \(f_{i}\) as follows: let \(\alpha_{i} \in \overline{K}_{v}\) be a zero of \(f_{i}\) and let \[ \tau_ {i}: L \to \overline {{K}} _ {v}, \quad \alpha \mapsto \alpha_ {i}, \] be the corresponding K -embedding of L into \(\overline{K}_{v}\) . Then one has \[ w _ {i} = \bar {v} \circ \tau_ {i}. \] \(\tau_{i}\) extends to an isomorphism \[ \tau_ {i}: L _ {w _ {i}} \stackrel {{\sim}} {{\longrightarrow}} K _ {v} (\alpha_ {i}) \] on the completion \(L_{w_i}\) of \(L\) with respect to \(w_i\) .

Definition / construction

FC09-C02-U098 · Chapter II, §8, source L6882 · not formalized

Let \(L|K\) be again an arbitrary finite extension. We will write \(w|v\) to indicate that w is an extension of the valuation v of K to L. The inclusions \(L \hookrightarrow L_w\) induce homomorphisms \(L \otimes_K K_v \to L_w\) via \(a \otimes b \mapsto ab\) , and hence a canonical homomorphism \[ \varphi : L \otimes_ {K} K _ {v} \longrightarrow \prod_ {w | v} L _ {w}. \] To begin with, the tensor product is taken in the sense of vector spaces, i.e., the K-vector space L is lifted to a \(K_{v}\) -vector space \(L \otimes_{K} K_{v}\) . This latter, however, is in fact a \(K_{v}\) -algebra, with the multiplication \((a \otimes b)(a' \otimes b') = aa' \otimes bb'\) , and \(\varphi\) is a homomorphism of \(K_{v}\) -algebras. This homomorphism is the subject of the proposition (8.3): if \(L|K\) is separable, then \(L \otimes_{K} K_{v} \cong \prod_{w \mid v} L_{w}\).

Proposition (8.3)

FC09-C02-U099 · Chapter II, §8, source L6890 · not formalized

(8.3) Proposition. If \(L|K\) is separable, then \(L \otimes_K K_v \cong \prod_{w|v} L_w\) .

Corollary (8.4)

FC09-C02-U100 · Chapter II, §8, source L6900 · not formalized

(8.4) Corollary. If \(L|K\) is separable, then one has \[ [ L: K ] = \sum_ {w | v} [ L _ {w}: K _ {v} ] \] and \[ N _ {L | K} (\alpha) = \prod_ {w | v} N _ {L _ {w} | K _ {v}} (\alpha), \quad T r _ {L | K} (\alpha) = \sum_ {w | v} T r _ {L _ {w} | K _ {v}} (\alpha). \]

Definition / construction

FC09-C02-U101 · Chapter II, §8, source L6926 · after FC09-C02-U100, FC09-C02-U077 · not formalized

If v is a nonarchimedean valuation, then we define, as in the henselian case, the ramification index of an extension \(w|v\) by \[ e _ {w} = \left(w (L ^ {*}): v (K ^ {*})\right) \] and the inertia degree by \[ f _ {w} = [ \lambda_ {w}: \kappa ], \] where \(\lambda_{w}\) , resp. \(\kappa\) , is the residue class field of w, resp. v. From (8.4) and (6.8), we obtain the fundamental identity of valuation theory:

Proposition (8.5)

FC09-C02-U102 · Chapter II, §8, source L6940 · not formalized

(8.5) Proposition. If \(v\) is discrete and \(L|K\) separable, then \[ \sum_ {w \mid v} e _ {w} f _ {w} = [ L: K ]. \]

Definition / construction

FC09-C02-U103 · Chapter II, §9, source L6996 · in Mathlib

In the case of a Galois extension \(L|K\) of infinite degree, the main theorem of ordinary Galois theory, concerning the 1-1 correspondence between the intermediate fields of \(L|K\) and the subgroups of the Galois group \(G(L|K)\) ceases to hold; there are more subgroups than intermediate fields. The correspondence can be salvaged, however, by considering a canonical topology on the group \(G(L|K)\) , the Krull topology. It is given by defining, for every \(\sigma \in G(L|K)\) , as a basis of neighbourhoods the cosets \(\sigma G(L|M)\) , where \(M|K\) varies over the finite Galois subextensions of \(L|K\) . \(G(L|K)\) is thus turned into a compact, Hausdorff topological group. The main theorem of Galois theory then has to be modified in the infinite case by the condition that the intermediate fields of \(L|K\) correspond 1-1 to the closed subgroups of \(G(L|K)\) . Otherwise, everything goes through as in the finite case. So one tacitly restricts attention to closed subgroups, and accordingly to continuous homomorphisms of \(G(L|K)\) .

Formalized. Mathlib/FieldTheory/KrullTopology.lean::krullTopology_t2, fixingSubgroup_isClosed; Mathlib/FieldTheory/Galois/Profinite.lean::CompactSpace Gal(K/k), profiniteGalGrp; Mathlib/FieldTheory/Galois/Infinite.lean::IntermediateFieldEquivClosedSubgroup — The Krull topology is Hausdorff, an infinite Galois group is compact/profinite, and IntermediateFieldEquivClosedSubgroup is exactly the closed-subgroup form of the fundamental theorem.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Proposition (9.1)

FC09-C02-U104 · Chapter II, §9, source L7000 · not formalized

(9.1) Proposition. The group G acts transitively on the set of extensions \(w|v\) , i.e., every two extensions are conjugate.

Not formalized. Pinned/current Mathlib has Krull topology, fixed fields, and valuation-subring decomposition/inertia primitives, but this row bundles additional valuation-extension, ramification-group, exact-sequence, local-completion, coset, or maximal-subextension clauses not exported as a complete compatible theorem.

Definition (9.2)

FC09-C02-U105 · Chapter II, §9, source L7018 · not formalized

(9.2) Definition. The decomposition group of an extension \(w\) of \(v\) to \(L\) is defined by \[ G _ {w} = G _ {w} (L | K) = \left\{\sigma \in G (L | K) \mid w \circ \sigma = w \right\}. \]

Definition (9.3)

FC09-C02-U106 · Chapter II, §9, source L7032 · not formalized

(9.3) Definition. The inertia group of \(w|v\) is defined by \[ I _ {w} = I _ {w} (L | K) = \left\{\sigma \in G _ {w} \mid \sigma x \equiv x \bmod \mathfrak {P} \quad \text { for all } \quad x \in \mathcal {O} \right\} \] and the ramification group by \[ R _ {w} = R _ {w} (L | K) = \left\{\sigma \in G _ {w} \mid \frac {\sigma x}{x} \equiv 1 \bmod \mathfrak {P} \quad \text { for all } \quad x \in L ^ {*} \right\}. \]

Definition / construction

FC09-C02-U107 · Chapter II, §9, source L7052 · not formalized

Consider two Galois extensions \(L|K\) and \(L'|K'\) and a commutative diagram with homomorphisms \(\tau\) which will typically be inclusions. They induce a homomorphism \[ \tau^ {*}: G (L ^ {\prime} | K ^ {\prime}) \longrightarrow G (L | K), \quad \tau^ {*} (\sigma^ {\prime}) = \tau^ {- 1} \sigma^ {\prime} \tau . \] Observe here that, \(L|K\) being normal, the same is true of \(\tau L|\tau K\) , and thus one has \(\sigma' \tau L \subseteq \tau L\) , so that composing with \(\tau^{-1}\) makes sense. Now let \(w'\) be a valuation of \(L'\) , \(v' = w'|_{K'}\) and \(w = w' \circ \tau\) , \(v = w|_K\) . Then we have the proposition (9.4): \(\tau^{*} \colon G(L'|K') \to G(L|K)\) induces homomorphisms \(G_{w'}(L'|K') \to G_{w}(L|K)\) on decomposition groups and \(I_{w'}(L'|K') \to I_{w}(L|K)\) on inertia groups.

Proposition (9.4)

FC09-C02-U108 · Chapter II, §9, source L7066 · not formalized

(9.4) Proposition. \(\tau^{*}: G(L^{\prime}|K^{\prime}) \to G(L|K)\) induces homomorphisms \[ G _ {w ^ {\prime}} (L ^ {\prime} | K ^ {\prime}) \longrightarrow G _ {w} (L | K), \] \[ I _ {w ^ {\prime}} (L ^ {\prime} | K ^ {\prime}) \longrightarrow I _ {w} (L | K), \] \[ R _ {w ^ {\prime}} (L ^ {\prime} | K ^ {\prime}) \longrightarrow R _ {w} (L | K). \] In the latter two cases, v is assumed to be nonarchimedean.

Proposition (9.5)

FC09-C02-U109 · Chapter II, §9, source L7118 · not formalized

(9.5) Proposition. For the extensions \(K \subseteq M \subseteq L\) , one has \[ \begin{array}{r} G _ {w} (L | M) = G _ {w} (L | K) \cap G (L | M), \\ I _ {w} (L | M) = I _ {w} (L | K) \cap G (L | M), \\ R _ {w} (L | M) = R _ {w} (L | K) \cap G (L | M). \end{array} \]

Convention / notation

FC09-C02-U110 · Chapter II, §9, source L7128 · not formalized

Since in the local extension \(L_w|K_v\) the extension of the valuation is unique, we denote the decomposition, inertia, and ramification groups simply by \(G(L_w|K_v)\) , \(I(L_w|K_v)\) , \(R(L_w|K_v)\) . In this case, the homomorphism \(\tau^*\) is the restriction map \[ G (L _ {w} | K _ {v}) \longrightarrow G (L | K), \quad \sigma \longmapsto \sigma | _ {L}, \] and we have the proposition (9.6): \[ G_{w}(L|K) \cong G(L_{w}|K_{v}), \qquad I_{w}(L|K) \cong I(L_{w}|K_{v}), \qquad R_{w}(L|K) \cong R(L_{w}|K_{v}). \]

Proposition (9.6)

FC09-C02-U111 · Chapter II, §9, source L7136 · not formalized

(9.6) Proposition. \[ \begin{array}{r} G _ {w} (L | K) \cong G (L _ {w} | K _ {v}), \\ I _ {w} (L | K) \cong I (L _ {w} | K _ {v}), \\ R _ {w} (L | K) \cong R (L _ {w} | K _ {v}). \end{array} \]

Convention / notation

FC09-C02-U112 · Chapter II, §9, source L7152 · not formalized

The above proposition reduces the problems concerning a single valuation of K to the local situation. We identify the decomposition group \(G_{w}(L|K)\) with the Galois group of \(L_{w}|K_{v}\) and write \[ G _ {w} (L | K) = G \left(L _ {w} \mid K _ {v}\right), \] and similarly \(I_w(L|K) = I(L_w|K_v)\) and \(R_w(L|K) = R(L_w|K_v)\) .

Definition / construction

FC09-C02-U113 · Chapter II, §9, source L7162 · after FC09-C02-U111 · not formalized

The decomposition group \(G_{w}\) consists – as was shown in the proof of (9.6) – of all automorphisms \(\sigma \in G\) that are continuous with respect to the valuation w. It controls the extension of v to L in a group-theoretic manner. Denoting by \(G_{w} \backslash G\) the set of all right cosets \(G_{w}\sigma\) , by \(W_{v}\) the set of extensions of v to L and choosing a fixed extension w, we obtain a bijection \[ G _ {w} \backslash G \stackrel {{\sim}} {{\longrightarrow}} W _ {v}, \quad G _ {w} \sigma \longmapsto w \sigma . \] In particular, the number \(\# W_v\) of extensions equals the index \((G: G_w)\) . As mentioned already in chap. I, §9 - and left for the reader to verify - the decomposition group also describes the way a valuation \(v\) extends to an arbitrary separable extension \(L|K\) . For this, we embed \(L|K\) into a Galois extension \(N|K\) , choose an extension \(w\) of \(v\) to \(N\) , and put \(G = G(N|K)\) , \(H = G(N|L)\) , \(G_w = G_w(N|K)\) , to get a bijection \[ G _ {w} \backslash G / H \stackrel {{\sim}} {{\longrightarrow}} W _ {v}, \quad G _ {w} \sigma H \longmapsto w \circ \sigma | _ {L}. \]

Definition (9.7)

FC09-C02-U114 · Chapter II, §9, source L7174 · in Mathlib

(9.7) Definition. The fixed field of \(G_{w}\) , \[ Z _ {w} = Z _ {w} (L | K) = \left\{x \in L \mid \sigma x = x \text {for all} \sigma \in G _ {w} \right\}, \] is called the decomposition field of w over K.

Formalized. Mathlib/FieldTheory/Galois/Basic.lean::def fixedField — IntermediateField.fixedField is exactly {x | σx=x for every σ in the subgroup}; applied to the previously defined decomposition subgroup it is Neukirch’s decomposition field.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Proposition (9.8)

FC09-C02-U115 · Chapter II, §9, source L7184 · not formalized

(9.8) Proposition. (i) The restriction \(w_{Z}\) of \(w\) to \(Z_{w}\) extends uniquely to \(L\) . (ii) If \(v\) is nonarchimedean, \(w_{Z}\) has the same residue class field and the same value group as \(v\) . (iii) \(Z_{w} = L\cap K_{v}\) (the intersection is taken inside \(L_{w}\) ).

Definition / construction

FC09-C02-U116 · Chapter II, §9, source L7198 · in Mathlib

The inertia group \(I_{w}\) is defined only if w is a nonarchimedean valuation of L. It is the kernel of a canonical homomorphism of \(G_{w}\) . For if O is the valuation ring of w and P the maximal ideal, then, since \(\sigma O = O\) and \(\sigma P = P\) , every \(\sigma \in G_{w}\) induces a \(\kappa\) -automorphism \[ \overline {{{\sigma}}}: \mathcal {O} / \mathfrak {P} \longrightarrow \mathcal {O} / \mathfrak {P}, \quad x \bmod \mathfrak {P} \longmapsto \sigma x \bmod \mathfrak {P}, \] of the residue class field \(\lambda\) , and we obtain a homomorphism \[ G _ {w} \longrightarrow \operatorname{Aut} _ {\kappa} (\lambda) \] with kernel \(I_w\) .

Formalized. Mathlib/RingTheory/Valuation/RamificationGroup.lean::decompositionSubgroup, inertiaSubgroup, MulSemiringAction.toRingAut — ValuationSubring.inertiaSubgroup is defined exactly as the kernel of the decomposition subgroup action on the residue field.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Proposition (9.9)

FC09-C02-U117 · Chapter II, §9, source L7212 · not formalized

(9.9) Proposition. The residue class field extension \(\lambda|\kappa\) is normal, and we have an exact sequence \[ 1 \longrightarrow I _ {w} \longrightarrow G _ {w} \longrightarrow G (\lambda | \kappa) \longrightarrow 1. \]

Definition (9.10)

FC09-C02-U118 · Chapter II, §9, source L7226 · in Mathlib

(9.10) Definition. The fixed field of \(I_w\) , \[ T _ {w} = T _ {w} (L | K) = \left\{x \in L \mid \sigma x = x \text {for all} \sigma \in I _ {w} \right\}, \] is called the inertia field of \(w\) over \(K\) .

Formalized. Mathlib/FieldTheory/Galois/Basic.lean::def fixedField; Mathlib/RingTheory/Valuation/RamificationGroup.lean::inertiaSubgroup — Applying the generic fixed-field construction to the pinned inertia subgroup gives exactly Neukirch’s inertia field.

Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d

Proposition (9.11)

FC09-C02-U119 · Chapter II, §9, source L7242 · not formalized

(9.11) Proposition. \(T_w|Z_w\) is the maximal unramified subextension of \(L|Z_w\) .

Proposition (9.12)

FC09-C02-U120 · Chapter II, §9, source L7288 · not formalized

(9.12) Proposition. \(R_w\) is the unique \(p\) -Sylow subgroup of \(I_w\) .

Definition (9.13)

FC09-C02-U121 · Chapter II, §9, source L7296 · not formalized

(9.13) Definition. The fixed field of \(R_w\) , \[ V _ {w} = V _ {w} (L | K) = \left\{x \in L \mid \sigma x = x \quad \text {for all} \quad \sigma \in R _ {w} \right\}, \] is called the ramification field of w over K.

Proposition (9.14)

FC09-C02-U122 · Chapter II, §9, source L7304 · not formalized

(9.14) Proposition. \(V_{w}|Z_{w}\) is the maximal tamely ramified subextension of \(L|Z_{w}\) .

Corollary (9.15)

FC09-C02-U123 · Chapter II, §9, source L7308 · not formalized

(9.15) Corollary. We have the exact sequence \[ 1 \longrightarrow R _ {w} \longrightarrow I _ {w} \longrightarrow \chi (L | K) \longrightarrow 1. \]

Convention / notation

FC09-C02-U124 · Chapter II, §10, source L7358 · not formalized

The inertia group and the ramification group inside the Galois group of valued fields are only the first terms in a whole series of subgroups that we are now going to study. We assume that \(L|K\) is a finite Galois extension and that \(v_{K}\) is a discrete normalized valuation of K, with positive residue field characteristic p, which admits a unique extension w to L. We denote by \(v_{L}=ew\) the associated normalized valuation of L.

Not formalized. Pinned and current Mathlib explicitly lack higher ramification groups in lower numbering; consequently no checked compatible owner closes this lower/upper numbering or Herbrand-theory row.

Definition (10.1)

FC09-C02-U125 · Chapter II, §10, source L7360 · not formalized

(10.1) Definition. For every real number \(s \geq -1\) we define the \(s\) -th ramification group of \(L|K\) by \[ G _ {s} = G _ {s} (L | K) = \left\{\sigma \in G \mid v _ {L} (\sigma a - a) \geq s + 1 \text { for all } a \in \mathcal {O} \right\}. \]

Proposition (10.2)

FC09-C02-U126 · Chapter II, §10, source L7380 · not formalized

(10.2) Proposition. Let \(\pi_L \in \mathcal{O}\) be a prime element of \(L\) . For every integer \(s \geq 0\) , the mapping \[ G _ {s} / G _ {s + 1} \longrightarrow U _ {L} ^ {(s)} / U _ {L} ^ {(s + 1)}, \quad \sigma \longmapsto \frac {\sigma \pi_ {L}}{\pi_ {L}}, \] is an injective homomorphism which is independent of the prime element \(\pi_{L}\) . Here \(U_{L}^{(s)}\) denotes the s-th group of principal units of L, i.e., \(U_{L}^{(0)} = \mathcal{O}^{*}\) and \(U_{L}^{(s)} = 1 + \pi_{L}^{s} \mathcal{O}\) , for \(s \geq 1\) .

Proposition (10.3)

FC09-C02-U127 · Chapter II, §10, source L7392 · not formalized

(10.3) Proposition. If \(K'\) is an intermediate field of \(L|K\) , then one has, for all \(s \geq -1\) , that \[ G _ {s} (L | K ^ {\prime}) = G _ {s} (L | K) \cap G (L | K ^ {\prime}). \]

Lemma (10.4)

FC09-C02-U128 · Chapter II, §10, source L7400 · not formalized

(10.4) Lemma. The ring extension O of O is monogenous, i.e., there exists an \(x \in O\) such that O = O[x].

Definition / construction

FC09-C02-U129 · Chapter II, §10, source L7416 · not formalized

For every \(\sigma \in G\) we now put \[ i _ {L | K} (\sigma) = v _ {L} (\sigma x - x), \] where \(O = o[x]\) . This definition does not depend on the choice of the generator x and we may write \[ G _ {s} (L | K) = \left\{\sigma \in G \mid i _ {L | K} (\sigma) \geq s + 1 \right\}. \]

Proposition (10.5)

FC09-C02-U130 · Chapter II, §10, source L7430 · not formalized

(10.5) Proposition. If \(e' = e_{L|L'}\) is the ramification index of \(L|L'\) , then \[ i _ {L ^ {\prime} | K} (\sigma^ {\prime}) = \frac {1}{e ^ {\prime}} \sum_ {\sigma | _ {L ^ {\prime}} = \sigma^ {\prime}} i _ {L | K} (\sigma). \]

Proposition (10.6)

FC09-C02-U131 · Chapter II, §10, source L7480 · not formalized

(10.6) Proposition. \(\eta_{L|K}(s) = \frac{1}{g_0}\sum_{\sigma \in G}\min \left\{i_{L|K}(\sigma),s + 1\right\} -1.\)

Theorem (10.7)

FC09-C02-U132 · Chapter II, §10, source L7492 · not formalized

(10.7) Theorem (HERBRAND). Let \(L' | K\) be a Galois subextension of \(L | K\) and \(H = G(L | L')\) . Then one has \[ G _ {s} (L | K) H / H = G _ {t} \left(L ^ {\prime} | K\right) \quad \text { where } \quad t = \eta_ {L | L ^ {\prime}} (s). \]

Definition / construction

FC09-C02-U133 · Chapter II, §10, source L7516 · not formalized

The function \(\eta_{L|K}\) is by definition strictly increasing. Let the inverse function be \(\psi_{L|K}:[-1,\infty)\to[-1,\infty)\) . One defines the upper numbering of the ramification groups by \[ G ^ {t} (L | K) := G _ {s} (L | K) \quad \text { where } \quad s = \psi_ {L | K} (t). \]

Proposition (10.8)

FC09-C02-U134 · Chapter II, §10, source L7524 · not formalized

(10.8) Proposition. If \(L' | K\) is a Galois subextension of \(L | K\) , then \[ \eta_ {L | K} = \eta_ {L ^ {\prime} | K} \circ \eta_ {L | L ^ {\prime}} \quad a n d \quad \psi_ {L | K} = \psi_ {L | L ^ {\prime}} \circ \psi_ {L ^ {\prime} | K}. \]

Proposition (10.9)

FC09-C02-U135 · Chapter II, §10, source L7546 · not formalized

(10.9) Proposition. Let \(L' | K\) be a Galois subextension of \(L | K\) and \(H = G(L | L')\) . Then one has \[ G ^ {t} (L | K) H / H = G ^ {t} (L ^ {\prime} | K). \]