English
Let R and S be commutative rings, f the ring homomorphism R → S, p an ideal of R, and P a prime ideal of S. If map f p ≠ ⊥, then the ramification index of P over p equals the multiplicity of P in the image of p under f.
Русский
Пусть R и S — коммутативные кольца, f — гомоморфизм колец R → S, p — идеал R, P — простый идеал S. Пусть map f p ≠ ⊥. Тогда рамфикационный индекс P над p равен кратности P в разложении образа p по \(f\).
LaTeX
$$$\\\\operatorname{ramificationIdx} f p P = \\\\operatorname{multiplicity} P (\\\\operatorname{Ideal.map} f p) $$$
Lean4
theorem ramificationIdx_eq_multiplicity (hp : map f p ≠ ⊥) (hP : P.IsPrime) :
ramificationIdx f p P = multiplicity P (Ideal.map f p) := by
classical
by_cases hP₂ : P = ⊥
· rw [hP₂, ← Ideal.zero_eq_bot, multiplicity_zero_eq_zero_of_ne_zero _ hp]
exact Ideal.ramificationIdx_of_not_le (mt le_bot_iff.mp hp)
rw [multiplicity_eq_of_emultiplicity_eq_some]
rw [ramificationIdx_eq_normalizedFactors_count hp hP hP₂, ← normalize_eq P, ←
UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors _ hp, normalize_eq]
exact irreducible_iff_prime.mpr <| prime_of_isPrime hP₂ hP
