AlgHom.normal_bijective
theorem AlgHom.normal_bijective :
∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K] (E : Type u_3)
[inst_3 : Field E] [inst_4 : Algebra F E] [inst_5 : Algebra K E] [inst_6 : IsScalarTower F K E] [h : Normal F E]
(ϕ : E →ₐ[F] K), Function.Bijective ⇑ϕ
The given theorem, `AlgHom.normal_bijective`, states that for any fields `F`, `K`, and `E` with `F` and `K` being subfields of `E` (as indicated by the algebra and scalar tower structures), and given that `E` is a normal extension of `F`, every algebra homomorphism `ϕ` from `E` to `K` that respects `F` (denoted `E →ₐ[F] K`), is a bijective function. Here, a function is called bijective if it is both injective (meaning every element of its domain maps to a unique element of its codomain) and surjective (meaning every element of its codomain is the image of some element of its domain).
More concisely: If `F` and `K` are subfields of a normal extension field `E`, and `ϕ: E → K` is an algebra homomorphism respecting `F`, then `ϕ` is a bijective function.
|
Normal.of_algEquiv
theorem Normal.of_algEquiv :
∀ {F : Type u_1} {E : Type u_3} {E' : Type u_4} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
[inst_3 : Field E'] [inst_4 : Algebra F E'] [h : Normal F E], (E ≃ₐ[F] E') → Normal F E'
The theorem `Normal.of_algEquiv` states that for any three types `F`, `E`, and `E'`, where `F` is a field, `E` and `E'` are fields that are also algebras over `F`, if `E` is a normal extension of `F`, then if `E` is algebraically equivalent to `E'` (denoted as `E ≃ₐ[F] E'`), `E'` is also a normal extension of `F`. Essentially, it says that the property of being a normal extension is preserved under algebraic equivalence.
More concisely: If `F` is a field, `E` and `E'` are fields and algebras over `F`, `E` is a normal extension of `F`, and `E ≃ₐ[F] E'`, then `E'` is a normal extension of `F`.
|
Normal.splits
theorem Normal.splits :
∀ {F : Type u_1} {K : Type u_2} [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K],
Normal F K → ∀ (x : K), Polynomial.Splits (algebraMap F K) (minpoly F x)
The theorem `Normal.splits` asserts that for any fields `F` and `K` with an algebra structure between them, if `K` is a normal extension of `F`, then for any element `x` of `K`, the minimal polynomial of `x` over `F` splits over `K`. This implies that either the minimal polynomial is zero or all of its irreducible factors have degree 1 when considered as a polynomial over `K`. The algebra structure provides an embedding of `F` in `K`, and the "splits" property is defined with respect to this embedding.
More concisely: If `F` is a subfield of `K` with an algebra structure, and `K` is a normal extension of `F`, then every irreducible factor of the minimal polynomial of any element `x` in `K` over `F` has degree 1.
|
IntermediateField.splits_of_mem_adjoin
theorem IntermediateField.splits_of_mem_adjoin :
∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K] {L : Type u_3}
[inst_3 : Field L] [inst_4 : Algebra F L] {S : Set K},
(∀ x ∈ S, IsIntegral F x ∧ Polynomial.Splits (algebraMap F L) (minpoly F x)) →
∀ {x : K}, x ∈ IntermediateField.adjoin F S → Polynomial.Splits (algebraMap F L) (minpoly F x)
The theorem states that if we have a set of algebraic elements in a field extension `K/F`, and the minimal polynomials of each element in the set split in another extension `L/F`, then all minimal polynomials in the intermediate field generated by the set will also split in `L/F`. In other words, if each algebraic element in the set has a minimal polynomial that factors completely into linear factors in `L/F`, then any algebraic element in the field generated by the set will also have a minimal polynomial that factors completely into linear factors in `L/F`.
More concisely: If a set of algebraic elements in a field extension has minimal polynomials that factor completely into linear factors in another extension, then all minimal polynomials in the intermediate field generated by the set also factor completely into linear factors in that extension.
|
AlgHom.restrictNormal_commutes
theorem AlgHom.restrictNormal_commutes :
∀ {F : Type u_1} {K₁ : Type u_3} {K₂ : Type u_4} [inst : Field F] [inst_1 : Field K₁] [inst_2 : Field K₂]
[inst_3 : Algebra F K₁] [inst_4 : Algebra F K₂] (ϕ : K₁ →ₐ[F] K₂) (E : Type u_6) [inst_5 : Field E]
[inst_6 : Algebra F E] [inst_7 : Algebra E K₁] [inst_8 : Algebra E K₂] [inst_9 : IsScalarTower F E K₁]
[inst_10 : IsScalarTower F E K₂] [inst_11 : Normal F E] (x : E),
(algebraMap E K₂) ((ϕ.restrictNormal E) x) = ϕ ((algebraMap E K₁) x)
This theorem states that for any fields `F`, `K₁`, `K₂`, and `E`, given that `F` is a base field and `K₁` and `K₂` are extension fields of `F`, with `E` being an intermediate field between `F` and `K₁`, then for any algebra homomorphism `ϕ` from `K₁` to `K₂` over `F`, and any element `x` from `E`, applying the algebra map from `E` to `K₂` to the result of restricting the homomorphism `ϕ` to `E` and applying it to `x`, is the same as applying `ϕ` directly to the result of applying the algebra map from `E` to `K₁` to `x`. In mathematical terms, it states that `(algebraMap E K₂) ((AlgHom.restrictNormal ϕ E) x) = ϕ ((algebraMap E K₁) x)`. This states a kind of 'commutativity' property of the restrictions of the algebra homomorphisms and the algebra maps.
More concisely: For any algebra homomorphisms ϕ : K₁ -> K₂ over a base field F, and any intermediate field E between K₁ and K₂, the restriction of ϕ to E commutes with the algebra maps, i.e., algebraMap E K₂ (restrictNormal ϕ E x) = ϕ (algebraMap E K₁ x) for all x in E.
|
normal_iff
theorem normal_iff :
∀ {F : Type u_1} {K : Type u_2} [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K],
Normal F K ↔ ∀ (x : K), IsIntegral F x ∧ Polynomial.Splits (algebraMap F K) (minpoly F x)
This theorem, `normal_iff`, defines the equivalence for a field extension `F` to `K` to be normal. According to this theorem, a field extension is normal if and only if for every element `x` in `K`, two conditions are satisfied: `x` is integral over `F` and the minimal polynomial of `x` over `F`, `minpoly F x`, splits into linear factors under the mapping from `F` to `K` given by the algebra structure. An element `x` is said to be integral over `F` if it is a root of some monic polynomial with coefficients in `F`. A polynomial splits if it is zero or all of its irreducible factors are of degree 1.
More concisely: A field extension is normal if and only if every element in the larger field is integral and the minimal polynomial over the smaller field splits into linear factors.
|