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 ofFfixed_points by every element ofG, whereGis a group that acts onF.
def
fixed_by.subfield
{M : Type u}
[monoid M]
(F : Type v)
[field F]
[mul_semiring_action M F]
(m : M) :
subfield F
The subfield of F fixed by the field endomorphism m.
@[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]
def
is_invariant_subfield.to_mul_semiring_action
(M : Type u)
[monoid M]
{F : Type v}
[field F]
[mul_semiring_action M F]
(S : subfield F)
[is_invariant_subfield M S] :
Equations
- is_invariant_subfield.to_mul_semiring_action M S = {to_distrib_mul_action := {to_mul_action := {to_has_smul := {smul := λ (m : M) (x : ↥S), ⟨m • ↑x, _⟩}, one_smul := _, mul_smul := _}, smul_zero := _, smul_add := _}, smul_one := _, smul_mul := _}
@[protected, instance]
def
subfield.to_subring.is_invariant_subring
(M : Type u)
[monoid M]
{F : Type v}
[field F]
[mul_semiring_action M F]
(S : subfield F)
[is_invariant_subfield M S] :
def
fixed_points.subfield
(M : Type u)
[monoid M]
(F : Type v)
[field F]
[mul_semiring_action M F] :
subfield F
The subfield of fixed points by a monoid action.
Equations
- fixed_points.subfield M F = (⨅ (m : M), fixed_by.subfield F m).copy (mul_action.fixed_points M F) _
Instances for fixed_points.subfield
@[protected, instance]
def
fixed_points.subfield.is_invariant_subfield
(M : Type u)
[monoid M]
(F : Type v)
[field F]
[mul_semiring_action M F] :
@[protected, instance]
def
fixed_points.smul_comm_class
(M : Type u)
[monoid M]
(F : Type v)
[field F]
[mul_semiring_action M F] :
smul_comm_class M ↥(fixed_points.subfield M F) F
@[protected, instance]
def
fixed_points.smul_comm_class'
(M : Type u)
[monoid M]
(F : Type v)
[field F]
[mul_semiring_action M F] :
smul_comm_class ↥(fixed_points.subfield M F) M F
@[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)) :
@[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)) :
@[protected, instance]
def
fixed_points.algebra
(M : Type u)
[monoid M]
(F : Type v)
[field F]
[mul_semiring_action M F] :
algebra ↥(fixed_points.subfield M F) F
Equations
- fixed_points.algebra M F = (fixed_points.subfield M F).to_algebra
theorem
fixed_points.coe_algebra_map
(M : Type u)
[monoid M]
(F : Type v)
[field F]
[mul_semiring_action M F] :
algebra_map ↥(fixed_points.subfield M F) F = (fixed_points.subfield M F).subtype
theorem
fixed_points.linear_independent_smul_of_linear_independent
(G : Type u)
[group G]
(F : Type v)
[field F]
[mul_semiring_action G F]
{s : finset F} :
linear_independent ↥(fixed_points.subfield G F) (λ (i : ↥↑s), ↑i) → linear_independent F (λ (i : ↥↑s), ⇑(mul_action.to_fun G F) ↑i)
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
- fixed_points.minpoly G F x = (prod_X_sub_smul G F x).to_subring (fixed_points.subfield G F).to_subring _
theorem
fixed_points.minpoly.monic
(G : Type u)
[group G]
(F : Type v)
[field F]
[mul_semiring_action G F]
[fintype G]
(x : F) :
(fixed_points.minpoly G F x).monic
theorem
fixed_points.minpoly.eval₂
(G : Type u)
[group G]
(F : Type v)
[field F]
[mul_semiring_action G F]
[fintype G]
(x : F) :
polynomial.eval₂ (fixed_points.subfield G F).to_subring.subtype x (fixed_points.minpoly G F x) = 0
theorem
fixed_points.minpoly.eval₂'
(G : Type u)
[group G]
(F : Type v)
[field F]
[mul_semiring_action G F]
[fintype G]
(x : F) :
polynomial.eval₂ (fixed_points.subfield G F).subtype x (fixed_points.minpoly G F x) = 0
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) :
fixed_points.minpoly G F x ≠ 1
theorem
fixed_points.minpoly.of_eval₂
(G : Type u)
[group G]
(F : Type v)
[field F]
[mul_semiring_action G F]
[fintype G]
(x : F)
(f : polynomial ↥(fixed_points.subfield G F))
(hf : polynomial.eval₂ (fixed_points.subfield G F).subtype x f = 0) :
fixed_points.minpoly G F 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) :
theorem
fixed_points.minpoly.irreducible
(G : Type u)
[group G]
(F : Type v)
[field F]
[mul_semiring_action G F]
[fintype G]
(x : F) :
irreducible (fixed_points.minpoly G F x)
theorem
fixed_points.is_integral
(G : Type u)
[group G]
(F : Type v)
[field F]
[mul_semiring_action G F]
[finite G]
(x : F) :
is_integral ↥(fixed_points.subfield G F) x
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) :
fixed_points.minpoly G F x = minpoly ↥(fixed_points.subfield G F) x
theorem
fixed_points.rank_le_card
(G : Type u)
[group G]
(F : Type v)
[field F]
[mul_semiring_action G F]
[fintype G] :
module.rank ↥(fixed_points.subfield G F) F ≤ ↑(fintype.card G)
@[protected, instance]
def
fixed_points.normal
(G : Type u)
[group G]
(F : Type v)
[field F]
[mul_semiring_action G F]
[finite G] :
normal ↥(fixed_points.subfield G F) F
@[protected, instance]
def
fixed_points.separable
(G : Type u)
[group G]
(F : Type v)
[field F]
[mul_semiring_action G F]
[finite G] :
is_separable ↥(fixed_points.subfield G F) F
@[protected, instance]
def
fixed_points.finite_dimensional
(G : Type u)
[group G]
(F : Type v)
[field F]
[mul_semiring_action G F]
[finite G] :
theorem
fixed_points.finrank_le_card
(G : Type u)
[group G]
(F : Type v)
[field F]
[mul_semiring_action G F]
[fintype G] :
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] :
cardinal.mk (V →ₐ[K] W) ≤ ↑(finite_dimensional.finrank W (V →ₗ[K] W))
@[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
- alg_equiv.fintype K V = fintype.of_equiv (V →ₐ[K] V) ↑((alg_equiv_equiv_alg_hom K V).symm)
theorem
finrank_alg_hom
(K : Type u)
(V : Type v)
[field K]
[field V]
[algebra K V]
[finite_dimensional K V] :
fintype.card (V →ₐ[K] V) ≤ finite_dimensional.finrank V (V →ₗ[K] V)
theorem
fixed_points.finrank_eq_card
(G : Type u)
(F : Type v)
[group G]
[field F]
[fintype G]
[mul_semiring_action G F]
[has_faithful_smul G F] :
theorem
fixed_points.to_alg_hom_bijective
(G : Type u)
(F : Type v)
[group G]
[field F]
[finite G]
[mul_semiring_action G F]
[has_faithful_smul G 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]
[mul_semiring_action G F]
[has_faithful_smul G F] :
G ≃ (F →ₐ[↥(fixed_points.subfield G F)] F)
Bijection between G and algebra homomorphisms that fix the fixed points