ZModXQuotSpanEquivQuotSpan — Mathlib

English

A restatement of the isomorphism action on mk of a polynomial via the same construction.

Русский

Повторение описания действия изоморфизма на mk полинома через ту же конструкцию.

LaTeX

$$$$ (ZModXQuotSpanEquivQuotSpan\\, hp)\\big(\\mathrm{Quot.mk}(...)(Q)\\big) = \\mathrm{Quot.mk}(...)(\\mathrm{aeval}_{θ}(Q)). $$$$

Lean4

/-- If `p` doesn't divide the exponent of `θ`, then `(ℤ / pℤ)[X] / (minpoly θ) ≃+* 𝓞 K / p(𝓞 K)`.
-/
def ZModXQuotSpanEquivQuotSpan (hp : ¬p ∣ exponent θ) :
    (ZMod p)[X] ⧸ span {map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)} ≃+* 𝓞 K ⧸ span {(p : 𝓞 K)} :=
  (quotientEquivAlgOfEq ℤ (by simp [Ideal.map_span, Polynomial.map_map])).toRingEquiv.trans
    ((quotientEquiv _ _ (mapEquiv (Int.quotientSpanNatEquivZMod p)) rfl).symm.trans
      ((quotMapEquivQuotQuotMap (not_dvd_exponent_iff.mp hp).eq_top θ.isIntegral).symm.trans
        (quotientEquivAlgOfEq ℤ (by simp [map_span])).toRingEquiv))

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