English
The ideal in 𝓞_K corresponding to the class of Q modulo p is exactly the span of p and Q(θ) inside 𝓞_K.
Русский
Идеал в 𝓞_K, соответствующий классу Q модуль p, равен порождению p и Q(θ) в 𝓞_K.
LaTeX
$$((primesOverSpanEquivMonicFactorsMod hp).symm ⟨Q.map (Int.castRingHom (ZMod p)), hQ⟩ : \mathcal{O}_K) = \operatorname{span}\{p, Q(\theta)\}$$
Lean4
/-- The ideal corresponding to the class of `Q ∈ ℤ[X]` modulo `p` via
`NumberField.Ideal.primesOverSpanEquivMonicFactorsMod` is spanned by `p` and `Q(θ)`.
-/
theorem primesOverSpanEquivMonicFactorsMod_symm_apply_eq_span (hp : ¬p ∣ exponent θ) {Q : ℤ[X]}
(hQ : Q.map (Int.castRingHom (ZMod p)) ∈ monicFactorsMod θ p) :
((primesOverSpanEquivMonicFactorsMod hp).symm ⟨Q.map (Int.castRingHom (ZMod p)), hQ⟩ : Ideal (𝓞 K)) =
span {(p : (𝓞 K)), aeval θ Q} :=
by
simp only [primesOverSpanEquivMonicFactorsMod_symm_apply, Polynomial.map_map,
Int.quotientSpanNatEquivZMod_comp_castRingHom]
rw [normalizedFactorsMapEquivNormalizedFactorsMinPolyMk_symm_apply_eq_span, span_union, span_eq, map_span,
Set.image_singleton, map_natCast, ← span_insert]
