Fixed field under a group action.
This is the basis of the Fundamental Theorem of Galois Theory.
Given a (finite) group G that acts on a field F, we define fixed_points G F,
the subfield consisting of elements of F fixed_points by every element of G.
This subfield is then normal and separable, and in addition (TODO) if G acts faithfully on F
then findim (fixed_points G F) F = fintype.card G.
Main Definitions
fixed_points G F, the subfield consisting of elements ofFfixed_points by every element ofG, whereGis a group that acts onF.
@[instance]
def
fixed_by.is_subfield
(G : Type u)
[group G]
(F : Type v)
[field F]
[mul_semiring_action G F]
(g : G) :
is_subfield (mul_action.fixed_by G F g)
Equations
- _ = _
@[instance]
def
fixed_points.is_subfield
(G : Type u)
[group G]
(F : Type v)
[field F]
[mul_semiring_action G F] :
Equations
- _ = _
@[instance]
def
fixed_points.is_invariant_subring
(G : Type u)
[group G]
(F : Type v)
[field F]
[mul_semiring_action G F] :
Equations
- _ = _
@[simp]
theorem
fixed_points.smul
(G : Type u)
[group G]
(F : Type v)
[field F]
[mul_semiring_action G F]
(g : G)
(x : ↥(mul_action.fixed_points G F)) :
@[simp]
theorem
fixed_points.smul_polynomial
(G : Type u)
[group G]
(F : Type v)
[field F]
[mul_semiring_action G F]
(g : G)
(p : polynomial ↥(mul_action.fixed_points G F)) :
@[instance]
def
fixed_points.algebra
(G : Type u)
[group G]
(F : Type v)
[field F]
[mul_semiring_action G F] :
algebra ↥(mul_action.fixed_points G F) F
Equations
theorem
fixed_points.coe_algebra_map
(G : Type u)
[group G]
(F : Type v)
[field F]
[mul_semiring_action G F] :
def
fixed_points.minpoly
(G : Type u)
[group G]
(F : Type v)
[field F]
[mul_semiring_action G F]
[fintype G] :
F → polynomial ↥(mul_action.fixed_points G F)
fixed_points.minpoly G F x is the minimal polynomial of (x : F) over fixed_points G F.
Equations
- fixed_points.minpoly G F x = (prod_X_sub_smul G F x).to_subring (mul_action.fixed_points G F) _
theorem
fixed_points.minpoly.monic
(G : Type u)
[group G]
(F : Type v)
[field F]
[mul_semiring_action G F]
[fintype G]
(x : F) :
(fixed_points.minpoly G F x).monic
theorem
fixed_points.minpoly.eval₂
(G : Type u)
[group G]
(F : Type v)
[field F]
[mul_semiring_action G F]
[fintype G]
(x : F) :
polynomial.eval₂ (is_subring.subtype (mul_action.fixed_points G F)) x (fixed_points.minpoly G F x) = 0
theorem
fixed_points.is_integral
(G : Type u)
[group G]
(F : Type v)
[field F]
[mul_semiring_action G F]
[fintype G]
(x : F) :
is_integral ↥(mul_action.fixed_points G F) x
theorem
fixed_points.minpoly.ne_one
(G : Type u)
[group G]
(F : Type v)
[field F]
[mul_semiring_action G F]
[fintype G]
(x : F) :
fixed_points.minpoly G F x ≠ 1
theorem
fixed_points.of_eval₂
(G : Type u)
[group G]
(F : Type v)
[field F]
[mul_semiring_action G F]
[fintype G]
(x : F)
(f : polynomial ↥(mul_action.fixed_points G F)) :
polynomial.eval₂ (is_subring.subtype (mul_action.fixed_points G F)) x f = 0 → fixed_points.minpoly G F x ∣ f
theorem
fixed_points.minpoly.irreducible_aux
(G : Type u)
[group G]
(F : Type v)
[field F]
[mul_semiring_action G F]
[fintype G]
(x : F)
(f g : polynomial ↥(mul_action.fixed_points G F)) :
theorem
fixed_points.minpoly.irreducible
(G : Type u)
[group G]
(F : Type v)
[field F]
[mul_semiring_action G F]
[fintype G]
(x : F) :
irreducible (fixed_points.minpoly G F x)
theorem
fixed_points.minpoly.minimal_polynomial
(G : Type u)
[group G]
(F : Type v)
[field F]
[mul_semiring_action G F]
[fintype G]
(x : F) :
fixed_points.minpoly G F x = minimal_polynomial _
@[instance]
def
fixed_points.normal
(G : Type u)
[group G]
(F : Type v)
[field F]
[mul_semiring_action G F]
[fintype G] :
normal ↥(mul_action.fixed_points G F) F
Equations
- _ = _
@[instance]
def
fixed_points.separable
(G : Type u)
[group G]
(F : Type v)
[field F]
[mul_semiring_action G F]
[fintype G] :
is_separable ↥(mul_action.fixed_points G F) F
Equations
- _ = _