Documentation

Mathlib.FieldTheory.Fixed

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 #

def FixedBy.subfield {M : Type u} [Monoid M] (F : Type v) [Field F] [MulSemiringAction M F] (m : M) :

The subfield of F fixed by the field endomorphism m.

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

    • smul_mem : ∀ (m : M) {x : F}, x Sm x S
    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 Sm x S
      Equations
      • =
      def FixedPoints.subfield (M : Type u) [Monoid M] (F : Type v) [Field F] [MulSemiringAction M F] :

      The subfield of fixed points by a monoid action.

      Equations
      Instances For
        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
        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) :

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

        Equations
        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.ne_one (G : Type u) [Group G] (F : Type v) [Field F] [MulSemiringAction G F] [Fintype G] (x : F) :
          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) :
          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.isIntegral (G : Type u) [Group G] (F : Type v) [Field F] [MulSemiringAction G F] [Finite G] (x : F) :
          instance FixedPoints.normal (G : Type u) [Group G] (F : Type v) [Field F] [MulSemiringAction G F] [Finite G] :
          Equations
          • =
          Equations
          • =
          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] :
          noncomputable instance AlgEquiv.fintype (K : Type u) (V : Type v) [Field K] [Field V] [Algebra K V] [FiniteDimensional K V] :
          Equations
          theorem finrank_algHom (K : Type u) (V : Type v) [Field K] [Field V] [Algebra K V] [FiniteDimensional K V] :

          Bijection between G and algebra homomorphisms that fix the fixed points

          Equations
          Instances For