theorem SomeLocalRings.theorem_2_8 {𝕜 : Type u_1} [Field 𝕜] (P₁ P₂ : Polynomial 𝕜) (hP₁ : Irreducible P₁) (hP₂ : Irreducible P₂) (f : Polynomial 𝕜 ⧸ Ideal.span {P₁} ≃+* Polynomial 𝕜 ⧸ Ideal.span {P₂}) (σ_f : 𝕜 ≃+* 𝕜) (hf : RingHom.StabilizesBaseFieldWith f.toRingHom σ_f) (σX : Polynomial 𝕜 ≃+* Polynomial 𝕜) (hσX : σX Polynomial.X = Polynomial.X ∧ RingHom.StabilizesBaseFieldWith σX.toRingHom σ_f) (Qf : Polynomial 𝕜) (hQf : Qf.natDegree < P₁.natDegree ∧ 1 ≤ Qf.natDegree) (fX : Polynomial 𝕜 →+* Polynomial 𝕜) (hfX_X : fX Polynomial.X = Qf) (hfX : RingHom.StabilizesBaseFieldWith fX σ_f) (hfX_def : ∀ (P : Polynomial 𝕜), fX P = (σX P).comp Qf) (hIJ : Ideal.span {P₁} ≤ Ideal.comap fX (Ideal.span {P₂})) (hf_ind : Ideal.quotientMap (Ideal.span {P₂}) fX hIJ = f.toRingHom) (Sf : Polynomial 𝕜) (hSf : (σX P₁).comp Qf = Sf * P₂) (n : ℕ) (hn : 1 < n) (hIJn : Ideal.span {P₁ ^ n} ≤ Ideal.comap fX (Ideal.span {P₂ ^ n})) : (∃ (e : Polynomial 𝕜 ⧸ Ideal.span {P₁ ^ n} ≃+* Polynomial 𝕜 ⧸ Ideal.span {P₂ ^ n}), e.toRingHom = Ideal.quotientMap (Ideal.span {P₂ ^ n}) fX hIJn) ∧ RingHom.StabilizesBaseFieldWith (Ideal.quotientMap (Ideal.span {P₂ ^ n}) fX hIJn) σ_f ↔ Polynomial.derivative Qf ≠ 0

Theorem 2.8. Assume 𝕜 is a field and P₁, P₂ are irreducible polynomials in 𝕜[X]. Take n > 1. If f : 𝕜[X]/(P₁) → 𝕜[X]/(P₂) is a ring isomorphism stabilizing 𝕜, then the induced map f_{X,n} : 𝕜[X]/(P₁^n) → 𝕜[X]/(P₂^n) from Proposition 2.4 is a ring isomorphism stabilizing 𝕜 if and only if the formal derivative Q_f' is nonzero.

theorem SomeLocalRings.corollary_2_9 {𝕜 : Type u_1} [Field 𝕜] (P₁ P₂ : Polynomial 𝕜) (hP₁ : Irreducible P₁) (hP₂ : Irreducible P₂) (f : Polynomial 𝕜 ⧸ Ideal.span {P₁} ≃+* Polynomial 𝕜 ⧸ Ideal.span {P₂}) (σ_f : 𝕜 ≃+* 𝕜) (hf : RingHom.StabilizesBaseFieldWith f.toRingHom σ_f) (σX : Polynomial 𝕜 ≃+* Polynomial 𝕜) (hσX : σX Polynomial.X = Polynomial.X ∧ RingHom.StabilizesBaseFieldWith σX.toRingHom σ_f) (Qf : Polynomial 𝕜) (hQf : Qf.natDegree < P₁.natDegree ∧ 1 ≤ Qf.natDegree) (fX : Polynomial 𝕜 →+* Polynomial 𝕜) (hfX_X : fX Polynomial.X = Qf) (hfX : RingHom.StabilizesBaseFieldWith fX σ_f) (hfX_def : ∀ (P : Polynomial 𝕜), fX P = (σX P).comp Qf) (hIJ : Ideal.span {P₁} ≤ Ideal.comap fX (Ideal.span {P₂})) (hf_ind : Ideal.quotientMap (Ideal.span {P₂}) fX hIJ = f.toRingHom) (hQf' : Polynomial.derivative Qf ≠ 0) (n : ℕ) : 1 ≤ n → ∃ (e : Polynomial 𝕜 ⧸ Ideal.span {P₁ ^ n} ≃+* Polynomial 𝕜 ⧸ Ideal.span {P₂ ^ n}), RingHom.StabilizesBaseFieldWith e.toRingHom σ_f

Corollary 2.9. Assume 𝕜 is a field and P₁, P₂ are irreducible polynomials in 𝕜[X]. If f : 𝕜[X]/(P₁) ≃+* 𝕜[X]/(P₂) is a ring isomorphism stabilizing 𝕜 such that the formal derivative Q_f' (associated to f as in Proposition 2.4) is nonzero, then for all n ≥ 1 the quotient rings 𝕜[X]/(P₁^n) and 𝕜[X]/(P₂^n) are isomorphic.

theorem SomeLocalRings.span_pow_le_span {𝕜 : Type u_1} [Field 𝕜] (P : Polynomial 𝕜) (m : ℕ) (hm : 1 ≤ m) : Ideal.span {P ^ m} ≤ Ideal.span {P}

The ideal generated by P ^ m is contained in the ideal generated by P when 1 ≤ m.

theorem SomeLocalRings.theorem_2_10 {𝕜 : Type u_1} [Field 𝕜] (P₁ P₂ : Polynomial 𝕜) (hP₁ : Irreducible P₁) (hP₂ : Irreducible P₂) (m : ℕ) (hm : 1 ≤ m) (f_m : Polynomial 𝕜 ⧸ Ideal.span {P₁ ^ m} ≃+* Polynomial 𝕜 ⧸ Ideal.span {P₂ ^ m}) (hf_m : RingHom.StabilizesBaseField f_m.toRingHom) (hX : ∃ (R : Polynomial 𝕜), f_m ((Ideal.Quotient.mk (Ideal.span {P₁ ^ m})) Polynomial.X) = (Ideal.Quotient.mk (Ideal.span {P₂ ^ m})) R ∧ Polynomial.derivative (R % P₂) ≠ 0) (n : ℕ) : 1 ≤ n → Nonempty (Polynomial 𝕜 ⧸ Ideal.span {P₁ ^ n} ≃+* Polynomial 𝕜 ⧸ Ideal.span {P₂ ^ n})

Theorem 2.10. Assume 𝕜 is a field and P₁, P₂ are irreducible polynomials in 𝕜[X]. Let f_m : 𝕜[X]/(P₁^m) ≃+* 𝕜[X]/(P₂^m) be a ring isomorphism stabilizing 𝕜, for some m ≥ 1. Assume that f_m maps the class of X to the class of some polynomial R : 𝕜[X], and let Q be the remainder of dividing R by P₂ (this Q does not depend on the choice of R). If the formal derivative Q' is nonzero, then the rings 𝕜[X]/(P₁^n) and 𝕜[X]/(P₂^n) are isomorphic for all n ≥ 1.