mathlib docs: field_theory.splitting

source

def polynomial.splits {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) (f : polynomial α) :

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 : polynomial β}, irreducible g → g ∣ polynomial.map i f → g.degree = 1)

source

@[simp]

theorem polynomial.splits_zero {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) :

polynomial.splits i 0

source

@[simp]

theorem polynomial.splits_C {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) (a : α) :

polynomial.splits i (⇑polynomial.C a)

source

theorem polynomial.splits_of_degree_eq_one {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) {f : polynomial α} (hf : f.degree = 1) :

polynomial.splits i f

source

theorem polynomial.splits_of_degree_le_one {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) {f : polynomial α} (hf : f.degree ≤ 1) :

polynomial.splits i f

source

theorem polynomial.splits_mul {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) {f g : polynomial α} (hf : polynomial.splits i f) (hg : polynomial.splits i g) :

polynomial.splits i (f * g)

source

theorem polynomial.splits_of_splits_mul {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) {f g : polynomial α} (hfg : f * g ≠ 0) (h : polynomial.splits i (f * g)) :

polynomial.splits i f ∧ polynomial.splits i g

source

theorem polynomial.splits_of_splits_of_dvd {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) {f g : polynomial α} (hf0 : f ≠ 0) (hf : polynomial.splits i f) (hgf : g ∣ f) :

polynomial.splits i g

source

theorem polynomial.splits_of_splits_gcd_left {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) {f g : polynomial α} (hf0 : f ≠ 0) (hf : polynomial.splits i f) :

polynomial.splits i (euclidean_domain.gcd f g)

source

theorem polynomial.splits_of_splits_gcd_right {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) {f g : polynomial α} (hg0 : g ≠ 0) (hg : polynomial.splits i g) :

polynomial.splits i (euclidean_domain.gcd f g)

source

theorem polynomial.splits_map_iff {α : Type u} {β : Type v} {γ : Type w} [field α] [field β] [field γ] (i : α →+* β) (j : β →+* γ) {f : polynomial α} :

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

source

theorem polynomial.splits_one {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) :

polynomial.splits i 1

source

theorem polynomial.splits_of_is_unit {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) {u : polynomial α} (hu : is_unit u) :

polynomial.splits i u

source

theorem polynomial.splits_X_sub_C {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) {x : α} :

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

source

theorem polynomial.splits_id_iff_splits {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) {f : polynomial α} :

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

source

theorem polynomial.splits_mul_iff {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) {f g : polynomial α} (hf : f ≠ 0) (hg : g ≠ 0) :

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

source

theorem polynomial.splits_prod {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) {ι : Type w} {s : ι → polynomial α} {t : finset ι} (a : ∀ (j : ι), j ∈ t → polynomial.splits i (s j)) :

polynomial.splits i (∏ (x : ι) in t, s x)

source

theorem polynomial.splits_prod_iff {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) {ι : Type w} {s : ι → polynomial α} {t : finset ι} (a : ∀ (j : ι), j ∈ t → s j ≠ 0) :

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

source

theorem polynomial.degree_eq_one_of_irreducible_of_splits {β : Type v} [field β] {p : polynomial β} (h_nz : p ≠ 0) (hp : irreducible p) (hp_splits : polynomial.splits (ring_hom.id β) p) :

p.degree = 1

source

theorem polynomial.exists_root_of_splits {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) {f : polynomial α} (hs : polynomial.splits i f) (hf0 : f.degree ≠ 0) :

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

source

theorem polynomial.exists_multiset_of_splits {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) {f : polynomial α} (a : polynomial.splits i f) :

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

source

def polynomial.root_of_splits {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) {f : polynomial α} (hf : polynomial.splits i f) (hfd : f.degree ≠ 0) :

β

Pick a root of a polynomial that splits.

Equations

polynomial.root_of_splits i hf hfd = classical.some _

source

theorem polynomial.map_root_of_splits {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) {f : polynomial α} (hf : polynomial.splits i f) (hfd : f.degree ≠ 0) :

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

source

theorem polynomial.roots_map {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) {f : polynomial α} (hf : polynomial.splits (ring_hom.id α) f) :

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

source

theorem polynomial.eq_prod_roots_of_splits {α : Type u} {β : Type v} [field α] [field β] {p : polynomial α} {i : α →+* β} (hsplit : polynomial.splits i p) :

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

source

theorem polynomial.eq_X_sub_C_of_splits_of_single_root {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) {x : α} {h : polynomial α} (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)

source

theorem polynomial.nat_degree_multiset_prod {R : Type u_1} [integral_domain R] {s : multiset (polynomial R)} (h : ∀ (p : polynomial R), p ∈ s → p ≠ 0) :

s.prod.nat_degree = (multiset.map polynomial.nat_degree s).sum

source

theorem polynomial.nat_degree_eq_card_roots {α : Type u} {β : Type v} [field α] [field β] {p : polynomial α} {i : α →+* β} (hsplit : polynomial.splits i p) :

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

source

theorem polynomial.degree_eq_card_roots {α : Type u} {β : Type v} [field α] [field β] {p : polynomial α} {i : α →+* β} (p_ne_zero : p ≠ 0) (hsplit : polynomial.splits i p) :

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

source

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

polynomial.splits i f

source

theorem polynomial.splits_of_splits_id {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) {f : polynomial α} (a : polynomial.splits (ring_hom.id α) f) :

polynomial.splits i f

source

theorem polynomial.splits_iff_exists_multiset {α : Type u} {β : Type v} [field α] [field β] (i : α →+* β) {f : polynomial α} :

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

source

theorem polynomial.splits_comp_of_splits {α : Type u} {β : Type v} {γ : Type w} [field α] [field β] [field γ] (i : α →+* β) (j : β →+* γ) {f : polynomial α} (h : polynomial.splits i f) :

polynomial.splits (j.comp i) f

source

def alg_equiv.adjoin_singleton_equiv_adjoin_root_minimal_polynomial (F : Type u_1) [field F] {R : Type u_2} [comm_ring R] [algebra F R] (x : R) (hx : is_integral F x) :

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

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_minimal_polynomial F x hx = (alg_equiv.of_bijective ((adjoin_root.alg_hom (minimal_polynomial hx) x _).cod_restrict (algebra.adjoin F {x}) _) _).symm

source

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) (a : ∀ (x : K), x ∈ s → (∃ (H : is_integral F x), polynomial.splits (algebra_map F L) (minimal_polynomial H))) :

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.

source

def polynomial.factor {α : Type u} [field α] (f : polynomial α) :

polynomial α

Non-computably choose an irreducible factor from a polynomial.

Equations

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

source

@[instance]

def polynomial.irreducible_factor {α : Type u} [field α] (f : polynomial α) :

irreducible f.factor

source

theorem polynomial.factor_dvd_of_not_is_unit {α : Type u} [field α] {f : polynomial α} (hf1 : ¬is_unit f) :

f.factor ∣ f

source

theorem polynomial.factor_dvd_of_degree_ne_zero {α : Type u} [field α] {f : polynomial α} (hf : f.degree ≠ 0) :

f.factor ∣ f

source

theorem polynomial.factor_dvd_of_nat_degree_ne_zero {α : Type u} [field α] {f : polynomial α} (hf : f.nat_degree ≠ 0) :

f.factor ∣ f

source

def polynomial.remove_factor {α : Type u} [field α] (f : polynomial α) :

polynomial (adjoin_root f.factor)

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

source

theorem polynomial.X_sub_C_mul_remove_factor {α : Type u} [field α] (f : polynomial α) (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

source

theorem polynomial.nat_degree_remove_factor {α : Type u} [field α] (f : polynomial α) :

f.remove_factor.nat_degree = f.nat_degree - 1

source

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

f.remove_factor.nat_degree = n

source

def polynomial.splitting_field_aux (n : ℕ) {α : Type u} [field α] (f : polynomial α) (a : 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 (λ (α : Type u) (_x : field α) (_x_1 : polynomial α) (_x : _x_1.nat_degree = 0), α) (λ (n : ℕ) (ih : Π {α : Type u} [_inst_4 : field α] (f : polynomial α), f.nat_degree = n → Type u) (α : Type u) (_x : field α) (f : polynomial α) (hf : f.nat_degree = n.succ), ih f.remove_factor _)

source

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

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

source

@[instance]

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

field (polynomial.splitting_field_aux n f hfn)

Equations

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

source

@[instance]

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

inhabited (polynomial.splitting_field_aux n f hfn)

Equations

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

source

@[instance]

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

algebra α (polynomial.splitting_field_aux n f hfn)

Equations

polynomial.splitting_field_aux.algebra n = n.rec_on (λ (α : Type u) (_x : field α) (_x_1 : polynomial α) (_x_1 : _x_1.nat_degree = 0), algebra.id α) (λ (n : ℕ) (ih : Π {α : Type u} [_inst_4 : field α] {f : polynomial α} (hfn : f.nat_degree = n), algebra α (polynomial.splitting_field_aux n f hfn)) (α : Type u) (_x : field α) (f : polynomial α) (hfn : f.nat_degree = n.succ), algebra.comap.algebra α (adjoin_root f.factor) (polynomial.splitting_field_aux n f.remove_factor _))

source

@[instance]

def polynomial.splitting_field_aux.algebra' {α : Type u} [field α] {n : ℕ} {f : polynomial α} (hfn : f.nat_degree = n + 1) :

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

Equations

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

source

@[instance]

def polynomial.splitting_field_aux.algebra'' {α : Type u} [field α] {n : ℕ} {f : polynomial α} (hfn : f.nat_degree = n + 1) :

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

Equations

polynomial.splitting_field_aux.algebra'' hfn = polynomial.splitting_field_aux.algebra (n + 1) hfn

source

@[instance]

def polynomial.splitting_field_aux.algebra''' {α : Type u} [field α] {n : ℕ} {f : polynomial α} (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 _

source

@[instance]

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

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

source

@[instance]

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

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

source

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

algebra_map α (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)

source

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

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

source

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

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

source

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

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

source

def polynomial.splitting_field {α : Type u} [field α] (f : polynomial α) :

Type u

A splitting field of a polynomial.

Equations

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

source

@[instance]

def polynomial.splitting_field.field {α : Type u} [field α] (f : polynomial α) :

field f.splitting_field

Equations

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

source

@[instance]

def polynomial.splitting_field.inhabited {α : Type u} [field α] (f : polynomial α) :

inhabited f.splitting_field

Equations

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

source

@[instance]

def polynomial.splitting_field.algebra {α : Type u} [field α] (f : polynomial α) :

algebra α f.splitting_field

Equations

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

source

theorem polynomial.splitting_field.splits {α : Type u} [field α] (f : polynomial α) :

polynomial.splits (algebra_map α f.splitting_field) f

source

def polynomial.splitting_field.lift {α : Type u} {β : Type v} [field α] [field β] (f : polynomial α) [algebra α β] (hb : polynomial.splits (algebra_map α β) f) :

f.splitting_field →ₐ[α] β

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' := _}

source

theorem polynomial.splitting_field.adjoin_roots {α : Type u} [field α] (f : polynomial α) :

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

source

@[class]

structure polynomial.is_splitting_field (α : Type u) (β : Type v) [field α] [field β] [algebra α β] (f : polynomial α) :

Prop

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

Typeclass characterising splitting fields.

Instances

source

@[instance]

def polynomial.is_splitting_field.splitting_field {α : Type u} [field α] (f : polynomial α) :

polynomial.is_splitting_field α f.splitting_field f

source

@[instance]

def polynomial.is_splitting_field.map {α : Type u} {β : Type v} {γ : Type w} [field α] [field β] [field γ] [algebra α β] [algebra β γ] [algebra α γ] [is_scalar_tower α β γ] (f : polynomial α) [polynomial.is_splitting_field α γ f] :

polynomial.is_splitting_field β γ (polynomial.map (algebra_map α β) f)

source

theorem polynomial.is_splitting_field.splits_iff {α : Type u} (β : Type v) [field α] [field β] [algebra α β] (f : polynomial α) [polynomial.is_splitting_field α β f] :

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

source

theorem polynomial.is_splitting_field.mul {α : Type u} (β : Type v) {γ : Type w} [field α] [field β] [field γ] [algebra α β] [algebra β γ] [algebra α γ] [is_scalar_tower α β γ] (f g : polynomial α) (hf : f ≠ 0) (hg : g ≠ 0) [polynomial.is_splitting_field α β f] [polynomial.is_splitting_field β γ (polynomial.map (algebra_map α β) g)] :

polynomial.is_splitting_field α γ (f * g)

source

def polynomial.is_splitting_field.lift {α : Type u} (β : Type v) {γ : Type w} [field α] [field β] [field γ] [algebra α β] [algebra α γ] (f : polynomial α) [polynomial.is_splitting_field α β f] (hf : polynomial.splits (algebra_map α γ) f) :

β →ₐ[α] γ

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

Equations

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

source

theorem polynomial.is_splitting_field.finite_dimensional {α : Type u} (β : Type v) [field α] [field β] [algebra α β] (f : polynomial α) [polynomial.is_splitting_field α β f] :

finite_dimensional α β

source

def polynomial.is_splitting_field.alg_equiv {α : Type u} (β : Type v) [field α] [field β] [algebra α β] (f : polynomial α) [polynomial.is_splitting_field α β f] :

β ≃ₐ[α] f.splitting_field

Any splitting field is isomorphic to splitting_field f.

Equations

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