def
polynomial.splits
{α : Type u}
{β : Type v}
[field α]
[field β] :
(α →+* β) → 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)
@[simp]
@[simp]
theorem
polynomial.splits_of_degree_eq_one
{α : Type u}
{β : Type v}
[field α]
[field β]
(i : α →+* β)
{f : polynomial α} :
f.degree = 1 → polynomial.splits i f
theorem
polynomial.splits_of_degree_le_one
{α : Type u}
{β : Type v}
[field α]
[field β]
(i : α →+* β)
{f : polynomial α} :
f.degree ≤ 1 → polynomial.splits i f
theorem
polynomial.splits_mul
{α : Type u}
{β : Type v}
[field α]
[field β]
(i : α →+* β)
{f g : polynomial α} :
polynomial.splits i f → polynomial.splits i g → polynomial.splits i (f * g)
theorem
polynomial.splits_of_splits_mul
{α : Type u}
{β : Type v}
[field α]
[field β]
(i : α →+* β)
{f g : polynomial α} :
f * g ≠ 0 → polynomial.splits i (f * g) → polynomial.splits i f ∧ polynomial.splits i g
theorem
polynomial.splits_of_splits_of_dvd
{α : Type u}
{β : Type v}
[field α]
[field β]
(i : α →+* β)
{f g : polynomial α} :
f ≠ 0 → polynomial.splits i f → g ∣ f → polynomial.splits i g
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
theorem
polynomial.splits_of_is_unit
{α : Type u}
{β : Type v}
[field α]
[field β]
(i : α →+* β)
{u : polynomial α} :
is_unit u → polynomial.splits i u
theorem
polynomial.splits_X_sub_C
{α : Type u}
{β : Type v}
[field α]
[field β]
(i : α →+* β)
{x : α} :
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
theorem
polynomial.splits_mul_iff
{α : Type u}
{β : Type v}
[field α]
[field β]
(i : α →+* β)
{f g : polynomial α} :
f ≠ 0 → g ≠ 0 → (polynomial.splits i (f * g) ↔ polynomial.splits i f ∧ polynomial.splits i g)
theorem
polynomial.splits_prod
{α : Type u}
{β : Type v}
[field α]
[field β]
(i : α →+* β)
{ι : Type w}
{s : ι → polynomial α}
{t : finset ι} :
(∀ (j : ι), j ∈ t → polynomial.splits i (s j)) → polynomial.splits i (t.prod (λ (x : ι), s x))
theorem
polynomial.splits_prod_iff
{α : Type u}
{β : Type v}
[field α]
[field β]
(i : α →+* β)
{ι : Type w}
{s : ι → polynomial α}
{t : finset ι} :
(∀ (j : ι), j ∈ t → s j ≠ 0) → (polynomial.splits i (t.prod (λ (x : ι), s x)) ↔ ∀ (j : ι), j ∈ t → polynomial.splits i (s j))
theorem
polynomial.exists_root_of_splits
{α : Type u}
{β : Type v}
[field α]
[field β]
(i : α →+* β)
{f : polynomial α} :
polynomial.splits i f → f.degree ≠ 0 → (∃ (x : β), polynomial.eval₂ i x f = 0)
theorem
polynomial.exists_multiset_of_splits
{α : 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)
def
polynomial.root_of_splits
{α : Type u}
{β : Type v}
[field α]
[field β]
(i : α →+* β)
{f : polynomial α} :
polynomial.splits i f → f.degree ≠ 0 → β
Pick a root of a polynomial that splits.
Equations
- polynomial.root_of_splits i hf hfd = classical.some _
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
theorem
polynomial.roots_map
{α : Type u}
{β : Type v}
[field α]
[field β]
(i : α →+* β)
{f : polynomial α} :
polynomial.splits (ring_hom.id α) f → (polynomial.map i f).roots = finset.image ⇑i f.roots
theorem
polynomial.splits_of_exists_multiset
{α : Type u}
{β : Type v}
[field α]
[field β]
(i : α →+* β)
{f : polynomial α}
{s : multiset β} :
polynomial.map i f = ⇑polynomial.C (⇑i f.leading_coeff) * (multiset.map (λ (a : β), polynomial.X - ⇑polynomial.C a) s).prod → polynomial.splits i f
theorem
polynomial.splits_of_splits_id
{α : Type u}
{β : Type v}
[field α]
[field β]
(i : α →+* β)
{f : polynomial α} :
polynomial.splits (ring_hom.id α) f → polynomial.splits i f
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
theorem
polynomial.splits_comp_of_splits
{α : Type u}
{β : Type v}
{γ : Type w}
[field α]
[field β]
[field γ]
(i : α →+* β)
(j : β →+* γ)
{f : polynomial α} :
polynomial.splits i f → polynomial.splits (j.comp i) f
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
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 → (∃ (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.
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)
@[instance]
Equations
- _ = _
theorem
polynomial.factor_dvd_of_nat_degree_ne_zero
{α : Type u}
[field α]
{f : polynomial α} :
f.nat_degree ≠ 0 → f.factor ∣ f
Divide a polynomial f by X - C r where r is a root of f in a bigger field extension.
Equations
theorem
polynomial.X_sub_C_mul_remove_factor
{α : Type u}
[field α]
(f : polynomial α) :
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
{α : Type u}
[field α]
(f : polynomial α) :
f.remove_factor.nat_degree = f.nat_degree - 1
theorem
polynomial.nat_degree_remove_factor'
{α : Type u}
[field α]
{f : polynomial α}
{n : ℕ} :
f.nat_degree = n + 1 → f.remove_factor.nat_degree = n
def
polynomial.splitting_field_aux
(n : ℕ)
{α : Type u}
[field α]
(f : polynomial α) :
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 _)
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 _
@[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 _)
@[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}
@[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 _))
@[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
@[instance]
def
polynomial.splitting_field_aux.algebra''
{α : Type u}
[field α]
{n : ℕ}
{f : polynomial α}
(hfn : f.nat_degree = n + 1) :
Equations
@[instance]
def
polynomial.splitting_field_aux.algebra'''
{α : Type u}
[field α]
{n : ℕ}
{f : polynomial α}
(hfn : f.nat_degree = n + 1) :
Equations
@[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)
Equations
- _ = _
@[instance]
def
polynomial.splitting_field_aux.scalar_tower'
{α : Type u}
[field α]
{n : ℕ}
{f : polynomial α}
(hfn : f.nat_degree = n + 1) :
Equations
- _ = _
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)
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
theorem
polynomial.splitting_field_aux.exists_lift
(n : ℕ)
{α : Type u}
[field α]
(f : polynomial α)
(hfn : f.nat_degree = n)
{β : Type u_1}
[field β]
(j : α →+* β) :
polynomial.splits j f → (∃ (k : polynomial.splitting_field_aux n f hfn →+* β), k.comp (algebra_map α (polynomial.splitting_field_aux n f hfn)) = j)
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) = ⊤
A splitting field of a polynomial.
Equations
@[instance]
@[instance]
Equations
@[instance]
def
polynomial.splitting_field.lift
{α : Type u}
{β : Type v}
[field α]
[field β]
(f : polynomial α)
[algebra α β] :
polynomial.splits (algebra_map α β) f → (f.splitting_field →ₐ[α] β)
Embeds the splitting field into any other field that splits the polynomial.
theorem
polynomial.splitting_field.adjoin_roots
{α : Type u}
[field α]
(f : polynomial α) :
algebra.adjoin α ↑((polynomial.map (algebra_map α f.splitting_field) f).roots) = ⊤
@[class]
structure
polynomial.is_splitting_field
(α : Type u)
(β : Type v)
[field α]
[field β]
[algebra α β] :
polynomial α → Prop
- splits : polynomial.splits (algebra_map α β) f
- adjoin_roots : algebra.adjoin α ↑((polynomial.map (algebra_map α β) f).roots) = ⊤
Typeclass characterising splitting fields.
@[instance]
Equations
- _ = _
@[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)
Equations
- _ = _
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 ↔ ⊤ = ⊥
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)
def
polynomial.is_splitting_field.lift
{α : Type u}
(β : Type v)
{γ : Type w}
[field α]
[field β]
[field γ]
[algebra α β]
[algebra α γ]
(f : polynomial α)
[polynomial.is_splitting_field α β f] :
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)
theorem
polynomial.is_splitting_field.finite_dimensional
{α : Type u}
(β : Type v)
[field α]
[field β]
[algebra α β]
(f : polynomial α)
[polynomial.is_splitting_field α β f] :
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.