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 FixedPoints.subfield 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 (FixedPoints.subfield G F) F = Fintype.card G
.
Main Definitions #
FixedPoints.subfield G F
, the subfield consisting of elements ofF
fixed_points by every element ofG
, whereG
is a group that acts onF
.
def
FixedBy.subfield
{M : Type u}
[Monoid M]
(F : Type v)
[Field F]
[MulSemiringAction M F]
(m : M)
:
Subfield F
The subfield of F fixed by the field endomorphism m
.
Equations
- FixedBy.subfield F m = { carrier := MulAction.fixedBy F m, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯, inv_mem' := ⋯ }
Instances For
class
IsInvariantSubfield
(M : Type u)
[Monoid M]
{F : Type v}
[Field F]
[MulSemiringAction M F]
(S : Subfield F)
:
A typeclass for subrings invariant under a MulSemiringAction
.
Instances
theorem
IsInvariantSubfield.smul_mem
{M : Type u}
:
∀ {inst : Monoid M} {F : Type v} {inst_1 : Field F} {inst_2 : MulSemiringAction M F} {S : Subfield F}
[self : IsInvariantSubfield M S] (m : M) {x : F}, x ∈ S → m • x ∈ S
instance
IsInvariantSubfield.toMulSemiringAction
(M : Type u)
[Monoid M]
{F : Type v}
[Field F]
[MulSemiringAction M F]
(S : Subfield F)
[IsInvariantSubfield M S]
:
MulSemiringAction M ↥S
Equations
instance
instIsInvariantSubringOfIsInvariantSubfield
(M : Type u)
[Monoid M]
{F : Type v}
[Field F]
[MulSemiringAction M F]
(S : Subfield F)
[IsInvariantSubfield M S]
:
IsInvariantSubring M S.toSubring
Equations
- ⋯ = ⋯
def
FixedPoints.subfield
(M : Type u)
[Monoid M]
(F : Type v)
[Field F]
[MulSemiringAction M F]
:
Subfield F
The subfield of fixed points by a monoid action.
Equations
- FixedPoints.subfield M F = (⨅ (m : M), FixedBy.subfield F m).copy (MulAction.fixedPoints M F) ⋯
Instances For
instance
FixedPoints.instIsInvariantSubfieldSubfield
(M : Type u)
[Monoid M]
(F : Type v)
[Field F]
[MulSemiringAction M F]
:
Equations
- ⋯ = ⋯
instance
FixedPoints.instSMulCommClassSubtypeMemSubfieldSubfield
(M : Type u)
[Monoid M]
(F : Type v)
[Field F]
[MulSemiringAction M F]
:
SMulCommClass M (↥(FixedPoints.subfield M F)) F
Equations
- ⋯ = ⋯
instance
FixedPoints.smulCommClass'
(M : Type u)
[Monoid M]
(F : Type v)
[Field F]
[MulSemiringAction M F]
:
SMulCommClass (↥(FixedPoints.subfield M F)) M F
Equations
- ⋯ = ⋯
@[simp]
theorem
FixedPoints.smul
(M : Type u)
[Monoid M]
(F : Type v)
[Field F]
[MulSemiringAction M F]
(m : M)
(x : ↥(FixedPoints.subfield M F))
:
@[simp]
theorem
FixedPoints.smul_polynomial
(M : Type u)
[Monoid M]
(F : Type v)
[Field F]
[MulSemiringAction M F]
(m : M)
(p : Polynomial ↥(FixedPoints.subfield M F))
:
instance
FixedPoints.instAlgebraSubtypeMemSubfieldSubfield
(M : Type u)
[Monoid M]
(F : Type v)
[Field F]
[MulSemiringAction M F]
:
Algebra (↥(FixedPoints.subfield M F)) F
Equations
- FixedPoints.instAlgebraSubtypeMemSubfieldSubfield M F = inferInstance
theorem
FixedPoints.coe_algebraMap
(M : Type u)
[Monoid M]
(F : Type v)
[Field F]
[MulSemiringAction M F]
:
algebraMap (↥(FixedPoints.subfield M F)) F = (FixedPoints.subfield M F).subtype
theorem
FixedPoints.linearIndependent_smul_of_linearIndependent
(G : Type u)
[Group G]
(F : Type v)
[Field F]
[MulSemiringAction G F]
{s : Finset F}
:
(LinearIndependent ↥(FixedPoints.subfield G F) fun (i : ↑↑s) => ↑i) →
LinearIndependent F fun (i : ↑↑s) => (MulAction.toFun G F) ↑i
def
FixedPoints.minpoly
(G : Type u)
[Group G]
(F : Type v)
[Field F]
[MulSemiringAction G F]
[Fintype G]
(x : F)
:
Polynomial ↥(FixedPoints.subfield G F)
minpoly G F x
is the minimal polynomial of (x : F)
over FixedPoints.subfield G F
.
Equations
- FixedPoints.minpoly G F x = (prodXSubSMul G F x).toSubring (FixedPoints.subfield G F).toSubring ⋯
Instances For
theorem
FixedPoints.minpoly.monic
(G : Type u)
[Group G]
(F : Type v)
[Field F]
[MulSemiringAction G F]
[Fintype G]
(x : F)
:
(FixedPoints.minpoly G F x).Monic
theorem
FixedPoints.minpoly.eval₂
(G : Type u)
[Group G]
(F : Type v)
[Field F]
[MulSemiringAction G F]
[Fintype G]
(x : F)
:
Polynomial.eval₂ (FixedPoints.subfield G F).subtype x (FixedPoints.minpoly G F x) = 0
theorem
FixedPoints.minpoly.eval₂'
(G : Type u)
[Group G]
(F : Type v)
[Field F]
[MulSemiringAction G F]
[Fintype G]
(x : F)
:
Polynomial.eval₂ (FixedPoints.subfield G F).subtype x (FixedPoints.minpoly G F x) = 0
theorem
FixedPoints.minpoly.ne_one
(G : Type u)
[Group G]
(F : Type v)
[Field F]
[MulSemiringAction G F]
[Fintype G]
(x : F)
:
FixedPoints.minpoly G F x ≠ 1
theorem
FixedPoints.minpoly.of_eval₂
(G : Type u)
[Group G]
(F : Type v)
[Field F]
[MulSemiringAction G F]
[Fintype G]
(x : F)
(f : Polynomial ↥(FixedPoints.subfield G F))
(hf : Polynomial.eval₂ (FixedPoints.subfield G F).subtype x f = 0)
:
FixedPoints.minpoly G F x ∣ f
theorem
FixedPoints.minpoly.irreducible_aux
(G : Type u)
[Group G]
(F : Type v)
[Field F]
[MulSemiringAction G F]
[Fintype G]
(x : F)
(f : Polynomial ↥(FixedPoints.subfield G F))
(g : Polynomial ↥(FixedPoints.subfield G F))
(hf : f.Monic)
(hg : g.Monic)
(hfg : f * g = FixedPoints.minpoly G F x)
:
theorem
FixedPoints.minpoly.irreducible
(G : Type u)
[Group G]
(F : Type v)
[Field F]
[MulSemiringAction G F]
[Fintype G]
(x : F)
:
Irreducible (FixedPoints.minpoly G F x)
theorem
FixedPoints.isIntegral
(G : Type u)
[Group G]
(F : Type v)
[Field F]
[MulSemiringAction G F]
[Finite G]
(x : F)
:
IsIntegral (↥(FixedPoints.subfield G F)) x
theorem
FixedPoints.minpoly_eq_minpoly
(G : Type u)
[Group G]
(F : Type v)
[Field F]
[MulSemiringAction G F]
[Fintype G]
(x : F)
:
FixedPoints.minpoly G F x = minpoly (↥(FixedPoints.subfield G F)) x
theorem
FixedPoints.rank_le_card
(G : Type u)
[Group G]
(F : Type v)
[Field F]
[MulSemiringAction G F]
[Fintype G]
:
Module.rank (↥(FixedPoints.subfield G F)) F ≤ ↑(Fintype.card G)
instance
FixedPoints.normal
(G : Type u)
[Group G]
(F : Type v)
[Field F]
[MulSemiringAction G F]
[Finite G]
:
Normal (↥(FixedPoints.subfield G F)) F
Equations
- ⋯ = ⋯
instance
FixedPoints.isSeparable
(G : Type u)
[Group G]
(F : Type v)
[Field F]
[MulSemiringAction G F]
[Finite G]
:
Algebra.IsSeparable (↥(FixedPoints.subfield G F)) F
Equations
- ⋯ = ⋯
instance
FixedPoints.instFiniteDimensionalSubtypeMemSubfieldSubfield
(G : Type u)
[Group G]
(F : Type v)
[Field F]
[MulSemiringAction G F]
[Finite G]
:
FiniteDimensional (↥(FixedPoints.subfield G F)) F
Equations
- ⋯ = ⋯
theorem
FixedPoints.finrank_le_card
(G : Type u)
[Group G]
(F : Type v)
[Field F]
[MulSemiringAction G F]
[Fintype G]
:
Module.finrank (↥(FixedPoints.subfield G F)) F ≤ Fintype.card G
theorem
linearIndependent_toLinearMap
(R : Type u)
(A : Type v)
(B : Type w)
[CommSemiring R]
[Ring A]
[Algebra R A]
[CommRing B]
[IsDomain B]
[Algebra R B]
:
LinearIndependent B AlgHom.toLinearMap
theorem
cardinal_mk_algHom
(K : Type u)
(V : Type v)
(W : Type w)
[Field K]
[Field V]
[Algebra K V]
[FiniteDimensional K V]
[Field W]
[Algebra K W]
:
Cardinal.mk (V →ₐ[K] W) ≤ ↑(Module.finrank W (V →ₗ[K] W))
noncomputable instance
AlgEquiv.fintype
(K : Type u)
(V : Type v)
[Field K]
[Field V]
[Algebra K V]
[FiniteDimensional K V]
:
Equations
- AlgEquiv.fintype K V = Fintype.ofEquiv (V →ₐ[K] V) ↑(algEquivEquivAlgHom K V).symm
theorem
finrank_algHom
(K : Type u)
(V : Type v)
[Field K]
[Field V]
[Algebra K V]
[FiniteDimensional K V]
:
Fintype.card (V →ₐ[K] V) ≤ Module.finrank V (V →ₗ[K] V)
theorem
FixedPoints.finrank_eq_card
(G : Type u)
(F : Type v)
[Group G]
[Field F]
[Fintype G]
[MulSemiringAction G F]
[FaithfulSMul G F]
:
Module.finrank (↥(FixedPoints.subfield G F)) F = Fintype.card G
theorem
FixedPoints.toAlgHom_bijective
(G : Type u)
(F : Type v)
[Group G]
[Field F]
[Finite G]
[MulSemiringAction G F]
[FaithfulSMul G F]
:
MulSemiringAction.toAlgHom
is bijective.
def
FixedPoints.toAlgHomEquiv
(G : Type u)
(F : Type v)
[Group G]
[Field F]
[Finite G]
[MulSemiringAction G F]
[FaithfulSMul G F]
:
G ≃ (F →ₐ[↥(FixedPoints.subfield G F)] F)
Bijection between G and algebra homomorphisms that fix the fixed points
Equations
- FixedPoints.toAlgHomEquiv G F = Equiv.ofBijective (MulSemiringAction.toAlgHom (↥(FixedPoints.subfield G F)) F) ⋯