IntermediateField.exists_algHom_of_splits_of_aeval
theorem IntermediateField.exists_algHom_of_splits_of_aeval :
∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
[inst_3 : Algebra F E] [inst_4 : Algebra F K],
(∀ (s : E), IsIntegral F s ∧ Polynomial.Splits (algebraMap F K) (minpoly F s)) →
∀ {x : E} {y : K}, (Polynomial.aeval y) (minpoly F x) = 0 → ∃ φ, φ x = y
This theorem states that for any three fields `F`, `E`, and `K`, where `F` is a field of scalars for both `E` (via an algebra structure) and `K` (via another algebra structure), if every element `s` in `E` is integral over `F`, and its minimal polynomial over `F` splits into linear factors over `K` under the mapping induced by the `F` to `K` algebra structure, then for any element `x` in `E` and any element `y` in `K` such that `y` is a root of the minimal polynomial of `x` over `F`, there exists an algebra homomorphism `φ` from `E` to `K` mapping `x` to `y`. Essentially, this theorem provides a condition under which we can construct an algebra homomorphism between two fields that sends a specific element in the source field to a specific element in the target field.
More concisely: Given fields `F`, `E`, and `K` with `F` being a common subfield of `E` and `K` as scalars, if every element in `E` is integral over `F` with a minimal polynomial splitting linearly over `K`, then there exists an algebra homomorphism from `E` to `K` mapping any element in `E` to a root of its minimal polynomial in `K`.
|
IntermediateField.Lifts.exists_lift_of_splits'
theorem IntermediateField.Lifts.exists_lift_of_splits' :
∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
[inst_3 : Algebra F E] [inst_4 : Algebra F K] (x : IntermediateField.Lifts F E K) {s : E},
IsIntegral (↥x.carrier) s →
Polynomial.Splits x.emb.toRingHom (minpoly (↥x.carrier) s) → ∃ y, x ≤ y ∧ s ∈ y.carrier
The theorem `IntermediateField.Lifts.exists_lift_of_splits'` states that for any field homomorphism `x` from an intermediate field `E` (between fields `F` and `K`), and any element `s` of `E` that is integral over the carrier of `x` - if all roots of the minimal polynomial of `s` over the carrier of `x` are in `K` (i.e., the minimal polynomial splits over `K`), then there exists a field homomorphism `y` that extends `x` and whose carrier contains `s`. In simpler terms, if an element `s` and all its conjugates can be mapped from an intermediate field `E` to a field `K`, then we can always find a field homomorphism that includes `s`.
More concisely: If `x` is a field homomorphism from an intermediate field `E` to `K`, and `s` is an element of `E` integral over the carrier of `x` with all conjugates in `K`, then there exists a field homomorphism `y` extending `x` containing `s` in its carrier.
|
IntermediateField.Lifts.exists_lift_of_splits
theorem IntermediateField.Lifts.exists_lift_of_splits :
∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
[inst_3 : Algebra F E] [inst_4 : Algebra F K] (x : IntermediateField.Lifts F E K) {s : E},
IsIntegral F s → Polynomial.Splits (algebraMap F K) (minpoly F s) → ∃ y, x ≤ y ∧ s ∈ y.carrier
This theorem states that for any field `F`, `E`, and `K` with `F` being an algebra over `E` and `K`, if you have a function `x` that lifts `F` to `E` and `K`, and an element `s` in `E` that is integral over `F`, then if the minimal polynomial of `s` over `F` splits when mapped from `F` to `K` (meaning it is either zero or all of its irreducible factors have degree 1), there exists a lift `y` such that `x` is less than or equal to `y` and `s` is included in the carrier of `y`. In other words, any lifting of `F` to `E` and `K` can be extended to one that includes `s` if `s` is integral over `F` and its minimal polynomial splits over `K`.
More concisely: If `F` is a field algebraically extended by `E` and `K`, `x` is a lifting of `F` to `E` and `K`, `s` is an element of `E` integral over `F`, and the minimal polynomial of `s` over `F` splits in `K`, then there exists a lifting `y` of `F` to `E` and `K` such that `x <= y` and `s` is in the carrier of `y`.
|
IntermediateField.Lifts.exists_upper_bound
theorem IntermediateField.Lifts.exists_upper_bound :
∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
[inst_3 : Algebra F E] [inst_4 : Algebra F K] (c : Set (IntermediateField.Lifts F E K)),
IsChain (fun x x_1 => x ≤ x_1) c → ∃ ub, ∀ a ∈ c, a ≤ ub
The theorem `IntermediateField.Lifts.exists_upper_bound` states that for any set of lifts `c` in an intermediate field, if the set `c` forms a chain (i.e., for every pair of elements `x` and `y` in the set `c`, either `x` is less than or equal to `y`, or `y` is less than or equal to `x`), then there exists an upper bound `ub` for the set `c`. This upper bound `ub` is an element such that every element `a` in the set `c` is less than or equal to `ub`. The fields `F`, `E`, and `K` are algebraic structures with addition, multiplication, and scalar multiplication operations. The types `F`, `E`, and `K` represent respectively the base field, the extension field, and the field of scalars in the algebraic structures.
More concisely: If `c` is a chain in an intermediate field between `F` and `K`, then there exists an upper bound `ub` in `K` such that every element in `c` is less than or equal to `ub`.
|
Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly_of_splits
theorem Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly_of_splits :
∀ {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 L] [inst_4 : Algebra F K],
(∀ (x : K), Polynomial.Splits (algebraMap F L) (minpoly F x)) →
Algebra.IsAlgebraic F K → ∀ (x : K), (Set.range fun ψ => ψ x) = (minpoly F x).rootSet L
This theorem states that, given an algebraic extension of fields `K/F` and a field `L` where all the minimal polynomials over `F` of elements from `K` split, for any `x` in `K`, the images of `x` under the `F`-algebra morphisms mapping `K` to `L` are precisely the roots in `L` of the minimal polynomial of `x` over `F`. In simpler terms, it tells us that in certain conditions, the values we get by applying the algebra morphisms from `K` to `L` to an element `x` will be the roots of `x`'s minimal polynomial in `L`.
More concisely: Given an algebraic extension `K/F` and a field `L` where all minimal polynomials of elements from `K` split, for any `x` in `K`, the images of `x` under `F`-algebra morphisms from `K` to `L` are exactly the roots of `x`'s minimal polynomial in `L`.
|