IntermediateField.eq_bot_of_isSepClosed_of_isSeparable
theorem IntermediateField.eq_bot_of_isSepClosed_of_isSeparable :
∀ {k : Type u} [inst : Field k] {K : Type v} [inst_1 : Field K] [inst_2 : IsSepClosed k] [inst_3 : Algebra k K]
(L : IntermediateField k K) [inst_4 : IsSeparable k ↥L], L = ⊥
This theorem states that if `k` is a separably closed field, `K / k` is a field extension, and `L / k` is an intermediate field that is separable, then `L` is equal to `k`. This is a corollary of the theorem `IsSepClosed.algebraMap_surjective`.
In mathematical terms, for separably closed field `k` and any field `K` such that `K / k` is a field extension, if there exists an intermediate field `L` that is separable over `k`, then this intermediate field `L` must be equivalent to the field `k`.
More concisely: If `k` is a separably closed field, and `L` is a separable intermediate field of the field extension `K/k`, then `L = k`.
|
IsSepClosed.splits_codomain
theorem IsSepClosed.splits_codomain :
∀ {k : Type u} [inst : Field k] {K : Type v} [inst_1 : Field K] [inst_2 : IsSepClosed K] {f : k →+* K}
(p : Polynomial k), p.Separable → Polynomial.Splits f p
The theorem `IsSepClosed.splits_codomain` states that for any field `k` and `K` where `K` is separably closed, and for any ring homomorphism `f` from `k` to `K`, every separable polynomial `p` over `k` satisfies the property that it splits through `f` to `K`. Here, a polynomial `p` is said to "split" if it is either zero or all of its irreducible factors have degree 1 after mapping from `k` to `K` via `f`. The theorem also mentions a related theorem `IsSepClosed.splits_domain` for the case where the field `k` itself is separably closed.
More concisely: For any separable polynomial over a field `k` and a ring homomorphism from `k` to a separably closed field `K`, the polynomial splits in `K` via the homomorphism.
|
IsSepClosed.exists_root
theorem IsSepClosed.exists_root :
∀ {k : Type u} [inst : Field k] [inst_1 : IsSepClosed k] (p : Polynomial k),
p.degree ≠ 0 → p.Separable → ∃ x, p.IsRoot x
The theorem `IsSepClosed.exists_root` states that for all fields `k` which also have the property of being separably closed (as per the `IsSepClosed` typeclass instance), for any polynomial `p` over `k`, if the degree of `p` is not zero and the polynomial is separable (i.e., it is coprime with its derivative), then there exists an element `x` in `k` that is a root of the polynomial `p`. In other words, a non-constant separable polynomial over a separably closed field always has at least one root in the field.
More concisely: A separable polynomial of positive degree over a separably closed field has a root in the field.
|
IsSepClosed.splits_domain
theorem IsSepClosed.splits_domain :
∀ {k : Type u} [inst : Field k] {K : Type v} [inst_1 : Field K] [inst_2 : IsSepClosed k] {f : k →+* K}
(p : Polynomial k), p.Separable → Polynomial.Splits f p
The theorem `IsSepClosed.splits_domain` states that for any field `k`, if `k` is separably closed, then any separable polynomial `p` defined over `k` splits in the field extension determined by a ring homomorphism `f` from `k` to another field `K`. "Splits" means that the polynomial is either zero or all of its irreducible factors have degree 1. The theorem also refers to a related result, `IsSepClosed.splits_codomain`, which deals with the case where `k` is separably closed.
More concisely: If `k` is a separably closed field and `p` is a separable polynomial over `k`, then `p` splits into linear factors in the field extension determined by any homomorphism from `k` to another field `K`.
|