Documentation

Mathlib.RingTheory.WittVector.Verschiebung

The Verschiebung operator #

References #

def WittVector.verschiebungFun {p : } {R : Type u_1} [CommRing R] (x : WittVector p R) :

verschiebungFun x shifts the coefficients of x up by one, by inserting 0 as the 0th coefficient. x.coeff i then becomes (verchiebungFun x).coeff (i + 1).

verschiebungFun is the underlying function of the additive monoid hom WittVector.verschiebung.

Equations
  • x.verschiebungFun = { coeff := fun (n : ) => if n = 0 then 0 else x.coeff (n - 1) }
Instances For
    theorem WittVector.verschiebungFun_coeff {p : } {R : Type u_1} [CommRing R] (x : WittVector p R) (n : ) :
    x.verschiebungFun.coeff n = if n = 0 then 0 else x.coeff (n - 1)
    theorem WittVector.verschiebungFun_coeff_zero {p : } {R : Type u_1} [CommRing R] (x : WittVector p R) :
    x.verschiebungFun.coeff 0 = 0
    @[simp]
    theorem WittVector.verschiebungFun_coeff_succ {p : } {R : Type u_1} [CommRing R] (x : WittVector p R) (n : ) :
    x.verschiebungFun.coeff n.succ = x.coeff n
    theorem WittVector.ghostComponent_zero_verschiebungFun {p : } {R : Type u_1} [hp : Fact p.Prime] [CommRing R] (x : WittVector p R) :
    (WittVector.ghostComponent 0) x.verschiebungFun = 0
    theorem WittVector.ghostComponent_verschiebungFun {p : } {R : Type u_1} [hp : Fact p.Prime] [CommRing R] (x : WittVector p R) (n : ) :
    (WittVector.ghostComponent (n + 1)) x.verschiebungFun = p * (WittVector.ghostComponent n) x

    The 0th Verschiebung polynomial is 0. For n > 0, the nth Verschiebung polynomial is the variable X (n-1).

    Equations
    Instances For
      theorem WittVector.aeval_verschiebung_poly' {p : } {R : Type u_1} [CommRing R] (x : WittVector p R) (n : ) :
      (MvPolynomial.aeval x.coeff) (WittVector.verschiebungPoly n) = x.verschiebungFun.coeff n
      instance WittVector.verschiebungFun_isPoly (p : ) :
      WittVector.IsPoly p fun (R : Type u_3) (_Rcr : CommRing R) => WittVector.verschiebungFun

      WittVector.verschiebung has polynomial structure given by WittVector.verschiebungPoly.

      Equations
      • =
      noncomputable def WittVector.verschiebung {p : } {R : Type u_1} [hp : Fact p.Prime] [CommRing R] :

      verschiebung x shifts the coefficients of x up by one, by inserting 0 as the 0th coefficient. x.coeff i then becomes (verchiebung x).coeff (i + 1).

      This is an additive monoid hom with underlying function verschiebung_fun.

      Equations
      • WittVector.verschiebung = { toFun := WittVector.verschiebungFun, map_zero' := , map_add' := }
      Instances For
        theorem WittVector.verschiebung_isPoly {p : } [hp : Fact p.Prime] :
        WittVector.IsPoly p fun (R : Type u_3) (_Rcr : CommRing R) => WittVector.verschiebung

        WittVector.verschiebung is a polynomial function.

        @[simp]
        theorem WittVector.map_verschiebung {p : } {R : Type u_1} {S : Type u_2} [hp : Fact p.Prime] [CommRing R] [CommRing S] (f : R →+* S) (x : WittVector p R) :
        (WittVector.map f) (WittVector.verschiebung x) = WittVector.verschiebung ((WittVector.map f) x)

        verschiebung is a natural transformation

        theorem WittVector.ghostComponent_zero_verschiebung {p : } {R : Type u_1} [hp : Fact p.Prime] [CommRing R] (x : WittVector p R) :
        (WittVector.ghostComponent 0) (WittVector.verschiebung x) = 0
        theorem WittVector.ghostComponent_verschiebung {p : } {R : Type u_1} [hp : Fact p.Prime] [CommRing R] (x : WittVector p R) (n : ) :
        (WittVector.ghostComponent (n + 1)) (WittVector.verschiebung x) = p * (WittVector.ghostComponent n) x
        @[simp]
        theorem WittVector.verschiebung_coeff_zero {p : } {R : Type u_1} [hp : Fact p.Prime] [CommRing R] (x : WittVector p R) :
        (WittVector.verschiebung x).coeff 0 = 0
        theorem WittVector.verschiebung_coeff_add_one {p : } {R : Type u_1} [hp : Fact p.Prime] [CommRing R] (x : WittVector p R) (n : ) :
        (WittVector.verschiebung x).coeff (n + 1) = x.coeff n
        @[simp]
        theorem WittVector.verschiebung_coeff_succ {p : } {R : Type u_1} [hp : Fact p.Prime] [CommRing R] (x : WittVector p R) (n : ) :
        (WittVector.verschiebung x).coeff n.succ = x.coeff n
        theorem WittVector.aeval_verschiebungPoly {p : } {R : Type u_1} [hp : Fact p.Prime] [CommRing R] (x : WittVector p R) (n : ) :
        (MvPolynomial.aeval x.coeff) (WittVector.verschiebungPoly n) = (WittVector.verschiebung x).coeff n