Results about minpoly R x / (X - C x)

Main definition

• minpolyDiv: The polynomial minpoly R x / (X - C x).

We used the contents of this file to describe the dual basis of a powerbasis under the trace form. See traceForm_dualBasis_powerBasis_eq.

Main results

• span_coeff_minpolyDiv: The coefficients of minpolyDiv spans R<x>.

noncomputable def minpolyDiv (R : Type u_1) {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (x : S) : Polynomial S

minpolyDiv R x : S[X] for x : S is the polynomial minpoly R x / (X - C x).

Equations

• minpolyDiv R x = (Polynomial.map (algebraMap R S) (minpoly R x)).divByMonic (Polynomial.X - Polynomial.C x)

theorem minpolyDiv_spec (R : Type u_2) {S : Type u_1} [CommRing R] [CommRing S] [Algebra R S] (x : S) : minpolyDiv R x * (Polynomial.X - Polynomial.C x) = Polynomial.map (algebraMap R S) (minpoly R x)

theorem coeff_minpolyDiv (R : Type u_2) {S : Type u_1} [CommRing R] [CommRing S] [Algebra R S] (x : S) (i : ℕ) : (minpolyDiv R x).coeff i = (algebraMap R S) ((minpoly R x).coeff (i + 1)) + (minpolyDiv R x).coeff (i + 1) * x

theorem minpolyDiv_ne_zero {R : Type u_2} {S : Type u_1} [CommRing R] [CommRing S] [Algebra R S] {x : S} (hx : IsIntegral R x) [Nontrivial S] : minpolyDiv R x ≠ 0

theorem minpolyDiv_eq_zero {R : Type u_2} {S : Type u_1} [CommRing R] [CommRing S] [Algebra R S] {x : S} (hx : ¬IsIntegral R x) : minpolyDiv R x = 0

theorem minpolyDiv_monic {R : Type u_2} {S : Type u_1} [CommRing R] [CommRing S] [Algebra R S] {x : S} (hx : IsIntegral R x) : (minpolyDiv R x).Monic

theorem eval_minpolyDiv_self {R : Type u_2} {S : Type u_1} [CommRing R] [CommRing S] [Algebra R S] {x : S} : Polynomial.eval x (minpolyDiv R x) = (Polynomial.aeval x) (Polynomial.derivative (minpoly R x))

theorem minpolyDiv_eval_eq_zero_of_ne_of_aeval_eq_zero {R : Type u_2} {S : Type u_1} [CommRing R] [CommRing S] [Algebra R S] {x : S} [IsDomain S] {y : S} (hxy : y ≠ x) (hy : (Polynomial.aeval y) (minpoly R x) = 0) : Polynomial.eval y (minpolyDiv R x) = 0

theorem eval₂_minpolyDiv_of_eval₂_eq_zero {R : Type u_3} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_1} [CommRing T] [IsDomain T] [DecidableEq T] {x : S} {y : T} (σ : S →+* T) (hy : Polynomial.eval₂ (σ.comp (algebraMap R S)) y (minpoly R x) = 0) : Polynomial.eval₂ σ y (minpolyDiv R x) = if σ x = y then σ ((Polynomial.aeval x) (Polynomial.derivative (minpoly R x))) else 0

theorem eval₂_minpolyDiv_self {R : Type u_2} {S : Type u_3} [CommRing R] [CommRing S] [Algebra R S] {T : Type u_1} [CommRing T] [Algebra R T] [IsDomain T] [DecidableEq T] (x : S) (σ₁ : S →ₐ[R] T) (σ₂ : S →ₐ[R] T) : Polynomial.eval₂ (↑σ₁) (σ₂ x) (minpolyDiv R x) = if σ₁ x = σ₂ x then σ₁ ((Polynomial.aeval x) (Polynomial.derivative (minpoly R x))) else 0

theorem eval_minpolyDiv_of_aeval_eq_zero {R : Type u_2} {S : Type u_1} [CommRing R] [CommRing S] [Algebra R S] {x : S} [IsDomain S] [DecidableEq S] {y : S} (hy : (Polynomial.aeval y) (minpoly R x) = 0) : Polynomial.eval y (minpolyDiv R x) = if x = y then (Polynomial.aeval x) (Polynomial.derivative (minpoly R x)) else 0

theorem natDegree_minpolyDiv_succ {R : Type u_2} {S : Type u_1} [CommRing R] [CommRing S] [Algebra R S] {x : S} (hx : IsIntegral R x) [Nontrivial S] : (minpolyDiv R x).natDegree + 1 = (minpoly R x).natDegree

theorem natDegree_minpolyDiv {R : Type u_2} {S : Type u_1} [CommRing R] [CommRing S] [Algebra R S] {x : S} : (minpolyDiv R x).natDegree = (minpoly R x).natDegree - 1

theorem natDegree_minpolyDiv_lt {R : Type u_2} {S : Type u_1} [CommRing R] [CommRing S] [Algebra R S] {x : S} (hx : IsIntegral R x) [Nontrivial S] : (minpolyDiv R x).natDegree < (minpoly R x).natDegree

theorem coeff_minpolyDiv_mem_adjoin {R : Type u_2} {S : Type u_1} [CommRing R] [CommRing S] [Algebra R S] (x : S) (i : ℕ) : (minpolyDiv R x).coeff i ∈ Algebra.adjoin R {x}

theorem minpolyDiv_eq_of_isIntegrallyClosed {R : Type u_1} (K : Type u_3) {S : Type u_2} [CommRing R] [Field K] [CommRing S] [Algebra R S] {x : S} (hx : IsIntegral R x) [IsDomain R] [IsIntegrallyClosed R] [IsDomain S] [Algebra R K] [Algebra K S] [IsScalarTower R K S] [IsFractionRing R K] : minpolyDiv R x = minpolyDiv K x

theorem coeff_minpolyDiv_sub_pow_mem_span {R : Type u_2} {S : Type u_1} [CommRing R] [CommRing S] [Algebra R S] {x : S} (hx : IsIntegral R x) {i : ℕ} (hi : i ≤ (minpolyDiv R x).natDegree) : (minpolyDiv R x).coeff ((minpolyDiv R x).natDegree - i) - x ^ i ∈ Submodule.span R ((fun (x_1 : ℕ) => x ^ x_1) '' Set.Iio i)

theorem span_coeff_minpolyDiv {R : Type u_2} {S : Type u_1} [CommRing R] [CommRing S] [Algebra R S] {x : S} (hx : IsIntegral R x) : Submodule.span R (Set.range (minpolyDiv R x).coeff) = Subalgebra.toSubmodule (Algebra.adjoin R {x})

theorem sum_smul_minpolyDiv_eq_X_pow {K : Type u_2} {L : Type u_3} [Field K] [Field L] [Algebra K L] (E : Type u_1) [Field E] [Algebra K E] [IsAlgClosed E] [FiniteDimensional K L] [IsSeparable K L] {x : L} (hxL : Algebra.adjoin K {x} = ⊤) {r : ℕ} (hr : r < FiniteDimensional.finrank K L) : (Finset.univ.sum fun (σ : L →ₐ[K] E) => Polynomial.map (↑σ) ((x ^ r / (Polynomial.aeval x) (Polynomial.derivative (minpoly K x))) • minpolyDiv K x)) = Polynomial.X ^ r