liesOver_primesOverSpanEquivMonicFactorsMod_symm

English

The same inverse correspondence also expresses the ideal as the span of p and the evaluation of Q at θ, matching the factorization coming from minpoly modulo p.

Русский

Обратная корреспонденция задаёт тот же идеал как порождение p и Q(θ), согласуясь с разложением minpoly modulo p.

LaTeX

$$((primesOverSpanEquivMonicFactorsMod hp).symm ⟨Q.map (Int.castRingHom (ZMod p)), hQ⟩ : \mathcal{O}_K) = \operatorname{span}\{p, aeval(\theta) Q\}$$

Lean4

theorem liesOver_primesOverSpanEquivMonicFactorsMod_symm (hp : ¬p ∣ exponent θ) {Q : ℤ[X]}
    (hQ : Q.map (Int.castRingHom (ZMod p)) ∈ monicFactorsMod θ p) :
    LiesOver (span {(p : (𝓞 K)), aeval θ Q}) (span {(p : ℤ)}) :=
  by
  rw [← Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply_eq_span hp hQ]
  exact ((primesOverSpanEquivMonicFactorsMod hp).symm ⟨_, hQ⟩).prop.2

Похожие утверждения