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 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
  • smul_mem : ∀ (m : M) {x : F}, x Sm x S

A typeclass for subrings invariant under a mul_semiring_action.

Instances
@[instance]
Equations
def fixed_points.subfield (M : Type u) [monoid M] (F : Type v) [field F] [mul_semiring_action M F] :

The subfield of fixed points by a monoid action.

Equations
@[instance]
@[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
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.eval₂' (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.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 linear_independent_to_linear_map (R : Type u) (A : Type v) (B : Type w) [comm_semiring R] [ring A] [algebra R A] [comm_ring B] [is_domain B] [algebra R B] :
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 finrank_alg_hom (K : Type u) (V : Type v) [field K] [field V] [algebra K V] [finite_dimensional K V] :
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_scalar G F] :

Bijection between G and algebra homomorphisms that fix the fixed points

Equations