Mathlib.FieldTheory.SplittingField.IsSplittingField

Polynomial.IsSplittingField structure

(f : K[X])

Full source

/-- Typeclass characterising splitting fields. -/
@[stacks 09HV "Predicate version"]
class IsSplittingField (f : K[X]) : Prop where
  splits' : Splits (algebraMap K L) f
  adjoin_rootSet' : Algebra.adjoin K (f.rootSet L : Set L) = ⊤

Splitting Field of a Polynomial

Informal description

A structure characterizing a field extension $ L $ of $ K $ as a splitting field for a polynomial $ f \in K[X] $. This means that $ L $ is the smallest field extension of $ K $ where $ f $ splits completely into linear factors (i.e., all irreducible factors of $ f $ over $ L $ have degree 1).

Polynomial.IsSplittingField.splits theorem

(f : K[X]) [IsSplittingField K L f] : Splits (algebraMap K L) f

Full source

theorem splits (f : K[X]) [IsSplittingField K L f] : Splits (algebraMap K L) f :=
  splits'

Polynomial Splits in its Splitting Field

Informal description

Let $K$ be a field and $f \in K[X]$ a polynomial. If $L$ is a splitting field of $f$ over $K$, then $f$ splits completely in $L$ (i.e., the polynomial $f$ factors into linear factors over $L$ when viewed via the canonical embedding $K \hookrightarrow L$).

Polynomial.IsSplittingField.adjoin_rootSet theorem

(f : K[X]) [IsSplittingField K L f] : Algebra.adjoin K (f.rootSet L : Set L) = ⊤

Full source

theorem adjoin_rootSet (f : K[X]) [IsSplittingField K L f] :
    Algebra.adjoin K (f.rootSet L : Set L) = ⊤ :=
  adjoin_rootSet'

Splitting Field Generated by Roots of Polynomial

Informal description

Let $K$ be a field and $f \in K[X]$ a polynomial. If $L$ is a splitting field of $f$ over $K$, then the smallest subalgebra of $L$ containing $K$ and all roots of $f$ in $L$ is equal to the entire field $L$. In other words, $L$ is generated over $K$ by the roots of $f$.

Polynomial.IsSplittingField.map instance

(f : F[X]) [IsSplittingField F L f] : IsSplittingField K L (f.map <| algebraMap F K)

Full source

instance map (f : F[X]) [IsSplittingField F L f] : IsSplittingField K L (f.map <| algebraMap F K) :=
  ⟨by rw [splits_map_iff, ← IsScalarTower.algebraMap_eq]; exact splits L f,
    Subalgebra.restrictScalars_injective F <| by
      rw [rootSet, aroots, map_map, ← IsScalarTower.algebraMap_eq, Subalgebra.restrictScalars_top,
        eq_top_iff, ← adjoin_rootSet L f, Algebra.adjoin_le_iff]
      exact fun x hx => @Algebra.subset_adjoin K _ _ _ _ _ _ hx⟩

Splitting Field Preservation under Field Extension

Informal description

Let $F$ be a field and $f \in F[X]$ a polynomial. If $L$ is a splitting field of $f$ over $F$, then for any field extension $K$ of $F$, $L$ is also a splitting field of the polynomial $f$ mapped via the canonical embedding $F \hookrightarrow K$.

Polynomial.IsSplittingField.splits_iff theorem

(f : K[X]) [IsSplittingField K L f] : Splits (RingHom.id K) f ↔ (⊤ : Subalgebra K L) = ⊥

Full source

theorem splits_iff (f : K[X]) [IsSplittingField K L f] :
    SplitsSplits (RingHom.id K) f ↔ (⊤ : Subalgebra K L) = ⊥ :=
  ⟨fun h => by
    rw [eq_bot_iff, ← adjoin_rootSet L f, rootSet, aroots, roots_map (algebraMap K L) h,
      Algebra.adjoin_le_iff]
    intro y hy
    classical
    rw [Multiset.toFinset_map, Finset.mem_coe, Finset.mem_image] at hy
    obtain ⟨x : K, -, hxy : algebraMap K L x = y⟩ := hy
    rw [← hxy]
    exact SetLike.mem_coe.2 <| Subalgebra.algebraMap_mem _ _,
    fun h => @RingEquiv.toRingHom_refl K _ ▸ RingEquiv.self_trans_symm
      (RingEquiv.ofBijective _ <| Algebra.bijective_algebraMap_iff.2 h) ▸ by
        rw [RingEquiv.toRingHom_trans]
        exact splits_comp_of_splits _ _ (splits L f)⟩

Splitting Criterion for Polynomials over their Splitting Field: $f$ splits over $K$ iff $L$ has no proper intermediate subalgebras

Informal description

Let $K$ be a field and $f \in K[X]$ a polynomial. If $L$ is a splitting field of $f$ over $K$, then $f$ splits over $K$ (i.e., factors into linear factors in $K[X]$) if and only if the only subalgebra of $L$ containing $K$ is $L$ itself (i.e., $\top = \bot$ in the subalgebra lattice of $L$ over $K$).

Polynomial.IsSplittingField.mul theorem

 (f g : F[X]) (hf : f ≠ 0) (hg : g ≠ 0) [IsSplittingField F K f] [IsSplittingField K L (g.map <| algebraMap F K)] :
  IsSplittingField F L (f * g)

Full source

theorem mul (f g : F[X]) (hf : f ≠ 0) (hg : g ≠ 0) [IsSplittingField F K f]
    [IsSplittingField K L (g.map <| algebraMap F K)] : IsSplittingField F L (f * g) :=
  ⟨(IsScalarTower.algebraMap_eq F K L).symm ▸
      splits_mul _ (splits_comp_of_splits _ _ (splits K f))
        ((splits_map_iff _ _).1 (splits L <| g.map <| algebraMap F K)), by
    classical
    rw [rootSet, aroots_mul (mul_ne_zero hf hg),
      Multiset.toFinset_add, Finset.coe_union, Algebra.adjoin_union_eq_adjoin_adjoin,
      aroots_def, aroots_def, IsScalarTower.algebraMap_eq F K L, ← map_map,
      roots_map (algebraMap K L) ((splits_id_iff_splits <| algebraMap F K).2 <| splits K f),
      Multiset.toFinset_map, Finset.coe_image, Algebra.adjoin_algebraMap, ← rootSet, adjoin_rootSet,
      Algebra.map_top, IsScalarTower.adjoin_range_toAlgHom, ← map_map, ← rootSet, adjoin_rootSet,
      Subalgebra.restrictScalars_top]⟩

Splitting Field of Product of Polynomials

Informal description

Let $F$ be a field and $f, g \in F[X]$ be nonzero polynomials. If $K$ is a splitting field of $f$ over $F$ and $L$ is a splitting field of $g$ (viewed as a polynomial over $K$ via the canonical embedding $F \hookrightarrow K$) over $K$, then $L$ is a splitting field of the product polynomial $f \cdot g$ over $F$.

Polynomial.IsSplittingField.lift definition

[Algebra K F] (f : K[X]) [IsSplittingField K L f] (hf : Splits (algebraMap K F) f) : L →ₐ[K] F

Full source

/-- Splitting field of `f` embeds into any field that splits `f`. -/
def lift [Algebra K F] (f : K[X]) [IsSplittingField K L f]
    (hf : Splits (algebraMap K F) f) : L →ₐ[K] F :=
  if hf0 : f = 0 then
    (Algebra.ofId K F).comp <|
      (Algebra.botEquiv K L : (⊥ : Subalgebra K L) →ₐ[K] K).comp <| by
        rw [← (splits_iff L f).1 (show f.Splits (RingHom.id K) from hf0.symm ▸ splits_zero _)]
        exact Algebra.toTop
  else AlgHom.comp (by
    rw [← adjoin_rootSet L f]
    exact Classical.choice (lift_of_splits _ fun y hy =>
      have : aeval y f = 0 := (eval₂_eq_eval_map _).trans <|
        (mem_roots <| map_ne_zero hf0).1 (Multiset.mem_toFinset.mp hy)
    ⟨IsAlgebraic.isIntegral ⟨f, hf0, this⟩,
      splits_of_splits_of_dvd _ hf0 hf <| minpoly.dvd _ _ this⟩)) Algebra.toTop

Embedding of a Splitting Field into a Field Where the Polynomial Splits

Informal description

Given a polynomial $ f \in K[X] $ and a field extension $ L $ of $ K $ that is a splitting field for $ f $, there exists an algebra homomorphism $ L \to F $ over $ K $ whenever $ f $ splits in $ F $. This homomorphism embeds the splitting field $ L $ into any field $ F $ where $ f $ splits.

Polynomial.IsSplittingField.finiteDimensional theorem

(f : K[X]) [IsSplittingField K L f] : FiniteDimensional K L

Full source

theorem finiteDimensional (f : K[X]) [IsSplittingField K L f] : FiniteDimensional K L := by
  classical
  exact ⟨@Algebra.top_toSubmodule K L _ _ _ ▸
    adjoin_rootSet L f ▸ fg_adjoin_of_finite (Finset.finite_toSet _) fun y hy ↦
      if hf : f = 0 then by rw [hf, rootSet_zero] at hy; cases hy
      else IsAlgebraic.isIntegral ⟨f, hf, (mem_rootSet'.mp hy).2⟩⟩

Finite-Dimensionality of Splitting Fields

Informal description

For any polynomial $f \in K[X]$, if $L$ is a splitting field of $f$ over $K$, then $L$ is a finite-dimensional vector space over $K$.

Polynomial.IsSplittingField.of_algEquiv theorem

[Algebra K F] (p : K[X]) (f : F ≃ₐ[K] L) [IsSplittingField K F p] : IsSplittingField K L p

Full source

theorem of_algEquiv [Algebra K F] (p : K[X]) (f : F ≃ₐ[K] L) [IsSplittingField K F p] :
    IsSplittingField K L p := by
  constructor
  · rw [← f.toAlgHom.comp_algebraMap]
    exact splits_comp_of_splits _ _ (splits F p)
  · rw [← (AlgHom.range_eq_top f.toAlgHom).mpr f.surjective,
      adjoin_rootSet_eq_range (splits F p), adjoin_rootSet F p]

Splitting Field Property Preserved Under Algebra Isomorphism

Informal description

Let $K$ be a field and $p \in K[X]$ a polynomial. Given an algebra isomorphism $f: F \to L$ over $K$, if $F$ is a splitting field of $p$ over $K$, then $L$ is also a splitting field of $p$ over $K$.

Polynomial.IsSplittingField.adjoin_rootSet_eq_range theorem

[Algebra K F] (f : K[X]) [IsSplittingField K L f] (i : L →ₐ[K] F) : Algebra.adjoin K (rootSet f F) = i.range

Full source

theorem adjoin_rootSet_eq_range [Algebra K F] (f : K[X]) [IsSplittingField K L f] (i : L →ₐ[K] F) :
    Algebra.adjoin K (rootSet f F) = i.range :=
  (Polynomial.adjoin_rootSet_eq_range (splits L f) i).mpr (adjoin_rootSet L f)

Splitting Field Adjoin Roots Equals Homomorphism Range

Informal description

Let $K$ be a field and $f \in K[X]$ a polynomial. Suppose $L$ is a splitting field of $f$ over $K$, and let $F$ be another field extension of $K$ with an algebra homomorphism $i: L \to F$ over $K$. Then the smallest subalgebra of $F$ containing $K$ and all roots of $f$ in $F$ is equal to the image of $i$.

IntermediateField.splits_of_splits theorem

(h : p.Splits (algebraMap K L)) (hF : ∀ x ∈ p.rootSet L, x ∈ F) : p.Splits (algebraMap K F)

Full source

theorem IntermediateField.splits_of_splits (h : p.Splits (algebraMap K L))
    (hF : ∀ x ∈ p.rootSet L, x ∈ F) : p.Splits (algebraMap K F) := by
  classical
  simp_rw [← F.fieldRange_val, rootSet_def, Finset.mem_coe, Multiset.mem_toFinset] at hF
  exact splits_of_comp _ F.val.toRingHom h hF

Splitting of Polynomial in Intermediate Field Containing All Roots

Informal description

Let $K$ be a field and $L$ a field extension of $K$. For a polynomial $p \in K[X]$, if $p$ splits in $L$ (i.e., all roots of $p$ are in $L$), and if every root of $p$ in $L$ belongs to an intermediate field $F$ between $K$ and $L$, then $p$ also splits in $F$.

IntermediateField.splits_iff_mem theorem

(h : p.Splits (algebraMap K L)) : p.Splits (algebraMap K F) ↔ ∀ x ∈ p.rootSet L, x ∈ F

Full source

theorem IntermediateField.splits_iff_mem (h : p.Splits (algebraMap K L)) :
    p.Splits (algebraMap K F) ↔ ∀ x ∈ p.rootSet L, x ∈ F := by
  refine ⟨?_, IntermediateField.splits_of_splits h⟩
  intro hF
  rw [← Polynomial.image_rootSet hF F.val, Set.forall_mem_image]
  exact fun x _ ↦ x.2

Splitting Criterion for Polynomials in Intermediate Fields: $p$ splits in $F$ iff all roots in $L$ belong to $F$

Informal description

Let $K$ be a field and $L$ a field extension of $K$. For a polynomial $p \in K[X]$ that splits in $L$, and an intermediate field $F$ between $K$ and $L$, the following are equivalent: 1. $p$ splits in $F$. 2. Every root of $p$ in $L$ belongs to $F$. In symbols: \[ p \text{ splits in } F \leftrightarrow (\forall x \in p.\text{rootSet}(L),\, x \in F). \]

IsIntegral.mem_intermediateField_of_minpoly_splits theorem

{x : L} (int : IsIntegral K x) {F : IntermediateField K L} (h : Splits (algebraMap K F) (minpoly K x)) : x ∈ F

Full source

theorem IsIntegral.mem_intermediateField_of_minpoly_splits {x : L} (int : IsIntegral K x)
    {F : IntermediateField K L} (h : Splits (algebraMap K F) (minpoly K x)) : x ∈ F := by
  rw [← F.fieldRange_val]; exact int.mem_range_algebraMap_of_minpoly_splits h

Integral Elements with Split Minimal Polynomial Lie in Intermediate Fields

Informal description

Let $ K \subseteq L $ be a field extension and $ x \in L $ be an element integral over $ K $. If the minimal polynomial of $ x $ over $ K $ splits in an intermediate field $ F $ between $ K $ and $ L $, then $ x $ belongs to $ F $.

isSplittingField_iff_intermediateField theorem

: p.IsSplittingField K L ↔ p.Splits (algebraMap K L) ∧ IntermediateField.adjoin K (p.rootSet L) = ⊤

Full source

/-- Characterize `IsSplittingField` with `IntermediateField.adjoin` instead of `Algebra.adjoin`. -/
theorem isSplittingField_iff_intermediateField : p.IsSplittingField K L ↔
    p.Splits (algebraMap K L) ∧ IntermediateField.adjoin K (p.rootSet L) = ⊤ := by
  rw [← IntermediateField.toSubalgebra_injective.eq_iff,
      IntermediateField.adjoin_algebraic_toSubalgebra fun _ ↦ isAlgebraic_of_mem_rootSet]
  exact ⟨fun ⟨spl, adj⟩ ↦ ⟨spl, adj⟩, fun ⟨spl, adj⟩ ↦ ⟨spl, adj⟩⟩

Characterization of Splitting Fields via Adjoining Roots

Informal description

A field extension $ L $ of $ K $ is a splitting field of a polynomial $ p \in K[X] $ if and only if the following two conditions hold: 1. The polynomial $ p $ splits completely in $ L $, i.e., $ p $ factors into linear factors over $ L $. 2. The intermediate field generated by $ K $ and the roots of $ p $ in $ L $ is equal to $ L $ itself, i.e., $ K(p.\text{rootSet}(L)) = L $. In symbols: \[ L \text{ is a splitting field of } p \text{ over } K \leftrightarrow \big( p \text{ splits in } L \big) \land \big( \text{adjoin}_K(p.\text{rootSet}(L)) = L \big). \]

IntermediateField.isSplittingField_iff theorem

: p.IsSplittingField K F ↔ p.Splits (algebraMap K F) ∧ F = adjoin K (p.rootSet L)

Full source

theorem IntermediateField.isSplittingField_iff :
    p.IsSplittingField K F ↔ p.Splits (algebraMap K F) ∧ F = adjoin K (p.rootSet L) := by
  suffices _ → (Algebra.adjoinAlgebra.adjoin K (p.rootSet F) = ⊤ ↔ F = adjoin K (p.rootSet L)) by
    exact ⟨fun h ↦ ⟨h.1, (this h.1).mp h.2⟩, fun h ↦ ⟨h.1, (this h.1).mpr h.2⟩⟩
  rw [← toSubalgebra_injective.eq_iff,
      adjoin_algebraic_toSubalgebra fun x ↦ isAlgebraic_of_mem_rootSet]
  refine fun hp ↦ (adjoin_rootSet_eq_range hp F.val).symm.trans ?_
  rw [← F.range_val, eq_comm]

Characterization of Splitting Fields via Splitting and Root Adjoin

Informal description

Let $K$ be a field and $p \in K[X]$ a polynomial. An intermediate field $F$ between $K$ and $L$ is a splitting field of $p$ over $K$ if and only if the polynomial $p$ splits in $F$ (i.e., all irreducible factors of $p$ over $F$ have degree 1) and $F$ is equal to the field extension $K(S)$ where $S$ is the set of roots of $p$ in $L$.

IntermediateField.adjoin_rootSet_isSplittingField theorem

(hp : p.Splits (algebraMap K L)) : p.IsSplittingField K (adjoin K (p.rootSet L))

Full source

theorem IntermediateField.adjoin_rootSet_isSplittingField (hp : p.Splits (algebraMap K L)) :
    p.IsSplittingField K (adjoin K (p.rootSet L)) :=
  isSplittingField_iff.mpr ⟨splits_of_splits hp fun _ hx ↦ subset_adjoin K (p.rootSet L) hx, rfl⟩

Adjoining Roots Yields Splitting Field

Informal description

Let $K$ be a field and $L$ a field extension of $K$. For a polynomial $p \in K[X]$, if $p$ splits in $L$ (i.e., all roots of $p$ are in $L$), then the intermediate field $K(S)$ obtained by adjoining the set $S$ of roots of $p$ in $L$ to $K$ is a splitting field of $p$ over $K$.

Mathlib.FieldTheory.SplittingField.IsSplittingField

Main definitions

Main statements