How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Unique extension of a nonarchimedean absolute value
Statement
For every finite field extension L/K with K complete nonarchimedean, the unique extending absolute value is It is nonarchimedean and makes L complete. Separability and discreteness are not assumed; the trivial valuation is included.
Facts & Assumptions
Given: The data and hypotheses of the statement.
Uniqueness of an extended complete field absolute value: For a finite extension E/F of a complete absolutely valued field F, at most one absolute value on E extends the given absolute value on F. Any such extension makes E complete.
Irreducible polynomial coefficients in a complete valuation ring: Let F be complete nonarchimedean. If is monic irreducible of positive degree and , then every coefficient of f has absolute value at most one.
Norm is multiplicative, trace is -linear, and both are transitive in towers: Let be a finite extension and let . 1. . 2. and for every . 3. If is a tower of finite extensions, then
Field norm and trace agree with the determinant and trace of multiplication by an element: Let be a finite extension and let . If is the -linear multiplication operator, then where the right-hand side uses the published linear-operator determinant and trace.
Proof
Put and . The determinant interpretation shows that v vanishes exactly at zero and for , since multiplication by a is a scalar n by n matrix. Norm multiplicativity gives .
For , let and m=[E:K]. The tower law and determinant of the scalar E-linear action give . The companion matrix of multiplication by x shows that its norm is for the monic minimal polynomial f. Thus , so all coefficients lie in the valuation ring. It follows that , and the same companion-matrix calculation for x+1 gives .
For y nonzero and , apply the preceding step to x/y to obtain . If y=0 there is nothing to prove; interchange x,y when needed. This proves the strong triangle inequality. The uniqueness lemma gives uniqueness and completeness. Its proof applies in arbitrary characteristic; no conjugate count or separability was used. For the trivial base value the norm formula is identically one on nonzero elements.
Depends on
Used by
Dependency tree · two levels
15 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- §6, Lemma 6.1 and Theorem 6.4, pp.10–11; Milne Theorem 7.38 for discrete separable specialization (standard reference, not scraped)