English
The ramification index of the ideal corresponding to Q over p equals the multiplicity of Q modulo p in the minpoly modulo p.
Русский
Инервирование над p равно кратности Q по модулю p в минимальном полиноме по модулю p.
LaTeX
$$ramificationIdx (algebraMap Z (𝓞_K)) (span {p : Z}) ((primesOverSpanEquivMonicFactorsMod hp).symm ⟨Q.map (Int.castRingHom (ZMod p)), hQ⟩ : Ideal (𝓞_K)) = multiplicity (Q.map (Int.castRingHom (ZMod p))) ((minpoly Z θ).map (Int.castRingHom (ZMod p)))$$
Lean4
/-- The ramification index of the ideal corresponding to the class of `Q ∈ ℤ[X]` modulo `p` via
`NumberField.Ideal.primesOverSpanEquivMonicFactorsMod` is equal to the multiplicity of `Q mod p` in
`minpoly ℤ θ`.
-/
theorem ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply (hp : ¬p ∣ exponent θ) {Q : ℤ[X]}
(hQ : Q.map (Int.castRingHom (ZMod p)) ∈ monicFactorsMod θ p) :
ramificationIdx (algebraMap ℤ (𝓞 K)) (span {(p : ℤ)})
((primesOverSpanEquivMonicFactorsMod hp).symm ⟨Q.map (Int.castRingHom (ZMod p)), hQ⟩ : Ideal (𝓞 K)) =
multiplicity (Q.map (Int.castRingHom (ZMod p))) ((minpoly ℤ θ).map (Int.castRingHom (ZMod p))) :=
by
rw [ramificationIdx_eq_multiplicity (map_ne_bot_of_ne_bot (by simp [NeZero.ne p])) inferInstance]
· apply multiplicity_eq_of_emultiplicity_eq
rw [← emultiplicity_map_eq (mapEquiv (Int.quotientSpanNatEquivZMod p).symm),
emultiplicity_factors_map_eq_emultiplicity inferInstance (by simp [NeZero.ne p])
(not_dvd_exponent_iff.mp hp).eq_top θ.isIntegral]
·
simp only [primesOverSpanEquivMonicFactorsMod_symm_apply,
Equiv.apply_symm_apply (normalizedFactorsMapEquivNormalizedFactorsMinPolyMk _ _ _ _), Polynomial.map_map,
Int.quotientSpanNatEquivZMod_comp_castRingHom, mapEquiv_apply]
· rw [← mem_primesOver_iff_mem_normalizedFactors _ (by simp [NeZero.ne p])]
exact ((primesOverSpanEquivMonicFactorsMod hp).symm ⟨_, hQ⟩).coe_prop
