Documentation

Mathlib.RingTheory.WittVector.InitTail

init and tail #

Given a Witt vector x, we are sometimes interested in its components before and after an index n. This file defines those operations, proves that init is polynomial, and shows how that polynomial interacts with MvPolynomial.bind₁.

Main declarations #

References #

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

WittVector.select P x, for a predicate P : ℕ → Prop is the Witt vector whose n-th coefficient is x.coeff n if P n is true, and 0 otherwise.

Equations
Instances For

    The polynomial that witnesses that WittVector.select is a polynomial function. selectPoly n is X n if P n holds, and 0 otherwise.

    Equations
    Instances For
      theorem WittVector.coeff_select {p : } {R : Type u_1} [CommRing R] (P : Prop) (x : WittVector p R) (n : ) :
      instance WittVector.select_isPoly {p : } {P : Prop} :
      WittVector.IsPoly p fun (x : Type u_2) (x_1 : CommRing x) (x_2 : WittVector p x) => WittVector.select P x_2
      Equations
      • =
      theorem WittVector.select_add_select_not {p : } {R : Type u_1} [CommRing R] (P : Prop) [hp : Fact (Nat.Prime p)] (x : WittVector p R) :
      WittVector.select P x + WittVector.select (fun (i : ) => ¬P i) x = x
      theorem WittVector.coeff_add_of_disjoint {p : } (n : ) {R : Type u_1} [CommRing R] [hp : Fact (Nat.Prime p)] (x : WittVector p R) (y : WittVector p R) (h : ∀ (n : ), x.coeff n = 0 y.coeff n = 0) :
      (x + y).coeff n = x.coeff n + y.coeff n
      def WittVector.init {p : } {R : Type u_1} [CommRing R] (n : ) :

      WittVector.init n x is the Witt vector of which the first n coefficients are those from x and all other coefficients are 0. See WittVector.tail for the complementary part.

      Equations
      Instances For
        def WittVector.tail {p : } {R : Type u_1} [CommRing R] (n : ) :

        WittVector.tail n x is the Witt vector of which the first n coefficients are 0 and all other coefficients are those from x. See WittVector.init for the complementary part.

        Equations
        Instances For
          @[simp]
          theorem WittVector.init_add_tail {p : } {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] (x : WittVector p R) (n : ) :

          init_ring is an auxiliary tactic that discharges goals factoring init over ring operations.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem WittVector.init_init {p : } {R : Type u_1} [CommRing R] (x : WittVector p R) (n : ) :
            theorem WittVector.init_add {p : } {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] (x : WittVector p R) (y : WittVector p R) (n : ) :
            theorem WittVector.init_mul {p : } {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] (x : WittVector p R) (y : WittVector p R) (n : ) :
            theorem WittVector.init_neg {p : } {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] (x : WittVector p R) (n : ) :
            theorem WittVector.init_sub {p : } {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] (x : WittVector p R) (y : WittVector p R) (n : ) :
            theorem WittVector.init_nsmul {p : } {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] (m : ) (x : WittVector p R) (n : ) :
            theorem WittVector.init_zsmul {p : } {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] (m : ) (x : WittVector p R) (n : ) :
            theorem WittVector.init_pow {p : } {R : Type u_1} [CommRing R] [Fact (Nat.Prime p)] (m : ) (x : WittVector p R) (n : ) :
            theorem WittVector.init_isPoly (p : ) (n : ) :
            WittVector.IsPoly p fun (x : Type u_2) (x_1 : CommRing x) => WittVector.init n

            WittVector.init n x is polynomial in the coefficients of x.