mathlib documentation

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

@[instance]
def fixed_by.is_subfield (G : Type u) [group G] (F : Type v) [field F] [mul_semiring_action G F] (g : G) :

@[instance]
def fixed_points.is_subfield (G : Type u) [group G] (F : Type v) [field F] [mul_semiring_action G F] :

@[instance]

@[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)) :
g x = x

@[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)) :
g p = p

def fixed_points.minpoly (G : Type u) [group G] (F : Type v) [field F] [mul_semiring_action G F] [fintype G] :

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

Equations
theorem fixed_points.minpoly.monic (G : Type u) [group G] (F : Type v) [field F] [mul_semiring_action G F] [fintype G] (x : F) :

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) :

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)) :
f.monicg.monicf * g = fixed_points.minpoly G F xf = 1 g = 1

theorem fixed_points.minpoly.irreducible (G : Type u) [group G] (F : Type v) [field F] [mul_semiring_action G F] [fintype G] (x : F) :

theorem fixed_points.is_integral (G : Type u) [group G] (F : Type v) [field F] [mul_semiring_action G F] [fintype G] (x : F) :

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) :

@[instance]
def fixed_points.normal (G : Type u) [group G] (F : Type v) [field F] [mul_semiring_action G F] [fintype G] :

@[instance]
def fixed_points.separable (G : Type u) [group G] (F : Type v) [field F] [mul_semiring_action G F] [fintype G] :

@[instance]

theorem cardinal_mk_alg_hom (K : Type u) (V : Type v) [field K] [field V] [algebra K V] [finite_dimensional K V] :

@[instance]
def alg_hom.fintype (K : Type u) (V : Type v) [field K] [field V] [algebra K V] [finite_dimensional K V] :

Equations
theorem findim_alg_hom (K : Type u) (V : Type v) [field K] [field V] [algebra K V] [finite_dimensional K V] :

@[simp]
theorem fixed_points.to_alg_hom_apply (G : Type u) (F : Type v) [group G] [field F] [faithful_mul_semiring_action G F] :

def fixed_points.to_alg_hom (G : Type u) (F : Type v) [group G] [field F] [faithful_mul_semiring_action G F] :

Embedding produced from a faithful action.

Equations
theorem fixed_points.to_alg_hom_apply_apply {G : Type u} {F : Type v} [group G] [field F] [faithful_mul_semiring_action G F] (g : G) (x : F) :