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
fixed_points G F, the subfield consisting of elements ofFfixed_points by every element ofG, whereGis a group that acts onF.
@[instance]
def
fixed_by.is_subfield
(G : Type u)
[group G]
(F : Type v)
[field F]
[mul_semiring_action G F]
(g : G) :
is_subfield (mul_action.fixed_by G F g)
@[instance]
def
fixed_points.is_subfield
(G : Type u)
[group G]
(F : Type v)
[field F]
[mul_semiring_action G F] :
@[instance]
def
fixed_points.is_invariant_subring
(G : Type u)
[group G]
(F : Type v)
[field F]
[mul_semiring_action G F] :
@[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)) :
@[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)) :
@[instance]
def
fixed_points.algebra
(G : Type u)
[group G]
(F : Type v)
[field F]
[mul_semiring_action G F] :
algebra ↥(mul_action.fixed_points G F) F
Equations
theorem
fixed_points.coe_algebra_map
(G : Type u)
[group G]
(F : Type v)
[field F]
[mul_semiring_action G F] :
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}
(a : linear_independent ↥(mul_action.fixed_points G F) (λ (i : ↥↑s), ↑i)) :
linear_independent F (λ (i : ↥↑s), ⇑(mul_action.to_fun G F) ↑i)
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 (mul_action.fixed_points G F) _
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₂ (is_subring.subtype (mul_action.fixed_points G F)) 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 ↥(mul_action.fixed_points G F))
(hf : polynomial.eval₂ (is_subring.subtype (mul_action.fixed_points G F)) 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 ↥(mul_action.fixed_points 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]
[fintype G]
(x : F) :
is_integral ↥(mul_action.fixed_points G F) x
theorem
fixed_points.minpoly.minimal_polynomial
(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 = minimal_polynomial _
@[instance]
def
fixed_points.normal
(G : Type u)
[group G]
(F : Type v)
[field F]
[mul_semiring_action G F]
[fintype G] :
normal ↥(mul_action.fixed_points G F) F
@[instance]
def
fixed_points.separable
(G : Type u)
[group G]
(F : Type v)
[field F]
[mul_semiring_action G F]
[fintype G] :
is_separable ↥(mul_action.fixed_points G F) F
theorem
fixed_points.dim_le_card
(G : Type u)
[group G]
(F : Type v)
[field F]
[mul_semiring_action G F]
[fintype G] :
vector_space.dim ↥(mul_action.fixed_points G F) F ≤ ↑(fintype.card G)
@[instance]
def
fixed_points.finite_dimensional
(G : Type u)
[group G]
(F : Type v)
[field F]
[mul_semiring_action G F]
[fintype G] :
theorem
fixed_points.findim_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)
[comm_semiring R]
[integral_domain A]
[algebra R A] :
theorem
cardinal_mk_alg_hom
(K : Type u)
(V : Type v)
[field K]
[field V]
[algebra K V]
[finite_dimensional K V] :
@[instance]
def
alg_hom.fintype
(K : Type u)
(V : Type v)
[field K]
[field V]
[algebra K V]
[finite_dimensional K V] :
Equations
- alg_hom.fintype K V = classical.choice _
theorem
findim_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.findim V (V →ₗ[K] V)
@[simp]
theorem
fixed_points.to_alg_hom_to_fun
(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] :
G ↪ F →ₐ[↥(mul_action.fixed_points G F)] F
Embedding produced from a faithful action.
theorem
fixed_points.to_alg_hom_apply
{G : Type u}
{F : Type v}
[group G]
[field F]
[faithful_mul_semiring_action G F]
(g : G)
(x : F) :
⇑(⇑(fixed_points.to_alg_hom G F) g) x = g • x
theorem
fixed_points.findim_eq_card
(G : Type u)
(F : Type v)
[group G]
[field F]
[fintype G]
[faithful_mul_semiring_action G F] :