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 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 of F fixed_points by every element of G, where G is a group that acts on F.

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' := ⋯ }

@[simp]

theorem FixedBy.subfield_mem_iff {M : Type u} [Monoid M] (F : Type v) [Field F] [MulSemiringAction M F] (m : M) (x : F) : x ∈ subfield F m ↔ m • x = x

def FixedBy.intermediateField {M : Type u} [Monoid M] (K : Type u_1) (F : Type v) [Field F] [MulSemiringAction M F] (m : M) [Field K] [Algebra K F] [SMulCommClass M K F] : IntermediateField K F

The intermediate field between K and F fixed by the field endomorphism m.

Equations

• FixedBy.intermediateField K F m = { toSubsemiring := (FixedBy.subfield F m).toSubsemiring, algebraMap_mem' := ⋯, inv_mem' := ⋯ }

@[simp]

theorem FixedBy.intermediateField_mem_iff {M : Type u} [Monoid M] (K : Type u_1) (F : Type v) [Field F] [MulSemiringAction M F] (m : M) [Field K] [Algebra K F] [SMulCommClass M K F] (x : F) : x ∈ intermediateField K F m ↔ m • x = x

class IsInvariantSubfield (M : Type u) [Monoid M] {F : Type v} [Field F] [MulSemiringAction M F] (S : Subfield F) : Prop

A typeclass for subrings invariant under a MulSemiringAction.

• smul_mem (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

• IsInvariantSubfield.toMulSemiringAction M S = { smul := fun (m : M) (x : ↥S) => ⟨m • ↑x, ⋯⟩, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, smul_one := ⋯, smul_mul := ⋯ }

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

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) ⋯

instance FixedPoints.instIsInvariantSubfieldSubfield (M : Type u) [Monoid M] (F : Type v) [Field F] [MulSemiringAction M F] : IsInvariantSubfield M (subfield M F)

instance FixedPoints.instSMulCommClassSubtypeMemSubfieldSubfield (M : Type u) [Monoid M] (F : Type v) [Field F] [MulSemiringAction M F] : SMulCommClass M (↥(subfield M F)) F

instance FixedPoints.smulCommClass' (M : Type u) [Monoid M] (F : Type v) [Field F] [MulSemiringAction M F] : SMulCommClass (↥(subfield M F)) M F

@[simp]

theorem FixedPoints.smul (M : Type u) [Monoid M] (F : Type v) [Field F] [MulSemiringAction M F] (m : M) (x : ↥(subfield M F)) : m • x = x

@[simp]

theorem FixedPoints.smul_polynomial (M : Type u) [Monoid M] (F : Type v) [Field F] [MulSemiringAction M F] (m : M) (p : Polynomial ↥(subfield M F)) : m • p = p

instance FixedPoints.instAlgebraSubtypeMemSubfieldSubfield (M : Type u) [Monoid M] (F : Type v) [Field F] [MulSemiringAction M F] : Algebra (↥(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 (↥(subfield M F)) F = (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} : LinearIndepOn (↥(subfield G F)) id ↑s → LinearIndepOn F ⇑(MulAction.toFun G F) ↑s

def FixedPoints.minpoly (G : Type u) [Group G] (F : Type v) [Field F] [MulSemiringAction G F] [Fintype G] (x : F) : Polynomial ↥(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 ⋯

theorem FixedPoints.minpoly.monic (G : Type u) [Group G] (F : Type v) [Field F] [MulSemiringAction G F] [Fintype G] (x : F) : (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₂ (subfield G F).subtype x (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₂ (subfield G F).subtype x (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) : 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 ↥(subfield G F)) (hf : Polynomial.eval₂ (subfield G F).subtype x f = 0) : 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 g : Polynomial ↥(subfield G F)) (hf : f.Monic) (hg : g.Monic) (hfg : f * g = minpoly G F x) : f = 1 ∨ g = 1

theorem FixedPoints.minpoly.irreducible (G : Type u) [Group G] (F : Type v) [Field F] [MulSemiringAction G F] [Fintype G] (x : F) : Irreducible (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 (↥(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) : minpoly G F x = _root_.minpoly (↥(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 (↥(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 (↥(subfield G F)) F

instance FixedPoints.isSeparable (G : Type u) [Group G] (F : Type v) [Field F] [MulSemiringAction G F] [Finite G] : Algebra.IsSeparable (↥(subfield G F)) F

instance FixedPoints.instFiniteDimensionalSubtypeMemSubfieldSubfield (G : Type u) [Group G] (F : Type v) [Field F] [MulSemiringAction G F] [Finite G] : FiniteDimensional (↥(subfield G F)) F

theorem FixedPoints.finrank_le_card (G : Type u) [Group G] (F : Type v) [Field F] [MulSemiringAction G F] [Fintype G] : Module.finrank (↥(subfield G F)) F ≤ Fintype.card G

theorem linearIndependent_toLinearMap (R : Type u) (A : Type v) (B : Type w) [CommSemiring R] [Semiring A] [Algebra R A] [CommRing B] [IsDomain B] [Algebra R B] : LinearIndependent B AlgHom.toLinearMap

theorem cardinalMk_algHom (K : Type u) (V : Type v) (W : Type w) [Field K] [Ring 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] : Fintype Gal(V/K)

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 AlgHom.card_le {F : Type u_2} {K : Type u_3} [Field F] [Field K] [Algebra F K] [FiniteDimensional F K] : Fintype.card (K →ₐ[F] K) ≤ Module.finrank F K

theorem AlgEquiv.card_le {F : Type u_2} {K : Type u_3} [Field F] [Field K] [Algebra F K] [FiniteDimensional F K] : Fintype.card Gal(K/F) ≤ Module.finrank F K

theorem FixedPoints.finrank_eq_card (G : Type u_2) (F : Type u_3) [Group G] [Field F] [MulSemiringAction G F] [Fintype G] [FaithfulSMul G F] : Module.finrank (↥(subfield G F)) F = Fintype.card G

Let $F$ be a field. Let $G$ be a finite group acting faithfully on $F$. Then $[F : F^G] = |G|$.

theorem FixedPoints.toAlgHom_bijective (G : Type u_2) (F : Type u_3) [Group G] [Field F] [MulSemiringAction G F] [Finite G] [FaithfulSMul G F] : Function.Bijective (MulSemiringAction.toAlgHom (↥(subfield G F)) F)

MulSemiringAction.toAlgHom is bijective.

def FixedPoints.toAlgHomEquiv (G : Type u_2) (F : Type u_3) [Group G] [Field F] [MulSemiringAction G F] [Finite G] [FaithfulSMul G F] : G ≃ (F →ₐ[↥(subfield G F)] F)

Bijection between G and algebra endomorphisms of F that fix the fixed points.

Equations

• FixedPoints.toAlgHomEquiv G F = Equiv.ofBijective (MulSemiringAction.toAlgHom (↥(FixedPoints.subfield G F)) F) ⋯

theorem FixedPoints.toAlgAut_bijective (G : Type u_2) (F : Type u_3) [Group G] [Field F] [MulSemiringAction G F] [Finite G] [FaithfulSMul G F] : Function.Bijective ⇑(MulSemiringAction.toAlgAut G (↥(subfield G F)) F)

MulSemiringAction.toAlgAut is bijective.

def FixedPoints.toAlgAutMulEquiv (G : Type u_2) (F : Type u_3) [Group G] [Field F] [MulSemiringAction G F] [Finite G] [FaithfulSMul G F] : G ≃* Gal(F/↥(subfield G F))

Bijection between G and algebra automorphisms of F that fix the fixed points.

Equations

• FixedPoints.toAlgAutMulEquiv G F = MulEquiv.ofBijective (MulSemiringAction.toAlgAut G (↥(FixedPoints.subfield G F)) F) ⋯

theorem FixedPoints.toAlgAut_surjective (G : Type u_2) (F : Type u_3) [Group G] [Field F] [MulSemiringAction G F] [Finite G] : Function.Surjective ⇑(MulSemiringAction.toAlgAut G (↥(subfield G F)) F)

MulSemiringAction.toAlgAut is surjective.