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) :
@[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] (x : F) :

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)) (hf : f.monic) (hg : g.monic) (hfg : f * g = fixed_points.minpoly G F x) :
f = 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_eq_minpoly (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) (W : Type w) [field K] [field V] [algebra K V] [finite_dimensional K V] [field W] [algebra K W] [finite_dimensional K W] :
@[instance]
def alg_hom.fintype (K : Type u) (V : Type v) (W : Type w) [field K] [field V] [algebra K V] [finite_dimensional K V] [field W] [algebra K W] [finite_dimensional K W] :
Equations
@[instance]
def alg_equiv.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) :

Bijection between G and algebra homomorphisms that fix the fixed points

Equations