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 #

Main statements #

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

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

Equations
@[simp]
theorem polynomial.splits_zero {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) :
@[simp]
theorem polynomial.splits_C {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) (a : K) :
theorem polynomial.splits_of_degree_eq_one {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : polynomial K} (hf : f.degree = 1) :
theorem polynomial.splits_of_degree_le_one {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : polynomial K} (hf : f.degree 1) :
theorem polynomial.splits_of_nat_degree_le_one {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : polynomial K} (hf : f.nat_degree 1) :
theorem polynomial.splits_of_nat_degree_eq_one {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : polynomial K} (hf : f.nat_degree = 1) :
theorem polynomial.splits_mul {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f g : polynomial K} (hf : polynomial.splits i f) (hg : polynomial.splits i g) :
theorem polynomial.splits_of_splits_mul {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f g : polynomial K} (hfg : f * g 0) (h : polynomial.splits i (f * g)) :
theorem polynomial.splits_of_splits_of_dvd {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f g : polynomial K} (hf0 : f 0) (hf : polynomial.splits i f) (hgf : g f) :
theorem polynomial.splits_of_splits_gcd_left {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f g : polynomial K} (hf0 : f 0) (hf : polynomial.splits i f) :
theorem polynomial.splits_of_splits_gcd_right {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f g : polynomial K} (hg0 : g 0) (hg : polynomial.splits i 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 : polynomial K} :
theorem polynomial.splits_one {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) :
theorem polynomial.splits_of_is_unit {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {u : polynomial K} (hu : is_unit u) :
theorem polynomial.splits_X_sub_C {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {x : K} :
theorem polynomial.splits_X {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) :
theorem polynomial.splits_id_iff_splits {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : polynomial K} :
theorem polynomial.splits_mul_iff {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f g : polynomial K} (hf : f 0) (hg : g 0) :
theorem polynomial.splits_prod {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {ι : Type u} {s : ι → polynomial K} {t : finset ι} :
(∀ (j : ι), j tpolynomial.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 : polynomial K} (hf : polynomial.splits i f) (n : ) :
theorem polynomial.splits_X_pow {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) (n : ) :
theorem polynomial.splits_prod_iff {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {ι : Type u} {s : ι → polynomial K} {t : finset ι} :
(∀ (j : ι), j ts j 0)(polynomial.splits i (∏ (x : ι) in t, s x) ∀ (j : ι), j tpolynomial.splits i (s j))
theorem polynomial.degree_eq_one_of_irreducible_of_splits {L : Type w} [field L] {p : polynomial L} (h_nz : p 0) (hp : irreducible p) (hp_splits : polynomial.splits (ring_hom.id L) p) :
p.degree = 1
theorem polynomial.exists_root_of_splits {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : polynomial K} (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 : polynomial K} :
def polynomial.root_of_splits {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : polynomial K} (hf : polynomial.splits i f) (hfd : f.degree 0) :
L

Pick a root of a polynomial that splits.

Equations
theorem polynomial.map_root_of_splits {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : polynomial K} (hf : polynomial.splits i f) (hfd : f.degree 0) :
theorem polynomial.roots_map {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : polynomial K} (hf : polynomial.splits (ring_hom.id K) f) :
theorem polynomial.eq_prod_roots_of_splits {K : Type v} {L : Type w} [field K] [field L] {p : polynomial K} {i : K →+* L} (hsplit : polynomial.splits i p) :
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 : polynomial K} (h_splits : polynomial.splits i h) (h_roots : (polynomial.map i h).roots = {i x}) :
theorem polynomial.nat_degree_eq_card_roots {K : Type v} {L : Type w} [field K] [field L] {p : polynomial K} {i : K →+* L} (hsplit : polynomial.splits i p) :
theorem polynomial.degree_eq_card_roots {K : Type v} {L : Type w} [field K] [field L] {p : polynomial K} {i : K →+* L} (p_ne_zero : p 0) (hsplit : polynomial.splits i p) :
theorem polynomial.splits_of_exists_multiset {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : polynomial K} {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) :
theorem polynomial.splits_of_splits_id {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : polynomial K} :
theorem polynomial.splits_iff_exists_multiset {K : Type v} {L : Type w} [field K] [field L] (i : K →+* L) {f : polynomial K} :
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 : polynomial K} (h : polynomial.splits i f) :

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

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.

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

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) :

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

Equations
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)) :

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 sis_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.

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

Non-computably choose an irreducible factor from a polynomial.

Equations
@[instance]
theorem polynomial.factor_dvd_of_not_is_unit {K : Type v} [field K] {f : polynomial K} (hf1 : ¬is_unit f) :
theorem polynomial.factor_dvd_of_degree_ne_zero {K : Type v} [field K] {f : polynomial K} (hf : f.degree 0) :
theorem polynomial.factor_dvd_of_nat_degree_ne_zero {K : Type v} [field K] {f : polynomial K} (hf : f.nat_degree 0) :

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

Equations
theorem polynomial.nat_degree_remove_factor' {K : Type v} [field K] {f : polynomial K} {n : } (hfn : f.nat_degree = n + 1) :
def polynomial.splitting_field_aux (n : ) {K : Type u} [field K] (f : polynomial K) :
f.nat_degree = nType u

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

Equations
@[instance]
def polynomial.splitting_field_aux.field (n : ) {K : Type u} [field K] {f : polynomial K} (hfn : f.nat_degree = n) :
Equations
@[instance]
def polynomial.splitting_field_aux.algebra (n : ) {K : Type u} [field K] {f : polynomial K} (hfn : f.nat_degree = n) :
Equations
@[instance]
theorem polynomial.splitting_field_aux.exists_lift (n : ) {K : Type u} [field K] (f : polynomial K) (hfn : f.nat_degree = n) {L : Type u_1} [field L] (j : K →+* L) (hf : polynomial.splits j f) :
def polynomial.splitting_field {K : Type v} [field K] (f : polynomial K) :
Type v

A splitting field of a polynomial.

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

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

Equations
@[class]
structure polynomial.is_splitting_field (K : Type v) (L : Type w) [field K] [field L] [algebra K L] (f : polynomial K) :
Prop

Typeclass characterising splitting fields.

Instances
@[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 : polynomial F) [polynomial.is_splitting_field F L 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 : polynomial F) (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)] :
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 : polynomial K) [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

Any splitting field is isomorphic to splitting_field f.

Equations