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 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.

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

• smul_mem : ∀ (m : M) {x : F}, x ∈ S → m • x ∈ S

A typeclass for subrings invariant under a MulSemiringAction.

instance IsInvariantSubfield.toMulSemiringAction (M : Type u) [Monoid M] {F : Type v} [Field F] [MulSemiringAction M F] (S : Subfield F) [IsInvariantSubfield M S] : MulSemiringAction M { x // x ∈ S }

instance instIsInvariantSubringToRingToDivisionRingToSubring (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.

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

instance FixedPoints.instSMulCommClassSubtypeMemSubfieldInstMembershipInstSetLikeSubfieldSubfieldToSMulToZeroToCommMonoidWithZeroToCommGroupWithZeroToSemifieldToSMulZeroClassToAddZeroClassToAddMonoidToAddMonoidWithOneToAddGroupWithOneToRingToDivisionRingToDistribSMulToDistribMulActionToSemiringInstSMulSubtypeMemSubringInstMembershipInstSetLikeSubringToSMulToCommSemiringToSemiringToDivisionSemiringIdToSubring (M : Type u) [Monoid M] (F : Type v) [Field F] [MulSemiringAction M F] : SMulCommClass M { x // x ∈ FixedPoints.subfield M F } F

instance FixedPoints.smulCommClass' (M : Type u) [Monoid M] (F : Type v) [Field F] [MulSemiringAction M F] : SMulCommClass { x // x ∈ FixedPoints.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 : { x // 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 { x // x ∈ FixedPoints.subfield M F }) : m • p = p

instance FixedPoints.instAlgebraSubtypeMemSubfieldInstMembershipInstSetLikeSubfieldSubfieldToCommSemiringToCommSemiringToSemifieldToSubsemiringToRingToDivisionRingToSubringToSemiringToDivisionSemiring (M : Type u) [Monoid M] (F : Type v) [Field F] [MulSemiringAction M F] : Algebra { x // x ∈ FixedPoints.subfield M F } F

theorem FixedPoints.coe_algebraMap (M : Type u) [Monoid M] (F : Type v) [Field F] [MulSemiringAction M F] : algebraMap { x // x ∈ FixedPoints.subfield M F } F = Subfield.subtype (FixedPoints.subfield M F)

theorem FixedPoints.linearIndependent_smul_of_linearIndependent (G : Type u) [Group G] (F : Type v) [Field F] [MulSemiringAction G F] {s : Finset F} : (LinearIndependent { x // x ∈ FixedPoints.subfield G F } fun i => ↑i) → LinearIndependent F fun i => ↑(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 { x // x ∈ FixedPoints.subfield G F }

minpoly G F x is the minimal polynomial of (x : F) over FixedPoints.subfield G F.

theorem FixedPoints.minpoly.monic (G : Type u) [Group G] (F : Type v) [Field F] [MulSemiringAction G F] [Fintype G] (x : F) : Polynomial.Monic (FixedPoints.minpoly G F x)

theorem FixedPoints.minpoly.eval₂ (G : Type u) [Group G] (F : Type v) [Field F] [MulSemiringAction G F] [Fintype G] (x : F) : Polynomial.eval₂ (Subring.subtype (FixedPoints.subfield G F).toSubring) 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₂ (Subfield.subtype (FixedPoints.subfield G F)) 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 { x // x ∈ FixedPoints.subfield G F }) (hf : Polynomial.eval₂ (Subfield.subtype (FixedPoints.subfield G F)) 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 { x // x ∈ FixedPoints.subfield G F }) (g : Polynomial { x // x ∈ FixedPoints.subfield G F }) (hf : Polynomial.Monic f) (hg : Polynomial.Monic g) (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 { x // x ∈ 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 { x // x ∈ 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 { x // x ∈ 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 { x // x ∈ FixedPoints.subfield G F } F

instance FixedPoints.separable (G : Type u) [Group G] (F : Type v) [Field F] [MulSemiringAction G F] [Finite G] : IsSeparable { x // x ∈ FixedPoints.subfield G F } F

instance FixedPoints.instFiniteDimensionalSubtypeMemSubfieldInstMembershipInstSetLikeSubfieldSubfieldToMonoidToDivInvMonoidToDivisionRingToFieldToAddCommGroupToRingInstModuleSubtypeMemSubringInstMembershipInstSetLikeSubringToSemiringToSemiringToSubsemiringToAddCommMonoidToModuleToSemiringToSubring (G : Type u) [Group G] (F : Type v) [Field F] [MulSemiringAction G F] [Finite G] : FiniteDimensional { x // x ∈ FixedPoints.subfield G F } F

theorem FixedPoints.finrank_le_card (G : Type u) [Group G] (F : Type v) [Field F] [MulSemiringAction G F] [Fintype G] : FiniteDimensional.finrank { x // x ∈ 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] [FiniteDimensional K W] : Cardinal.mk (V →ₐ[K] W) ≤ ↑(FiniteDimensional.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)

theorem finrank_algHom (K : Type u) (V : Type v) [Field K] [Field V] [Algebra K V] [FiniteDimensional K V] : Fintype.card (V →ₐ[K] V) ≤ FiniteDimensional.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] : FiniteDimensional.finrank { x // x ∈ 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] : Function.Bijective (MulSemiringAction.toAlgHom { x // x ∈ FixedPoints.subfield G F } F)

MulSemiringAction.toAlgHom is bijective.

def FixedPoints.toAlgHomEquiv (G : Type u) (F : Type v) [Group G] [Field F] [Fintype G] [MulSemiringAction G F] [FaithfulSMul G F] : G ≃ (F →ₐ[{ x // x ∈ FixedPoints.subfield G F }] F)

Bijection between G and algebra homomorphisms that fix the fixed points