English
In the prime factorization of map p, every nonzero ramification index occurs with nonzero exponent.
Русский
В разложении на множители map(p) каждый ненулевой рамфикационный индекс встречается с ненуловым показателем.
LaTeX
$$$\\\\operatorname{fact_ramificationIdx_neZero} (p P) \\\\Rightarrow P \\\\neq 0$$$
Lean4
/-- The **fundamental identity** of ramification index `e` and inertia degree `f`:
for `P` ranging over the primes lying over `p`, `∑ P, e P * f P = [Frac(S) : Frac(R)]`;
here `S` is a finite `R`-module (and thus `Frac(S) : Frac(R)` is a finite extension) and `p`
is maximal. -/
theorem sum_ramification_inertia (K L : Type*) [Field K] [Field L] [IsDedekindDomain R] [Algebra R K]
[IsFractionRing R K] [Algebra S L] [IsFractionRing S L] [Algebra K L] [Algebra R L] [IsScalarTower R S L]
[IsScalarTower R K L] [Module.Finite R S] {p : Ideal R} [p.IsMaximal] (hp0 : p ≠ ⊥) :
∑ P ∈ primesOverFinset p S, ramificationIdx (algebraMap R S) p P * inertiaDeg p P = finrank K L :=
by
set e := ramificationIdx (algebraMap R S) p
set f := inertiaDeg p (S := S)
calc
(∑ P ∈ (factors (map (algebraMap R S) p)).toFinset, e P * f P) =
∑ P ∈ (factors (map (algebraMap R S) p)).toFinset.attach, finrank (R ⧸ p) (S ⧸ (P : Ideal S) ^ e P) :=
?_
_ = finrank (R ⧸ p) (∀ P : (factors (map (algebraMap R S) p)).toFinset, S ⧸ (P : Ideal S) ^ e P) :=
(finrank_pi_fintype (R ⧸ p)).symm
_ = finrank (R ⧸ p) (S ⧸ map (algebraMap R S) p) := ?_
_ = finrank K L := ?_
· rw [← Finset.sum_attach]
refine Finset.sum_congr rfl fun P _ => ?_
rw [Factors.finrank_pow_ramificationIdx]
· refine LinearEquiv.finrank_eq (Factors.piQuotientLinearEquiv S p ?_).symm
rwa [Ne, Ideal.map_eq_bot_iff_le_ker,
(RingHom.injective_iff_ker_eq_bot _).mp <| algebraMap_injective_of_field_isFractionRing R S K L, le_bot_iff]
· exact finrank_quotient_map p K L
