FixedPoints.minpoly.eval₂
theorem FixedPoints.minpoly.eval₂ :
∀ (G : Type u) [inst : Group G] (F : Type v) [inst_1 : Field F] [inst_2 : MulSemiringAction G F]
[inst_3 : Fintype G] (x : F),
Polynomial.eval₂ (FixedPoints.subfield G F).subtype x (FixedPoints.minpoly G F x) = 0
The theorem `FixedPoints.minpoly.eval₂` states that for any group `G`, field `F`, and element `x` of `F`, if `G` acts on `F` through a multiplicative semiring action and `G` is finite, then the polynomial obtained by evaluating the minimal polynomial of `x` over the subfield of fixed points by the monoid action of `G` on `F` at `x` using the natural ring homomorphism from the subring of the subfield to the field `F`, is equal to zero. In essence, this theorem is a generalization of the property that the minimal polynomial of an element in a field, when evaluated at this element, is always zero.
More concisely: For any finite group action on a field through a multiplicative semiring, the minimal polynomial of an element evaluated by the group action at that element is equal to zero.
|
FixedPoints.minpoly.proof_1
theorem FixedPoints.minpoly.proof_1 :
∀ (G : Type u_2) [inst : Group G] (F : Type u_1) [inst_1 : Field F] [inst_2 : MulSemiringAction G F]
[inst_3 : Fintype G] (x x_1 : F), x_1 ∈ ↑(prodXSubSMul G F x).frange → ∀ (g : G), g • x_1 = x_1
The theorem `FixedPoints.minpoly.proof_1` states that for any group `G`, field `F`, and `x` and `x_1` in `F`, if `x_1` is in the finset of nonzero coefficients of the polynomial obtained by taking the product of `(X - g • x)` over all distinct `g • x`, then `x_1` is a fixed point under the action of any element `g` of the group `G`. That is, for any `g` in `G`, the scalar multiplication of `g` and `x_1` is `x_1` itself. Here, `G` is endowed with a multiplicative semiring action on `F`, and the operation `g • x_1` denotes the scalar multiplication of `g` and `x_1` under this action.
More concisely: If `x_1` is in the set of nonzero coefficients of the minimal polynomial of `x` over the group action of `G` in the ring `F`, then `x_1` is a fixed point under the action of any `g` in `G`, i.e., `g • x_1 = x_1` for all `g` in `G`.
|
FixedPoints.toAlgHom_bijective
theorem FixedPoints.toAlgHom_bijective :
∀ (G : Type u) (F : Type v) [inst : Group G] [inst_1 : Field F] [inst_2 : Finite G] [inst_3 : MulSemiringAction G F]
[inst_4 : FaithfulSMul G F], Function.Bijective (MulSemiringAction.toAlgHom (↥(FixedPoints.subfield G F)) F)
The theorem `FixedPoints.toAlgHom_bijective` states that for any type `G` forming a group, any type `F` forming a field, where `G` is finite and there exists a multiplication semiring action of `G` on `F` which is faithful, the function `MulSemiringAction.toAlgHom` mapping the subfield of fixed points by the group action `G` on `F` to `F` is bijective. In other words, each element in `F` corresponds to exactly one element in the subfield of fixed points by the group action, and every element in the subfield of fixed points corresponds to exactly one element in `F`.
More concisely: For any finite group action `G` on a field `F` via a faithful multiplication semiring action, the resulting function mapping the fixed points to `F` is a bijective algebra homomorphism.
|
FixedPoints.minpoly.monic
theorem FixedPoints.minpoly.monic :
∀ (G : Type u) [inst : Group G] (F : Type v) [inst_1 : Field F] [inst_2 : MulSemiringAction G F]
[inst_3 : Fintype G] (x : F), (FixedPoints.minpoly G F x).Monic
The theorem `FixedPoints.minpoly.monic` states that for any group `G` and field `F` with a multiplicative semiring action of `G` on `F`, and any element `x` of `F`, the minimal polynomial of `x` over the subfield of fixed points of `G` in `F` is monic. In other words, the leading coefficient of the minimal polynomial is 1. This theorem holds for any finite group `G`.
More concisely: The minimal polynomial of an element in a field with respect to the action of a finite group's subfield of fixed points is always monic.
|