English
In a Dedekind domain R with R-algebra structure on S, and p a prime in Z (raw prime), the absolute norm of P over p equals |p| raised to the inertia degree of P over span{p} in R.
Русский
В Дедекдиновом кольце R, при p простом в Z и P над p, нормa P над p равна |p|^{inertiaDeg(span{p}) P}.
LaTeX
$$$\\\\operatorname{absNorm} P = |p|^{\\\\operatorname{inertiaDeg} (span\\{p\\}) P}$$$
Lean4
/-- The absolute norm of an ideal `P` above a rational prime `p` is
`|p| ^ ((span {p}).inertiaDeg P)`. -/
theorem absNorm_eq_pow_inertiaDeg [IsDedekindDomain R] [Module.Free ℤ R] [Module.Finite ℤ R] {p : ℤ} (P : Ideal R)
[P.LiesOver (span { p })] (hp : Prime p) : absNorm P = p.natAbs ^ ((span { p }).inertiaDeg P) :=
by
have : (span { p }).IsMaximal := (isPrime_of_prime (prime_span_singleton_iff.mpr hp)).isMaximal (by simp [hp.ne_zero])
have h : Module.Finite (ℤ ⧸ span { p }) (R ⧸ P) := module_finite_of_liesOver P (span { p })
let _ : Field (ℤ ⧸ span { p }) := Quotient.field (span { p })
rw [inertiaDeg_algebraMap, absNorm_apply, Submodule.cardQuot_apply,
Module.natCard_eq_pow_finrank (K := ℤ ⧸ span { p })]
simp [Nat.card_congr (Int.quotientSpanEquivZMod p).toEquiv]
