Documentation

Mathlib.FieldTheory.Perfect

Perfect fields and rings #

In this file we define perfect fields, together with a generalisation to (commutative) rings in prime characteristic.

Main definitions / statements: #

class PerfectRing (R : Type u_1) (p : ) [CommSemiring R] [ExpChar R p] :

A perfect ring of characteristic p (prime) in the sense of Serre.

NB: This is not related to the concept with the same name introduced by Bass (related to projective covers of modules).

Instances
    theorem PerfectRing.bijective_frobenius {R : Type u_1} {p : } [CommSemiring R] [ExpChar R p] [self : PerfectRing R p] :

    A ring is perfect if the Frobenius map is bijective.

    theorem PerfectRing.ofSurjective (R : Type u_2) (p : ) [CommRing R] [ExpChar R p] [IsReduced R] (h : Function.Surjective (frobenius R p)) :

    For a reduced ring, surjectivity of the Frobenius map is a sufficient condition for perfection.

    instance PerfectRing.ofFiniteOfIsReduced (p : ) (R : Type u_2) [CommRing R] [ExpChar R p] [Finite R] [IsReduced R] :
    Equations
    • =
    @[simp]
    theorem bijective_frobenius (R : Type u_1) (p : ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] :
    @[simp]
    theorem injective_frobenius (R : Type u_1) (p : ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] :
    @[simp]
    theorem surjective_frobenius (R : Type u_1) (p : ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] :
    @[simp]
    theorem frobeniusEquiv_apply (R : Type u_1) (p : ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] (a : R) :
    (frobeniusEquiv R p) a = (frobenius R p) a
    noncomputable def frobeniusEquiv (R : Type u_1) (p : ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] :
    R ≃+* R

    The Frobenius automorphism for a perfect ring.

    Equations
    Instances For
      @[simp]
      theorem coe_frobeniusEquiv (R : Type u_1) (p : ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] :
      (frobeniusEquiv R p) = (frobenius R p)
      theorem frobeniusEquiv_def (R : Type u_1) (p : ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] (x : R) :
      (frobeniusEquiv R p) x = x ^ p
      @[simp]
      theorem iterateFrobeniusEquiv_apply (R : Type u_1) (p : ) (n : ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] (a : R) :
      noncomputable def iterateFrobeniusEquiv (R : Type u_1) (p : ) (n : ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] :
      R ≃+* R

      The iterated Frobenius automorphism for a perfect ring.

      Equations
      Instances For
        @[simp]
        theorem coe_iterateFrobeniusEquiv (R : Type u_1) (p : ) (n : ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] :
        theorem iterateFrobeniusEquiv_def (R : Type u_1) (p : ) (n : ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] (x : R) :
        (iterateFrobeniusEquiv R p n) x = x ^ p ^ n
        theorem iterateFrobeniusEquiv_add_apply (R : Type u_1) (p : ) (m : ) (n : ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] (x : R) :
        theorem iterateFrobeniusEquiv_add (R : Type u_1) (p : ) (m : ) (n : ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] :
        theorem iterateFrobeniusEquiv_symm_add_apply (R : Type u_1) (p : ) (m : ) (n : ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] (x : R) :
        (iterateFrobeniusEquiv R p (m + n)).symm x = (iterateFrobeniusEquiv R p m).symm ((iterateFrobeniusEquiv R p n).symm x)
        theorem iterateFrobeniusEquiv_symm_add (R : Type u_1) (p : ) (m : ) (n : ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] :
        (iterateFrobeniusEquiv R p (m + n)).symm = (iterateFrobeniusEquiv R p n).symm.trans (iterateFrobeniusEquiv R p m).symm
        theorem iterateFrobeniusEquiv_zero_apply (R : Type u_1) (p : ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] (x : R) :
        theorem iterateFrobeniusEquiv_one_apply (R : Type u_1) (p : ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] (x : R) :
        (iterateFrobeniusEquiv R p 1) x = x ^ p
        theorem iterateFrobeniusEquiv_symm (R : Type u_1) (p : ) (n : ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] :
        (iterateFrobeniusEquiv R p n).symm = (frobeniusEquiv R p).symm ^ n
        @[simp]
        theorem frobeniusEquiv_symm_apply_frobenius (R : Type u_1) (p : ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] (x : R) :
        (frobeniusEquiv R p).symm ((frobenius R p) x) = x
        @[simp]
        theorem frobenius_apply_frobeniusEquiv_symm (R : Type u_1) (p : ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] (x : R) :
        (frobenius R p) ((frobeniusEquiv R p).symm x) = x
        @[simp]
        theorem frobenius_comp_frobeniusEquiv_symm (R : Type u_1) (p : ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] :
        (frobenius R p).comp (frobeniusEquiv R p).symm = RingHom.id R
        @[simp]
        theorem frobeniusEquiv_symm_comp_frobenius (R : Type u_1) (p : ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] :
        ((frobeniusEquiv R p).symm).comp (frobenius R p) = RingHom.id R
        @[simp]
        theorem frobeniusEquiv_symm_pow_p (R : Type u_1) (p : ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] (x : R) :
        (frobeniusEquiv R p).symm x ^ p = x
        theorem injective_pow_p (R : Type u_1) (p : ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] {x : R} {y : R} (h : x ^ p = y ^ p) :
        x = y
        theorem polynomial_expand_eq (R : Type u_1) (p : ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] (f : Polynomial R) :
        (Polynomial.expand R p) f = Polynomial.map ((frobeniusEquiv R p).symm) f ^ p
        @[simp]
        theorem not_irreducible_expand (R : Type u_2) (p : ) [CommSemiring R] [Fact (Nat.Prime p)] [CharP R p] [PerfectRing R p] (f : Polynomial R) :
        instance instPerfectRingProd (R : Type u_1) (p : ) [CommSemiring R] [ExpChar R p] [PerfectRing R p] (S : Type u_2) [CommSemiring S] [ExpChar S p] [PerfectRing S p] :
        PerfectRing (R × S) p
        Equations
        • =
        class PerfectField (K : Type u_1) [Field K] :

        A perfect field.

        See also PerfectRing for a generalisation in positive characteristic.

        • separable_of_irreducible : ∀ {f : Polynomial K}, Irreducible ff.Separable

          A field is perfect if every irreducible polynomial is separable.

        Instances
          theorem PerfectField.separable_of_irreducible {K : Type u_1} [Field K] [self : PerfectField K] {f : Polynomial K} :
          Irreducible ff.Separable

          A field is perfect if every irreducible polynomial is separable.

          Equations
          • =
          instance PerfectField.ofFinite {K : Type u_1} [Field K] [Finite K] :
          Equations
          • =
          instance PerfectField.toPerfectRing {K : Type u_1} [Field K] [PerfectField K] (p : ) [ExpChar K p] :

          A perfect field of characteristic p (prime) is a perfect ring.

          Equations
          • =

          If L / K is an algebraic extension, K is a perfect field, then L / K is separable.

          Equations
          • =

          If L / K is an algebraic extension, K is a perfect field, then so is L.

          theorem Polynomial.roots_expand_pow_map_iterateFrobenius_le {R : Type u_1} [CommRing R] [IsDomain R] (p : ) (n : ) [ExpChar R p] (f : Polynomial R) :
          Multiset.map ((iterateFrobenius R p n)) ((Polynomial.expand R (p ^ n)) f).roots p ^ n f.roots
          theorem Polynomial.roots_expand_map_frobenius_le {R : Type u_1} [CommRing R] [IsDomain R] (p : ) [ExpChar R p] (f : Polynomial R) :
          Multiset.map ((frobenius R p)) ((Polynomial.expand R p) f).roots p f.roots
          theorem Polynomial.roots_expand_pow_image_iterateFrobenius_subset {R : Type u_1} [CommRing R] [IsDomain R] (p : ) (n : ) [ExpChar R p] (f : Polynomial R) [DecidableEq R] :
          Finset.image ((iterateFrobenius R p n)) ((Polynomial.expand R (p ^ n)) f).roots.toFinset f.roots.toFinset
          theorem Polynomial.roots_expand_image_frobenius_subset {R : Type u_1} [CommRing R] [IsDomain R] (p : ) [ExpChar R p] (f : Polynomial R) [DecidableEq R] :
          Finset.image ((frobenius R p)) ((Polynomial.expand R p) f).roots.toFinset f.roots.toFinset
          theorem Polynomial.roots_expand_pow {R : Type u_1} [CommRing R] [IsDomain R] {p : } {n : } [ExpChar R p] {f : Polynomial R} [PerfectRing R p] :
          ((Polynomial.expand R (p ^ n)) f).roots = p ^ n Multiset.map ((iterateFrobeniusEquiv R p n).symm) f.roots
          theorem Polynomial.roots_expand {R : Type u_1} [CommRing R] [IsDomain R] {p : } [ExpChar R p] {f : Polynomial R} [PerfectRing R p] :
          ((Polynomial.expand R p) f).roots = p Multiset.map ((frobeniusEquiv R p).symm) f.roots
          theorem Polynomial.roots_X_pow_char_pow_sub_C {R : Type u_1} [CommRing R] [IsDomain R] {p : } {n : } [ExpChar R p] [PerfectRing R p] {y : R} :
          (Polynomial.X ^ p ^ n - Polynomial.C y).roots = p ^ n {(iterateFrobeniusEquiv R p n).symm y}
          theorem Polynomial.roots_X_pow_char_pow_sub_C_pow {R : Type u_1} [CommRing R] [IsDomain R] {p : } {n : } [ExpChar R p] [PerfectRing R p] {y : R} {m : } :
          ((Polynomial.X ^ p ^ n - Polynomial.C y) ^ m).roots = (m * p ^ n) {(iterateFrobeniusEquiv R p n).symm y}
          theorem Polynomial.roots_X_pow_char_sub_C {R : Type u_1} [CommRing R] [IsDomain R] {p : } [ExpChar R p] [PerfectRing R p] {y : R} :
          (Polynomial.X ^ p - Polynomial.C y).roots = p {(frobeniusEquiv R p).symm y}
          theorem Polynomial.roots_X_pow_char_sub_C_pow {R : Type u_1} [CommRing R] [IsDomain R] {p : } [ExpChar R p] [PerfectRing R p] {y : R} {m : } :
          ((Polynomial.X ^ p - Polynomial.C y) ^ m).roots = (m * p) {(frobeniusEquiv R p).symm y}
          theorem Polynomial.roots_expand_pow_map_iterateFrobenius {R : Type u_1} [CommRing R] [IsDomain R] {p : } {n : } [ExpChar R p] {f : Polynomial R} [PerfectRing R p] :
          Multiset.map ((iterateFrobenius R p n)) ((Polynomial.expand R (p ^ n)) f).roots = p ^ n f.roots
          theorem Polynomial.roots_expand_map_frobenius {R : Type u_1} [CommRing R] [IsDomain R] {p : } [ExpChar R p] {f : Polynomial R} [PerfectRing R p] :
          Multiset.map ((frobenius R p)) ((Polynomial.expand R p) f).roots = p f.roots
          theorem Polynomial.roots_expand_image_iterateFrobenius {R : Type u_1} [CommRing R] [IsDomain R] {p : } {n : } [ExpChar R p] {f : Polynomial R} [PerfectRing R p] [DecidableEq R] :
          Finset.image ((iterateFrobenius R p n)) ((Polynomial.expand R (p ^ n)) f).roots.toFinset = f.roots.toFinset
          theorem Polynomial.roots_expand_image_frobenius {R : Type u_1} [CommRing R] [IsDomain R] {p : } [ExpChar R p] {f : Polynomial R} [PerfectRing R p] [DecidableEq R] :
          Finset.image ((frobenius R p)) ((Polynomial.expand R p) f).roots.toFinset = f.roots.toFinset
          noncomputable def Polynomial.rootsExpandToRoots {R : Type u_1} [CommRing R] [IsDomain R] (p : ) [ExpChar R p] (f : Polynomial R) [DecidableEq R] :
          { x : R // x ((Polynomial.expand R p) f).roots.toFinset } { x : R // x f.roots.toFinset }

          If f is a polynomial over an integral domain R of characteristic p, then there is a map from the set of roots of Polynomial.expand R p f to the set of roots of f. It's given by x ↦ x ^ p, see rootsExpandToRoots_apply.

          Equations
          Instances For
            @[simp]
            theorem Polynomial.rootsExpandToRoots_apply {R : Type u_1} [CommRing R] [IsDomain R] (p : ) [ExpChar R p] (f : Polynomial R) [DecidableEq R] (x : { x : R // x ((Polynomial.expand R p) f).roots.toFinset }) :
            ((Polynomial.rootsExpandToRoots p f) x) = x ^ p
            noncomputable def Polynomial.rootsExpandPowToRoots {R : Type u_1} [CommRing R] [IsDomain R] (p : ) (n : ) [ExpChar R p] (f : Polynomial R) [DecidableEq R] :
            { x : R // x ((Polynomial.expand R (p ^ n)) f).roots.toFinset } { x : R // x f.roots.toFinset }

            If f is a polynomial over an integral domain R of characteristic p, then there is a map from the set of roots of Polynomial.expand R (p ^ n) f to the set of roots of f. It's given by x ↦ x ^ (p ^ n), see rootsExpandPowToRoots_apply.

            Equations
            Instances For
              @[simp]
              theorem Polynomial.rootsExpandPowToRoots_apply {R : Type u_1} [CommRing R] [IsDomain R] (p : ) (n : ) [ExpChar R p] (f : Polynomial R) [DecidableEq R] (x : { x : R // x ((Polynomial.expand R (p ^ n)) f).roots.toFinset }) :
              ((Polynomial.rootsExpandPowToRoots p n f) x) = x ^ p ^ n
              noncomputable def Polynomial.rootsExpandEquivRoots {R : Type u_1} [CommRing R] [IsDomain R] (p : ) [ExpChar R p] (f : Polynomial R) [PerfectRing R p] [DecidableEq R] :
              { x : R // x ((Polynomial.expand R p) f).roots.toFinset } { x : R // x f.roots.toFinset }

              If f is a polynomial over a perfect integral domain R of characteristic p, then there is a bijection from the set of roots of Polynomial.expand R p f to the set of roots of f. It's given by x ↦ x ^ p, see rootsExpandEquivRoots_apply.

              Equations
              Instances For
                @[simp]
                theorem Polynomial.rootsExpandEquivRoots_apply {R : Type u_1} [CommRing R] [IsDomain R] (p : ) [ExpChar R p] (f : Polynomial R) [PerfectRing R p] [DecidableEq R] (x : { x : R // x ((Polynomial.expand R p) f).roots.toFinset }) :
                noncomputable def Polynomial.rootsExpandPowEquivRoots {R : Type u_1} [CommRing R] [IsDomain R] (p : ) [ExpChar R p] (f : Polynomial R) [PerfectRing R p] [DecidableEq R] (n : ) :
                { x : R // x ((Polynomial.expand R (p ^ n)) f).roots.toFinset } { x : R // x f.roots.toFinset }

                If f is a polynomial over a perfect integral domain R of characteristic p, then there is a bijection from the set of roots of Polynomial.expand R (p ^ n) f to the set of roots of f. It's given by x ↦ x ^ (p ^ n), see rootsExpandPowEquivRoots_apply.

                Equations
                Instances For
                  @[simp]
                  theorem Polynomial.rootsExpandPowEquivRoots_apply {R : Type u_1} [CommRing R] [IsDomain R] (p : ) [ExpChar R p] (f : Polynomial R) [PerfectRing R p] [DecidableEq R] (n : ) (x : { x : R // x ((Polynomial.expand R (p ^ n)) f).roots.toFinset }) :
                  ((Polynomial.rootsExpandPowEquivRoots p f n) x) = x ^ p ^ n