mathlib documentation

field_theory.splitting_field

Splitting fields #

This file introduces the notion of a splitting field of a polynomial and provides an embedding from a splitting field to any field that splits the polynomial. A polynomial f : polynomial K splits over a field extension L of K if it is zero or all of its irreducible factors over L have degree 1. A field extension of K of a polynomial f : polynomial K is called a splitting field if it is the smallest field extension of K such that f splits.

Main definitions #

polynomial.splits i f: A predicate on a field homomorphism i : K → L and a polynomial f saying that f is zero or all of its irreducible factors over L have degree 1.
polynomial.splitting_field f: A fixed splitting field of the polynomial f.
polynomial.is_splitting_field: A predicate on a field to be a splitting field of a polynomial f.

Main statements #

polynomial.C_leading_coeff_mul_prod_multiset_X_sub_C: If a polynomial has as many roots as its degree, it can be written as the product of its leading coefficient with ∏ (X - a) where a ranges through its roots.
lift_of_splits: If K and L are field extensions of a field F and for some finite subset S of K, the minimal polynomial of every x ∈ K splits as a polynomial with coefficients in L, then algebra.adjoin F S embeds into L.
polynomial.is_splitting_field.lift: An embedding of a splitting field of the polynomial f into another field such that f splits.
polynomial.is_splitting_field.alg_equiv: Every splitting field of a polynomial f is isomorphic to splitting_field f and thus, being a splitting field is unique up to isomorphism.

def polynomial.splits {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) (f : K[X]) :

Prop

A polynomial splits iff it is zero or all of its irreducible factors have degree 1.

Equations

polynomial.splits i f = (f = 0 ∨ ∀ {g : L[X]}, irreducible g → g ∣ polynomial.map i f → g.degree = 1)

@[simp]

theorem polynomial.splits_zero {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) :

polynomial.splits i 0

@[simp]

theorem polynomial.splits_C {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) (a : K) :

polynomial.splits i (⇑polynomial.C a)

theorem polynomial.splits_of_degree_eq_one {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : K[X]} (hf : f.degree = 1) :

polynomial.splits i f

theorem polynomial.splits_of_degree_le_one {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : K[X]} (hf : f.degree ≤ 1) :

polynomial.splits i f

theorem polynomial.splits_of_nat_degree_le_one {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : K[X]} (hf : f.nat_degree ≤ 1) :

polynomial.splits i f

theorem polynomial.splits_of_nat_degree_eq_one {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : K[X]} (hf : f.nat_degree = 1) :

polynomial.splits i f

theorem polynomial.splits_mul {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f g : K[X]} (hf : polynomial.splits i f) (hg : polynomial.splits i g) :

polynomial.splits i (f * g)

theorem polynomial.splits_of_splits_mul {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f g : K[X]} (hfg : f * g ≠ 0) (h : polynomial.splits i (f * g)) :

polynomial.splits i f ∧ polynomial.splits i g

theorem polynomial.splits_of_splits_of_dvd {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f g : K[X]} (hf0 : f ≠ 0) (hf : polynomial.splits i f) (hgf : g ∣ f) :

polynomial.splits i g

theorem polynomial.splits_of_splits_gcd_left {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f g : K[X]} (hf0 : f ≠ 0) (hf : polynomial.splits i f) :

polynomial.splits i (euclidean_domain.gcd f g)

theorem polynomial.splits_of_splits_gcd_right {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f g : K[X]} (hg0 : g ≠ 0) (hg : polynomial.splits i g) :

polynomial.splits i (euclidean_domain.gcd f g)

theorem polynomial.splits_map_iff {F : Type u} {K : Type v} {L : Type w} [field K] [field L] [field F] (i : K →+* L) (j : L →+* F) {f : K[X]} :

polynomial.splits j (polynomial.map i f) ↔ polynomial.splits (j.comp i) f

theorem polynomial.splits_one {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) :

polynomial.splits i 1

theorem polynomial.splits_of_is_unit {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {u : K[X]} (hu : is_unit u) :

polynomial.splits i u

theorem polynomial.splits_X_sub_C {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {x : K} :

polynomial.splits i (polynomial.X - ⇑polynomial.C x)

theorem polynomial.splits_X {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) :

polynomial.splits i polynomial.X

theorem polynomial.splits_id_iff_splits {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : K[X]} :

polynomial.splits (ring_hom.id L) (polynomial.map i f) ↔ polynomial.splits i f

theorem polynomial.splits_mul_iff {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f g : K[X]} (hf : f ≠ 0) (hg : g ≠ 0) :

polynomial.splits i (f * g) ↔ polynomial.splits i f ∧ polynomial.splits i g

theorem polynomial.splits_prod {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {ι : Type u} {s : ι → K[X]} {t : finset ι} :

(∀ (j : ι), j ∈ t → polynomial.splits i (s j)) → polynomial.splits i (∏ (x : ι) in t, s x)

theorem polynomial.splits_pow {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : K[X]} (hf : polynomial.splits i f) (n : ℕ) :

polynomial.splits i (f ^ n)

theorem polynomial.splits_X_pow {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) (n : ℕ) :

polynomial.splits i (polynomial.X ^ n)

theorem polynomial.splits_prod_iff {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {ι : Type u} {s : ι → K[X]} {t : finset ι} :

(∀ (j : ι), j ∈ t → s j ≠ 0) → (polynomial.splits i (∏ (x : ι) in t, s x) ↔ ∀ (j : ι), j ∈ t → polynomial.splits i (s j))

theorem polynomial.degree_eq_one_of_irreducible_of_splits {L : Type w} [field L] {p : L[X]} (hp : irreducible p) (hp_splits : polynomial.splits (ring_hom.id L) p) :

theorem polynomial.exists_root_of_splits {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : K[X]} (hs : polynomial.splits i f) (hf0 : f.degree ≠ 0) :

∃ (x : L), polynomial.eval₂ i x f = 0

theorem polynomial.exists_multiset_of_splits {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : K[X]} :

polynomial.splits i f → (∃ (s : multiset L), polynomial.map i f = (⇑polynomial.C (⇑i f.leading_coeff)) * (multiset.map (λ (a : L), polynomial.X - ⇑polynomial.C a) s).prod)

noncomputable def polynomial.root_of_splits {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : K[X]} (hf : polynomial.splits i f) (hfd : f.degree ≠ 0) :

L

Pick a root of a polynomial that splits.

Equations

polynomial.root_of_splits i hf hfd = classical.some _

theorem polynomial.map_root_of_splits {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : K[X]} (hf : polynomial.splits i f) (hfd : f.degree ≠ 0) :

polynomial.eval₂ i (polynomial.root_of_splits i hf hfd) f = 0

theorem polynomial.roots_map {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : K[X]} (hf : polynomial.splits (ring_hom.id K) f) :

(polynomial.map i f).roots = multiset.map ⇑i f.roots

theorem polynomial.eq_prod_roots_of_splits {K : Type v} {L : Type w} [field K] [field L] {p : K[X]} {i : K →+* L} (hsplit : polynomial.splits i p) :

polynomial.map i p = (⇑polynomial.C (⇑i p.leading_coeff)) * (multiset.map (λ (a : L), polynomial.X - ⇑polynomial.C a) (polynomial.map i p).roots).prod

theorem polynomial.eq_prod_roots_of_splits_id {K : Type v} [field K] {p : K[X]} (hsplit : polynomial.splits (ring_hom.id K) p) :

p = (⇑polynomial.C p.leading_coeff) * (multiset.map (λ (a : K), polynomial.X - ⇑polynomial.C a) p.roots).prod

theorem polynomial.eq_prod_roots_of_monic_of_splits_id {K : Type v} [field K] {p : K[X]} (m : p.monic) (hsplit : polynomial.splits (ring_hom.id K) p) :

p = (multiset.map (λ (a : K), polynomial.X - ⇑polynomial.C a) p.roots).prod

theorem polynomial.eq_X_sub_C_of_splits_of_single_root {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {x : K} {h : K[X]} (h_splits : polynomial.splits i h) (h_roots : (polynomial.map i h).roots = {⇑i x}) :

h = (⇑polynomial.C h.leading_coeff) * (polynomial.X - ⇑polynomial.C x)

theorem polynomial.nat_degree_eq_card_roots {K : Type v} {L : Type w} [field K] [field L] {p : K[X]} {i : K →+* L} (hsplit : polynomial.splits i p) :

p.nat_degree = ⇑multiset.card (polynomial.map i p).roots

theorem polynomial.degree_eq_card_roots {K : Type v} {L : Type w} [field K] [field L] {p : K[X]} {i : K →+* L} (p_ne_zero : p ≠ 0) (hsplit : polynomial.splits i p) :

p.degree = ↑(⇑multiset.card (polynomial.map i p).roots)

theorem polynomial.splits_of_exists_multiset {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : K[X]} {s : multiset L} (hs : polynomial.map i f = (⇑polynomial.C (⇑i f.leading_coeff)) * (multiset.map (λ (a : L), polynomial.X - ⇑polynomial.C a) s).prod) :

polynomial.splits i f

theorem polynomial.splits_of_splits_id {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : K[X]} :

polynomial.splits (ring_hom.id K) f → polynomial.splits i f

theorem polynomial.splits_iff_exists_multiset {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : K[X]} :

polynomial.splits i f ↔ ∃ (s : multiset L), polynomial.map i f = (⇑polynomial.C (⇑i f.leading_coeff)) * (multiset.map (λ (a : L), polynomial.X - ⇑polynomial.C a) s).prod

theorem polynomial.splits_comp_of_splits {F : Type u} {K : Type v} {L : Type w} [field K] [field L] [field F] (i : K →+* L) (j : L →+* F) {f : K[X]} (h : polynomial.splits i f) :

polynomial.splits (j.comp i) f

theorem polynomial.prod_multiset_X_sub_C_of_monic_of_roots_card_eq {K : Type u_1} [comm_ring K] [is_domain K] {p : K[X]} (hmonic : p.monic) (hroots : ⇑multiset.card p.roots = p.nat_degree) :

(multiset.map (λ (a : K), polynomial.X - ⇑polynomial.C a) p.roots).prod = p

theorem polynomial.C_leading_coeff_mul_prod_multiset_X_sub_C {K : Type u_1} [comm_ring K] [is_domain K] {p : K[X]} (hroots : ⇑multiset.card p.roots = p.nat_degree) :

(⇑polynomial.C p.leading_coeff) * (multiset.map (λ (a : K), polynomial.X - ⇑polynomial.C a) p.roots).prod = p

A polynomial p that has as many roots as its degree can be written p = p.leading_coeff * ∏(X - a), for a in p.roots.

theorem polynomial.splits_iff_card_roots {K : Type v} [field K] {p : K[X]} :

polynomial.splits (ring_hom.id K) p ↔ ⇑multiset.card p.roots = p.nat_degree

A polynomial splits if and only if it has as many roots as its degree.

theorem polynomial.aeval_root_derivative_of_splits {K : Type v} {L : Type w} [field K] [field L] [algebra K L] {P : K[X]} (hmo : P.monic) (hP : polynomial.splits (algebra_map K L) P) {r : L} (hr : r ∈ (polynomial.map (algebra_map K L) P).roots) :

⇑(polynomial.aeval r) (⇑polynomial.derivative P) = (multiset.map (λ (a : L), r - a) ((polynomial.map (algebra_map K L) P).roots.erase r)).prod

theorem polynomial.prod_roots_eq_coeff_zero_of_monic_of_split {K : Type v} [field K] {P : K[X]} (hmo : P.monic) (hP : polynomial.splits (ring_hom.id K) P) :

P.coeff 0 = ((-1) ^ P.nat_degree) * P.roots.prod

If P is a monic polynomial that splits, then coeff P 0 equals the product of the roots.

theorem polynomial.sum_roots_eq_next_coeff_of_monic_of_split {K : Type v} [field K] {P : K[X]} (hmo : P.monic) (hP : polynomial.splits (ring_hom.id K) P) :

P.next_coeff = -P.roots.sum

If P is a monic polynomial that splits, then P.next_coeff equals the sum of the roots.

noncomputable def alg_equiv.adjoin_singleton_equiv_adjoin_root_minpoly (F : Type u) [field F] {R : Type u_1} [comm_ring R] [algebra F R] (x : R) :

↥(algebra.adjoin F {x}) ≃ₐ[F] adjoin_root (minpoly F x)

If p is the minimal polynomial of a over F then F[a] ≃ₐ[F] F[x]/(p)

Equations

alg_equiv.adjoin_singleton_equiv_adjoin_root_minpoly F x = (alg_equiv.of_bijective ((adjoin_root.lift_hom (minpoly F x) x _).cod_restrict (algebra.adjoin F {x}) _) _).symm

theorem finite_dimensional.of_subalgebra_to_submodule {K : Type u_1} {V : Type u_2} [field K] [ring V] [algebra K V] {s : subalgebra K V} (h : finite_dimensional K ↥(s.to_submodule)) :

finite_dimensional K ↥s

If a subalgebra is finite_dimensional as a submodule then it is finite_dimensional.

theorem lift_of_splits {F : Type u_1} {K : Type u_2} {L : Type u_3} [field F] [field K] [field L] [algebra F K] [algebra F L] (s : finset K) :

(∀ (x : K), x ∈ s → is_integral F x ∧ polynomial.splits (algebra_map F L) (minpoly F x)) → nonempty (↥(algebra.adjoin F ↑s) →ₐ[F] L)

If K and L are field extensions of F and we have s : finset K such that the minimal polynomial of each x ∈ s splits in L then algebra.adjoin F s embeds in L.

noncomputable def polynomial.factor {K : Type v} [field K] (f : K[X]) :

Non-computably choose an irreducible factor from a polynomial.

Equations

f.factor = dite (∃ (g : K[X]), irreducible g ∧ g ∣ f) (λ (H : ∃ (g : K[X]), irreducible g ∧ g ∣ f), classical.some H) (λ (H : ¬∃ (g : K[X]), irreducible g ∧ g ∣ f), polynomial.X)

@[protected, instance]

def polynomial.irreducible_factor {K : Type v} [field K] (f : K[X]) :

irreducible f.factor

theorem polynomial.factor_dvd_of_not_is_unit {K : Type v} [field K] {f : K[X]} (hf1 : ¬is_unit f) :

theorem polynomial.factor_dvd_of_degree_ne_zero {K : Type v} [field K] {f : K[X]} (hf : f.degree ≠ 0) :

theorem polynomial.factor_dvd_of_nat_degree_ne_zero {K : Type v} [field K] {f : K[X]} (hf : f.nat_degree ≠ 0) :

noncomputable def polynomial.remove_factor {K : Type v} [field K] (f : K[X]) :

(adjoin_root f.factor)[X]

Divide a polynomial f by X - C r where r is a root of f in a bigger field extension.

Equations

f.remove_factor = polynomial.map (adjoin_root.of f.factor) f /ₘ (polynomial.X - ⇑polynomial.C (adjoin_root.root f.factor))

theorem polynomial.X_sub_C_mul_remove_factor {K : Type v} [field K] (f : K[X]) (hf : f.nat_degree ≠ 0) :

(polynomial.X - ⇑polynomial.C (adjoin_root.root f.factor)) * f.remove_factor = polynomial.map (adjoin_root.of f.factor) f

theorem polynomial.nat_degree_remove_factor {K : Type v} [field K] (f : K[X]) :

f.remove_factor.nat_degree = f.nat_degree - 1

theorem polynomial.nat_degree_remove_factor' {K : Type v} [field K] {f : K[X]} {n : ℕ} (hfn : f.nat_degree = n + 1) :

f.remove_factor.nat_degree = n

def polynomial.splitting_field_aux (n : ℕ) {K : Type u} [field K] (f : K[X]) :

f.nat_degree = n → Type u

Auxiliary construction to a splitting field of a polynomial. Uses induction on the degree.

Equations

polynomial.splitting_field_aux n = n.rec_on (λ (K : Type u) (_x : field K) (_x_1 : K[X]) (_x : _x_1.nat_degree = 0), K) (λ (n : ℕ) (ih : Π {K : Type u} [_inst_4 : field K] (f : K[X]), f.nat_degree = n → Type u) (K : Type u) (_x : field K) (f : K[X]) (hf : f.nat_degree = n.succ), ih f.remove_factor _)

theorem polynomial.splitting_field_aux.succ {K : Type v} [field K] (n : ℕ) (f : K[X]) (hfn : f.nat_degree = n + 1) :

polynomial.splitting_field_aux (n + 1) f hfn = polynomial.splitting_field_aux n f.remove_factor _

@[protected, instance]

noncomputable def polynomial.splitting_field_aux.field (n : ℕ) {K : Type u} [field K] {f : K[X]} (hfn : f.nat_degree = n) :

field (polynomial.splitting_field_aux n f hfn)

Equations

polynomial.splitting_field_aux.field n = n.rec_on (λ (K : Type u) (_x : field K) (_x_1 : K[X]) (_x_1 : _x_1.nat_degree = 0), _x) (λ (n : ℕ) (ih : Π {K : Type u} [_inst_4 : field K] {f : K[X]} (hfn : f.nat_degree = n), field (polynomial.splitting_field_aux n f hfn)) (K : Type u) (_x : field K) (f : K[X]) (hf : f.nat_degree = n.succ), ih _)

@[protected, instance]

noncomputable def polynomial.splitting_field_aux.inhabited {K : Type v} [field K] {n : ℕ} {f : K[X]} (hfn : f.nat_degree = n) :

inhabited (polynomial.splitting_field_aux n f hfn)

Equations

polynomial.splitting_field_aux.inhabited hfn = {default := 37}

@[protected, instance]

noncomputable def polynomial.splitting_field_aux.algebra (n : ℕ) (R : Type u_1) {K : Type u} [comm_semiring R] [field K] [algebra R K] {f : K[X]} (hfn : f.nat_degree = n) :

algebra R (polynomial.splitting_field_aux n f hfn)

Equations

polynomial.splitting_field_aux.algebra n = n.rec_on (λ (R : Type u_1) (K : Type u) (_x : comm_semiring R) (_x_1 : field K) (_x : algebra R K) (_x_2 : K[X]) (_x_1 : _x_2.nat_degree = 0), _x) (λ (n : ℕ) (ih : Π (R : Type u_1) {K : Type u} [_inst_4 : comm_semiring R] [_inst_5 : field K] [_inst_6 : algebra R K] {f : K[X]} (hfn : f.nat_degree = n), algebra R (polynomial.splitting_field_aux n f hfn)) (R : Type u_1) (K : Type u) (_x : comm_semiring R) (_x_1 : field K) (_x_2 : algebra R K) (f : K[X]) (hfn : f.nat_degree = n.succ), ih R _)

@[protected, instance]

def polynomial.splitting_field_aux.is_scalar_tower (n : ℕ) (R₁ : Type u_1) (R₂ : Type u_2) {K : Type u} [comm_semiring R₁] [comm_semiring R₂] [has_scalar R₁ R₂] [field K] [algebra R₁ K] [algebra R₂ K] [is_scalar_tower R₁ R₂ K] {f : K[X]} (hfn : f.nat_degree = n) :

is_scalar_tower R₁ R₂ (polynomial.splitting_field_aux n f hfn)

@[protected, instance]

noncomputable def polynomial.splitting_field_aux.algebra''' {K : Type v} [field K] {n : ℕ} {f : K[X]} (hfn : f.nat_degree = n + 1) :

algebra (adjoin_root f.factor) (polynomial.splitting_field_aux n f.remove_factor _)

Equations

polynomial.splitting_field_aux.algebra''' hfn = polynomial.splitting_field_aux.algebra n (adjoin_root f.factor) _

@[protected, instance]

noncomputable def polynomial.splitting_field_aux.algebra' {K : Type v} [field K] {n : ℕ} {f : K[X]} (hfn : f.nat_degree = n + 1) :

algebra (adjoin_root f.factor) (polynomial.splitting_field_aux n.succ f hfn)

Equations

polynomial.splitting_field_aux.algebra' hfn = polynomial.splitting_field_aux.algebra''' hfn

@[protected, instance]

noncomputable def polynomial.splitting_field_aux.algebra'' {K : Type v} [field K] {n : ℕ} {f : K[X]} (hfn : f.nat_degree = n + 1) :

algebra K (polynomial.splitting_field_aux n f.remove_factor _)

Equations

polynomial.splitting_field_aux.algebra'' hfn = polynomial.splitting_field_aux.algebra n K _

@[protected, instance]

def polynomial.splitting_field_aux.scalar_tower' {K : Type v} [field K] {n : ℕ} {f : K[X]} (hfn : f.nat_degree = n + 1) :

is_scalar_tower K (adjoin_root f.factor) (polynomial.splitting_field_aux n f.remove_factor _)

@[protected, instance]

def polynomial.splitting_field_aux.scalar_tower {K : Type v} [field K] {n : ℕ} {f : K[X]} (hfn : f.nat_degree = n + 1) :

is_scalar_tower K (adjoin_root f.factor) (polynomial.splitting_field_aux (n + 1) f hfn)

theorem polynomial.splitting_field_aux.algebra_map_succ {K : Type v} [field K] (n : ℕ) (f : K[X]) (hfn : f.nat_degree = n + 1) :

algebra_map K (polynomial.splitting_field_aux (n + 1) f hfn) = (algebra_map (adjoin_root f.factor) (polynomial.splitting_field_aux n f.remove_factor _)).comp (adjoin_root.of f.factor)

@[protected]

theorem polynomial.splitting_field_aux.splits (n : ℕ) {K : Type u} [field K] (f : K[X]) (hfn : f.nat_degree = n) :

polynomial.splits (algebra_map K (polynomial.splitting_field_aux n f hfn)) f

theorem polynomial.splitting_field_aux.exists_lift (n : ℕ) {K : Type u} [field K] (f : K[X]) (hfn : f.nat_degree = n) {L : Type u_1} [field L] (j : K →+* L) (hf : polynomial.splits j f) :

∃ (k : polynomial.splitting_field_aux n f hfn →+* L), k.comp (algebra_map K (polynomial.splitting_field_aux n f hfn)) = j

theorem polynomial.splitting_field_aux.adjoin_roots (n : ℕ) {K : Type u} [field K] (f : K[X]) (hfn : f.nat_degree = n) :

algebra.adjoin K ↑((polynomial.map (algebra_map K (polynomial.splitting_field_aux n f hfn)) f).roots.to_finset) = ⊤

def polynomial.splitting_field {K : Type v} [field K] (f : K[X]) :

Type v

A splitting field of a polynomial.

Equations

f.splitting_field = polynomial.splitting_field_aux f.nat_degree f _

@[protected, instance]

noncomputable def polynomial.splitting_field.field {K : Type v} [field K] (f : K[X]) :

field f.splitting_field

Equations

polynomial.splitting_field.field f = polynomial.splitting_field_aux.field f.nat_degree _

@[protected, instance]

noncomputable def polynomial.splitting_field.inhabited {K : Type v} [field K] (f : K[X]) :

inhabited f.splitting_field

Equations

polynomial.splitting_field.inhabited f = {default := 37}

@[protected, instance]

noncomputable def polynomial.splitting_field.algebra' {K : Type v} [field K] (f : K[X]) {R : Type u_1} [comm_semiring R] [algebra R K] :

algebra R f.splitting_field

This should be an instance globally, but it creates diamonds with the ℕ and ℤ actions:

example :
  (add_comm_monoid.nat_module : module ℕ (splitting_field f)) =
    @algebra.to_module _ _ _ _ (splitting_field.algebra' f) :=
rfl  -- fails

example :
  (add_comm_group.int_module _ : module ℤ (splitting_field f)) =
    @algebra.to_module _ _ _ _ (splitting_field.algebra' f) :=
rfl  -- fails

Until we resolve these diamonds, it's more convenient to only turn this instance on with local attribute [instance] in places where the benefit of having the instance outweighs the cost.

In the meantime, the splitting_field.algebra instance below is immune to these particular diamonds since K = ℕ and K = ℤ are not possible due to the field K assumption. Diamonds in algebra ℚ (splitting_field f) instances are still possible, but this is a problem throughout the library and not unique to this algebra instance.

Equations

polynomial.splitting_field.algebra' f = polynomial.splitting_field_aux.algebra f.nat_degree R _

@[protected, instance]

noncomputable def polynomial.splitting_field.algebra {K : Type v} [field K] (f : K[X]) :

algebra K f.splitting_field

Equations

polynomial.splitting_field.algebra f = polynomial.splitting_field_aux.algebra f.nat_degree K _

@[protected]

theorem polynomial.splitting_field.splits {K : Type v} [field K] (f : K[X]) :

polynomial.splits (algebra_map K f.splitting_field) f

noncomputable def polynomial.splitting_field.lift {K : Type v} {L : Type w} [field K] [field L] (f : K[X]) [algebra K L] (hb : polynomial.splits (algebra_map K L) f) :

f.splitting_field →ₐ[K] L

Embeds the splitting field into any other field that splits the polynomial.

Equations

polynomial.splitting_field.lift f hb = {to_fun := (classical.some _).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}

theorem polynomial.splitting_field.adjoin_roots {K : Type v} [field K] (f : K[X]) :

algebra.adjoin K ↑((polynomial.map (algebra_map K f.splitting_field) f).roots.to_finset) = ⊤

theorem polynomial.splitting_field.adjoin_root_set {K : Type v} [field K] (f : K[X]) :

algebra.adjoin K (f.root_set f.splitting_field) = ⊤

@[class]

structure polynomial.is_splitting_field (K : Type v) (L : Type w) [field K] [field L] [algebra K L] (f : K[X]) :

Prop

splits : polynomial.splits (algebra_map K L) f
adjoin_roots : algebra.adjoin K ↑((polynomial.map (algebra_map K L) f).roots.to_finset) = ⊤

Typeclass characterising splitting fields.

Instances

@[protected, instance]

def polynomial.is_splitting_field.splitting_field {K : Type v} [field K] (f : K[X]) :

polynomial.is_splitting_field K f.splitting_field f

@[protected, instance]

def polynomial.is_splitting_field.map {F : Type u} {K : Type v} {L : Type w} [field K] [field L] [field F] [algebra K L] [algebra F K] [algebra F L] [is_scalar_tower F K L] (f : F[X]) [polynomial.is_splitting_field F L f] :

polynomial.is_splitting_field K L (polynomial.map (algebra_map F K) f)

theorem polynomial.is_splitting_field.splits_iff {K : Type v} (L : Type w) [field K] [field L] [algebra K L] (f : K[X]) [polynomial.is_splitting_field K L f] :

polynomial.splits (ring_hom.id K) f ↔ ⊤ = ⊥

theorem polynomial.is_splitting_field.mul {F : Type u} {K : Type v} (L : Type w) [field K] [field L] [field F] [algebra K L] [algebra F K] [algebra F L] [is_scalar_tower F K L] (f g : F[X]) (hf : f ≠ 0) (hg : g ≠ 0) [polynomial.is_splitting_field F K f] [polynomial.is_splitting_field K L (polynomial.map (algebra_map F K) g)] :

polynomial.is_splitting_field F L (f * g)

noncomputable def polynomial.is_splitting_field.lift {F : Type u} {K : Type v} (L : Type w) [field K] [field L] [field F] [algebra K L] [algebra K F] (f : K[X]) [polynomial.is_splitting_field K L f] (hf : polynomial.splits (algebra_map K F) f) :

Splitting field of f embeds into any field that splits f.

Equations

polynomial.is_splitting_field.lift L f hf = dite (f = 0) (λ (hf0 : f = 0), (algebra.of_id K F).comp (↑(algebra.bot_equiv K L).comp (_.mpr algebra.to_top))) (λ (hf0 : ¬f = 0), (_.mpr (classical.choice _)).comp algebra.to_top)

theorem polynomial.is_splitting_field.finite_dimensional {K : Type v} (L : Type w) [field K] [field L] [algebra K L] (f : K[X]) [polynomial.is_splitting_field K L f] :

finite_dimensional K L

@[protected, instance]

def polynomial.is_splitting_field.polynomial.splitting_field.finite_dimensional {K : Type v} [field K] (f : K[X]) :

finite_dimensional K f.splitting_field

noncomputable def polynomial.is_splitting_field.alg_equiv {K : Type v} (L : Type w) [field K] [field L] [algebra K L] (f : K[X]) [polynomial.is_splitting_field K L f] :

L ≃ₐ[K] f.splitting_field

Any splitting field is isomorphic to splitting_field f.

Equations

polynomial.is_splitting_field.alg_equiv L f = alg_equiv.of_bijective (polynomial.is_splitting_field.lift L f _) _