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 : K[X] 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 : K[X] is called a splitting field if it is the smallest field extension of K such that f splits.

Main definitions #

Main statements #

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

Non-computably choose an irreducible factor from a polynomial.

Equations
source
theorem polynomial.irreducible_factor {K : Type v} [field K] (f : polynomial K) :
irreducible f.factor
source
theorem polynomial.fact_irreducible_factor {K : Type v} [field K] (f : polynomial K) :
fact (irreducible f.factor)

See note [fact non-instances].

source
theorem polynomial.factor_dvd_of_not_is_unit {K : Type v} [field K] {f : polynomial K} (hf1 : ¬is_unit f) :
f.factor ∣ f
source
theorem polynomial.factor_dvd_of_degree_ne_zero {K : Type v} [field K] {f : polynomial K} (hf : f.degree ≠ 0) :
f.factor ∣ f
source
theorem polynomial.factor_dvd_of_nat_degree_ne_zero {K : Type v} [field K] {f : polynomial K} (hf : f.nat_degree ≠ 0) :
f.factor ∣ f
source
noncomputable def polynomial.remove_factor {K : Type v} [field K] (f : polynomial K) :
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
source
theorem polynomial.X_sub_C_mul_remove_factor {K : Type v} [field K] (f : polynomial K) (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 {K : Type v} [field K] (f : polynomial K) :
f.remove_factor.nat_degree = f.nat_degree - 1
source
theorem polynomial.nat_degree_remove_factor' {K : Type v} [field K] {f : polynomial K} {n : ℕ} (hfn : f.nat_degree = n + 1) :
f.remove_factor.nat_degree = n
source
def polynomial.splitting_field_aux (n : ℕ) {K : Type u} [field K] (f : polynomial K) :
Type u

Auxiliary construction to a splitting field of a polynomial, which removes n (arbitrarily-chosen) factors.

Uses recursion on the degree. For better definitional behaviour, structures including splitting_field_aux (such as instances) should be defined using this recursion in each field, rather than defining the whole tuple through recursion.

Equations
Instances for polynomial.splitting_field_aux
source
theorem polynomial.splitting_field_aux.succ {K : Type v} [field K] (n : ℕ) (f : polynomial K) :
polynomial.splitting_field_aux (n + 1) f = polynomial.splitting_field_aux n f.remove_factor

Instances on splitting_field_aux #

In order to avoid diamond issues, we have to be careful to define each data field of algebraic instances on splitting_field_aux by recursion, rather than defining the whole structure by recursion at once.

The important detail is that the smul instances can be lifted before we create the algebraic instances; if we do not do this, this creates a mutual dependence on both on each other, and it is impossible to untangle this mess. In order to do this, we need that these smul instances are distributive in the sense of distrib_smul, which is weak enough to be guaranteed at this stage. This is sufficient to lift an action to adjoin_root f (remember that this is a quotient, so these conditions are equivalent to well-definedness), which is all we need.

source
@[protected]
noncomputable def polynomial.splitting_field_aux.zero (n : ℕ) {K : Type u} [field K] {f : polynomial K} :
polynomial.splitting_field_aux n f

Splitting fields have a zero.

Equations
source
@[protected]
noncomputable def polynomial.splitting_field_aux.add (n : ℕ) {K : Type u} [field K] {f : polynomial K} :
polynomial.splitting_field_aux n f → polynomial.splitting_field_aux n f → polynomial.splitting_field_aux n f

Splitting fields have an addition.

Equations
source
@[protected]
noncomputable def polynomial.splitting_field_aux.smul (n : ℕ) (α : Type u_1) {K : Type u} [field K] [distrib_smul α K] [is_scalar_tower α K K] {f : polynomial K} :
α → polynomial.splitting_field_aux n f → polynomial.splitting_field_aux n f

Splitting fields inherit scalar multiplication.

Equations
source
@[protected, instance]
noncomputable def polynomial.splitting_field_aux.has_smul (α : Type u_1) (n : ℕ) {K : Type u} [field K] [distrib_smul α K] [is_scalar_tower α K K] {f : polynomial K} :
has_smul α (polynomial.splitting_field_aux n f)
Equations
source
@[protected, instance]
def polynomial.splitting_field_aux.is_scalar_tower (n : ℕ) (R₁ : Type u_1) (R₂ : Type u_2) {K : Type u} [has_smul R₁ R₂] [field K] [distrib_smul R₂ K] [distrib_smul R₁ K] [is_scalar_tower R₁ K K] [is_scalar_tower R₂ K K] [is_scalar_tower R₁ R₂ K] {f : polynomial K} :
is_scalar_tower R₁ R₂ (polynomial.splitting_field_aux n f)
source
@[protected]
noncomputable def polynomial.splitting_field_aux.neg (n : ℕ) {K : Type u} [field K] {f : polynomial K} :
polynomial.splitting_field_aux n f → polynomial.splitting_field_aux n f

Splitting fields have a negation.

Equations
source
@[protected]
noncomputable def polynomial.splitting_field_aux.sub (n : ℕ) {K : Type u} [field K] {f : polynomial K} :
polynomial.splitting_field_aux n f → polynomial.splitting_field_aux n f → polynomial.splitting_field_aux n f

Splitting fields have subtraction.

Equations
source
@[protected]
noncomputable def polynomial.splitting_field_aux.one (n : ℕ) {K : Type u} [field K] {f : polynomial K} :
polynomial.splitting_field_aux n f

Splitting fields have a one.

Equations
source
@[protected]
noncomputable def polynomial.splitting_field_aux.mul (n : ℕ) {K : Type u} [field K] {f : polynomial K} :
polynomial.splitting_field_aux n f → polynomial.splitting_field_aux n f → polynomial.splitting_field_aux n f

Splitting fields have a multiplication.

Equations
source
@[protected]
noncomputable def polynomial.splitting_field_aux.npow (n : ℕ) {K : Type u} [field K] {f : polynomial K} :
ℕ → polynomial.splitting_field_aux n f → polynomial.splitting_field_aux n f

Splitting fields have a power operation.

Equations
source
@[protected]
noncomputable def polynomial.splitting_field_aux.mk (n : ℕ) {K : Type u} [field K] {f : polynomial K} :
K → polynomial.splitting_field_aux n f

Splitting fields have an injection from the base field.

Equations
source
@[protected]
noncomputable def polynomial.splitting_field_aux.inv (n : ℕ) {K : Type u} [field K] {f : polynomial K} :
polynomial.splitting_field_aux n f → polynomial.splitting_field_aux n f

Splitting fields have an inverse.

Equations
source
@[protected]
noncomputable def polynomial.splitting_field_aux.div (n : ℕ) {K : Type u} [field K] {f : polynomial K} :
polynomial.splitting_field_aux n f → polynomial.splitting_field_aux n f → polynomial.splitting_field_aux n f

Splitting fields have a division.

Equations
source
@[protected]
noncomputable def polynomial.splitting_field_aux.zpow (n : ℕ) {K : Type u} [field K] {f : polynomial K} :
ℤ → polynomial.splitting_field_aux n f → polynomial.splitting_field_aux n f

Splitting fields have powers by integers.

Equations
source
@[protected, instance]
noncomputable def polynomial.splitting_field_aux.field (n : ℕ) {K : Type u} [field K] {f : polynomial K} :
field (polynomial.splitting_field_aux n f)
Equations
source
@[protected, instance]
noncomputable def polynomial.splitting_field_aux.inhabited {K : Type v} [field K] {n : ℕ} {f : polynomial K} :
inhabited (polynomial.splitting_field_aux n f)
Equations
source
@[protected]
noncomputable def polynomial.splitting_field_aux.mk_hom (n : ℕ) {K : Type u} [field K] {f : polynomial K} :
K →+* polynomial.splitting_field_aux n f

The injection from the base field as a ring homomorphism.

Equations
source
@[simp]
theorem polynomial.splitting_field_aux.mk_hom_apply (n : ℕ) {K : Type u} [field K] {f : polynomial K} (ᾰ : K) :
⇑(polynomial.splitting_field_aux.mk_hom n) ᾰ = polynomial.splitting_field_aux.mk n ᾰ
source
@[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 : polynomial K} :
algebra R (polynomial.splitting_field_aux n f)
Equations
source
@[protected, instance]
noncomputable def polynomial.splitting_field_aux.algebra''' {K : Type v} [field K] {n : ℕ} {f : polynomial K} :
algebra (adjoin_root f.factor) (polynomial.splitting_field_aux n f.remove_factor)
Equations
source
@[protected, instance]
noncomputable def polynomial.splitting_field_aux.algebra' {K : Type v} [field K] {n : ℕ} {f : polynomial K} :
algebra (adjoin_root f.factor) (polynomial.splitting_field_aux n.succ f)
Equations
source
@[protected, instance]
noncomputable def polynomial.splitting_field_aux.algebra'' {K : Type v} [field K] {n : ℕ} {f : polynomial K} :
algebra K (polynomial.splitting_field_aux n f.remove_factor)
Equations
source
@[protected, instance]
def polynomial.splitting_field_aux.scalar_tower' {K : Type v} [field K] {n : ℕ} {f : polynomial K} :
is_scalar_tower K (adjoin_root f.factor) (polynomial.splitting_field_aux n f.remove_factor)
source
@[protected, instance]
def polynomial.splitting_field_aux.scalar_tower {K : Type v} [field K] {n : ℕ} {f : polynomial K} :
is_scalar_tower K (adjoin_root f.factor) (polynomial.splitting_field_aux (n + 1) f)
source
theorem polynomial.splitting_field_aux.algebra_map_succ {K : Type v} [field K] (n : ℕ) (f : polynomial K) :
algebra_map K (polynomial.splitting_field_aux (n + 1) f) = (algebra_map (adjoin_root f.factor) (polynomial.splitting_field_aux n f.remove_factor)).comp (adjoin_root.of f.factor)
source
@[protected]
theorem polynomial.splitting_field_aux.splits (n : ℕ) {K : Type u} [field K] (f : polynomial K) (hfn : f.nat_degree = n) :
polynomial.splits (algebra_map K (polynomial.splitting_field_aux n f)) f
source
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) :
∃ (k : polynomial.splitting_field_aux n f →+* L), k.comp (algebra_map K (polynomial.splitting_field_aux n f)) = j
source
theorem polynomial.splitting_field_aux.adjoin_roots (n : ℕ) {K : Type u} [field K] (f : polynomial K) (hfn : f.nat_degree = n) :
algebra.adjoin K ↑((polynomial.map (algebra_map K (polynomial.splitting_field_aux n f)) f).roots.to_finset) = ⊤
source
def polynomial.splitting_field {K : Type v} [field K] (f : polynomial K) :
Type v

A splitting field of a polynomial.

Equations
Instances for polynomial.splitting_field
source
@[protected, instance]
noncomputable def polynomial.splitting_field.field {K : Type v} [field K] (f : polynomial K) :
field f.splitting_field
Equations
source
@[protected, instance]
noncomputable def polynomial.splitting_field.inhabited {K : Type v} [field K] (f : polynomial K) :
inhabited f.splitting_field
Equations
source
@[protected, instance]
noncomputable def polynomial.splitting_field.algebra' {K : Type v} [field K] (f : polynomial K) {R : Type u_1} [comm_semiring R] [algebra R K] :
algebra R f.splitting_field
Equations
source
@[protected, instance]
noncomputable def polynomial.splitting_field.algebra {K : Type v} [field K] (f : polynomial K) :
algebra K f.splitting_field
Equations
source
@[protected, instance]
def polynomial.splitting_field.char_zero {K : Type v} [field K] (f : polynomial K) [char_zero K] :
char_zero f.splitting_field
source
@[protected]
theorem polynomial.splitting_field.splits {K : Type v} [field K] (f : polynomial K) :
polynomial.splits (algebra_map K f.splitting_field) f
source
noncomputable 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) :
f.splitting_field →ₐ[K] L

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

Equations
source
theorem polynomial.splitting_field.adjoin_roots {K : Type v} [field K] (f : polynomial K) :
algebra.adjoin K ↑((polynomial.map (algebra_map K f.splitting_field) f).roots.to_finset) = ⊤
source
theorem polynomial.splitting_field.adjoin_root_set {K : Type v} [field K] (f : polynomial K) :
algebra.adjoin K (f.root_set f.splitting_field) = ⊤
source
@[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 of this typeclass
source
@[protected, instance]
def polynomial.is_splitting_field.splitting_field {K : Type v} [field K] (f : polynomial K) :
polynomial.is_splitting_field K f.splitting_field f
source
@[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 : polynomial F) [polynomial.is_splitting_field F L f] :
polynomial.is_splitting_field K L (polynomial.map (algebra_map F K) f)
source
theorem polynomial.is_splitting_field.splits_iff {K : Type v} (L : Type w) [field K] [field L] [algebra K L] (f : polynomial K) [polynomial.is_splitting_field K L f] :
polynomial.splits (ring_hom.id K) f ↔ ⊤ = ⊥
source
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)] :
polynomial.is_splitting_field F L (f * g)
source
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 : polynomial K) [polynomial.is_splitting_field K L f] (hf : polynomial.splits (algebra_map K F) f) :
L →ₐ[K] F

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

Equations
source
theorem polynomial.is_splitting_field.finite_dimensional {K : Type v} (L : Type w) [field K] [field L] [algebra K L] (f : polynomial K) [polynomial.is_splitting_field K L f] :
finite_dimensional K L
source
@[protected, instance]
def polynomial.is_splitting_field.polynomial.splitting_field.finite_dimensional {K : Type v} [field K] (f : polynomial K) :
finite_dimensional K f.splitting_field
source
noncomputable def polynomial.is_splitting_field.alg_equiv {K : Type v} (L : Type w) [field K] [field L] [algebra K L] (f : polynomial K) [polynomial.is_splitting_field K L f] :
L ≃ₐ[K] f.splitting_field

Any splitting field is isomorphic to splitting_field f.

Equations
source
theorem polynomial.is_splitting_field.of_alg_equiv {F : Type u} {K : Type v} (L : Type w) [field K] [field L] [field F] [algebra K L] [algebra K F] (p : polynomial K) (f : F ≃ₐ[K] L) [polynomial.is_splitting_field K F p] :
polynomial.is_splitting_field K L p
source
theorem intermediate_field.splits_of_splits {K : Type v} {L : Type w} [field K] [field L] [algebra K L] {p : polynomial K} {F : intermediate_field K L} (h : polynomial.splits (algebra_map K L) p) (hF : ∀ (x : L), x ∈ p.root_set L → x ∈ F) :
polynomial.splits (algebra_map K ↥F) p