# mathlib3documentation

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 #

• fixed_points 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 fixed_by.subfield {M : Type u} [monoid M] (F : Type v) [field F] [ 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] [ F] (S : subfield F) :
Prop

A typeclass for subrings invariant under a mul_semiring_action.

Instances of this typeclass
@[protected, instance]
def is_invariant_subfield.to_mul_semiring_action (M : Type u) [monoid M] {F : Type v} [field F] [ F] (S : subfield F)  :
Equations
@[protected, instance]
def subfield.to_subring.is_invariant_subring (M : Type u) [monoid M] {F : Type v} [field F] [ F] (S : subfield F)  :
def fixed_points.subfield (M : Type u) [monoid M] (F : Type v) [field F] [ F] :

The subfield of fixed points by a monoid action.

Equations
Instances for fixed_points.subfield
Instances for ↥fixed_points.subfield
@[protected, instance]
def fixed_points.subfield.is_invariant_subfield (M : Type u) [monoid M] (F : Type v) [field F] [ F] :
@[protected, instance]
def fixed_points.smul_comm_class (M : Type u) [monoid M] (F : Type v) [field F] [ F] :
F
@[protected, instance]
def fixed_points.smul_comm_class' (M : Type u) [monoid M] (F : Type v) [field F] [ F] :
F
@[simp]
theorem fixed_points.smul (M : Type u) [monoid M] (F : Type v) [field F] [ F] (m : M) (x : ) :
m x = x
@[simp]
theorem fixed_points.smul_polynomial (M : Type u) [monoid M] (F : Type v) [field F] [ F] (m : M) (p : polynomial ) :
m p = p
@[protected, instance]
def fixed_points.algebra (M : Type u) [monoid M] (F : Type v) [field F] [ F] :
F
Equations
theorem fixed_points.coe_algebra_map (M : Type u) [monoid M] (F : Type v) [field F] [ F] :
theorem fixed_points.linear_independent_smul_of_linear_independent (G : Type u) [group G] (F : Type v) [field F] [ F] {s : finset F} :
(λ (i : s), i) (λ (i : s), F) i)
noncomputable def fixed_points.minpoly (G : Type u) [group G] (F : Type v) [field F] [ 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] [ F] [fintype G] (x : F) :
x).monic
theorem fixed_points.minpoly.eval₂ (G : Type u) [group G] (F : Type v) [field F] [ F] [fintype G] (x : F) :
x) = 0
theorem fixed_points.minpoly.eval₂' (G : Type u) [group G] (F : Type v) [field F] [ F] [fintype G] (x : F) :
x) = 0
theorem fixed_points.minpoly.ne_one (G : Type u) [group G] (F : Type v) [field F] [ F] [fintype G] (x : F) :
x 1
theorem fixed_points.minpoly.of_eval₂ (G : Type u) [group G] (F : Type v) [field F] [ F] [fintype G] (x : F) (f : polynomial ) (hf : f = 0) :
x f
theorem fixed_points.minpoly.irreducible_aux (G : Type u) [group G] (F : Type v) [field F] [ F] [fintype G] (x : F) (f g : polynomial ) (hf : f.monic) (hg : g.monic) (hfg : f * g = x) :
f = 1 g = 1
theorem fixed_points.minpoly.irreducible (G : Type u) [group G] (F : Type v) [field F] [ F] [fintype G] (x : F) :
theorem fixed_points.is_integral (G : Type u) [group G] (F : Type v) [field F] [ F] [finite G] (x : F) :
theorem fixed_points.minpoly_eq_minpoly (G : Type u) [group G] (F : Type v) [field F] [ F] [fintype G] (x : F) :
x = x
theorem fixed_points.rank_le_card (G : Type u) [group G] (F : Type v) [field F] [ F] [fintype G] :
@[protected, instance]
def fixed_points.normal (G : Type u) [group G] (F : Type v) [field F] [ F] [finite G] :
F
@[protected, instance]
def fixed_points.separable (G : Type u) [group G] (F : Type v) [field F] [ F] [finite G] :
@[protected, instance]
def fixed_points.finite_dimensional (G : Type u) [group G] (F : Type v) [field F] [ F] [finite G] :
theorem fixed_points.finrank_le_card (G : Type u) [group G] (F : Type v) [field F] [ F] [fintype G] :
theorem linear_independent_to_linear_map (R : Type u) (A : Type v) (B : Type w) [ring A] [ A] [comm_ring B] [is_domain B] [ B] :
theorem cardinal_mk_alg_hom (K : Type u) (V : Type v) (W : Type w) [field K] [field V] [ V] [ V] [field W] [ W] [ W] :
@[protected, instance]
noncomputable def alg_equiv.fintype (K : Type u) (V : Type v) [field K] [field V] [ V] [ V] :
Equations
theorem finrank_alg_hom (K : Type u) (V : Type v) [field K] [field V] [ V] [ V] :
theorem fixed_points.finrank_eq_card (G : Type u) (F : Type v) [group G] [field F] [fintype G] [ F] [ F] :
theorem fixed_points.to_alg_hom_bijective (G : Type u) (F : Type v) [group G] [field F] [finite G] [ F] [ F] :

mul_semiring_action.to_alg_hom is bijective.

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

Bijection between G and algebra homomorphisms that fix the fixed points

Equations