Mathlib.FieldTheory.IsSepClosed

Module docstring

{"# Separably Closed Field

In this file we define the typeclass for separably closed fields and separable closures, and prove some of their properties.

Main Definitions

IsSepClosed k is the typeclass saying k is a separably closed field, i.e. every separable polynomial in k splits.
IsSepClosure k K is the typeclass saying K is a separable closure of k, where k is a field. This means that K is separably closed and separable over k.
IsSepClosed.lift is a map from a separable extension L of K, into any separably closed extension M of K.
IsSepClosure.equiv is a proof that any two separable closures of the same field are isomorphic.
IsSepClosure.isAlgClosure_of_perfectField, IsSepClosure.of_isAlgClosure_of_perfectField: if k is a perfect field, then its separable closure coincides with its algebraic closure.

Tags

separable closure, separably closed

separableClosure: maximal separable subextension of K/k, consisting of all elements of K which are separable over k.
separableClosure.isSepClosure: if K is a separably closed field containing k, then the maximal separable subextension of K/k is a separable closure of k.
In particular, a separable closure (SeparableClosure) exists.
Algebra.IsAlgebraic.isPurelyInseparable_of_isSepClosed: an algebraic extension of a separably closed field is purely inseparable.

IsSepClosed structure

Full source

/-- Typeclass for separably closed fields.

To show `Polynomial.Splits p f` for an arbitrary ring homomorphism `f`,
see `IsSepClosed.splits_codomain` and `IsSepClosed.splits_domain`.
-/
class IsSepClosed : Prop where
  splits_of_separable : ∀ p : k[X], p.Separable → (p.Splits <| RingHom.id k)

Separably Closed Field

Informal description

A field $ k $ is called *separably closed* if every separable polynomial over $ k $ splits completely into linear factors in $ k $. This means that for any separable polynomial $ p \in k[X] $, there exists a factorization $ p = c \prod_{i=1}^n (X - a_i) $ where $ c, a_i \in k $.

IsSepClosed.of_isAlgClosed instance

[IsAlgClosed k] : IsSepClosed k

Full source

/-- An algebraically closed field is also separably closed. -/
instance IsSepClosed.of_isAlgClosed [IsAlgClosed k] : IsSepClosed k :=
  ⟨fun p _ ↦ IsAlgClosed.splits p⟩

Algebraically Closed Fields are Separably Closed

Informal description

Every algebraically closed field $k$ is also separably closed.

IsSepClosed.splits_codomain theorem

[IsSepClosed K] {f : k →+* K} (p : k[X]) (h : p.Separable) : p.Splits f

Full source

/-- Every separable polynomial splits in the field extension `f : k →+* K` if `K` is
separably closed.

See also `IsSepClosed.splits_domain` for the case where `k` is separably closed.
-/
theorem IsSepClosed.splits_codomain [IsSepClosed K] {f : k →+* K}
    (p : k[X]) (h : p.Separable) : p.Splits f := by
  convert IsSepClosed.splits_of_separable (p.map f) (Separable.map h); simp [splits_map_iff]

Splitting of Separable Polynomials over Separably Closed Field Extensions

Informal description

Let $K$ be a separably closed field and $f \colon k \to K$ be a ring homomorphism. For any separable polynomial $p \in k[X]$, the polynomial $p$ splits completely in $K$ via $f$, i.e., there exist elements $a_1, \dots, a_n \in K$ and a constant $c \in K$ such that $p(f(X)) = c \prod_{i=1}^n (X - a_i)$ in $K[X]$.

IsSepClosed.splits_domain theorem

[IsSepClosed k] {f : k →+* K} (p : k[X]) (h : p.Separable) : p.Splits f

Full source

/-- Every separable polynomial splits in the field extension `f : k →+* K` if `k` is
separably closed.

See also `IsSepClosed.splits_codomain` for the case where `k` is separably closed.
-/
theorem IsSepClosed.splits_domain [IsSepClosed k] {f : k →+* K}
    (p : k[X]) (h : p.Separable) : p.Splits f :=
  Polynomial.splits_of_splits_id _ <| IsSepClosed.splits_of_separable _ h

Splitting of Separable Polynomials over Separably Closed Fields via Ring Homomorphism

Informal description

Let $k$ be a separably closed field and $f \colon k \to K$ be a ring homomorphism. For any separable polynomial $p \in k[X]$, the polynomial $p$ splits completely in $K$ via $f$, i.e., there exist elements $a_1, \dots, a_n \in K$ and a constant $c \in K$ such that $p(f(X)) = c \prod_{i=1}^n (X - a_i)$ in $K[X]$.

IsSepClosed.exists_root theorem

[IsSepClosed k] (p : k[X]) (hp : p.degree ≠ 0) (hsep : p.Separable) : ∃ x, IsRoot p x

Full source

theorem exists_root [IsSepClosed k] (p : k[X]) (hp : p.degree ≠ 0) (hsep : p.Separable) :
    ∃ x, IsRoot p x :=
  exists_root_of_splits _ (IsSepClosed.splits_of_separable p hsep) hp

Existence of Roots for Separable Polynomials over Separably Closed Fields

Informal description

Let $k$ be a separably closed field and $p \in k[X]$ be a separable polynomial of nonzero degree. Then there exists an element $x \in k$ such that $p(x) = 0$.

IsSepClosed.exists_root_C_mul_X_pow_add_C_mul_X_add_C theorem

 [IsSepClosed k] {n : ℕ} (a b c : k) (hn : (n : k) = 0) (hn' : 2 ≤ n) (hb : b ≠ 0) : ∃ x, a * x ^ n + b * x + c = 0

Full source

/-- If `n ≥ 2` equals zero in a separably closed field `k`, `b ≠ 0`,
then there exists `x` in `k` such that `a * x ^ n + b * x + c = 0`. -/
theorem exists_root_C_mul_X_pow_add_C_mul_X_add_C
    [IsSepClosed k] {n : ℕ} (a b c : k) (hn : (n : k) = 0) (hn' : 2 ≤ n) (hb : b ≠ 0) :
    ∃ x, a * x ^ n + b * x + c = 0 := by
  let f : k[X] := C a * X ^ n + C b * X + C c
  have hdeg : f.degree ≠ 0 := degree_ne_of_natDegree_ne <| by
    by_cases ha : a = 0
    · suffices f.natDegree = 1 from this ▸ one_ne_zero
      simp_rw [f, ha, map_zero, zero_mul, zero_add]
      compute_degree!
    · suffices f.natDegree = n from this ▸ (lt_of_lt_of_le zero_lt_two hn').ne'
      simp_rw [f]
      have h0 : n ≠ 0 := by linarith only [hn']
      have h1 : n ≠ 1 := by linarith only [hn']
      have : 1 ≤ n := le_trans one_le_two hn'
      compute_degree!
      simp [h0, h1, ha]
  have hsep : f.Separable := separable_C_mul_X_pow_add_C_mul_X_add_C a b c hn hb.isUnit
  obtain ⟨x, hx⟩ := exists_root f hdeg hsep
  exact ⟨x, by simpa [f] using hx⟩

Existence of roots for $a x^n + b x + c = 0$ in separably closed fields when $n \geq 2$ and $n = 0$ in $k$

Informal description

Let $k$ be a separably closed field, and let $n \geq 2$ be a natural number such that $n = 0$ in $k$. For any elements $a, b, c \in k$ with $b \neq 0$, there exists an element $x \in k$ satisfying the equation $a x^n + b x + c = 0$.

IsSepClosed.exists_root_C_mul_X_pow_add_C_mul_X_add_C' theorem

 [IsSepClosed k] (p n : ℕ) (a b c : k) [CharP k p] (hn : p ∣ n) (hn' : 2 ≤ n) (hb : b ≠ 0) :
  ∃ x, a * x ^ n + b * x + c = 0

Full source

/-- If a separably closed field `k` is of characteristic `p`, `n ≥ 2` is such that `p ∣ n`, `b ≠ 0`,
then there exists `x` in `k` such that `a * x ^ n + b * x + c = 0`. -/
theorem exists_root_C_mul_X_pow_add_C_mul_X_add_C'
    [IsSepClosed k] (p n : ℕ) (a b c : k) [CharP k p] (hn : p ∣ n) (hn' : 2 ≤ n) (hb : b ≠ 0) :
    ∃ x, a * x ^ n + b * x + c = 0 :=
  exists_root_C_mul_X_pow_add_C_mul_X_add_C a b c ((CharP.cast_eq_zero_iff k p n).2 hn) hn' hb

Existence of roots for $a x^n + b x + c = 0$ in separably closed fields of characteristic $p$ dividing $n$

Informal description

Let $k$ be a separably closed field of characteristic $p$, and let $n \geq 2$ be a natural number such that $p$ divides $n$. For any elements $a, b, c \in k$ with $b \neq 0$, there exists an element $x \in k$ satisfying the equation $a x^n + b x + c = 0$.

IsSepClosed.isAlgClosed_of_perfectField instance

[IsSepClosed k] [PerfectField k] : IsAlgClosed k

Full source

/-- A separably closed perfect field is also algebraically closed. -/
instance (priority := 100) isAlgClosed_of_perfectField [IsSepClosed k] [PerfectField k] :
    IsAlgClosed k :=
  IsAlgClosed.of_exists_root k fun p _ h ↦ exists_root p ((degree_pos_of_irreducible h).ne')
    (PerfectField.separable_of_irreducible h)

Separably Closed Perfect Fields are Algebraically Closed

Informal description

Every separably closed perfect field is algebraically closed.

IsSepClosed.exists_pow_nat_eq theorem

[IsSepClosed k] (x : k) (n : ℕ) [hn : NeZero (n : k)] : ∃ z, z ^ n = x

Full source

theorem exists_pow_nat_eq [IsSepClosed k] (x : k) (n : ℕ) [hn : NeZero (n : k)] :
    ∃ z, z ^ n = x := by
  have hn' : 0 < n := Nat.pos_of_ne_zero fun h => by
    rw [h, Nat.cast_zero] at hn
    exact hn.out rfl
  have : degreedegree (X ^ n - C x) ≠ 0 := by
    rw [degree_X_pow_sub_C hn' x]
    exact (WithBot.coe_lt_coe.2 hn').ne'
  by_cases hx : x = 0
  · exact ⟨0, by rw [hx, pow_eq_zero_iff hn'.ne']⟩
  · obtain ⟨z, hz⟩ := exists_root _ this <| separable_X_pow_sub_C x hn.out hx
    use z
    simpa [eval_C, eval_X, eval_pow, eval_sub, IsRoot.def, sub_eq_zero] using hz

Existence of $n$-th Roots in Separably Closed Fields

Informal description

Let $k$ be a separably closed field, $x \in k$ an element, and $n$ a natural number such that $n \neq 0$ in $k$. Then there exists an element $z \in k$ such that $z^n = x$.

IsSepClosed.exists_eq_mul_self theorem

[IsSepClosed k] (x : k) [h2 : NeZero (2 : k)] : ∃ z, x = z * z

Full source

theorem exists_eq_mul_self [IsSepClosed k] (x : k) [h2 : NeZero (2 : k)] : ∃ z, x = z * z := by
  rcases exists_pow_nat_eq x 2 with ⟨z, rfl⟩
  exact ⟨z, sq z⟩

Existence of Square Roots in Separably Closed Fields of Characteristic ≠ 2

Informal description

Let $k$ be a separably closed field and $x \in k$ an element. If $2 \neq 0$ in $k$, then there exists an element $z \in k$ such that $x = z^2$.

IsSepClosed.roots_eq_zero_iff theorem

[IsSepClosed k] {p : k[X]} (hsep : p.Separable) : p.roots = 0 ↔ p = Polynomial.C (p.coeff 0)

Full source

theorem roots_eq_zero_iff [IsSepClosed k] {p : k[X]} (hsep : p.Separable) :
    p.roots = 0 ↔ p = Polynomial.C (p.coeff 0) := by
  refine ⟨fun h => ?_, fun hp => by rw [hp, roots_C]⟩
  rcases le_or_lt (degree p) 0 with hd | hd
  · exact eq_C_of_degree_le_zero hd
  · obtain ⟨z, hz⟩ := IsSepClosed.exists_root p hd.ne' hsep
    rw [← mem_roots (ne_zero_of_degree_gt hd), h] at hz
    simp at hz

Roots of Separable Polynomial in Separably Closed Field are Empty iff Polynomial is Constant

Informal description

Let $k$ be a separably closed field and $p \in k[X]$ be a separable polynomial. The multiset of roots of $p$ is empty if and only if $p$ is a constant polynomial, i.e., $p = c$ where $c$ is the constant term of $p$.

IsSepClosed.exists_eval₂_eq_zero theorem

[IsSepClosed K] (f : k →+* K) (p : k[X]) (hp : p.degree ≠ 0) (hsep : p.Separable) : ∃ x, p.eval₂ f x = 0

Full source

theorem exists_eval₂_eq_zero [IsSepClosed K] (f : k →+* K)
    (p : k[X]) (hp : p.degree ≠ 0) (hsep : p.Separable) :
    ∃ x, p.eval₂ f x = 0 :=
  let ⟨x, hx⟩ := exists_root (p.map f) (by rwa [degree_map_eq_of_injective f.injective])
    (Separable.map hsep)
  ⟨x, by rwa [eval₂_eq_eval_map, ← IsRoot]⟩

Existence of Roots for Separable Polynomials under Ring Homomorphism in Separably Closed Fields

Informal description

Let $K$ be a separably closed field, $k$ be a field, and $f \colon k \to K$ be a ring homomorphism. For any separable polynomial $p \in k[X]$ of nonzero degree, there exists an element $x \in K$ such that the evaluation of $p$ at $x$ via $f$ is zero, i.e., $p.eval₂\, f\, x = 0$.

IsSepClosed.exists_aeval_eq_zero theorem

[IsSepClosed K] [Algebra k K] (p : k[X]) (hp : p.degree ≠ 0) (hsep : p.Separable) : ∃ x : K, aeval x p = 0

Full source

theorem exists_aeval_eq_zero [IsSepClosed K] [Algebra k K] (p : k[X])
    (hp : p.degree ≠ 0) (hsep : p.Separable) : ∃ x : K, aeval x p = 0 :=
  exists_eval₂_eq_zero (algebraMap k K) p hp hsep

Existence of Roots for Separable Polynomials in Separably Closed Field Extensions

Informal description

Let $K$ be a separably closed field with an algebra structure over a field $k$. For any separable polynomial $p \in k[X]$ of nonzero degree, there exists an element $x \in K$ such that the evaluation of $p$ at $x$ via the algebra map is zero, i.e., $\text{aeval}\, x\, p = 0$.

IsSepClosed.of_exists_root theorem

(H : ∀ p : k[X], p.Monic → Irreducible p → Separable p → ∃ x, p.eval x = 0) : IsSepClosed k

Full source

theorem of_exists_root (H : ∀ p : k[X], p.Monic → Irreducible p → Separable p → ∃ x, p.eval x = 0) :
    IsSepClosed k := by
  refine ⟨fun p hsep ↦ Or.inr ?_⟩
  intro q hq hdvd
  simp only [map_id] at hdvd
  have hlc : IsUnit (leadingCoeff q)⁻¹ := IsUnit.inv <| Ne.isUnit <|
    leadingCoeff_ne_zero.2 <| Irreducible.ne_zero hq
  have hsep' : Separable (q * C (leadingCoeff q)⁻¹) :=
    Separable.mul (Separable.of_dvd hsep hdvd) ((separable_C _).2 hlc)
    (by simpa only [← isCoprime_mul_unit_right_right (isUnit_C.2 hlc) q 1, one_mul]
      using isCoprime_one_right (x := q))
  have hirr' := hq
  rw [← irreducible_mul_isUnit (isUnit_C.2 hlc)] at hirr'
  obtain ⟨x, hx⟩ := H (q * C (leadingCoeff q)⁻¹) (monic_mul_leadingCoeff_inv hq.ne_zero) hirr' hsep'
  exact degree_mul_leadingCoeff_inv q hq.ne_zero ▸ degree_eq_one_of_irreducible_of_root hirr' hx

Characterization of Separably Closed Fields via Root Existence for Monic Irreducible Separable Polynomials

Informal description

A field $ k $ is separably closed if for every monic, irreducible, and separable polynomial $ p \in k[X] $, there exists an element $ x \in k $ such that $ p(x) = 0 $.

IsSepClosed.degree_eq_one_of_irreducible theorem

[IsSepClosed k] {p : k[X]} (hp : Irreducible p) (hsep : p.Separable) : p.degree = 1

Full source

theorem degree_eq_one_of_irreducible [IsSepClosed k] {p : k[X]}
    (hp : Irreducible p) (hsep : p.Separable) : p.degree = 1 :=
  degree_eq_one_of_irreducible_of_splits hp (IsSepClosed.splits_codomain p hsep)

Degree of Irreducible Separable Polynomials in Separably Closed Fields is One

Informal description

Let $k$ be a separably closed field. For any irreducible and separable polynomial $p \in k[X]$, the degree of $p$ is equal to $1$.

IsSepClosed.algebraMap_surjective theorem

[IsSepClosed k] [Algebra k K] [Algebra.IsSeparable k K] : Function.Surjective (algebraMap k K)

Full source

theorem algebraMap_surjective
    [IsSepClosed k] [Algebra k K] [Algebra.IsSeparable k K] :
    Function.Surjective (algebraMap k K) := by
  refine fun x => ⟨-(minpoly k x).coeff 0, ?_⟩
  have hq : (minpoly k x).leadingCoeff = 1 := minpoly.monic (Algebra.IsSeparable.isIntegral k x)
  have hsep : IsSeparable k x := Algebra.IsSeparable.isSeparable k x
  have h : (minpoly k x).degree = 1 :=
    degree_eq_one_of_irreducible k (minpoly.irreducible (Algebra.IsSeparable.isIntegral k x)) hsep
  have : aeval x (minpoly k x) = 0 := minpoly.aeval k x
  rw [eq_X_add_C_of_degree_eq_one h, hq, C_1, one_mul, aeval_add, aeval_X, aeval_C,
    add_eq_zero_iff_eq_neg] at this
  exact (RingHom.map_neg (algebraMap k K) ((minpoly k x).coeff 0)).symm ▸ this.symm

Surjectivity of the Algebra Map from a Separably Closed Field to a Separable Extension

Informal description

Let $k$ be a separably closed field and $K$ be a separable field extension of $k$. Then the algebra map $\text{algebraMap}\ k\ K$ from $k$ to $K$ is surjective.

IsSepClosure structure

[Algebra k K]

Full source

/-- Typeclass for an extension being a separable closure. -/
class IsSepClosure [Algebra k K] : Prop where
  sep_closed : IsSepClosed K
  separable : Algebra.IsSeparable k K

Separable Closure of a Field

Informal description

The structure `IsSepClosure k K` asserts that `K` is a separable closure of the field `k`, meaning that `K` is a separably closed field extension of `k` and that the extension `K/k` is separable.

IsSepClosure.self_of_isSepClosed instance

[IsSepClosed k] : IsSepClosure k k

Full source

/-- A separably closed field is its separable closure. -/
instance IsSepClosure.self_of_isSepClosed [IsSepClosed k] : IsSepClosure k k :=
  ⟨by assumption, Algebra.isSeparable_self k⟩

Separably Closed Field as Its Own Separable Closure

Informal description

For any separably closed field $k$, $k$ is its own separable closure.

IsSepClosure.isAlgClosure_of_perfectField_top instance

[Algebra k K] [IsSepClosure k K] [PerfectField K] : IsAlgClosure k K

Full source

/-- If `K` is perfect and is a separable closure of `k`,
then it is also an algebraic closure of `k`. -/
instance (priority := 100) IsSepClosure.isAlgClosure_of_perfectField_top
    [Algebra k K] [IsSepClosure k K] [PerfectField K] : IsAlgClosure k K :=
  haveI : IsSepClosed K := IsSepClosure.sep_closed k
  ⟨inferInstance, IsSepClosure.separable.isAlgebraic⟩

Separable Closure of a Perfect Field is Algebraically Closed

Informal description

For any field extension $ K $ of $ k $ that is a separable closure of $ k $, if $ K $ is perfect, then $ K $ is also an algebraic closure of $ k $.

IsSepClosure.isAlgClosure_of_perfectField instance

[Algebra k K] [IsSepClosure k K] [PerfectField k] : IsAlgClosure k K

Full source

/-- If `k` is perfect, `K` is a separable closure of `k`,
then it is also an algebraic closure of `k`. -/
instance (priority := 100) IsSepClosure.isAlgClosure_of_perfectField
    [Algebra k K] [IsSepClosure k K] [PerfectField k] : IsAlgClosure k K :=
  have halg : Algebra.IsAlgebraic k K := IsSepClosure.separable.isAlgebraic
  haveI := halg.perfectField; inferInstance

Separable Closure of a Perfect Field is Algebraic Closure

Informal description

For any perfect field $k$ and separable closure $K$ of $k$, $K$ is also an algebraic closure of $k$.

IsSepClosure.of_isAlgClosure_of_perfectField instance

[Algebra k K] [IsAlgClosure k K] [PerfectField k] : IsSepClosure k K

Full source

/-- If `k` is perfect, `K` is an algebraic closure of `k`,
then it is also a separable closure of `k`. -/
instance (priority := 100) IsSepClosure.of_isAlgClosure_of_perfectField
    [Algebra k K] [IsAlgClosure k K] [PerfectField k] : IsSepClosure k K :=
  ⟨haveI := IsAlgClosure.isAlgClosed (R := k) (K := K); inferInstance,
    (IsAlgClosure.isAlgebraic (R := k) (K := K)).isSeparable_of_perfectField⟩

Algebraic Closures of Perfect Fields are Separable Closures

Informal description

For any perfect field $k$ and algebraic closure $K$ of $k$, $K$ is also a separable closure of $k$.

isSepClosure_iff theorem

[Algebra k K] : IsSepClosure k K ↔ IsSepClosed K ∧ Algebra.IsSeparable k K

Full source

theorem isSepClosure_iff [Algebra k K] :
    IsSepClosureIsSepClosure k K ↔ IsSepClosed K ∧ Algebra.IsSeparable k K :=
  ⟨fun h ↦ ⟨h.1, h.2⟩, fun h ↦ ⟨h.1, h.2⟩⟩

Characterization of Separable Closure: $ K $ is a separable closure of $ k $ if and only if $ K $ is separably closed and $ K/k $ is separable.

Informal description

For a field extension $ K $ of $ k $, $ K $ is a separable closure of $ k $ if and only if $ K $ is separably closed and the extension $ K/k $ is separable.

IsSepClosure.isSeparable instance

[Algebra k K] [IsSepClosure k K] : Algebra.IsSeparable k K

Full source

instance isSeparable [Algebra k K] [IsSepClosure k K] : Algebra.IsSeparable k K :=
  IsSepClosure.separable

Separability of Separable Closure Extensions

Informal description

For any field extension $K$ of $k$ that is a separable closure of $k$, the extension $K/k$ is separable.

IsSepClosure.isGalois instance

[Algebra k K] [IsSepClosure k K] : IsGalois k K

Full source

instance (priority := 100) isGalois [Algebra k K] [IsSepClosure k K] : IsGalois k K where
  to_isSeparable := IsSepClosure.separable
  to_normal.toIsAlgebraic :=  inferInstance
  to_normal.splits' x := (IsSepClosure.sep_closed k).splits_codomain _
    (Algebra.IsSeparable.isSeparable k x)

Separable Closure is Galois Extension

Informal description

For any field extension $K$ of $k$ that is a separable closure of $k$, the extension $K/k$ is a Galois extension.

IsSepClosed.surjective_restrictDomain_of_isSeparable theorem

 {E : Type*} [Field E] [Algebra K E] [Algebra L E] [IsScalarTower K L E] [Algebra.IsSeparable L E] :
  Function.Surjective fun φ : E →ₐ[K] M ↦ φ.restrictDomain L

Full source

theorem surjective_restrictDomain_of_isSeparable {E : Type*}
    [Field E] [Algebra K E] [Algebra L E] [IsScalarTower K L E] [Algebra.IsSeparable L E] :
    Function.Surjective fun φ : E →ₐ[K] M ↦ φ.restrictDomain L :=
  fun f ↦ IntermediateField.exists_algHom_of_splits' (E := E) f
    fun s ↦ ⟨Algebra.IsSeparable.isIntegral L s,
      IsSepClosed.splits_codomain _ <| Algebra.IsSeparable.isSeparable L s⟩

Extension Theorem for Separable Field Homomorphisms into Separably Closed Fields

Informal description

Let $K$, $L$, $E$, and $M$ be fields with the following structure: - $E$ is a field extension of both $K$ and $L$, with $K \subseteq L \subseteq E$ forming a scalar tower (i.e., the $K$-algebra structure on $E$ factors through $L$). - $E$ is a separable extension of $L$. - $M$ is a separably closed field extension of $K$. Then the restriction map $\varphi \mapsto \varphi|_L$ from $K$-algebra homomorphisms $\varphi \colon E \to M$ to $L$-algebra homomorphisms $E \to M$ is surjective. In other words, every $L$-algebra homomorphism from $E$ to $M$ extends to a $K$-algebra homomorphism from $E$ to $M$.

IsSepClosed.lift definition

Full source

/-- A (random) homomorphism from a separable extension L of K into a separably
  closed extension M of K. -/
noncomputable irreducible_def lift : L →ₐ[K] M :=
  Classical.choice <| IntermediateField.nonempty_algHom_of_adjoin_splits
    (fun x _ ↦ ⟨Algebra.IsSeparable.isIntegral K x,
      splits_codomain _ (Algebra.IsSeparable.isSeparable K x)⟩)
    (IntermediateField.adjoin_univ K L)

Lift of a separable extension into a separably closed extension

Informal description

Given a separable field extension $ L $ of $ K $ and a separably closed field extension $ M $ of $ K $, there exists an algebra homomorphism from $ L $ to $ M $ over $ K $. This homomorphism is constructed by extending the inclusion map $ K \hookrightarrow M $ to $ L $ using the fact that $ L $ is generated over $ K $ by elements whose minimal polynomials are separable and split in $ M $.

IsSepClosed.lift_def theorem

: eta_helper Eq✝ @lift.{} @(delta% @definition✝)

Full source

/-- A (random) homomorphism from a separable extension L of K into a separably
  closed extension M of K. -/
noncomputable irreducible_def lift : L →ₐ[K] M :=
  Classical.choice <| IntermediateField.nonempty_algHom_of_adjoin_splits
    (fun x _ ↦ ⟨Algebra.IsSeparable.isIntegral K x,
      splits_codomain _ (Algebra.IsSeparable.isSeparable K x)⟩)
    (IntermediateField.adjoin_univ K L)

Definition of the Separable Extension Lifting Homomorphism

Informal description

The definition of the lifting homomorphism from a separable extension $L$ of $K$ to a separably closed extension $M$ of $K$ satisfies the expected properties of being an algebra homomorphism over $K$.

IsSepClosure.equiv definition

: L ≃ₐ[K] M

Full source

/-- A (random) isomorphism between two separable closures of `K`. -/
noncomputable def equiv : L ≃ₐ[K] M :=
  AlgEquiv.ofBijective _ (Normal.toIsAlgebraic.algHom_bijective₂
    (IsSepClosed.lift : L →ₐ[K] M) (IsSepClosed.lift : M →ₐ[K] L)).1

Isomorphism between separable closures of a field

Informal description

Given two separable closures $ L $ and $ M $ of a field $ K $, there exists an algebra isomorphism $ L \simeq M $ over $ K $. This isomorphism is constructed by lifting the inclusion maps $ K \hookrightarrow L $ and $ K \hookrightarrow M $ to algebra homomorphisms between $ L $ and $ M $ and showing that they are bijective.

Main Definitions

Tags

Related