mathlib3 documentation

field_theory.splitting_field.construction

Splitting fields #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we prove the existence and uniqueness of splitting fields.

Main definitions #

polynomial.splitting_field f: A fixed splitting field of the polynomial f.

Main statements #

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.

Implementation details #

We construct a splitting_field_aux without worrying about whether the instances satisfy nice definitional equalities. Then the actual splitting_field is defined to be a quotient of a mv_polynomial ring by the kernel of the obvious map into splitting_field_aux. Because the actual splitting_field will be a quotient of a mv_polynomial, it has nice instances on it.

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

Non-computably choose an irreducible factor from a polynomial.

Equations

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

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

irreducible f.factor

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

fact (irreducible f.factor)

See note [fact non-instances].

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

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

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

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

f.remove_factor.nat_degree = f.nat_degree - 1

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

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

Σ (L : Type u) (inst : field L), algebra K L

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

It constructs the type, proves that is a field and algebra over the base field.

Uses recursion on the degree.

Equations

polynomial.splitting_field_aux_aux n = n.rec_on (λ (K : Type u) (inst : field K) (f : polynomial K), ⟨K, ⟨inst, infer_instance (algebra.id K)⟩⟩) (λ (m : ℕ) (ih : Π {K : Type u} [_inst_4 : field K], polynomial K → (Σ (L : Type u) (inst : field L), algebra K L)) (K : Type u) (inst : field K) (f : polynomial K), let L : Σ (L : Type u) (inst_1 : field L), algebra (adjoin_root f.factor) L := ih f.remove_factor, h₁ : field L.fst := L.snd.fst, h₂ : algebra (adjoin_root f.factor) L.fst := L.snd.snd in ⟨L.fst, ⟨L.snd.fst, ((algebra_map (adjoin_root f.factor) L.fst).comp (adjoin_root.of f.factor)).to_algebra⟩⟩)

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

Auxiliary construction to a splitting field of a polynomial, which removes n (arbitrarily-chosen) factors. It is the type constructed in splitting_field_aux_aux.

Equations

polynomial.splitting_field_aux n f = (polynomial.splitting_field_aux_aux n f).fst

Instances for polynomial.splitting_field_aux

@[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

polynomial.splitting_field_aux.field n f = (polynomial.splitting_field_aux_aux n f).snd.fst

@[protected, instance]

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

inhabited (polynomial.splitting_field_aux n f)

Equations

polynomial.splitting_field_aux.inhabited n f = {default := 0}

@[protected, instance]

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

algebra K (polynomial.splitting_field_aux n f)

Equations

polynomial.splitting_field_aux.algebra n f = (polynomial.splitting_field_aux_aux n f).snd.snd

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

@[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

polynomial.splitting_field_aux.algebra''' = polynomial.splitting_field_aux.algebra n f.remove_factor

@[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

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

@[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

polynomial.splitting_field_aux.algebra'' = ((algebra_map (adjoin_root f.factor) (polynomial.splitting_field_aux n f.remove_factor)).comp (adjoin_root.of f.factor)).to_algebra

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

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)

@[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

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

algebra.adjoin K (f.root_set (polynomial.splitting_field_aux n f)) = ⊤

@[protected, instance]

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

polynomial.is_splitting_field K (polynomial.splitting_field_aux f.nat_degree f) f

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

mv_polynomial ↥(f.root_set (polynomial.splitting_field_aux f.nat_degree f)) K →ₐ[K] polynomial.splitting_field_aux f.nat_degree f

The natural map from mv_polynomial (f.root_set (splitting_field_aux f.nat_degree f)) to splitting_field_aux f.nat_degree f sendind a variable to the corresponding root.

Equations

polynomial.splitting_field_aux.of_mv_polynomial f = mv_polynomial.aeval (λ (i : ↥(f.root_set (polynomial.splitting_field_aux f.nat_degree f))), i.val)

theorem polynomial.splitting_field_aux.of_mv_polynomial_surjective {K : Type v} [field K] (f : polynomial K) :

function.surjective ⇑(polynomial.splitting_field_aux.of_mv_polynomial f)

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

(mv_polynomial ↥(f.root_set (polynomial.splitting_field_aux f.nat_degree f)) K ⧸ ring_hom.ker (polynomial.splitting_field_aux.of_mv_polynomial f).to_ring_hom) ≃ₐ[K] polynomial.splitting_field_aux f.nat_degree f

The algebra isomorphism between the quotient of mv_polynomial (f.root_set (splitting_field_aux f.nat_degree f)) K by the kernel of of_mv_polynomial f and splitting_field_aux f.nat_degree f. It is used to transport all the algebraic structures from the latter to f.splitting_field, that is defined as the former.

Equations

polynomial.splitting_field_aux.alg_equiv_quotient_mv_polynomial f = ideal.quotient_ker_alg_equiv_of_surjective _

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

A splitting field of a polynomial.

Equations

f.splitting_field = (mv_polynomial ↥(f.root_set (polynomial.splitting_field_aux f.nat_degree f)) K ⧸ ring_hom.ker (polynomial.splitting_field_aux.of_mv_polynomial f).to_ring_hom)

Instances for polynomial.splitting_field

@[protected, instance]

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

comm_ring f.splitting_field

Equations

polynomial.splitting_field.comm_ring f = ideal.quotient.comm_ring (ring_hom.ker (polynomial.splitting_field_aux.of_mv_polynomial f).to_ring_hom)

@[protected, instance]

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

inhabited f.splitting_field

Equations

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

@[protected, instance]

noncomputable def polynomial.splitting_field.has_smul {K : Type v} [field K] (f : polynomial K) {S : Type u_1} [distrib_smul S K] [is_scalar_tower S K K] :

has_smul S f.splitting_field

Equations

polynomial.splitting_field.has_smul f = submodule.quotient.has_smul' (ring_hom.ker (polynomial.splitting_field_aux.of_mv_polynomial f).to_ring_hom)

@[protected, instance]

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

algebra K f.splitting_field

Equations

polynomial.splitting_field.algebra f = ideal.quotient.algebra K

@[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

polynomial.splitting_field.algebra' f = ideal.quotient.algebra R

@[protected, instance]

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

is_scalar_tower R K f.splitting_field

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

f.splitting_field ≃ₐ[K] polynomial.splitting_field_aux f.nat_degree f

The algebra equivalence with splitting_field_aux, which we will use to construct the field structure.

Equations

polynomial.splitting_field.alg_equiv_splitting_field_aux f = polynomial.splitting_field_aux.alg_equiv_quotient_mv_polynomial f

@[protected, instance]

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

field f.splitting_field

Equations

polynomial.splitting_field.field f = let e : f.splitting_field ≃ₐ[K] polynomial.splitting_field_aux f.nat_degree f := polynomial.splitting_field.alg_equiv_splitting_field_aux f in {add := comm_ring.add (polynomial.splitting_field.comm_ring f), add_assoc := _, zero := comm_ring.zero (polynomial.splitting_field.comm_ring f), zero_add := _, add_zero := _, nsmul := comm_ring.nsmul (polynomial.splitting_field.comm_ring f), nsmul_zero' := _, nsmul_succ' := _, neg := comm_ring.neg (polynomial.splitting_field.comm_ring f), sub := comm_ring.sub (polynomial.splitting_field.comm_ring f), sub_eq_add_neg := _, zsmul := comm_ring.zsmul (polynomial.splitting_field.comm_ring f), zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := comm_ring.int_cast (polynomial.splitting_field.comm_ring f), nat_cast := comm_ring.nat_cast (polynomial.splitting_field.comm_ring f), one := comm_ring.one (polynomial.splitting_field.comm_ring f), nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := comm_ring.mul (polynomial.splitting_field.comm_ring f), mul_assoc := _, one_mul := _, mul_one := _, npow := comm_ring.npow (polynomial.splitting_field.comm_ring f), npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := λ (a : f.splitting_field), ⇑(e.symm) (⇑e a)⁻¹, div := division_ring.div._default comm_ring.mul _ comm_ring.one _ _ comm_ring.npow _ _ (λ (a : f.splitting_field), ⇑(e.symm) (⇑e a)⁻¹), div_eq_mul_inv := _, zpow := division_ring.zpow._default comm_ring.mul _ comm_ring.one _ _ comm_ring.npow _ _ (λ (a : f.splitting_field), ⇑(e.symm) (⇑e a)⁻¹), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, rat_cast := λ (a : ℚ), ⇑(algebra_map K f.splitting_field) ↑a, mul_inv_cancel := _, inv_zero := _, rat_cast_mk := _, qsmul := has_smul.smul (polynomial.splitting_field.has_smul f), qsmul_eq_mul' := _}

@[protected, instance]

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

char_zero f.splitting_field

@[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

@[protected]

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

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

polynomial.splitting_field.lift f hb = polynomial.is_splitting_field.lift f.splitting_field f hb

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

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

@[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

@[protected, instance]

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

fintype f.splitting_field

Equations

polynomial.is_splitting_field.polynomial.splitting_field.fintype f = finite_dimensional.fintype_of_fintype K f.splitting_field

@[protected, instance]

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

no_zero_smul_divisors 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 : polynomial K) [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 _) _

@[protected, instance]

def polynomial.splitting_field.normal {F : Type u} [field F] (p : polynomial F) :

normal F p.splitting_field