Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly
theorem Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly :
∀ {F : Type u_1} {K : Type u_2} (A : Type u_3) [inst : Field F] [inst_1 : Field K] [inst_2 : Field A]
[inst_3 : Algebra F K] [inst_4 : Algebra F A],
Algebra.IsAlgebraic F K →
∀ [inst_5 : IsAlgClosed A] (x : K), (Set.range fun ψ => ψ x) = (minpoly F x).rootSet A
The theorem `Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly` states that for any algebraically closed field `A`, and any element `x` of a field `K` that is an algebraic extension of a field `F`, the set of images of `x` under any `F`-algebra homomorphism from `K` to `A` is exactly the set of roots of the minimal polynomial of `x` over `F` in `A`. In other words, applying any `F`-algebra homomorphism to `x` results in a root of `x`'s minimal polynomial over `F` in the algebraically closed field `A`.
More concisely: For any algebraically closed field `A`, and any algebraic extension `K/F`, the image of an element `x` in `K` under any `F`-algebra homomorphism to `A` is a root of `x`'s minimal polynomial over `F` in `A`.
|
IsAlgClosed.of_exists_root
theorem IsAlgClosed.of_exists_root :
∀ (k : Type u) [inst : Field k],
(∀ (p : Polynomial k), p.Monic → Irreducible p → ∃ x, Polynomial.eval x p = 0) → IsAlgClosed k
The theorem `IsAlgClosed.of_exists_root` states that for any field `k`, if for all monic, irreducible polynomials `p` over `k` there exists an `x` such that when `x` is plugged into `p`, the result is `0`, then `k` is an algebraically closed field. In more traditional mathematical language, this theorem asserts that a field is algebraically closed if all monic irreducible polynomials over that field have at least one root in the field.
More concisely: A field is algebraically closed if every monic irreducible polynomial over it has a root in the field.
|
IsAlgClosed.splits_domain
theorem IsAlgClosed.splits_domain :
∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : IsAlgClosed k] [inst_2 : Field K] {f : k →+* K}
(p : Polynomial k), Polynomial.Splits f p
The theorem `IsAlgClosed.splits_domain` states that for any two types `k` and `K` where `k` is a field and `K` is an algebraically closed field, and for any ring homomorphism `f` from `k` to `K`, every polynomial in `k` splits in the field extension defined by `f`. This means that the polynomial either becomes zero when mapped by `f` or all its irreducible factors in the field `K` have a degree of one. This theorem also refers to a similar case, `IsAlgClosed.splits_codomain`, where the codomain `k` is the algebraically closed field.
More concisely: For any field homomorphism from a field `k` to an algebraically closed field `K`, every polynomial in `k` splits in `K` with all irreducible factors having degree 1 or mapping to the constant 0.
|
IsAlgClosed.surjective_comp_algebraMap_of_isAlgebraic
theorem IsAlgClosed.surjective_comp_algebraMap_of_isAlgebraic :
∀ {K : Type u} [inst : Field K] {L : Type v} {M : Type w} [inst_1 : Field L] [inst_2 : Algebra K L]
[inst_3 : Field M] [inst_4 : Algebra K M] [inst_5 : IsAlgClosed M] {E : Type u_1} [inst_6 : Field E]
[inst_7 : Algebra K E] [inst_8 : Algebra L E] [inst_9 : IsScalarTower K L E],
Algebra.IsAlgebraic L E → Function.Surjective fun φ => φ.comp (IsScalarTower.toAlgHom K L E)
This theorem, known as the extension lemma (discussed in [this math stackexchange thread](https://math.stackexchange.com/a/687914)), states the following:
If we have a tower of field extensions E/L/K such that E/L is an algebraic extension, and M is an algebraically closed extension of K, then any embedding of L/K into M/K can be extended to an embedding of E/K. In other words, for each function embedding the field L into the field M (while maintaining the structure from the base field K), there exists a corresponding function that embeds the field E into M, again preserving the structure from K. This extension is surjective, meaning every element of the target field can be mapped from some element of the source field.
More concisely: Given a tower of field extensions K ⊆ L ⊆ E with E/L algebraic, and an algebraically closed extension M/K, any embedding of L/K into M can be extended to an embedding of E into M.
|
IsAlgClosed.exists_root
theorem IsAlgClosed.exists_root :
∀ {k : Type u} [inst : Field k] [inst_1 : IsAlgClosed k] (p : Polynomial k), p.degree ≠ 0 → ∃ x, p.IsRoot x := by
sorry
This theorem states that for any field `k`, given the condition that `k` is algebraically closed, for any polynomial `p` defined over `k`, if the degree of the polynomial is not zero, then there exists a root `x` in `k` such that `x` is a root of the polynomial `p`. In other words, any non-constant polynomial over an algebraically closed field has a root in that field.
More concisely: If `k` is an algebraically closed field and `p` is a non-constant polynomial over `k`, then `p` has a root in `k`.
|
IntermediateField.eq_bot_of_isAlgClosed_of_isAlgebraic
theorem IntermediateField.eq_bot_of_isAlgClosed_of_isAlgebraic :
∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : IsAlgClosed k] [inst_3 : Algebra k K]
(L : IntermediateField k K), Algebra.IsAlgebraic k ↥L → L = ⊥
The theorem `IntermediateField.eq_bot_of_isAlgClosed_of_isAlgebraic` states that if `k` is an algebraically closed field, `K / k` is a field extension, and `L / k` is an intermediate field which is algebraic, then `L` is equal to `k`. This is a corollary of the theorem `IsAlgClosed.algebraMap_surjective_of_isAlgebraic`. In other words, in the mentioned settings, an algebraic intermediate field of a field extension over an algebraically closed field is just the base field itself.
More concisely: If `k` is an algebraically closed field, and `K/k` is a field extension with an intermediate algebraic field `L/k`, then `L = k`.
|
IsAlgClosed.exists_pow_nat_eq
theorem IsAlgClosed.exists_pow_nat_eq :
∀ {k : Type u} [inst : Field k] [inst_1 : IsAlgClosed k] (x : k) {n : ℕ}, 0 < n → ∃ z, z ^ n = x
This theorem states that for any type `k` which forms a field and is algebraically closed, and for any element `x` of type `k` and natural number `n` greater than zero, there exists an element `z` in `k` such that `z` raised to the power `n` equals `x`. Essentially, the theorem guarantees the existence of `nth` roots in an algebraically closed field.
More concisely: In an algebraically closed field, every non-zero element has a root of any positive integer power.
|
IsAlgClosed.splits_codomain
theorem IsAlgClosed.splits_codomain :
∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : IsAlgClosed k] [inst_2 : Field K] {f : K →+* k}
(p : Polynomial K), Polynomial.Splits f p
This theorem states that every polynomial splits in the field extension represented by the function `f : K →+* k` if `k` is algebraically closed. Here, "splits" means that the polynomial is either zero or all of its irreducible factors have degree 1. The theorem applies to any polynomial `p` of the field `K`. Additionally, there is a related theorem, `IsAlgClosed.splits_domain`, which handles the case where `K` is algebraically closed.
More concisely: In an algebraically closed field extension `f : K →+* k`, every polynomial `p` from the base field `K` splits into linear factors.
|
IsAlgClosure.ofAlgebraic
theorem IsAlgClosure.ofAlgebraic :
∀ (K : Type u_1) (J : Type u_2) (L : Type v) [inst : Field K] [inst_1 : Field J] [inst_2 : Field L]
[inst_3 : Algebra K J] [inst_4 : Algebra J L] [inst_5 : IsAlgClosure J L] [inst_6 : Algebra K L]
[inst_7 : IsScalarTower K J L], Algebra.IsAlgebraic K J → IsAlgClosure K L
The theorem states that if `J` is an algebraic extension of a field `K` and `L` is an algebraic closure of `J`, then `L` is also an algebraic closure of `K`. In other words, if we have a hierarchy of field extensions where `J` extends `K` and `L` contains an algebraic closure of `J`, then any element in `L` is algebraic over `K`, making `L` an algebraic closure of `K`. This is contingent on the condition that all elements of `J` are algebraic over `K`, and that `K`, `J` and `L` form a scalar tower, meaning the algebra structure is consistent across the extensions.
More concisely: If `J` is an algebraic extension of a field `K` and `L` is an algebraic closure of `J` containing `K`, then `L` is an algebraic closure of `K`. (Assuming all elements of `J` are algebraic over `K` and the fields form a scalar tower.)
|