Mathlib.FieldTheory.Normal.Closure

IsNormalClosure structure

Full source

/-- `L/F` is a normal closure of `K/F` if the minimal polynomial of every element of `K` over `F`
  splits in `L`, and `L` is generated by roots of such minimal polynomials over `F`.
  (Since the minimal polynomial of a transcendental element is 0,
  the normal closure of `K/F` is the same as the normal closure over `F`
  of the algebraic closure of `F` in `K`.) -/
@[stacks 0BMF "Predicate version"]
class IsNormalClosure : Prop where
  splits (x : K) : (minpoly F x).Splits (algebraMap F L)
  adjoin_rootSet : ⨆ x : K, adjoin F ((minpoly F x).rootSet L) = ⊤

Normal closure of a field extension

Informal description

A field extension $L/F$ is called a normal closure of $K/F$ if: 1. The minimal polynomial of every element of $K$ over $F$ splits completely in $L$ 2. $L$ is generated over $F$ by the roots of such minimal polynomials For transcendental elements (whose minimal polynomial is 0), this is equivalent to taking the normal closure of the algebraic closure of $F$ in $K$.

IntermediateField.normalClosure definition

: IntermediateField F L

Full source

/-- The normal closure of `K/F` in `L/F`. -/
@[stacks 0BMF]
noncomputable def IntermediateField.normalClosure : IntermediateField F L :=
  ⨆ f : K →ₐ[F] L, f.fieldRange

Normal closure of $ K/F $ in $ L/F $

Informal description

The normal closure of a field extension $ K/F $ inside another field extension $ L/F $ is the smallest intermediate field of $ L/F $ that contains the image of every $ F $-algebra homomorphism from $ K $ to $ L $. It is constructed as the supremum (join) of the ranges of all such homomorphisms.

normalClosure_def theorem

: normalClosure F K L = ⨆ f : K →ₐ[F] L, f.fieldRange

Full source

lemma normalClosure_def : normalClosure F K L = ⨆ f : K →ₐ[F] L, f.fieldRange :=
  rfl

Definition of Normal Closure as Supremum of Homomorphism Ranges

Informal description

The normal closure of a field extension $K/F$ inside another field extension $L/F$ is equal to the supremum (join) of the ranges of all $F$-algebra homomorphisms from $K$ to $L$. In other words, \[ \text{normalClosure}(F, K, L) = \bigsqcup_{f \colon K \to_{F\text{-alg}} L} \text{fieldRange}(f). \]

IsNormalClosure.normal theorem

[h : IsNormalClosure F K L] : Normal F L

Full source

/-- A normal closure is always normal. -/
lemma IsNormalClosure.normal [h : IsNormalClosure F K L] : Normal F L :=
  Normal.of_algEquiv topEquiv (h := h.adjoin_rootSet ▸ IntermediateField.normal_iSup (h :=
    fun _ ↦ Normal.of_isSplittingField (hFEp := adjoin_rootSet_isSplittingField <| h.splits _)))

Normality of Normal Closures

Informal description

If $L/F$ is a normal closure of the field extension $K/F$, then $L/F$ is a normal extension. That is, $L$ is algebraic over $F$ and the minimal polynomial of every element of $L$ over $F$ splits completely in $L$.

normalClosure_le_iff theorem

{K' : IntermediateField F L} : normalClosure F K L ≤ K' ↔ ∀ f : K →ₐ[F] L, f.fieldRange ≤ K'

Full source

lemma normalClosure_le_iff {K' : IntermediateField F L} :
    normalClosurenormalClosure F K L ≤ K' ↔ ∀ f : K →ₐ[F] L, f.fieldRange ≤ K' :=
  iSup_le_iff

Characterization of Normal Closure Containment: $\text{normalClosure}(F,K,L) \leq K' \leftrightarrow \forall f \colon K \toₐ[F] L, \text{range}(f) \leq K'$

Informal description

For any intermediate field $K'$ between $F$ and $L$, the normal closure of $K/F$ in $L/F$ is contained in $K'$ if and only if for every $F$-algebra homomorphism $f \colon K \to L$, the range of $f$ is contained in $K'$.

AlgHom.fieldRange_le_normalClosure theorem

(f : K →ₐ[F] L) : f.fieldRange ≤ normalClosure F K L

Full source

lemma AlgHom.fieldRange_le_normalClosure (f : K →ₐ[F] L) : f.fieldRange ≤ normalClosure F K L :=
  le_iSup AlgHom.fieldRange f

Range of Algebra Homomorphism is Contained in Normal Closure

Informal description

For any $F$-algebra homomorphism $f \colon K \to L$ between field extensions $L/F$ and $K/F$, the range of $f$ is contained in the normal closure of $K/F$ in $L/F$. That is, $f(K) \subseteq \text{normalClosure}_F(K, L)$.

Algebra.IsAlgebraic.normalClosure_le_iSup_adjoin theorem

: normalClosure F K L ≤ ⨆ x : K, IntermediateField.adjoin F ((minpoly F x).rootSet L)

Full source

lemma normalClosure_le_iSup_adjoin :
    normalClosure F K L ≤ ⨆ x : K, IntermediateField.adjoin F ((minpoly F x).rootSet L) :=
  iSup_le fun f _ ⟨x, hx⟩ ↦ le_iSup (α := IntermediateField F L) _ x <|
    IntermediateField.subset_adjoin F _ <| by
      rw [mem_rootSet_of_ne (minpoly.ne_zero (Algebra.IsIntegral.isIntegral x)), ← hx,
        AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom, aeval_algHom_apply, minpoly.aeval, map_zero]

Normal Closure is Contained in Supremum of Adjoined Root Fields for Algebraic Extensions

Informal description

For an algebraic field extension $K/F$ and any field extension $L/F$, the normal closure of $K/F$ in $L/F$ is contained in the supremum of the fields obtained by adjoining to $F$ the roots in $L$ of the minimal polynomials of all elements $x \in K$ over $F$. In other words, \[ \text{normalClosure}_F(K, L) \leq \bigsqcup_{x \in K} F(\text{roots}_L(\text{minpoly}_F(x))). \]

Algebra.IsAlgebraic.normalClosure_eq_iSup_adjoin_of_splits theorem

: normalClosure F K L = ⨆ x : K, IntermediateField.adjoin F ((minpoly F x).rootSet L)

Full source

lemma normalClosure_eq_iSup_adjoin_of_splits :
    normalClosure F K L = ⨆ x : K, IntermediateField.adjoin F ((minpoly F x).rootSet L) :=
  normalClosure_le_iSup_adjoin.antisymm <|
    iSup_le fun x ↦ IntermediateField.adjoin_le_iff.mpr fun _ hy ↦
      let ⟨φ, hφ⟩ := IntermediateField.exists_algHom_of_splits_of_aeval
        (fun x ↦ ⟨Algebra.IsIntegral.isIntegral x, splits x⟩) (mem_rootSet.mp hy).2
      le_iSup AlgHom.fieldRange φ ⟨x, hφ⟩

Normal Closure Equals Supremum of Adjoined Root Fields for Splitting Algebraic Extensions

Informal description

For an algebraic field extension $K/F$ and any field extension $L/F$ such that the minimal polynomial of every element $x \in K$ splits in $L$, the normal closure of $K/F$ in $L/F$ is equal to the supremum of the fields obtained by adjoining to $F$ the roots in $L$ of the minimal polynomials of all elements $x \in K$ over $F$. In symbols: \[ \text{normalClosure}_F(K, L) = \bigsqcup_{x \in K} F(\text{roots}_L(\text{minpoly}_F(x))). \]

Algebra.IsAlgebraic.isNormalClosure_iff theorem

: IsNormalClosure F K L ↔ (∀ x : K, (minpoly F x).Splits (algebraMap F L)) ∧ normalClosure F K L = ⊤

Full source

/-- If `K/F` is algebraic, the "generated by roots" condition in IsNormalClosure can be replaced
  by "generated by images of embeddings". -/
lemma isNormalClosure_iff : IsNormalClosureIsNormalClosure F K L ↔
    (∀ x : K, (minpoly F x).Splits (algebraMap F L)) ∧ normalClosure F K L = ⊤ := by
  refine ⟨fun ⟨splits, h⟩ ↦ ⟨splits, ?_⟩, fun ⟨splits, h⟩ ↦ ⟨splits, ?_⟩⟩ <;>
    simpa only [normalClosure_eq_iSup_adjoin_of_splits splits] using h

Characterization of Normal Closures for Algebraic Extensions

Informal description

For an algebraic field extension $K/F$ and a field extension $L/F$, the following are equivalent: 1. $L/F$ is a normal closure of $K/F$, i.e., the minimal polynomial of every element $x \in K$ over $F$ splits in $L$ and $L$ is generated over $F$ by the roots of these minimal polynomials. 2. The minimal polynomial of every element $x \in K$ over $F$ splits in $L$ and the normal closure of $K/F$ in $L/F$ is equal to $L$ itself. In symbols: \[ \text{IsNormalClosure}(F, K, L) \iff \left( \forall x \in K, \text{Splits}(\text{minpoly}_F(x), L) \right) \land \text{normalClosure}_F(K, L) = L. \]

Algebra.IsAlgebraic.isNormalClosure_normalClosure theorem

: IsNormalClosure F K (normalClosure F K L)

Full source

/-- `normalClosure F K L` is a valid normal closure if `K/F` is algebraic
  and all minimal polynomials of `K/F` splits in `L/F`. -/
lemma isNormalClosure_normalClosure : IsNormalClosure F K (normalClosure F K L) := by
  rw [isNormalClosure_iff]; constructor
  · rw [normalClosure_eq_iSup_adjoin_of_splits splits]
    exact fun x ↦ splits_of_splits (splits x) ((IntermediateField.subset_adjoin F _).trans <|
      SetLike.coe_subset_coe.mpr <| by apply le_iSup _ x)
  simp_rw [normalClosure, ← top_le_iff]
  refine fun x _ ↦ ((⨆ f : K →ₐ[F] L, f.fieldRange).val).injective.mem_set_image |>.mp ?_
  rw [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, coe_val, ← IntermediateField.coe_val,
    ← IntermediateField.coe_map, IntermediateField.map_iSup]
  refine (iSup_le fun f ↦ ?_ : normalClosure F K L ≤ _) x.2
  refine le_iSup_of_le (f.codRestrict _ fun x ↦ f.fieldRange_le_normalClosure ⟨x, rfl⟩) ?_
  rw [AlgHom.map_fieldRange, val, AlgHom.val_comp_codRestrict]

Normal Closure of an Algebraic Extension is a Normal Closure

Informal description

For an algebraic field extension $K/F$ and any field extension $L/F$, the normal closure of $K/F$ in $L/F$ (denoted $\text{normalClosure}_F(K, L)$) is itself a normal closure of $K/F$. That is, the minimal polynomial of every element of $K$ over $F$ splits in $\text{normalClosure}_F(K, L)$, and $\text{normalClosure}_F(K, L)$ is generated over $F$ by the roots of these minimal polynomials.

IsNormalClosure.lift definition

 [h : IsNormalClosure F K L] {L'} [Field L'] [Algebra F L'] (splits : ∀ x : K, (minpoly F x).Splits (algebraMap F L')) :
  L →ₐ[F] L'

Full source

/-- A normal closure of `K/F` embeds into any `L/F`
  where the minimal polynomials of `K/F` splits. -/
noncomputable def IsNormalClosure.lift [h : IsNormalClosure F K L] {L'} [Field L'] [Algebra F L']
    (splits : ∀ x : K, (minpoly F x).Splits (algebraMap F L')) : L →ₐ[F] L' := by
  have := h.adjoin_rootSet; rw [← gc.l_iSup] at this
  refine Nonempty.some <| nonempty_algHom_of_adjoin_splits
    (fun x hx ↦ ⟨isAlgebraic_iff_isIntegral.mp ((h.normal).isAlgebraic x), ?_⟩) this
  obtain ⟨y, hx⟩ := Set.mem_iUnion.mp hx
  by_cases iy : IsIntegral F y
  · exact splits_of_splits_of_dvd _ (minpoly.ne_zero iy)
      (splits y) (minpoly.dvd F x (mem_rootSet.mp hx).2)
  · simp [minpoly.eq_zero iy] at hx

Lifting property of normal closures

Informal description

Given a normal closure $ L $ of $ K $ over $ F $ and another field extension $ L' $ of $ F $ where the minimal polynomial of every element of $ K $ splits in $ L' $, there exists an $ F $-algebra homomorphism from $ L $ to $ L' $.

IsNormalClosure.equiv definition

{L'} [Field L'] [Algebra F L'] [h : IsNormalClosure F K L] [h' : IsNormalClosure F K L'] : L ≃ₐ[F] L'

Full source

/-- Normal closures of `K/F` are unique up to F-algebra isomorphisms. -/
noncomputable def IsNormalClosure.equiv {L'} [Field L'] [Algebra F L']
    [h : IsNormalClosure F K L] [h' : IsNormalClosure F K L'] : L ≃ₐ[F] L' :=
  have := h.normal
  AlgEquiv.ofBijective _ <| And.left <|
    Normal.toIsAlgebraic.algHom_bijective₂
      (IsNormalClosure.lift fun _ : K ↦ h'.splits _)
      (IsNormalClosure.lift fun _ : K ↦ h.splits _)

Uniqueness of normal closures up to isomorphism

Informal description

Given two field extensions $ L $ and $ L' $ of $ F $, both being normal closures of $ K $ over $ F $, there exists an $ F $-algebra isomorphism between $ L $ and $ L' $. In other words, normal closures are unique up to $ F $-algebra isomorphism.

isNormalClosure_normalClosure instance

[ne : Nonempty (K →ₐ[F] L)] [h : Normal F L] : IsNormalClosure F K (normalClosure F K L)

Full source

instance isNormalClosure_normalClosure [ne : Nonempty (K →ₐ[F] L)] [h : Normal F L] :
    IsNormalClosure F K (normalClosure F K L) := by
  have ⟨φ⟩ := ne
  apply (h.toIsAlgebraic.of_injective φ φ.injective).isNormalClosure_normalClosure
  simp_rw [← minpoly.algHom_eq _ φ.injective]
  exact fun _ ↦ h.splits _

Normal Closure Construction Yields Normal Closure

Informal description

Let $F \subseteq K \subseteq L$ be field extensions with $L/F$ normal, and assume there exists at least one $F$-algebra homomorphism from $K$ to $L$. Then the normal closure of $K$ over $F$ in $L$ is itself a normal closure of $K$ over $F$. That is, the minimal polynomial of every element of $K$ over $F$ splits in $\text{normalClosure}_F(K, L)$, and $\text{normalClosure}_F(K, L)$ is generated over $F$ by the roots of these minimal polynomials.

normalClosure_eq_iSup_adjoin' theorem

[ne : Nonempty (K →ₐ[F] L)] [h : Normal F L] : normalClosure F K L = ⨆ x : K, adjoin F ((minpoly F x).rootSet L)

Full source

theorem normalClosure_eq_iSup_adjoin' [ne : Nonempty (K →ₐ[F] L)] [h : Normal F L] :
    normalClosure F K L = ⨆ x : K, adjoin F ((minpoly F x).rootSet L) := by
  have ⟨φ⟩ := ne
  refine h.toIsAlgebraic.of_injective φ φ.injective
    |>.normalClosure_eq_iSup_adjoin_of_splits fun x ↦ ?_
  rw [← minpoly.algHom_eq _ φ.injective]
  apply h.splits

Normal Closure as Supremum of Adjoined Root Fields

Informal description

Let $F \subseteq K \subseteq L$ be field extensions with $L/F$ normal, and assume there exists at least one $F$-algebra homomorphism from $K$ to $L$. Then the normal closure of $K$ over $F$ in $L$ is equal to the compositum of the fields obtained by adjoining to $F$ all roots in $L$ of the minimal polynomials of elements of $K$ over $F$. In symbols: \[ \text{normalClosure}_F(K, L) = \bigsqcup_{x \in K} F(\text{roots}_L(\text{minpoly}_F(x))). \]

normalClosure_eq_iSup_adjoin theorem

[Algebra K L] [IsScalarTower F K L] [Normal F L] : normalClosure F K L = ⨆ x : K, adjoin F ((minpoly F x).rootSet L)

Full source

theorem normalClosure_eq_iSup_adjoin [Algebra K L] [IsScalarTower F K L] [Normal F L] :
    normalClosure F K L = ⨆ x : K, adjoin F ((minpoly F x).rootSet L) :=
  normalClosure_eq_iSup_adjoin' (ne := ⟨IsScalarTower.toAlgHom F K L⟩)

Normal Closure as Supremum of Adjoined Root Fields in Tower Extension

Informal description

Let $F \subseteq K \subseteq L$ be field extensions such that $L/F$ is normal. Then the normal closure of $K$ over $F$ in $L$ is equal to the compositum of the fields obtained by adjoining to $F$ all roots in $L$ of the minimal polynomials of elements of $K$ over $F$. In symbols: \[ \text{normalClosure}_F(K, L) = \bigsqcup_{x \in K} F(\text{roots}_L(\text{minpoly}_F(x))). \]

normalClosure.algHomEquiv definition

: (K →ₐ[F] normalClosure F K L) ≃ (K →ₐ[F] L)

Full source

/-- All `F`-`AlgHom`s from `K` to `L` factor through the normal closure of `K/F` in `L/F`. -/
noncomputable def algHomEquiv : (K →ₐ[F] normalClosure F K L) ≃ (K →ₐ[F] L) where
  toFun := (normalClosure F K L).val.comp
  invFun f := f.codRestrict _ fun x ↦ f.fieldRange_le_normalClosure ⟨x, rfl⟩
  left_inv _ := rfl
  right_inv _ := rfl

Equivalence of algebra homomorphisms through normal closure

Informal description

The equivalence of algebra homomorphisms between $K \to_{\text{Alg}[F]} \text{normalClosure}(F, K, L)$ and $K \to_{\text{Alg}[F]} L$, where $\text{normalClosure}(F, K, L)$ is the normal closure of $K$ over $F$ in $L$. Specifically, every $F$-algebra homomorphism from $K$ to $L$ factors through the normal closure, and conversely, every such homomorphism to the normal closure can be extended to $L$ via the inclusion map.

normalClosure.normal instance

[h : Normal F L] : Normal F (normalClosure F K L)

Full source

@[stacks 0BMG "(1) normality."]
instance normal [h : Normal F L] : Normal F (normalClosure F K L) := by
  obtain _ | φ := isEmpty_or_nonempty (K →ₐ[F] L)
  · rw [normalClosure, iSup_of_empty]; exact Normal.of_algEquiv (botEquiv F L).symm
  · exact (isNormalClosure_normalClosure F K L).normal

Normality of the Normal Closure in a Normal Extension

Informal description

For any field extensions $ K/F $ and $ L/F $, if $ L/F $ is normal, then the normal closure of $ K $ over $ F $ in $ L $ is also a normal extension of $ F $.

normalClosure.is_finiteDimensional instance

[FiniteDimensional F K] : FiniteDimensional F (normalClosure F K L)

Full source

@[stacks 0BMG "When `L` is normal over `K`, this agrees with 0BMG (1) finiteness."]
instance is_finiteDimensional [FiniteDimensional F K] :
    FiniteDimensional F (normalClosure F K L) := by
  haveI : ∀ f : K →ₐ[F] L, FiniteDimensional F f.fieldRange := fun f ↦
    f.toLinearMap.finiteDimensional_range
  apply IntermediateField.finiteDimensional_iSup_of_finite

Finite-Dimensionality of the Normal Closure

Informal description

For field extensions $ K/F $ and $ L/F $, if $ K $ is finite-dimensional over $ F $, then the normal closure of $ K $ in $ L $ is also finite-dimensional over $ F $.

normalClosure.algebra instance

: Algebra K (normalClosure F K L)

Full source

noncomputable instance algebra :
    Algebra K (normalClosure F K L) :=
  IntermediateField.algebra'
    { ⨆ f : K →ₐ[F] L, f.fieldRange with
      algebraMap_mem' := fun r ↦ (toAlgHom F K L).fieldRange_le_normalClosure ⟨r, rfl⟩ }

Algebra Structure on the Normal Closure of $ K $ in $ L $

Informal description

For field extensions $ K/F $ and $ L/F $, the normal closure of $ K $ in $ L $ inherits an algebra structure over $ K $. This means there is a canonical ring homomorphism from $ K $ to the normal closure of $ K $ in $ L $, making it a $ K $-algebra.

normalClosure.instIsScalarTowerSubtypeMemIntermediateFieldNormalClosure instance

: IsScalarTower F K (normalClosure F K L)

Full source

instance : IsScalarTower F K (normalClosure F K L) := by
  apply of_algebraMap_eq'
  ext x
  exact algebraMap_apply F K L x

Scalar Tower Property of Normal Closure

Informal description

For field extensions $K/F$ and $L/F$, the normal closure of $K$ in $L$ forms a scalar tower with $F$ and $K$. That is, the scalar multiplication operations satisfy the compatibility condition $(f \cdot k) \cdot s = f \cdot (k \cdot s)$ for all $f \in F$, $k \in K$, and $s$ in the normal closure of $K$ in $L$.

normalClosure.instIsScalarTowerSubtypeMemIntermediateFieldNormalClosure_1 instance

: IsScalarTower K (normalClosure F K L) L

Full source

instance : IsScalarTower K (normalClosure F K L) L :=
  of_algebraMap_eq' rfl

Scalar Tower Property of Normal Closure with $ K $ and $ L $

Informal description

For field extensions $ K/F $ and $ L/F $, the normal closure of $ K $ in $ L $ forms a scalar tower with $ K $ and $ L $. That is, the scalar multiplication operations satisfy the compatibility condition $ (k \cdot s) \cdot l = k \cdot (s \cdot l) $ for all $ k \in K $, $ s $ in the normal closure of $ K $ in $ L $, and $ l \in L $.

normalClosure.restrictScalars_eq theorem

: (toAlgHom K (normalClosure F K L) L).fieldRange.restrictScalars F = normalClosure F K L

Full source

lemma restrictScalars_eq :
    (toAlgHom K (normalClosure F K L) L).fieldRange.restrictScalars F = normalClosure F K L :=
  SetLike.ext' Subtype.range_val

Restriction of Scalars Preserves Normal Closure

Informal description

Let $K/F$ and $L/F$ be field extensions. The restriction of scalars of the range of the canonical $K$-algebra homomorphism from the normal closure of $K$ in $L$ to $L$ (viewed as an $F$-algebra) is equal to the normal closure itself. In other words, if we consider the image of the normal closure under the inclusion map to $L$ and then restrict scalars from $K$ back to $F$, we recover the original normal closure.

Algebra.IsAlgebraic.algHomEmbeddingOfSplits definition

 [Algebra.IsAlgebraic F K] (h : ∀ x : K, (minpoly F x).Splits (algebraMap F L)) (L' : Type*) [Field L'] [Algebra F L'] :
  (K →ₐ[F] L') ↪ (K →ₐ[F] L)

Full source

/-- An extension `L/F` in which every minimal polynomial of `K/F` splits is maximal with respect
  to `F`-embeddings of `K`, in the sense that `K →ₐ[F] L` achieves maximal cardinality.
  We construct an explicit injective function from an arbitrary `K →ₐ[F] L'` into `K →ₐ[F] L`,
  using an embedding of `normalClosure F K L'` into `L`. -/
noncomputable def Algebra.IsAlgebraic.algHomEmbeddingOfSplits [Algebra.IsAlgebraic F K]
    (h : ∀ x : K, (minpoly F x).Splits (algebraMap F L)) (L' : Type*) [Field L'] [Algebra F L'] :
    (K →ₐ[F] L') ↪ (K →ₐ[F] L) :=
  let φ : ↑(⨆ x : K, IntermediateField.adjoin F ((minpoly F x).rootSet L')) →ₐ[F] L :=
    Nonempty.some <| by
      rw [← gc.l_iSup]
      refine nonempty_algHom_adjoin_of_splits fun x hx ↦ ?_
      obtain ⟨y, hx⟩ := Set.mem_iUnion.mp hx
      refine ⟨isAlgebraic_iff_isIntegral.mp (isAlgebraic_of_mem_rootSet hx), ?_⟩
      by_cases iy : IsIntegral F y
      · exact splits_of_splits_of_dvd _ (minpoly.ne_zero iy)
          (h y) (minpoly.dvd F x (mem_rootSet.mp hx).2)
      · simp [minpoly.eq_zero iy] at hx
  let φ' := (φ.comp <| inclusion normalClosure_le_iSup_adjoin)
  { toFun := φ'.comp ∘ (normalClosure.algHomEquiv F K L').symm
    inj' := fun _ _ h ↦ (normalClosure.algHomEquiv F K L').symm.injective <| by
      rw [DFunLike.ext'_iff] at h ⊢
      exact φ'.injective.comp_left h }

Injective embedding of algebra homomorphisms for algebraic extensions with splitting condition

Informal description

Given an algebraic field extension $K/F$ where every minimal polynomial of elements in $K$ splits in $L/F$, and another field extension $L'/F$, there exists an injective function embedding from the set of $F$-algebra homomorphisms from $K$ to $L'$ into the set of $F$-algebra homomorphisms from $K$ to $L$. This embedding is constructed by composing with the canonical map from the normal closure of $K$ in $L'$ to $L$. More precisely, for any $x \in K$, if the minimal polynomial $\text{minpoly}_F(x)$ splits in $L$, then there is an injective map $(K →_{\text{Alg}[F]} L') \hookrightarrow (K →_{\text{Alg}[F]} L)$.

IntermediateField.le_normalClosure theorem

: K ≤ normalClosure F K L

Full source

lemma le_normalClosure : K ≤ normalClosure F K L :=
  K.fieldRange_val.symm.trans_le K.val.fieldRange_le_normalClosure

Inclusion of Field in its Normal Closure

Informal description

For any field extensions $ K/F $ and $ L/F $, the field $ K $ is contained in its normal closure within $ L $, i.e., $ K \subseteq \text{normalClosure}_F(K, L) $.

IntermediateField.normalClosure_of_normal theorem

[Normal F K] : normalClosure F K L = K

Full source

lemma normalClosure_of_normal [Normal F K] : normalClosure F K L = K := by
  simp only [normalClosure_def, AlgHom.fieldRange_of_normal, iSup_const]

Normal Closure of Normal Extension is Itself

Informal description

If $K/F$ is a normal field extension, then the normal closure of $K$ over $F$ in any field extension $L/F$ is equal to $K$ itself, i.e., $\text{normalClosure}_F(K, L) = K$.

IntermediateField.normalClosure_def' theorem

: normalClosure F K L = ⨆ f : L →ₐ[F] L, K.map f

Full source

lemma normalClosure_def' : normalClosure F K L = ⨆ f : L →ₐ[F] L, K.map f := by
  refine (normalClosure_def F K L).trans (le_antisymm (iSup_le (fun f ↦ ?_)) (iSup_le (fun f ↦ ?_)))
  · exact le_iSup_of_le (f.liftNormal L) (fun b ⟨a, h⟩ ↦ ⟨a, a.2, h ▸ f.liftNormal_commutes L a⟩)
  · exact le_iSup_of_le (f.comp K.val) (fun b ⟨a, h⟩ ↦ ⟨⟨a, h.1⟩, h.2⟩)

Normal Closure as Supremum of Endomorphism Images

Informal description

Let $F$, $K$, and $L$ be fields with $K/F$ and $L/F$ field extensions. The normal closure of $K$ over $F$ in $L$ is equal to the supremum (join) of the images of $K$ under all $F$-algebra endomorphisms of $L$. In other words, \[ \text{normalClosure}(F, K, L) = \bigsqcup_{f \in \text{End}_{F\text{-alg}}(L)} f(K). \]

IntermediateField.normalClosure_def'' theorem

: normalClosure F K L = ⨆ f : L ≃ₐ[F] L, K.map f

Full source

lemma normalClosure_def'' : normalClosure F K L = ⨆ f : L ≃ₐ[F] L, K.map f := by
  refine (normalClosure_def' K).trans (le_antisymm (iSup_le (fun f ↦ ?_)) (iSup_le (fun f ↦ ?_)))
  · exact le_iSup_of_le (f.restrictNormal' L)
      (fun b ⟨a, h⟩ ↦ ⟨a, h.1, h.2 ▸ f.restrictNormal_commutes L a⟩)
  · exact le_iSup_of_le f le_rfl

Normal Closure as Supremum of Automorphism Images

Informal description

The normal closure of a field extension $K/F$ inside another field extension $L/F$ is equal to the supremum (join) of the images of $K$ under all $F$-algebra automorphisms of $L$. In other words, \[ \text{normalClosure}(F, K, L) = \bigsqcup_{\sigma \in \text{Aut}_{F}(L)} \sigma(K). \]

IntermediateField.normalClosure_mono theorem

(h : K ≤ K') : normalClosure F K L ≤ normalClosure F K' L

Full source

lemma normalClosure_mono (h : K ≤ K') : normalClosure F K L ≤ normalClosure F K' L := by
  rw [normalClosure_def', normalClosure_def']
  exact iSup_mono (fun f ↦ map_mono f h)

Monotonicity of Normal Closure with Respect to Field Inclusion

Informal description

For field extensions $ K/F $ and $ K'/F $ inside a field extension $ L/F $, if $ K $ is a subfield of $ K' $ (i.e., $ K \leq K' $), then the normal closure of $ K $ over $ F $ in $ L $ is contained in the normal closure of $ K' $ over $ F $ in $ L $. In other words, $ \text{normalClosure}(F, K, L) \leq \text{normalClosure}(F, K', L) $.

IntermediateField.closureOperator definition

: ClosureOperator (IntermediateField F L)

Full source

/-- `normalClosure` as a `ClosureOperator`. -/
@[simps]
noncomputable def closureOperator : ClosureOperator (IntermediateField F L) where
  toFun := fun K ↦ normalClosure F K L
  monotone' := fun K K' ↦ normalClosure_mono K K'
  le_closure' := le_normalClosure
  idempotent' := fun K ↦ normalClosure_of_normal (normalClosure F K L)

Closure operator for normal closures of intermediate fields

Informal description

The closure operator on the complete lattice of intermediate fields between $F$ and $L$ maps each intermediate field $K$ to its normal closure $\text{normalClosure}_F(K, L)$. This operator is: 1. Monotone: if $K \subseteq K'$ then $\text{normalClosure}_F(K, L) \subseteq \text{normalClosure}_F(K', L)$ 2. Extensive: $K \subseteq \text{normalClosure}_F(K, L)$ for all $K$ 3. Idempotent: $\text{normalClosure}_F(\text{normalClosure}_F(K, L), L) = \text{normalClosure}_F(K, L)$ for all $K$

IntermediateField.normal_iff_normalClosure_eq theorem

: Normal F K ↔ normalClosure F K L = K

Full source

lemma normal_iff_normalClosure_eq : NormalNormal F K ↔ normalClosure F K L = K :=
⟨@normalClosure_of_normal (K := K), fun h ↦ h ▸ normalClosure.normal F K L⟩

Normality Criterion via Normal Closure Equality

Informal description

A field extension $ K/F $ is normal if and only if the normal closure of $ K $ over $ F $ in any field extension $ L/F $ is equal to $ K $ itself, i.e., $ \text{normalClosure}_F(K, L) = K $.

IntermediateField.normal_iff_normalClosure_le theorem

: Normal F K ↔ normalClosure F K L ≤ K

Full source

lemma normal_iff_normalClosure_le : NormalNormal F K ↔ normalClosure F K L ≤ K :=
normal_iff_normalClosure_eq.trans (le_normalClosure K).le_iff_eq.symm

Normality Criterion via Normal Closure Containment

Informal description

A field extension $K/F$ is normal if and only if the normal closure of $K$ over $F$ in any field extension $L/F$ is contained in $K$, i.e., $\text{normalClosure}_F(K, L) \leq K$.

IntermediateField.normal_iff_forall_fieldRange_le theorem

: Normal F K ↔ ∀ σ : K →ₐ[F] L, σ.fieldRange ≤ K

Full source

lemma normal_iff_forall_fieldRange_le : NormalNormal F K ↔ ∀ σ : K →ₐ[F] L, σ.fieldRange ≤ K := by
  rw [normal_iff_normalClosure_le, normalClosure_def, iSup_le_iff]

Normality Criterion via Homomorphism Ranges: $K/F$ normal $\leftrightarrow$ all $F$-algebra homomorphisms $K \to L$ have range in $K$

Informal description

A field extension $K/F$ is normal if and only if for every $F$-algebra homomorphism $\sigma \colon K \to L$, the range of $\sigma$ is contained in $K$ (as an intermediate field between $F$ and $L$).

IntermediateField.normal_iff_forall_map_le theorem

: Normal F K ↔ ∀ σ : L →ₐ[F] L, K.map σ ≤ K

Full source

lemma normal_iff_forall_map_le : NormalNormal F K ↔ ∀ σ : L →ₐ[F] L, K.map σ ≤ K := by
  rw [normal_iff_normalClosure_le, normalClosure_def', iSup_le_iff]

Normality Criterion via Endomorphism Invariance: $K/F$ normal $\leftrightarrow$ $\sigma(K) \subseteq K$ for all $F$-algebra endomorphisms $\sigma$ of $L$

Informal description

A field extension $K/F$ is normal if and only if for every $F$-algebra homomorphism $\sigma : L \to L$, the image of $K$ under $\sigma$ is contained in $K$, i.e., $\sigma(K) \subseteq K$.

IntermediateField.normal_iff_forall_map_le' theorem

: Normal F K ↔ ∀ σ : L ≃ₐ[F] L, K.map ↑σ ≤ K

Full source

lemma normal_iff_forall_map_le' : NormalNormal F K ↔ ∀ σ : L ≃ₐ[F] L, K.map ↑σ ≤ K := by
  rw [normal_iff_normalClosure_le, normalClosure_def'', iSup_le_iff]

Normality Criterion via Automorphism Invariance: $K/F$ normal $\leftrightarrow$ $\sigma(K) \subseteq K$ for all $\sigma \in \text{Aut}_F(L)$

Informal description

A field extension $K/F$ is normal if and only if for every $F$-algebra automorphism $\sigma$ of $L$, the image of $K$ under $\sigma$ is contained in $K$.

IntermediateField.normal_iff_forall_fieldRange_eq theorem

: Normal F K ↔ ∀ σ : K →ₐ[F] L, σ.fieldRange = K

Full source

/-- If `L/K/F` is a field tower where `L/F` is normal, then
`K` is normal over `F` if and only if `σ(K) = K` for every `σ ∈ K →ₐ[F] L`. -/
@[stacks 09HQ "stronger version replacing an algebraic closure by a normal extension"]
lemma normal_iff_forall_fieldRange_eq : NormalNormal F K ↔ ∀ σ : K →ₐ[F] L, σ.fieldRange = K :=
⟨@AlgHom.fieldRange_of_normal (E := K), normal_iff_forall_fieldRange_le.2 ∘ fun h σ ↦ (h σ).le⟩

Normality Criterion via Homomorphism Range Equality: $K/F$ normal $\leftrightarrow$ all $F$-algebra homomorphisms $K \to L$ have range equal to $K$

Informal description

Let $F$ be a field and $K$ an algebraic extension of $F$. Then $K$ is normal over $F$ if and only if for every $F$-algebra homomorphism $\sigma \colon K \to L$, the range of $\sigma$ equals $K$ (when viewed as an intermediate field between $F$ and $L$).

IntermediateField.normal_iff_forall_map_eq theorem

: Normal F K ↔ ∀ σ : L →ₐ[F] L, K.map σ = K

Full source

lemma normal_iff_forall_map_eq : NormalNormal F K ↔ ∀ σ : L →ₐ[F] L, K.map σ = K :=
⟨fun h σ ↦ (K.fieldRange_val ▸ AlgHom.map_fieldRange K.val σ).trans
  (normal_iff_forall_fieldRange_eq.1 h _), fun h ↦ normal_iff_forall_map_le.2 (fun σ ↦ (h σ).le)⟩

Normality Criterion via Endomorphism Invariance: $K/F$ normal $\leftrightarrow$ $\sigma(K) = K$ for all $F$-algebra endomorphisms $\sigma$ of $L$

Informal description

A field extension $K/F$ is normal if and only if for every $F$-algebra homomorphism $\sigma \colon L \to L$, the image of $K$ under $\sigma$ equals $K$ itself, i.e., $\sigma(K) = K$.

IntermediateField.normal_iff_forall_map_eq' theorem

: Normal F K ↔ ∀ σ : L ≃ₐ[F] L, K.map ↑σ = K

Full source

lemma normal_iff_forall_map_eq' : NormalNormal F K ↔ ∀ σ : L ≃ₐ[F] L, K.map ↑σ = K :=
⟨fun h σ ↦ normal_iff_forall_map_eq.1 h σ, fun h ↦ normal_iff_forall_map_le'.2 (fun σ ↦ (h σ).le)⟩

Normality Criterion via Automorphism Invariance: $K/F$ normal $\leftrightarrow$ $\sigma(K) = K$ for all $\sigma \in \text{Aut}_F(L)$

Informal description

A field extension $K/F$ is normal if and only if for every $F$-algebra automorphism $\sigma$ of $L$, the image of $K$ under $\sigma$ equals $K$, i.e., $\sigma(K) = K$.

IntermediateField.normalClosure_map_eq theorem

(K : IntermediateField F L) (σ : L →ₐ[F] L) : normalClosure F (K.map σ) L = normalClosure F K L

Full source

@[simp]
lemma normalClosure_map_eq (K : IntermediateField F L) (σ : L →ₐ[F] L) :
    normalClosure F (K.map σ) L = normalClosure F K L := by
  have (σ : L ≃ₐ[F] L) : normalClosure F (K.map (σ : L →ₐ[F] L)) L = normalClosure F K L := by
    simp_rw [normalClosure_def'', map_map]
    exact (Equiv.mulRight σ).iSup_congr fun _ ↦ rfl
  exact this ((Algebra.IsAlgebraic.algEquivEquivAlgHom _ _).symm σ)

Invariance of Normal Closure under Algebra Homomorphisms

Informal description

Let $F$ be a field and $L/F$ a field extension. For any intermediate field $K$ between $F$ and $L$ and any $F$-algebra homomorphism $\sigma : L \to L$, the normal closure of $\sigma(K)$ over $F$ in $L$ equals the normal closure of $K$ over $F$ in $L$. In other words, \[ \text{normalClosure}_F(\sigma(K), L) = \text{normalClosure}_F(K, L). \]

IntermediateField.normalClosure_le_iff_of_normal theorem

{K₁ K₂ : IntermediateField F L} [Normal F K₂] : normalClosure F K₁ L ≤ K₂ ↔ K₁ ≤ K₂

Full source

@[simp]
theorem normalClosure_le_iff_of_normal {K₁ K₂ : IntermediateField F L} [Normal F K₂] :
    normalClosurenormalClosure F K₁ L ≤ K₂ ↔ K₁ ≤ K₂ := by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · rw [normalClosure_le_iff] at h
    simpa only [fieldRange_val] using h K₁.val
  · rw [← normalClosure_of_normal K₂]
    exact normalClosure_mono K₁ K₂ h

Containment of Normal Closure in Normal Extension $\leftrightarrow$ Original Field Containment

Informal description

Let $F$ be a field and $L/F$ a field extension. For any intermediate fields $K₁$ and $K₂$ between $F$ and $L$, if $K₂/F$ is normal, then the normal closure of $K₁$ over $F$ in $L$ is contained in $K₂$ if and only if $K₁$ is contained in $K₂$. In other words, $\text{normalClosure}_F(K₁, L) \leq K₂ \leftrightarrow K₁ \leq K₂$.

Main definitions