mathlib3 documentation

field_theory.fixed

Fixed field under a group action. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 finrank (fixed_points G F) F = fintype.card G.

Main Definitions #

def fixed_by.subfield {M : Type u} [monoid M] (F : Type v) [field F] [mul_semiring_action M F] (m : M) :

The subfield of F fixed by the field endomorphism m.

Equations
@[class]
structure is_invariant_subfield (M : Type u) [monoid M] {F : Type v} [field F] [mul_semiring_action M F] (S : subfield F) :
Prop

A typeclass for subrings invariant under a mul_semiring_action.

Instances of this typeclass
@[protected, instance]
@[protected, instance]
@[simp]
theorem fixed_points.smul (M : Type u) [monoid M] (F : Type v) [field F] [mul_semiring_action M F] (m : M) (x : (fixed_points.subfield M F)) :
m x = x
@[simp]
theorem fixed_points.smul_polynomial (M : Type u) [monoid M] (F : Type v) [field F] [mul_semiring_action M F] (m : M) (p : polynomial (fixed_points.subfield M F)) :
m p = p
@[protected, instance]
Equations
noncomputable 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 (fixed_points.subfield G F)) (hf : f.monic) (hg : g.monic) (hfg : f * g = fixed_points.minpoly G F x) :
f = 1 g = 1
theorem fixed_points.is_integral (G : Type u) [group G] (F : Type v) [field F] [mul_semiring_action G F] [finite G] (x : F) :
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
noncomputable def alg_equiv.fintype (K : Type u) (V : Type v) [field K] [field V] [algebra K V] [finite_dimensional K V] :
Equations
noncomputable def fixed_points.to_alg_hom_equiv (G : Type u) (F : Type v) [group G] [field F] [fintype G] [mul_semiring_action G F] [has_faithful_smul G F] :

Bijection between G and algebra homomorphisms that fix the fixed points

Equations