Separable polynomials #

We define a polynomial to be separable if it is coprime with its derivative. We prove basic properties about separable polynomials here.

Main definitions #

Polynomial.Separable f: a polynomial f is separable iff it is coprime with its derivative.

source

def Polynomial.Separable {R : Type u} [CommSemiring R] (f : Polynomial R) :

Prop

A polynomial is separable iff it is coprime with its derivative.

Equations

Polynomial.Separable f = IsCoprime f (↑Polynomial.derivative f)

Instances For

source

theorem Polynomial.separable_def {R : Type u} [CommSemiring R] (f : Polynomial R) :

Polynomial.Separable f ↔ IsCoprime f (↑Polynomial.derivative f)

source

theorem Polynomial.separable_def' {R : Type u} [CommSemiring R] (f : Polynomial R) :

Polynomial.Separable f ↔ ∃ a b, a * f + b * ↑Polynomial.derivative f = 1

source

theorem Polynomial.not_separable_zero {R : Type u} [CommSemiring R] [Nontrivial R] :

¬Polynomial.Separable 0

source

theorem Polynomial.separable_one {R : Type u} [CommSemiring R] :

Polynomial.Separable 1

source

theorem Polynomial.separable_of_subsingleton {R : Type u} [CommSemiring R] [Subsingleton R] (f : Polynomial R) :

Polynomial.Separable f

source

theorem Polynomial.separable_X_add_C {R : Type u} [CommSemiring R] (a : R) :

Polynomial.Separable (Polynomial.X + ↑Polynomial.C a)

source

theorem Polynomial.separable_X {R : Type u} [CommSemiring R] :

Polynomial.Separable Polynomial.X

source

theorem Polynomial.separable_C {R : Type u} [CommSemiring R] (r : R) :

Polynomial.Separable (↑Polynomial.C r) ↔ IsUnit r

source

theorem Polynomial.Separable.of_mul_left {R : Type u} [CommSemiring R] {f : Polynomial R} {g : Polynomial R} (h : Polynomial.Separable (f * g)) :

Polynomial.Separable f

source

theorem Polynomial.Separable.of_mul_right {R : Type u} [CommSemiring R] {f : Polynomial R} {g : Polynomial R} (h : Polynomial.Separable (f * g)) :

Polynomial.Separable g

source

theorem Polynomial.Separable.of_dvd {R : Type u} [CommSemiring R] {f : Polynomial R} {g : Polynomial R} (hf : Polynomial.Separable f) (hfg : g ∣ f) :

Polynomial.Separable g

source

theorem Polynomial.separable_gcd_left {F : Type u_1} [Field F] {f : Polynomial F} (hf : Polynomial.Separable f) (g : Polynomial F) :

Polynomial.Separable (EuclideanDomain.gcd f g)

source

theorem Polynomial.separable_gcd_right {F : Type u_1} [Field F] {g : Polynomial F} (f : Polynomial F) (hg : Polynomial.Separable g) :

Polynomial.Separable (EuclideanDomain.gcd f g)

source

theorem Polynomial.Separable.isCoprime {R : Type u} [CommSemiring R] {f : Polynomial R} {g : Polynomial R} (h : Polynomial.Separable (f * g)) :

IsCoprime f g

source

theorem Polynomial.Separable.of_pow' {R : Type u} [CommSemiring R] {f : Polynomial R} {n : ℕ} (_h : Polynomial.Separable (f ^ n)) :

IsUnit f ∨ Polynomial.Separable f ∧ n = 1 ∨ n = 0

source

theorem Polynomial.Separable.of_pow {R : Type u} [CommSemiring R] {f : Polynomial R} (hf : ¬IsUnit f) {n : ℕ} (hn : n ≠ 0) (hfs : Polynomial.Separable (f ^ n)) :

Polynomial.Separable f ∧ n = 1

source

theorem Polynomial.Separable.map {R : Type u} [CommSemiring R] {S : Type v} [CommSemiring S] {p : Polynomial R} (h : Polynomial.Separable p) {f : R →+* S} :

Polynomial.Separable (Polynomial.map f p)

source

theorem Polynomial.isUnit_of_self_mul_dvd_separable {R : Type u} [CommSemiring R] {p : Polynomial R} {q : Polynomial R} (hp : Polynomial.Separable p) (hq : q * q ∣ p) :

IsUnit q

source

theorem Polynomial.multiplicity_le_one_of_separable {R : Type u} [CommSemiring R] {p : Polynomial R} {q : Polynomial R} (hq : ¬IsUnit q) (hsep : Polynomial.Separable p) :

multiplicity q p ≤ 1

source

theorem Polynomial.Separable.squarefree {R : Type u} [CommSemiring R] {p : Polynomial R} (hsep : Polynomial.Separable p) :

Squarefree p

source

theorem Polynomial.separable_X_sub_C {R : Type u} [CommRing R] {x : R} :

Polynomial.Separable (Polynomial.X - ↑Polynomial.C x)

source

theorem Polynomial.Separable.mul {R : Type u} [CommRing R] {f : Polynomial R} {g : Polynomial R} (hf : Polynomial.Separable f) (hg : Polynomial.Separable g) (h : IsCoprime f g) :

Polynomial.Separable (f * g)

source

theorem Polynomial.separable_prod' {R : Type u} [CommRing R] {ι : Type u_1} {f : ι → Polynomial R} {s : Finset ι} :

(∀ (x : ι), x ∈ s → ∀ (y : ι), y ∈ s → x ≠ y → IsCoprime (f x) (f y)) → (∀ (x : ι), x ∈ s → Polynomial.Separable (f x)) → Polynomial.Separable (Finset.prod s fun x => f x)

source

theorem Polynomial.separable_prod {R : Type u} [CommRing R] {ι : Type u_1} [Fintype ι] {f : ι → Polynomial R} (h1 : Pairwise (IsCoprime on f)) (h2 : ∀ (x : ι), Polynomial.Separable (f x)) :

Polynomial.Separable (Finset.prod Finset.univ fun x => f x)

source

theorem Polynomial.Separable.inj_of_prod_X_sub_C {R : Type u} [CommRing R] [Nontrivial R] {ι : Type u_1} {f : ι → R} {s : Finset ι} (hfs : Polynomial.Separable (Finset.prod s fun i => Polynomial.X - ↑Polynomial.C (f i))) {x : ι} {y : ι} (hx : x ∈ s) (hy : y ∈ s) (hfxy : f x = f y) :

x = y

source

theorem Polynomial.Separable.injective_of_prod_X_sub_C {R : Type u} [CommRing R] [Nontrivial R] {ι : Type u_1} [Fintype ι] {f : ι → R} (hfs : Polynomial.Separable (Finset.prod Finset.univ fun i => Polynomial.X - ↑Polynomial.C (f i))) :

Function.Injective f

source

theorem Polynomial.nodup_of_separable_prod {R : Type u} [CommRing R] [Nontrivial R] {s : Multiset R} (hs : Polynomial.Separable (Multiset.prod (Multiset.map (fun a => Polynomial.X - ↑Polynomial.C a) s))) :

Multiset.Nodup s

source

theorem Polynomial.separable_X_pow_sub_C_unit {R : Type u} [CommRing R] {n : ℕ} (u : Rˣ) (hn : IsUnit ↑n) :

Polynomial.Separable (Polynomial.X ^ n - ↑Polynomial.C ↑u)

If IsUnit n in a CommRing R, then X ^ n - u is separable for any unit u.

source

theorem Polynomial.rootMultiplicity_le_one_of_separable {R : Type u} [CommRing R] [Nontrivial R] {p : Polynomial R} (hsep : Polynomial.Separable p) (x : R) :

Polynomial.rootMultiplicity x p ≤ 1

source

theorem Polynomial.count_roots_le_one {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hsep : Polynomial.Separable p) (x : R) :

Multiset.count x (Polynomial.roots p) ≤ 1

source

theorem Polynomial.nodup_roots {R : Type u} [CommRing R] [IsDomain R] {p : Polynomial R} (hsep : Polynomial.Separable p) :

Multiset.Nodup (Polynomial.roots p)

source

theorem Polynomial.separable_iff_derivative_ne_zero {F : Type u} [Field F] {f : Polynomial F} (hf : Irreducible f) :

Polynomial.Separable f ↔ ↑Polynomial.derivative f ≠ 0

source

theorem Polynomial.separable_map {F : Type u} [Field F] {K : Type v} [Field K] (f : F →+* K) {p : Polynomial F} :

Polynomial.Separable (Polynomial.map f p) ↔ Polynomial.Separable p

source

theorem Polynomial.separable_prod_X_sub_C_iff' {F : Type u} [Field F] {ι : Type u_1} {f : ι → F} {s : Finset ι} :

Polynomial.Separable (Finset.prod s fun i => Polynomial.X - ↑Polynomial.C (f i)) ↔ ∀ (x : ι), x ∈ s → ∀ (y : ι), y ∈ s → f x = f y → x = y

source

theorem Polynomial.separable_prod_X_sub_C_iff {F : Type u} [Field F] {ι : Type u_1} [Fintype ι] {f : ι → F} :

Polynomial.Separable (Finset.prod Finset.univ fun i => Polynomial.X - ↑Polynomial.C (f i)) ↔ Function.Injective f

source

theorem Polynomial.separable_or {F : Type u} [Field F] (p : ℕ) [HF : CharP F p] {f : Polynomial F} (hf : Irreducible f) :

Polynomial.Separable f ∨ ¬Polynomial.Separable f ∧ ∃ g, Irreducible g ∧ ↑(Polynomial.expand F p) g = f

source

theorem Polynomial.exists_separable_of_irreducible {F : Type u} [Field F] (p : ℕ) [HF : CharP F p] {f : Polynomial F} (hf : Irreducible f) (hp : p ≠ 0) :

∃ n g, Polynomial.Separable g ∧ ↑(Polynomial.expand F (p ^ n)) g = f

source

theorem Polynomial.isUnit_or_eq_zero_of_separable_expand {F : Type u} [Field F] (p : ℕ) [HF : CharP F p] {f : Polynomial F} (n : ℕ) (hp : 0 < p) (hf : Polynomial.Separable (↑(Polynomial.expand F (p ^ n)) f)) :

IsUnit f ∨ n = 0

source

theorem Polynomial.unique_separable_of_irreducible {F : Type u} [Field F] (p : ℕ) [HF : CharP F p] {f : Polynomial F} (hf : Irreducible f) (hp : 0 < p) (n₁ : ℕ) (g₁ : Polynomial F) (hg₁ : Polynomial.Separable g₁) (hgf₁ : ↑(Polynomial.expand F (p ^ n₁)) g₁ = f) (n₂ : ℕ) (g₂ : Polynomial F) (hg₂ : Polynomial.Separable g₂) (hgf₂ : ↑(Polynomial.expand F (p ^ n₂)) g₂ = f) :

n₁ = n₂ ∧ g₁ = g₂

source

theorem Polynomial.separable_X_pow_sub_C {F : Type u} [Field F] {n : ℕ} (a : F) (hn : ↑n ≠ 0) (ha : a ≠ 0) :

Polynomial.Separable (Polynomial.X ^ n - ↑Polynomial.C a)

If n ≠ 0 in F, then X ^ n - a is separable for any a ≠ 0.

source

theorem Polynomial.X_pow_sub_one_separable_iff {F : Type u} [Field F] {n : ℕ} :

Polynomial.Separable (Polynomial.X ^ n - 1) ↔ ↑n ≠ 0

In a field F, X ^ n - 1 is separable iff ↑n ≠ 0.

source

theorem Polynomial.card_rootSet_eq_natDegree {F : Type u} [Field F] {K : Type v} [Field K] [Algebra F K] {p : Polynomial F} (hsep : Polynomial.Separable p) (hsplit : Polynomial.Splits (algebraMap F K) p) :

Fintype.card ↑(Polynomial.rootSet p K) = Polynomial.natDegree p

source

theorem Polynomial.eq_X_sub_C_of_separable_of_root_eq {F : Type u} [Field F] {K : Type v} [Field K] {i : F →+* K} {x : F} {h : Polynomial F} (h_sep : Polynomial.Separable h) (h_root : Polynomial.eval x h = 0) (h_splits : Polynomial.Splits i h) (h_roots : ∀ (y : K), y ∈ Polynomial.roots (Polynomial.map i h) → y = ↑i x) :

h = ↑Polynomial.C (Polynomial.leadingCoeff h) * (Polynomial.X - ↑Polynomial.C x)

source

theorem Polynomial.exists_finset_of_splits {F : Type u} [Field F] {K : Type v} [Field K] (i : F →+* K) {f : Polynomial F} (sep : Polynomial.Separable f) (sp : Polynomial.Splits i f) :

∃ s, Polynomial.map i f = ↑Polynomial.C (↑i (Polynomial.leadingCoeff f)) * Finset.prod s fun a => Polynomial.X - ↑Polynomial.C a

source

theorem Irreducible.separable {F : Type u} [Field F] [CharZero F] {f : Polynomial F} (hf : Irreducible f) :

Polynomial.Separable f

source

class IsSeparable (F : Type u_1) (K : Type u_2) [CommRing F] [Ring K] [Algebra F K] :

Prop

isIntegral' : ∀ (x : K), IsIntegral F x
separable' : ∀ (x : K), Polynomial.Separable (minpoly F x)

Typeclass for separable field extension: K is a separable field extension of F iff the minimal polynomial of every x : K is separable.

We define this for general (commutative) rings and only assume F and K are fields if this is needed for a proof.

Instances

source

theorem IsSeparable.isIntegral (F : Type u_3) {K : Type u_4} [CommRing F] [Ring K] [Algebra F K] [IsSeparable F K] (x : K) :

IsIntegral F x

source

theorem IsSeparable.separable (F : Type u_3) {K : Type u_4} [CommRing F] [Ring K] [Algebra F K] [IsSeparable F K] (x : K) :

Polynomial.Separable (minpoly F x)

source

theorem isSeparable_iff {F : Type u_5} {K : Type u_6} [CommRing F] [Ring K] [Algebra F K] :

IsSeparable F K ↔ ∀ (x : K), IsIntegral F x ∧ Polynomial.Separable (minpoly F x)

source

instance isSeparable_self (F : Type u_1) [Field F] :

IsSeparable F F

Equations

isSeparable_self = isSeparable_self.proof_1

source

instance IsSeparable.of_finite (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [FiniteDimensional F K] [CharZero F] :

IsSeparable F K

A finite field extension in characteristic 0 is separable.

Equations

IsSeparable.of_finite = IsSeparable.of_finite.proof_1

source

theorem isSeparable_tower_top_of_isSeparable (F : Type u_1) (K : Type u_2) (E : Type u_3) [Field F] [Field K] [Field E] [Algebra F K] [Algebra F E] [Algebra K E] [IsScalarTower F K E] [IsSeparable F E] :

IsSeparable K E

source

theorem isSeparable_tower_bot_of_isSeparable (F : Type u_1) (K : Type u_2) (E : Type u_3) [Field F] [Field K] [Field E] [Algebra F K] [Algebra F E] [Algebra K E] [IsScalarTower F K E] [h : IsSeparable F E] :

IsSeparable F K

source

theorem IsSeparable.of_algHom (F : Type u_1) {E : Type u_3} [Field F] [Field E] [Algebra F E] (E' : Type u_4) [Field E'] [Algebra F E'] (f : E →ₐ[F] E') [IsSeparable F E'] :

IsSeparable F E

source

theorem AlgHom.card_of_powerBasis {S : Type u_2} [CommRing S] {K : Type u_4} {L : Type u_5} [Field K] [Field L] [Algebra K S] [Algebra K L] (pb : PowerBasis K S) (h_sep : Polynomial.Separable (minpoly K pb.gen)) (h_splits : Polynomial.Splits (algebraMap K L) (minpoly K pb.gen)) :

Fintype.card (S →ₐ[K] L) = pb.dim