2. Decomposition, inertia, Frobenius
Let L/K be a finite Galois extension of number fields with G = \Gal{L/K}.
The Galois group acts on ideals of \mathcal{O}_L (via the canonical G-action
restricted to \mathcal{O}_L and extended multiplicatively), and in particular
permutes the primes lying above a given prime \mathfrak{p} of \mathcal{O}_K.
A nonzero prime ideal \mathfrak{p} of \mathcal{O}_K is unramified in L
if every prime \mathfrak{P} of \mathcal{O}_L lying over \mathfrak{p} has
ramification index 1, i.e. \mathfrak{p}\mathcal{O}_L factors into distinct
primes.
Lean code for Definition2.1●1 definition
Associated Lean declarations
-
Chebotarev.UnramifiedIn[complete]
-
Chebotarev.UnramifiedIn[complete]
-
defdefined in CebotarevDensity/Frobenius.leancomplete
def Chebotarev.UnramifiedIn.{u_1, u_2} (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [IsGalois K L] (𝔭 : Ideal (NumberField.RingOfIntegers K)) : Prop
def Chebotarev.UnramifiedIn.{u_1, u_2} (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [IsGalois K L] (𝔭 : Ideal (NumberField.RingOfIntegers K)) : Prop
A prime `𝔭` of `𝓞 K` is unramified in `L` if it is nonzero and every **maximal** prime `𝔓` of `𝓞 L` lying over `𝔭` is unramified over `𝓞 K` (`Algebra.IsUnramifiedAt`). The `∀ 𝔓` clause has the same shape as the unramified condition in mathlib's `NumberField.not_dvd_discr_iff_forall_liesOver`. The `𝔭 ≠ ⊥` clause (on the base prime) is kept because the Frobenius `arithFrobAt 𝔓` needs a finite residue field `𝓞 L ⧸ 𝔓`; for nonzero `𝔭` the maximal primes over `𝔭` are exactly its prime divisors, so each has `e(𝔓 ∣ 𝔭) = 1` (`Algebra.isUnramifiedAt_iff_of_isDedekindDomain`).
- No associated Lean code or declarations.
For a prime \mathfrak{P} of \mathcal{O}_L, the decomposition group at
\mathfrak{P} is
D_\mathfrak{P} \;=\; \{\sigma \in G : \sigma(\mathfrak{P}) = \mathfrak{P}\} \;=\; \operatorname{Stab}_G(\mathfrak{P}).
In the formalisation this is mathlib's stabiliser MulAction.stabilizer G 𝔓 of the
G-action on the primes of \mathcal{O}_L, so it is not restated as a separate
project definition.
The inertia group at \mathfrak{P} is
I_\mathfrak{P} \;=\; \{\sigma \in G : \forall x \in \mathcal{O}_L,\ \sigma(x) \equiv x \pmod{\mathfrak{P}}\}.
This is the generic ideal-inertia subgroup Ideal.inertia from mathlib,
instantiated at the natural action of G on \mathcal{O}_L; acting trivially
mod \mathfrak{P} forces stabilising \mathfrak{P}, so I_\mathfrak{P} sits
inside D_\mathfrak{P}, and is the kernel of the action of D_\mathfrak{P} on
the residue field \mathcal{O}_L/\mathfrak{P}.
When \mathfrak{P} is unramified the inertia group is trivial:
|I_\mathfrak{P}| = e(\mathfrak{P} \mid \mathfrak{p}) = 1. Hence the surjection
D_\mathfrak{P} \to \Gal{(\mathcal{O}_L/\mathfrak{P})/(\mathcal{O}_K/\mathfrak{p})}
(mathlib's IsFractionRing.stabilizerHom_surjective) is an isomorphism, and the
residue Galois group of a finite-field extension is cyclic with distinguished
generator the absolute Frobenius x \mapsto x^{\Norm\mathfrak{p}}. So
D_\mathfrak{P} contains a unique element acting as
x \mapsto x^{\Norm\mathfrak{p}} on \mathcal{O}_L/\mathfrak{P}. In the
formalisation this existence and uniqueness is supplied directly by mathlib's
arithmetic-Frobenius API (IsArithFrobAt.exists_of_isInvariant for existence,
IsArithFrobAt.mul_inv_mem_inertia together with trivial inertia for uniqueness),
so it is not restated as a separate project result.
- No associated Lean code or declarations.
For an unramified nonzero prime \mathfrak{P} of \mathcal{O}_L, the Frobenius
automorphism \Frob_\mathfrak{P} \in G is mathlib's arithFrobAt for the action
of G on \mathcal{O}_L: the unique element of D_\mathfrak{P} characterised
by \Frob_\mathfrak{P}(x) \equiv x^{\Norm\mathfrak{p}} \pmod{\mathfrak{P}} for all
x \in \mathcal{O}_L.
For a nonzero prime \mathfrak{p} of \mathcal{O}_K unramified in L, the
Frobenius conjugacy class is
\sigma_\mathfrak{p} \;=\; \{\Frob_\mathfrak{P} : \mathfrak{P} \mid \mathfrak{p}\} \;\in\; \operatorname{Conj}(G),
the conjugacy class in G containing \Frob_\mathfrak{P} for any (equivalently
every) prime \mathfrak{P} of \mathcal{O}_L above \mathfrak{p}. The class is
independent of the choice of \mathfrak{P}.
Lean code for Definition2.5●1 definition
Associated Lean declarations
-
Chebotarev.frobeniusClass[complete]
-
Chebotarev.frobeniusClass[complete]
-
defdefined in CebotarevDensity/Frobenius.leancomplete
def Chebotarev.frobeniusClass.{u_1, u_2} (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [NumberField K] [NumberField L] [IsGalois K L] (𝔭 : Ideal (NumberField.RingOfIntegers K)) : ConjClasses Gal(L/K)
def Chebotarev.frobeniusClass.{u_1, u_2} (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [NumberField K] [NumberField L] [IsGalois K L] (𝔭 : Ideal (NumberField.RingOfIntegers K)) : ConjClasses Gal(L/K)
The Frobenius conjugacy class of a prime `𝔭` of `𝓞 K`. When `𝔭` is a nonzero unramified prime, this is the conjugacy class of any arithmetic Frobenius `σ` (`IsArithFrobAt`) at any prime `𝔓` of `𝓞 L` above `𝔭` (well-definedness from `exists_frobeniusClass`). For other primes the value is the trivial class — a junk value never used in the Chebotarev statement (which always restricts to unramified nonzero primes).
For a nonzero prime \mathfrak{p} of \mathcal{O}_K unramified in L, there
exists a conjugacy class C \subseteq \Gal{L/K} such that for every prime
\mathfrak{P} of \mathcal{O}_L above \mathfrak{p},
C = [\Frob_\mathfrak{P}]. (Equivalently, the Frobenius elements above
\mathfrak{p} are all conjugate.)
Lean code for Lemma2.6●1 theorem
Associated Lean declarations
-
Chebotarev.exists_frobeniusClass[complete]
-
Chebotarev.exists_frobeniusClass[complete]
-
theoremdefined in CebotarevDensity/Frobenius.leancomplete
theorem Chebotarev.exists_frobeniusClass.{u_1, u_2} (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [NumberField K] [NumberField L] [IsGalois K L] (𝔭 : Ideal (NumberField.RingOfIntegers K)) [𝔭.IsPrime] (hunr : Chebotarev.UnramifiedIn K L 𝔭) : ∃ C, ∀ (σ : Gal(L/K)) (𝔓 : Ideal (NumberField.RingOfIntegers L)) [𝔓.IsPrime], IsArithFrobAt (NumberField.RingOfIntegers K) σ 𝔓 → 𝔓.LiesOver 𝔭 → C = ConjClasses.mk σ
theorem Chebotarev.exists_frobeniusClass.{u_1, u_2} (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [NumberField K] [NumberField L] [IsGalois K L] (𝔭 : Ideal (NumberField.RingOfIntegers K)) [𝔭.IsPrime] (hunr : Chebotarev.UnramifiedIn K L 𝔭) : ∃ C, ∀ (σ : Gal(L/K)) (𝔓 : Ideal (NumberField.RingOfIntegers L)) [𝔓.IsPrime], IsArithFrobAt (NumberField.RingOfIntegers K) σ 𝔓 → 𝔓.LiesOver 𝔭 → C = ConjClasses.mk σ
Existence and well-definedness of the Frobenius conjugacy class of an unramified prime `𝔭` of `𝓞 K`: there is a single conjugacy class `C` such that `C = ConjClasses.mk σ` for every `σ` that is an arithmetic Frobenius (`IsArithFrobAt`) at some prime `𝔓` of `𝓞 L` above `𝔭`. Sharifi §7.2 + SL Appendix paragraph 1.
For a nonzero prime \mathfrak{p} of \mathcal{O}_K unramified in L, and any
prime \mathfrak{P} of \mathcal{O}_L above \mathfrak{p},
\sigma_\mathfrak{p} \;=\; [\Frob_\mathfrak{P}].
Lean code for Lemma2.7●1 theorem
Associated Lean declarations
-
theoremdefined in CebotarevDensity/Frobenius.leancomplete
theorem Chebotarev.frobeniusClass_eq_mk_of_isArithFrobAt.{u_1, u_2} (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [NumberField K] [NumberField L] [IsGalois K L] (𝔭 : Ideal (NumberField.RingOfIntegers K)) [𝔭.IsPrime] (hunr : Chebotarev.UnramifiedIn K L 𝔭) (σ : Gal(L/K)) (𝔓 : Ideal (NumberField.RingOfIntegers L)) [𝔓.IsPrime] (hσ : IsArithFrobAt (NumberField.RingOfIntegers K) σ 𝔓) (hP : 𝔓.LiesOver 𝔭) : Chebotarev.frobeniusClass K L 𝔭 = ConjClasses.mk σ
theorem Chebotarev.frobeniusClass_eq_mk_of_isArithFrobAt.{u_1, u_2} (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [NumberField K] [NumberField L] [IsGalois K L] (𝔭 : Ideal (NumberField.RingOfIntegers K)) [𝔭.IsPrime] (hunr : Chebotarev.UnramifiedIn K L 𝔭) (σ : Gal(L/K)) (𝔓 : Ideal (NumberField.RingOfIntegers L)) [𝔓.IsPrime] (hσ : IsArithFrobAt (NumberField.RingOfIntegers K) σ 𝔓) (hP : 𝔓.LiesOver 𝔭) : Chebotarev.frobeniusClass K L 𝔭 = ConjClasses.mk σ
`frobeniusClass K L 𝔭` is the conjugacy class of any arithmetic Frobenius `σ` (`IsArithFrobAt (𝓞 K) σ 𝔓`) at any prime `𝔓` of `𝓞 L` above `𝔭`.
Only finitely many nonzero primes of \mathcal{O}_K ramify in L.
Lean code for Lemma2.8●1 theorem
Associated Lean declarations
-
Chebotarev.finite_ramifiedIn[complete]
-
Chebotarev.finite_ramifiedIn[complete]
-
theoremdefined in CebotarevDensity/Frobenius.leancomplete
theorem Chebotarev.finite_ramifiedIn.{u_1, u_2} (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [NumberField K] [NumberField L] [IsGalois K L] : {𝔭 | 𝔭.IsPrime ∧ 𝔭 ≠ ⊥ ∧ ¬Chebotarev.UnramifiedIn K L 𝔭}.Finite
theorem Chebotarev.finite_ramifiedIn.{u_1, u_2} (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [NumberField K] [NumberField L] [IsGalois K L] : {𝔭 | 𝔭.IsPrime ∧ 𝔭 ≠ ⊥ ∧ ¬Chebotarev.UnramifiedIn K L 𝔭}.Finite
Only finitely many nonzero primes of `K` ramify in `L`.
The primes ramifying in L are exactly the divisors of the relative different
ideal \mathfrak{d}_{L/K} \subseteq \mathcal{O}_L, which has a finite prime
factorisation in the Dedekind domain \mathcal{O}_L.