# Documentation

Mathlib.FieldTheory.Fixed

# 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.

Instances For
class IsInvariantSubfield (M : Type u) [] {F : Type v} [] [] (S : ) :
• smul_mem : ∀ (m : M) {x : F}, x Sm x S

A typeclass for subrings invariant under a MulSemiringAction.

Instances
instance IsInvariantSubfield.toMulSemiringAction (M : Type u) [] {F : Type v} [] [] (S : ) [] :
MulSemiringAction M { x // x S }
instance instIsInvariantSubringToRingToDivisionRingToSubring (M : Type u) [] {F : Type v} [] [] (S : ) [] :
IsInvariantSubring M S.toSubring
def FixedPoints.subfield (M : Type u) [] (F : Type v) [] [] :

The subfield of fixed points by a monoid action.

Instances For
instance FixedPoints.instIsInvariantSubfieldSubfield (M : Type u) [] (F : Type v) [] [] :
instance FixedPoints.smulCommClass' (M : Type u) [] (F : Type v) [] [] :
SMulCommClass { x // } M F
@[simp]
theorem FixedPoints.smul (M : Type u) [] (F : Type v) [] [] (m : M) (x : { x // }) :
m x = x
@[simp]
theorem FixedPoints.smul_polynomial (M : Type u) [] (F : Type v) [] [] (m : M) (p : Polynomial { x // }) :
m p = p
theorem FixedPoints.coe_algebraMap (M : Type u) [] (F : Type v) [] [] :
algebraMap { x // } F =
theorem FixedPoints.linearIndependent_smul_of_linearIndependent (G : Type u) [] (F : Type v) [] [] {s : } :
(LinearIndependent { x // } fun i => i) → LinearIndependent F fun i => ↑() i
def FixedPoints.minpoly (G : Type u) [] (F : Type v) [] [] [] (x : F) :
Polynomial { x // }

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

Instances For
theorem FixedPoints.minpoly.monic (G : Type u) [] (F : Type v) [] [] [] (x : F) :
theorem FixedPoints.minpoly.eval₂ (G : Type u) [] (F : Type v) [] [] [] (x : F) :
Polynomial.eval₂ (Subring.subtype ().toSubring) x () = 0
theorem FixedPoints.minpoly.eval₂' (G : Type u) [] (F : Type v) [] [] [] (x : F) :
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 : Polynomial { x // }) (hf : = 0) :
f
theorem FixedPoints.minpoly.irreducible_aux (G : Type u) [] (F : Type v) [] [] [] (x : F) (f : Polynomial { x // }) (g : Polynomial { x // }) (hf : ) (hg : ) (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 // } x
theorem FixedPoints.minpoly_eq_minpoly (G : Type u) [] (F : Type v) [] [] [] (x : F) :
= minpoly { x // } x
theorem FixedPoints.rank_le_card (G : Type u) [] (F : Type v) [] [] [] :
Module.rank { x // } F ↑()
instance FixedPoints.normal (G : Type u) [] (F : Type v) [] [] [] :
Normal { x // } F
instance FixedPoints.separable (G : Type u) [] (F : Type v) [] [] [] :
IsSeparable { x // } F
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] [] :
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 →ₐ[{ x // }] F)

Bijection between G and algebra homomorphisms that fix the fixed points

Instances For