English
Let p be a prime not dividing the exponent of θ. If Q is a lift (to ℤ[X]) of a monic irreducible factor of minpoly_ℤ(θ) modulo p, then the quotient ring (ℤ/pℤ)[X] modulo Q is isomorphic to the quotient ring 𝓞_K modulo the ideal generated by p and Q(θ).
Русский
Пусть p — простое число, не делящее показатель θ. Если Q — подъём (из ℤ[X]) моничного иррд факторa minpolyℤ(θ) по модулю p, то тождение ⟨(ℤ/pℤ)[X]/(Q)⟩ ≅ 𝓞_K/(p, Q(θ)) держится.
LaTeX
$$$\left(\mathbb{Z}/p\mathbb{Z}\right)[X] / (Q) \cong \mathcal{O}_K / (p, Q(\theta)),$ where $p \nmid \operatorname{exponent}(\theta)$ and $Q$ is a lift of a monic irreducible factor of $\minpoly_{\mathbb{Z}}(\theta)$ modulo $p$.$$
Lean4
/-- If `p` does not divide `exponent θ` and `Q` is a lift of a monic irreducible factor of
`minpoly ℤ θ` modulo `p`, then `(ℤ / pℤ)[X] / Q ≃+* 𝓞 K / (p, Q(θ))`.
-/
def ZModXQuotSpanEquivQuotSpanPair (hp : ¬p ∣ exponent θ) {Q : ℤ[X]}
(hQ : Q.map (Int.castRingHom (ZMod p)) ∈ monicFactorsMod θ p) :
(ZMod p)[X] ⧸ span {Polynomial.map (Int.castRingHom (ZMod p)) Q} ≃+* 𝓞 K ⧸ span {(p : 𝓞 K), (aeval θ) Q} :=
have h₀ : map (Int.castRingHom (ZMod p)) (minpoly ℤ θ) ≠ 0 := map_monic_ne_zero (minpoly.monic θ.isIntegral)
have h_eq₁ :
span {map (Int.castRingHom (ZMod p)) Q} =
span {map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)} ⊔ span {map (Int.castRingHom (ZMod p)) Q} :=
by
rw [← span_insert, span_pair_comm, span_pair_eq_span_left_iff_dvd.mpr]
simp only [Multiset.mem_toFinset] at hQ
exact ((Polynomial.mem_normalizedFactors_iff h₀).mp hQ).2.2
have h_eq₂ : span {↑p} ⊔ span {(aeval θ) Q} = span {↑p, (aeval θ) Q} := by rw [span_insert]
((Ideal.quotEquivOfEq h_eq₁).trans (DoubleQuot.quotQuotEquivQuotSup _ _).symm).trans <|
(Ideal.quotientEquiv (Ideal.map (Ideal.Quotient.mk _) (span {(Polynomial.map (Int.castRingHom (ZMod p)) Q)}))
(Ideal.map (Ideal.Quotient.mk _) (span {aeval θ Q})) (ZModXQuotSpanEquivQuotSpan hp)
(by simp [map_span, ZModXQuotSpanEquivQuotSpan_mk_apply])).trans <|
(DoubleQuot.quotQuotEquivQuotSup _ _).trans (Ideal.quotEquivOfEq h_eq₂)
