# 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 FixedPoints.subfield 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 finrank (FixedPoints.subfield G F) F = Fintype.card G.

## Main Definitions #

• FixedPoints.subfield G F, the subfield consisting of elements of F fixed_points by every element of G, where G is a group that acts on F.
def FixedBy.subfield {M : Type u} [] (F : Type v) [] [] (m : M) :

The subfield of F fixed by the field endomorphism m.

Equations
• = { carrier := , mul_mem' := , one_mem' := , add_mem' := , zero_mem' := , neg_mem' := , inv_mem' := }
Instances For
class IsInvariantSubfield (M : Type u) [] {F : Type v} [] [] (S : ) :

A typeclass for subrings invariant under a MulSemiringAction.

• smul_mem : ∀ (m : M) {x : F}, x Sm x S
Instances
theorem IsInvariantSubfield.smul_mem {M : Type u} [] {F : Type v} [] [] {S : } [self : ] (m : M) {x : F} :
x Sm x S
instance IsInvariantSubfield.toMulSemiringAction (M : Type u) [] {F : Type v} [] [] (S : ) [] :
Equations
instance instIsInvariantSubringOfIsInvariantSubfield (M : Type u) [] {F : Type v} [] [] (S : ) [] :
IsInvariantSubring M S.toSubring
Equations
• =
def FixedPoints.subfield (M : Type u) [] (F : Type v) [] [] :

The subfield of fixed points by a monoid action.

Equations
• = (⨅ (m : M), ).copy ()
Instances For
instance FixedPoints.instIsInvariantSubfieldSubfield (M : Type u) [] (F : Type v) [] [] :
Equations
• =
Equations
• =
instance FixedPoints.smulCommClass' (M : Type u) [] (F : Type v) [] [] :
SMulCommClass (()) M F
Equations
• =
@[simp]
theorem FixedPoints.smul (M : Type u) [] (F : Type v) [] [] (m : M) (x : ()) :
m x = x
@[simp]
theorem FixedPoints.smul_polynomial (M : Type u) [] (F : Type v) [] [] (m : M) (p : ) :
m p = p
instance FixedPoints.instAlgebraSubtypeMemSubfieldSubfield (M : Type u) [] (F : Type v) [] [] :
Algebra (()) F
Equations
• = inferInstance
theorem FixedPoints.coe_algebraMap (M : Type u) [] (F : Type v) [] [] :
algebraMap (()) F = ().subtype
theorem FixedPoints.linearIndependent_smul_of_linearIndependent (G : Type u) [] (F : Type v) [] [] {s : } :
(LinearIndependent () fun (i : s) => i)LinearIndependent F fun (i : s) => () i
def FixedPoints.minpoly (G : Type u) [] (F : Type v) [] [] [] (x : F) :

minpoly G F x is the minimal polynomial of (x : F) over FixedPoints.subfield G F.

Equations
Instances For
theorem FixedPoints.minpoly.monic (G : Type u) [] (F : Type v) [] [] [] (x : F) :
().Monic
theorem FixedPoints.minpoly.eval₂ (G : Type u) [] (F : Type v) [] [] [] (x : F) :
Polynomial.eval₂ ().subtype x () = 0
theorem FixedPoints.minpoly.eval₂' (G : Type u) [] (F : Type v) [] [] [] (x : F) :
Polynomial.eval₂ ().subtype x () = 0
theorem FixedPoints.minpoly.ne_one (G : Type u) [] (F : Type v) [] [] [] (x : F) :
1
theorem FixedPoints.minpoly.of_eval₂ (G : Type u) [] (F : Type v) [] [] [] (x : F) (f : ) (hf : Polynomial.eval₂ ().subtype x f = 0) :
f
theorem FixedPoints.minpoly.irreducible_aux (G : Type u) [] (F : Type v) [] [] [] (x : F) (f : ) (g : ) (hf : f.Monic) (hg : g.Monic) (hfg : f * g = ) :
f = 1 g = 1
theorem FixedPoints.minpoly.irreducible (G : Type u) [] (F : Type v) [] [] [] (x : F) :
theorem FixedPoints.isIntegral (G : Type u) [] (F : Type v) [] [] [] (x : F) :
IsIntegral (()) x
theorem FixedPoints.minpoly_eq_minpoly (G : Type u) [] (F : Type v) [] [] [] (x : F) :
= minpoly (()) x
theorem FixedPoints.rank_le_card (G : Type u) [] (F : Type v) [] [] [] :
Module.rank (()) F ()
instance FixedPoints.normal (G : Type u) [] (F : Type v) [] [] [] :
Normal (()) F
Equations
• =
instance FixedPoints.separable (G : Type u) [] (F : Type v) [] [] [] :
IsSeparable (()) F
Equations
• =
Equations
• =
theorem FixedPoints.finrank_le_card (G : Type u) [] (F : Type v) [] [] [] :
theorem linearIndependent_toLinearMap (R : Type u) (A : Type v) (B : Type w) [] [Ring A] [Algebra R A] [] [] [Algebra R B] :
LinearIndependent B AlgHom.toLinearMap
theorem cardinal_mk_algHom (K : Type u) (V : Type v) (W : Type w) [] [] [Algebra K V] [] [] [Algebra K W] :
noncomputable instance AlgEquiv.fintype (K : Type u) (V : Type v) [] [] [Algebra K V] [] :
Equations
theorem finrank_algHom (K : Type u) (V : Type v) [] [] [Algebra K V] [] :
theorem FixedPoints.finrank_eq_card (G : Type u) (F : Type v) [] [] [] [] [] :
theorem FixedPoints.toAlgHom_bijective (G : Type u) (F : Type v) [] [] [] [] [] :

MulSemiringAction.toAlgHom is bijective.

def FixedPoints.toAlgHomEquiv (G : Type u) (F : Type v) [] [] [] [] [] :
G (F →ₐ[()] F)

Bijection between G and algebra homomorphisms that fix the fixed points

Equations
Instances For