theorem SomeLocalRings.isRoot_aeval_of_comp_eq_mul {𝕜 : Type u_1} [Field 𝕜] {K : Type u_4} [Field K] [Algebra 𝕜 K] {p q r s : Polynomial 𝕜} (h : p.comp q = r * s) {α : K} (hs : (Polynomial.map (algebraMap 𝕜 K) s).IsRoot α) : (Polynomial.map (algebraMap 𝕜 K) p).IsRoot ((Polynomial.aeval α) q)

If p.comp q = r * s, then every root of s maps to a root of p by evaluation of q.

This is the basic “root mapping” step used in Proposition 2.6.

theorem SomeLocalRings.finiteDimensional_quotient_span_of_ne_zero {𝕜 : Type u_1} [Field 𝕜] (P : Polynomial 𝕜) (hP0 : P ≠ 0) : FiniteDimensional 𝕜 (Polynomial 𝕜 ⧸ Ideal.span {P})

𝕜[X]⧸(P) is finite-dimensional over 𝕜, using the monic associate of P.

This is a local helper for Proposition 2.6.

theorem SomeLocalRings.prop2_5_coprime_of_exists_ringEquiv {𝕜 : Type u_1} [Field 𝕜] (P₁ P₂ : Polynomial 𝕜) (hP₁ : Irreducible P₁) (hP₂ : Irreducible P₂) (fX : Polynomial 𝕜 →+* Polynomial 𝕜) (Sf : Polynomial 𝕜) (hSf : fX P₁ = 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) → IsCoprime Sf P₂

Conversely, if f_{X,n} is an isomorphism and n > 1, then S_f is coprime to P₂.

theorem SomeLocalRings.proposition_2_5 {𝕜 : 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})) : IsCoprime Sf P₂ ↔ ∃ (e : Polynomial 𝕜 ⧸ Ideal.span {P₁ ^ n} ≃+* Polynomial 𝕜 ⧸ Ideal.span {P₂ ^ n}), e.toRingHom = Ideal.quotientMap (Ideal.span {P₂ ^ n}) fX hIJn

Proposition 2.5. Assume 𝕜 is a field and P₁, P₂ are irreducible polynomials in 𝕜[X]. Let f : 𝕜[X]/(P₁) → 𝕜[X]/(P₂) be a ring isomorphism stabilizing 𝕜, and let S_f and f_{X,n} be as in Proposition 2.4. For n > 1, S_f is prime to P₂ if and only if f_{X,n} : 𝕜[X]/(P₁^n) → 𝕜[X]/(P₂^n) is an isomorphism.

theorem SomeLocalRings.proposition_2_6 {𝕜 : 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 Sf : Polynomial 𝕜) (hSf : (σX P₁).comp Qf = Sf * P₂) : (∀ {K : Type u_4} [inst : Field K] [inst_1 : Algebra 𝕜 K] {α : K}, (Polynomial.map (algebraMap 𝕜 K) P₂).IsRoot α → (Polynomial.map (algebraMap 𝕜 K) (σX P₁)).IsRoot ((Polynomial.aeval α) Qf)) ∧ ∃ (e : { α : AlgebraicClosure 𝕜 // (Polynomial.map (algebraMap 𝕜 (AlgebraicClosure 𝕜)) P₂).IsRoot α } ≃ { β : AlgebraicClosure 𝕜 // (Polynomial.map (algebraMap 𝕜 (AlgebraicClosure 𝕜)) (σX P₁)).IsRoot β }), ∀ (a : { α : AlgebraicClosure 𝕜 // (Polynomial.map (algebraMap 𝕜 (AlgebraicClosure 𝕜)) P₂).IsRoot α }), ↑(e a) = (Polynomial.aeval ↑a) Qf

Proposition 2.6. Assume 𝕜 is a field and P₁, P₂ are irreducible polynomials in 𝕜[X]. Let f : 𝕜[X]/(P₁) ≃+* 𝕜[X]/(P₂) be a ring isomorphism stabilizing 𝕜, and let σ_f^X and Q_f be as in Proposition 2.4.

1. If α is a root of P₂, then Q_f(α) is a root of σ_f^X(P₁).
2. The map α ↦ Q_f(α) gives a bijection between the roots of P₂ and the roots of σ_f^X(P₁).

theorem SomeLocalRings.rootMultiplicity_comp_eq_mul {K : Type u_4} [Field K] [IsAlgClosed K] (p q : Polynomial K) (a : K) (hp : p ≠ 0) : Polynomial.rootMultiplicity a (p.comp q) = Polynomial.rootMultiplicity (Polynomial.eval a q) p * Polynomial.rootMultiplicity a (q - Polynomial.C (Polynomial.eval a q))

Root multiplicity for a composition over an algebraically closed field.

If b = q.eval a, then the multiplicity of a as a root of p.comp q is the multiplicity of b as a root of p, times the multiplicity of a as a root of q - C b.

theorem SomeLocalRings.rootMultiplicity_sub_C_eval_eq_one_iff {K : Type u_4} [Field K] (q : Polynomial K) (a : K) : Polynomial.rootMultiplicity a (q - Polynomial.C (Polynomial.eval a q)) = 1 ↔ ¬(Polynomial.derivative q).IsRoot a

For q : K[X], the multiplicity of a as a root of q - C (q.eval a) is 1 iff the derivative does not vanish at a.