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.

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.

    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 x_1 x_2 => WittVector.select P x_2
      theorem WittVector.select_add_select_not {p : } [hp : Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] (P : Prop) (x : WittVector p R) :
      WittVector.select P x + WittVector.select (fun i => ¬P i) x = x
      theorem WittVector.coeff_add_of_disjoint {p : } [hp : Fact (Nat.Prime p)] (n : ) {R : Type u_1} [CommRing R] (x : WittVector p R) (y : WittVector p R) (h : ∀ (n : ), WittVector.coeff x n = 0 WittVector.coeff y n = 0) :
      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.

      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.

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

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

          Instances For
            @[simp]
            theorem WittVector.init_init {p : } {R : Type u_1} [CommRing R] (x : WittVector p R) (n : ) :
            theorem WittVector.init_add {p : } [hp : Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] (x : WittVector p R) (y : WittVector p R) (n : ) :
            theorem WittVector.init_mul {p : } [hp : Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] (x : WittVector p R) (y : WittVector p R) (n : ) :
            theorem WittVector.init_neg {p : } [hp : Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] (x : WittVector p R) (n : ) :
            theorem WittVector.init_sub {p : } [hp : Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] (x : WittVector p R) (y : WittVector p R) (n : ) :
            theorem WittVector.init_nsmul {p : } [hp : Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] (m : ) (x : WittVector p R) (n : ) :
            theorem WittVector.init_zsmul {p : } [hp : Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] (m : ) (x : WittVector p R) (n : ) :
            theorem WittVector.init_pow {p : } [hp : Fact (Nat.Prime p)] {R : Type u_1} [CommRing R] (m : ) (x : WittVector p R) (n : ) :
            theorem WittVector.init_isPoly (p : ) (n : ) :

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