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.

Equations

• One or more equations did not get rendered due to their size.

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 = MulSemiringAction.mk ⋯ ⋯

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

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 = Subfield.copy (⨅ (m : M), FixedBy.subfield F m) (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.instSMulCommClassSubtypeMemSubfieldToDivisionRingInstMembershipInstSetLikeSubfieldSubfieldToSMulToZeroToCommMonoidWithZeroToCommGroupWithZeroToSemifieldToSMulZeroClassToAddZeroClassToAddMonoidToAddMonoidWithOneToAddGroupWithOneToRingToDistribSMulToDistribMulActionToSemiringInstSMulSubtypeMemSubringInstMembershipInstSetLikeSubringToSMulToCommSemiringToSemiringToDivisionSemiringIdToSubring (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.instAlgebraSubtypeMemSubfieldToDivisionRingInstMembershipInstSetLikeSubfieldSubfieldToCommSemiringToCommSemiringToSemifieldToSubsemiringToRingToSubringToSemiringToDivisionSemiring (M : Type u) [Monoid M] (F : Type v) [Field F] [MulSemiringAction M F] : Algebra (↥(FixedPoints.subfield M F)) F

Equations

• One or more equations did not get rendered due to their size.

theorem FixedPoints.coe_algebraMap (M : Type u) [Monoid M] (F : Type v) [Field F] [MulSemiringAction M F] : algebraMap (↥(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 ↥(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 = Polynomial.toSubring (prodXSubSMul G F x) (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) : 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 ↥(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 ↥(FixedPoints.subfield G F)) (g : Polynomial ↥(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 (↥(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.separable (G : Type u) [Group G] (F : Type v) [Field F] [MulSemiringAction G F] [Finite G] : IsSeparable (↥(FixedPoints.subfield G F)) F

Equations

• ⋯ = ⋯

instance FixedPoints.instFiniteDimensionalSubtypeMemSubfieldToDivisionRingInstMembershipInstSetLikeSubfieldSubfieldToMonoidToDivInvMonoidToDivisionRingToAddCommGroupToRingInstModuleSubtypeMemSubringInstMembershipInstSetLikeSubringToSemiringToSemiringToSubsemiringToAddCommMonoidToModuleToSemiringToSubring (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] : FiniteDimensional.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) ≤ ↑(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)

Equations

• AlgEquiv.fintype K V = Fintype.ofEquiv (V →ₐ[K] V) ↑(MulEquiv.symm (algEquivEquivAlgHom 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 (↥(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 (↥(FixedPoints.subfield G F)) 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) ⋯