Definitions/Def_NumberField_HeightOneSpectrum.lean
Countability of height-one spectra of rings of integers
This module records two instances, both of the form Countable (HeightOneSpectrum (π Β·)), for the type of height-one primes (the nonzero prime ideals) of a ring of integers. Standing context: K is a number field, so in particular its ring of integers \mathcal{O}_K is a Dedekind domain with K as fraction field.
The first instance asserts that HeightOneSpectrum (π β) is countable; this is obtained by transport along the bijection Rat.HeightOneSpectrum.primesEquiv between the nonzero primes of the ring of integers of \mathbb{Q} and the rational primes, a countable type.
The second instance asserts that HeightOneSpectrum (π K) is countable for every number field K. The mathematical content is that the map w \mapsto w\ \text{under}\ \mathcal{O}_{\mathbb{Q}}, sending a height-one prime of \mathcal{O}_K to the height-one prime of \mathcal{O}_{\mathbb{Q}} lying under it, has finite β hence countable β fibres: for a singleton \{y\} of height-one primes of \mathcal{O}_{\mathbb{Q}} its preimage is finite by preimage_comap_finite, applied with A = \mathcal{O}_{\mathbb{Q}}, K = \mathbb{Q}, L = K, B = \mathcal{O}_K; that lemma in turn rests on the finiteness of the set of primes of B extending a given prime of A. Since a type admitting a map to a countable type with countable point-preimages is countable, the countability of HeightOneSpectrum (π β) propagates to \mathcal{O}_K.
Relation to Mathlib
The bijection Rat.HeightOneSpectrum.primesEquiv between the height-one primes of the ring of integers of \mathbb{Q} and the rational primes is Mathlib's; the finiteness of the fibres of under comes from the project's preimage_comap_finite. What is added here are the two Countable instances themselves, so that countability of the set of finite places of a number field is available to instance search.
Where it is used
The instances make countability of the set of finite places of a number field available automatically, as needed wherever constructions over a number field are indexed by its height-one primes, for instance in the treatment of finite adeles and restricted products.
References
- J. Neukirch, Algebraic Number Theory, Grundlehren der mathematischen Wissenschaften 322, Springer, 1999, Chapter I
References are suggested automatically and have not been individually verified.
English text generated automatically from the Lean source; the Lean statement is authoritative.
- 16 lines
- 2 declarations
- used in the statements of 0 theorems and imported by 14 proofs
- imports 1 definition modules
Source file: Definitions/Def_NumberField_HeightOneSpectrum.lean
Imported by
- no other definition module
Declarations
Source
import Mathlib import Definitions.Def_DedekindDomain_IntegralClosure section variable (K : Type*) [Field K] [NumberField K] open IsDedekindDomain NumberField HeightOneSpectrum instance : Countable (HeightOneSpectrum (π β)) := Countable.of_equiv _ Rat.HeightOneSpectrum.primesEquiv.symm instance : Countable (HeightOneSpectrum (π K)) := Set.Countable.of_preimage_singleton <| fun y β¦ ((preimage_comap_finite (π β) β K (π K)) {y} (by simp)).countable
Statements phrased using this module (0)
No statement module imports it directly (it is used through other definition modules or by proofs).