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

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

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

• IsInvariantSubfield.toMulSemiringAction M S = MulSemiringAction.mk ⋯ ⋯

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

instance FixedPoints.instIsInvariantSubfieldSubfield (M : Type u) [Monoid M] (F : Type v) [Field F] [MulSemiringAction M F] : IsInvariantSubfield M (FixedPoints.subfield 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)) : 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 ↥(FixedPoints.subfield M F)) : m • p = p

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 ⋯

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) : 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 (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] : Fintype (V ≃ₐ[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_1) (F : Type u_2) [Group G] [Field F] [MulSemiringAction G F] [Fintype G] [FaithfulSMul G F] : Module.finrank (↥(FixedPoints.subfield G F)) F = Fintype.card G

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

MulSemiringAction.toAlgHom is bijective.

def FixedPoints.toAlgHomEquiv (G : Type u_1) (F : Type u_2) [Group G] [Field F] [MulSemiringAction G F] [Finite G] [FaithfulSMul G F] : G ≃ (F →ₐ[↥(FixedPoints.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_1) (F : Type u_2) [Group G] [Field F] [MulSemiringAction G F] [Finite G] [FaithfulSMul G F] : Function.Bijective ⇑(MulSemiringAction.toAlgAut G (↥(FixedPoints.subfield G F)) F)

MulSemiringAction.toAlgAut is bijective.

def FixedPoints.toAlgAutMulEquiv (G : Type u_1) (F : Type u_2) [Group G] [Field F] [MulSemiringAction G F] [Finite G] [FaithfulSMul G F] : G ≃* F ≃ₐ[↥(FixedPoints.subfield G F)] 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_1) (F : Type u_2) [Group G] [Field F] [MulSemiringAction G F] [Finite G] : Function.Surjective ⇑(MulSemiringAction.toAlgAut G (↥(FixedPoints.subfield G F)) F)

MulSemiringAction.toAlgAut is surjective.