Polynomial.Gal.restrict_smul
theorem Polynomial.Gal.restrict_smul :
∀ {F : Type u_1} [inst : Field F] {p : Polynomial F} {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E]
[inst_3 : Fact (Polynomial.Splits (algebraMap F E) p)] (ϕ : E ≃ₐ[F] E) (x : ↑(p.rootSet E)),
↑((Polynomial.Gal.restrict p E) ϕ • x) = ϕ ↑x
This theorem states that the restrict function, defined on the Galois group of a polynomial `p` with coefficients in a field `F` and values in a field extension `E`, is compatible with the action of the Galois group on the set of roots of `p` in `E`. More specifically, for any automorphism `ϕ` of `E` that fixes `F` and any root `x` of `p` in `E`, the action of the image of `ϕ` under the restrict function on `x` is exactly `ϕ` acting on `x`. This theorem is a kind of coherence property between the algebraic structure (the Galois group and its action) and the geometric data (the set of roots of the polynomial).
More concisely: The restrict function on the Galois group of a polynomial over a field preserves the action on the roots of the polynomial: for any automorphism ϕ fixing the base field and any root x in the extension, ρ(ϕ)(x) = ϕ(x), where ρ denotes the restrict function.
|
Polynomial.Gal.card_of_separable
theorem Polynomial.Gal.card_of_separable :
∀ {F : Type u_1} [inst : Field F] {p : Polynomial F},
p.Separable → Fintype.card p.Gal = FiniteDimensional.finrank F p.SplittingField
This theorem states that for a given separable polynomial over a field `F`, the cardinality of its Galois group is equal to the dimension of its splitting field over `F`. In other words, if `p` is a separable polynomial in the field `F`, then the number of elements in the Galois group of `p` matches the rank of the vector space formed by the splitting field of `p` over `F`.
More concisely: The order of the Galois group of a separable polynomial over a field equals the dimension of its splitting field extension.
|
Polynomial.Gal.restrictProd_injective
theorem Polynomial.Gal.restrictProd_injective :
∀ {F : Type u_1} [inst : Field F] (p q : Polynomial F), Function.Injective ⇑(Polynomial.Gal.restrictProd p q) := by
sorry
The theorem `Polynomial.Gal.restrictProd_injective` states that for any field `F` and any polynomials `p` and `q` over `F`, the function `Polynomial.Gal.restrictProd p q`, which maps the Galois group of the product of `p` and `q` into the product of the Galois groups of `p` and `q`, is injective. In other words, if two elements in the Galois group of the product `p*q` map to the same element in the product of the Galois groups of `p` and `q`, then those two elements are the same. This means the function `Polynomial.Gal.restrictProd p q` is a subgroup embedding.
More concisely: The restriction homomorphism from the Galois group of a product of polynomials to the product of their Galois groups is an injective group homomorphism.
|
Polynomial.Gal.galActionHom_injective
theorem Polynomial.Gal.galActionHom_injective :
∀ {F : Type u_1} [inst : Field F] (p : Polynomial F) (E : Type u_2) [inst_1 : Field E] [inst_2 : Algebra F E]
[inst_3 : Fact (Polynomial.Splits (algebraMap F E) p)], Function.Injective ⇑(Polynomial.Gal.galActionHom p E)
The theorem `Polynomial.Gal.galActionHom_injective` states that for any field `F`, any polynomial `p` over `F`, and any extension field `E` of `F`, if the polynomial `p` splits over `E` (which means that it can be factored into linear factors in `E`), then the Galois group of `p` can be embedded as a subgroup of the group of permutations of the roots of `p` in `E`. This embedding is injective, meaning that different elements of the Galois group correspond to distinct permutations of the roots of `p` in `E`.
More concisely: The Galois group of a polynomial that splits over an extension field is embeddable as a subgroup of the permutations of its roots in the extension field, with the embedding being injective.
|
Polynomial.Gal.splits_in_splittingField_of_comp
theorem Polynomial.Gal.splits_in_splittingField_of_comp :
∀ {F : Type u_1} [inst : Field F] (p q : Polynomial F),
q.natDegree ≠ 0 → Polynomial.Splits (algebraMap F (p.comp q).SplittingField) p
The theorem `Polynomial.Gal.splits_in_splittingField_of_comp` states that for any field `F` and any two polynomials `p` and `q` over `F`, if `q` is non-constant (i.e., its degree is not zero), then the polynomial `p` splits in the splitting field of the composition `p ∘ q`. In other words, `p` can be factored into linear factors over the splitting field of `p ∘ q`. The splitting field of a polynomial is a field extension in which the polynomial factors into linear polynomials (has all its roots).
More concisely: Given a field `F` and polynomials `p` and `q` over `F` with non-zero degree `q`, `p` splits into linear factors in the splitting field of their composition `p ∘ q`.
|