Documentation

Mathlib.RingTheory.WittVector.Frobenius

The Frobenius operator #

If R has characteristic p, then there is a ring endomorphism frobenius R p that raises r : R to the power p. By applying WittVector.map to frobenius R p, we obtain a ring endomorphism 𝕎 R →+* 𝕎 R. It turns out that this endomorphism can be described by polynomials over that do not depend on R or the fact that it has characteristic p. In this way, we obtain a Frobenius endomorphism WittVector.frobeniusFun : 𝕎 R → 𝕎 R for every commutative ring R.

Unfortunately, the aforementioned polynomials can not be obtained using the machinery of wittStructureInt that was developed in StructurePolynomial.lean. We therefore have to define the polynomials by hand, and check that they have the required property.

In case R has characteristic p, we show in frobenius_eq_map_frobenius that WittVector.frobeniusFun is equal to WittVector.map (frobenius R p).

Main definitions and results #

TODO: Show that WittVector.frobeniusFun is a ring homomorphism, and bundle it into WittVector.frobenius.

References #

The rational polynomials that give the coefficients of frobenius x, in terms of the coefficients of x. These polynomials actually have integral coefficients, see frobeniusPoly and map_frobeniusPoly.

Equations
Instances For
    @[irreducible]
    noncomputable def WittVector.frobeniusPolyAux (p : ) [hp : Fact (Nat.Prime p)] :

    An auxiliary polynomial over the integers, that satisfies p * (frobeniusPolyAux p n) + X n ^ p = frobeniusPoly p n. This makes it easy to show that frobeniusPoly p n is congruent to X n ^ p modulo p.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem WittVector.frobeniusPolyAux_eq (p : ) [hp : Fact (Nat.Prime p)] (n : ) :
      WittVector.frobeniusPolyAux p n = MvPolynomial.X (n + 1) - iFinset.range n, jFinset.range (p ^ (n - i)), (MvPolynomial.X i ^ p) ^ (p ^ (n - i) - (j + 1)) * WittVector.frobeniusPolyAux p i ^ (j + 1) * MvPolynomial.C ((p ^ (n - i)).choose (j + 1) / p ^ (n - i - WittVector.pnat_multiplicity p j + 1, ) * p ^ (j - WittVector.pnat_multiplicity p j + 1, ))

      The polynomials that give the coefficients of frobenius x, in terms of the coefficients of x.

      Equations
      Instances For
        theorem WittVector.map_frobeniusPoly.key₁ (p : ) [hp : Fact (Nat.Prime p)] (n : ) (j : ) (hj : j < p ^ n) :
        p ^ (n - WittVector.pnat_multiplicity p j + 1, ) (p ^ n).choose (j + 1)

        A key divisibility fact for the proof of WittVector.map_frobeniusPoly.

        theorem WittVector.map_frobeniusPoly.key₂ (p : ) [hp : Fact (Nat.Prime p)] {n : } {i : } {j : } (hi : i n) (hj : j < p ^ (n - i)) :
        j - WittVector.pnat_multiplicity p j + 1, + n = i + j + (n - i - WittVector.pnat_multiplicity p j + 1, )

        A key numerical identity needed for the proof of WittVector.map_frobeniusPoly.

        def WittVector.frobeniusFun {p : } {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (x : WittVector p R) :

        frobeniusFun is the function underlying the ring endomorphism frobenius : 𝕎 R →+* frobenius 𝕎 R.

        Equations
        Instances For
          theorem WittVector.coeff_frobeniusFun {p : } {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (x : WittVector p R) (n : ) :
          x.frobeniusFun.coeff n = (MvPolynomial.aeval x.coeff) (WittVector.frobeniusPoly p n)
          instance WittVector.frobeniusFun_isPoly (p : ) [hp : Fact (Nat.Prime p)] :
          WittVector.IsPoly p fun (R : Type u_3) (_Rcr : CommRing R) => WittVector.frobeniusFun

          frobeniusFun is tautologically a polynomial function.

          See also frobenius_isPoly.

          Equations
          • =
          theorem WittVector.ghostComponent_frobeniusFun {p : } {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (n : ) (x : WittVector p R) :
          def WittVector.frobenius {p : } {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] :

          If R has characteristic p, then there is a ring endomorphism that raises r : R to the power p. By applying WittVector.map to this endomorphism, we obtain a ring endomorphism frobenius R p : 𝕎 R →+* 𝕎 R.

          The underlying function of this morphism is WittVector.frobeniusFun.

          Equations
          • WittVector.frobenius = { toFun := WittVector.frobeniusFun, map_one' := , map_mul' := , map_zero' := , map_add' := }
          Instances For
            theorem WittVector.coeff_frobenius {p : } {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (x : WittVector p R) (n : ) :
            (WittVector.frobenius x).coeff n = (MvPolynomial.aeval x.coeff) (WittVector.frobeniusPoly p n)
            theorem WittVector.ghostComponent_frobenius {p : } {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] (n : ) (x : WittVector p R) :
            (WittVector.ghostComponent n) (WittVector.frobenius x) = (WittVector.ghostComponent (n + 1)) x
            instance WittVector.frobenius_isPoly (p : ) [hp : Fact (Nat.Prime p)] :
            WittVector.IsPoly p fun (R : Type u_3) (_Rcr : CommRing R) => WittVector.frobenius

            frobenius is tautologically a polynomial function.

            Equations
            • =
            @[simp]
            theorem WittVector.coeff_frobenius_charP (p : ) {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] [CharP R p] (x : WittVector p R) (n : ) :
            (WittVector.frobenius x).coeff n = x.coeff n ^ p
            theorem WittVector.frobenius_eq_map_frobenius (p : ) {R : Type u_1} [hp : Fact (Nat.Prime p)] [CommRing R] [CharP R p] :
            WittVector.frobenius = WittVector.map (frobenius R p)
            @[simp]
            theorem WittVector.frobenius_zmodp (p : ) [hp : Fact (Nat.Prime p)] (x : WittVector p (ZMod p)) :
            WittVector.frobenius x = x
            @[simp]
            theorem WittVector.frobeniusEquiv_symm_apply (p : ) (R : Type u_1) [hp : Fact (Nat.Prime p)] [CommRing R] [CharP R p] [PerfectRing R p] :
            (WittVector.frobeniusEquiv p R).symm = (WittVector.map (frobeniusEquiv R p).symm)
            @[simp]
            theorem WittVector.frobeniusEquiv_apply (p : ) (R : Type u_1) [hp : Fact (Nat.Prime p)] [CommRing R] [CharP R p] [PerfectRing R p] :
            (WittVector.frobeniusEquiv p R) = WittVector.frobenius
            def WittVector.frobeniusEquiv (p : ) (R : Type u_1) [hp : Fact (Nat.Prime p)] [CommRing R] [CharP R p] [PerfectRing R p] :

            WittVector.frobenius as an equiv.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              theorem WittVector.frobenius_bijective (p : ) (R : Type u_1) [hp : Fact (Nat.Prime p)] [CommRing R] [CharP R p] [PerfectRing R p] :
              Function.Bijective WittVector.frobenius