IntermediateField.normal_iff_normalClosure_le
theorem IntermediateField.normal_iff_normalClosure_le :
∀ {F : Type u_1} {L : Type u_3} [inst : Field F] [inst_1 : Field L] [inst_2 : Algebra F L] [inst_3 : Normal F L]
{K : IntermediateField F L}, Normal F ↥K ↔ normalClosure F (↥K) L ≤ K
This theorem states that for any Field F, Field L, and an Intermediate Field K between F and L, with F and L being algebraically related and L being a Normal field extension of F, the Intermediate Field K is a Normal field extension of F if and only if the normal closure of K in L is a subfield (or equal to) K. The normal closure here refers to the smallest normal extension of F in L that contains K. In other words, K is normal over F if and only if all elements of K that are algebraic over F are also elements of K.
More concisely: A field K between fields F and L, with F and L algebraically related and L a normal extension of F, is a normal extension of F if and only if the normal closure of K in L is contained in K.
|
Algebra.IsAlgebraic.isNormalClosure_normalClosure
theorem Algebra.IsAlgebraic.isNormalClosure_normalClosure :
∀ {F : Type u_1} {K : Type u_2} {L : Type u_3} [inst : Field F] [inst_1 : Field K] [inst_2 : Field L]
[inst_3 : Algebra F K] [inst_4 : Algebra F L],
Algebra.IsAlgebraic F K →
(∀ (x : K), Polynomial.Splits (algebraMap F L) (minpoly F x)) → IsNormalClosure F K ↥(normalClosure F K L)
The theorem `Algebra.IsAlgebraic.isNormalClosure_normalClosure` states that for any types `F`, `K`, `L` (representing fields), with algebraic structure over `F` for `K` and `L`, the `normalClosure` of `K/F` in `L/F` is a valid normal closure if `K/F` is an algebraic extension and all minimal polynomials of elements of `K` over `F` split in `L/F`. Here, a polynomial "splits" if it is zero or all of its irreducible factors have degree 1. The `normalClosure` of `K/F` in `L/F` is an intermediate field that contains all elements of `L` that are algebraic over `F`.
More concisely: If `K/F` is an algebraic extension of fields and all minimal polynomials of elements in `K` over `F` split and have degree 1 in `L/F`, then the normal closure of `K/F` in `L/F` is equal to the subfield of `L` consisting of all elements algebraic over `F`.
|
Algebra.IsAlgebraic.isNormalClosure_iff
theorem Algebra.IsAlgebraic.isNormalClosure_iff :
∀ {F : Type u_1} {K : Type u_2} {L : Type u_3} [inst : Field F] [inst_1 : Field K] [inst_2 : Field L]
[inst_3 : Algebra F K] [inst_4 : Algebra F L],
Algebra.IsAlgebraic F K →
(IsNormalClosure F K L ↔
(∀ (x : K), Polynomial.Splits (algebraMap F L) (minpoly F x)) ∧ normalClosure F K L = ⊤)
This theorem states that if the extension `K/F` in the field `F` is algebraic, the condition "generated by roots" in the definition of a normal closure can be replaced by "generated by images of embeddings". More specifically, it states that the algebra `K` over the field `F` being algebraic is equivalent to every element `x` in `K` having its minimal polynomial over `F` split into linear factors under the algebra map from `F` to `L` and the normal closure of `K` over `F` in `L` being the whole field `L`.
More concisely: If field extension `K/F` is algebraic, then the normal closure of `K` in `L` is generated by the images of embeddings of `K` into `L`.
|
AlgHom.fieldRange_le_normalClosure
theorem AlgHom.fieldRange_le_normalClosure :
∀ {F : Type u_1} {K : Type u_2} {L : Type u_3} [inst : Field F] [inst_1 : Field K] [inst_2 : Field L]
[inst_3 : Algebra F K] [inst_4 : Algebra F L] (f : K →ₐ[F] L), f.fieldRange ≤ normalClosure F K L
The theorem `AlgHom.fieldRange_le_normalClosure` states that for any fields `F`, `K`, and `L` with `K` and `L` being algebraic extensions of `F`, and for any algebra homomorphism `f` from `K` to `L`, the range of `f` is contained within the normal closure of `K/F` in `L/F`. In other words, the set of all values that `f` can take in `L` (the field range of `f`) is a subset of the "largest" intermediate field that is normal and contains `K` (the normal closure of `K` over `F` in `L`).
More concisely: For any field homomorphism f from a field K to a field L, where K and L are algebraic extensions of a base field F, the range of f is contained in the normal closure of K in L.
|
IsNormalClosure.normal
theorem IsNormalClosure.normal :
∀ {F : Type u_1} {K : Type u_2} {L : Type u_3} [inst : Field F] [inst_1 : Field K] [inst_2 : Field L]
[inst_3 : Algebra F K] [inst_4 : Algebra F L] [h : IsNormalClosure F K L], Normal F L
This theorem states that for any three types `F`, `K`, and `L` that are fields, if `K` is a normal closure of `F` in `L` (represented by `IsNormalClosure F K L`), then `L` is a normal extension of `F` (represented by `Normal F L`). Here, a "normal extension" means that every irreducible polynomial in `F[X]` that has a root in `L`, splits into linear factors in `L[X]`.
More concisely: If `F` is a subfield of `K` that is a normal closure of `F` in `L`, then `L` is a normal extension of `F`. In other words, if every irreducible polynomial in `F[X]` that has a root in `L` splits into linear factors in `L[X]`, then `L` is a normal extension of `F`.
|