The unramified primes carrying a prescribed Artin class #
Let L / K be a finite Galois extension of number fields and let C be a conjugacy class in
Gal(L/K). This file defines the set
frobeniusPrimeSet K L C : Set (HeightOneSpectrum (๐ K))
of height-one primes ๐ญ of ๐ K that are unramified in L and whose Artin class is C. It is
the set whose density the Chebotarev density theorem computes.
The dependent membership condition #
artinSymbol is a partial construction: it takes an unramifiedness proof as an argument and has
no value at a ramified prime. So membership cannot be an equation between two total functions;
it is stated as
โ hur : (๐ญ is unramified in L), artinSymbol ๐ญ.asIdeal hur = C,
an existential over a proof. Membership is nonetheless unambiguous: it does not depend on which
unramifiedness proof witnesses it, and mem_frobeniusPrimeSet_iff_artinSymbol_eq turns the
existential into the plain equation artinSymbol ๐ญ.asIdeal hur = C for whichever unramifiedness
proof hur the caller has in hand.
The alternative โ a total Gal(L/K)-valued or ConjClasses-valued function taking a junk value
at the ramified primes โ is worse for this set: the junk value carries no arithmetic content, yet
the ramified primes would sit inside the fibre of whichever class it names, so the fibres would
neither cover the unramified primes exactly nor be pinned down by a Frobenius element there. The
existential is what keeps the fibres free of them.
Main definitions #
NumberField.Chebotarev.frobeniusPrimeSet: the primes of๐ Kunramified inLwhose Artin class isC.
Main results #
NumberField.Chebotarev.mem_frobeniusPrimeSet_iff_artinSymbol_eq: proof-independence โ with any unramifiedness proof in hand, membership is the equationartinSymbol ๐ญ.asIdeal hur = C.NumberField.Chebotarev.mem_frobeniusPrimeSet_mk_iff_exists_isArithFrobAt: for an unramified๐ญand an elementฯ, membership in the fibre of[ฯ]says exactly thatฯis an arithmetic Frobenius at some prime of๐ Labove๐ญ.NumberField.Chebotarev.frobeniusPrimeSet_map_autCongr: equivariance โ an isomorphisme : L โโ[K] L'of extensions ofKmatches the fibre ofCinLwith the fibre inL'of the image ofCunder the induced isomorphismAlgEquiv.autCongr eof Galois groups.NumberField.Chebotarev.frobeniusPrimeSet_subset_map_restrictNormalHom: a fibre overLlies in the fibre over a Galois subextensionMof the restricted class.NumberField.Chebotarev.disjoint_frobeniusPrimeSet: distinct classes have disjoint fibres.NumberField.Chebotarev.iUnion_frobeniusPrimeSet: the fibres cover exactly the complement oframifiedPrimes K L, soexistsUnique_mem_frobeniusPrimeSetpartitions the unramified primes andfinite_compl_iUnion_frobeniusPrimeSetrecords that the discarded remainder is finite.
The last two are what let the density arguments discard a finite exceptional set and then work one class at a time: a lower density bound for each class can be squeezed against a partition of a cofinite set, which is how the crossing argument produces exact densities.
The primes of K with Artin class C in L. A height-one prime ๐ญ of ๐ K belongs to
frobeniusPrimeSet K L C when ๐ญ is unramified in L โ so that artinSymbol is applicable โ
and its Artin class is C.
The unramifiedness proof is packaged existentially rather than assumed, because artinSymbol
takes it as an argument and no value is assigned at a ramified prime. See
mem_frobeniusPrimeSet_iff_artinSymbol_eq for the form used once such a proof is available.
The carrier and this membership condition are taken from
TauCetiRoadmap/Chebotarev/Suggested.lean, lines 64โ76, described in the section
Frobenius prime sets and finite exceptional sets of TauCetiRoadmap/Chebotarev/README.md.
Instances For
Membership in frobeniusPrimeSet, unfolded. Downstream files should open the definition
through this lemma rather than through defeq.
Every prime lies in the unique Frobenius fibre of the trivial extension.
The unique Frobenius fibre of the trivial extension is the whole spectrum:
frobeniusPrimeSet K K C = Set.univ.
Proof-independence. Once an unramifiedness proof hur is available, membership in
frobeniusPrimeSet K L C is the plain equation artinSymbol ๐ญ.asIdeal hur = C: the existential
in the definition may be instantiated at hur, whatever proof it was introduced with.
Membership in frobeniusPrimeSet K L C is therefore independent of the unramifiedness proof used
to test it.
An unramified prime lies in the fibre of its own Artin class.
A member of frobeniusPrimeSet K L C is unramified in L.
No ramified prime carries an Artin class: the fibres avoid ramifiedPrimes K L.
A Frobenius witnesses membership. If ฯ is an arithmetic Frobenius at a prime Q of
๐ L above an unramified ๐ญ, then ๐ญ lies in the fibre of the class of ฯ.
Every representative is realized. If ๐ญ lies in the fibre of the class of ฯ, then ฯ
itself โ not merely some conjugate of it โ is an arithmetic Frobenius at some prime of ๐ L
above ๐ญ.
The fibre of a class, read off from any one representative. For ๐ญ unramified in L,
membership in the fibre of [ฯ] says exactly that ฯ is an arithmetic Frobenius at some prime
of ๐ L above ๐ญ.
Equivariance under an isomorphism of extensions. An isomorphism e : L โโ[K] L' carries
the fibre of C over L onto the fibre over L' of the image of C under the induced
isomorphism AlgEquiv.autCongr e of Galois groups.
So the fibres depend only on the extension L / K up to isomorphism, not on the model of L
chosen to compute the Artin symbol.
Fibres shrink along restriction to a normal subextension. For a tower L / M / K with
M / K Galois, a prime in the fibre of C over L lies in the fibre over M of the restriction
of C. Unramifiedness in M is part of the conclusion, not a hypothesis.
This is artinSymbol_map_restrictNormalHom read on fibres: restriction takes no power.
Distinct classes have disjoint fibres. A prime unramified in L has one Artin class.
The fibres of the Artin class are pairwise disjoint.
The fibres cover the unramified primes. The union of the Artin fibres over all conjugacy
classes of Gal(L/K) is exactly the complement of the finite set ramifiedPrimes K L.
Together with disjoint_frobeniusPrimeSet this is the partition that the density arguments run
on: everything outside a finite exceptional set is accounted for exactly once.
The Artin class partitions the unramified primes. A prime of ๐ K outside
ramifiedPrimes K L lies in the fibre of exactly one conjugacy class of Gal(L/K).
The uncovered set is finite. Only finitely many primes of ๐ K fail to lie in some Artin
fibre, so a density statement may discard them.