The Verschiebung operator #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
References #
def
witt_vector.verschiebung_fun
{p : ℕ}
{R : Type u_1}
[comm_ring R]
(x : witt_vector p R) :
witt_vector p R
verschiebung_fun x shifts the coefficients of x up by one,
by inserting 0 as the 0th coefficient.
x.coeff i then becomes (verchiebung_fun x).coeff (i + 1).
verschiebung_fun is the underlying function of the additive monoid hom witt_vector.verschiebung.
Instances for witt_vector.verschiebung_fun
theorem
witt_vector.verschiebung_fun_coeff
{p : ℕ}
{R : Type u_1}
[comm_ring R]
(x : witt_vector p R)
(n : ℕ) :
theorem
witt_vector.verschiebung_fun_coeff_zero
{p : ℕ}
{R : Type u_1}
[comm_ring R]
(x : witt_vector p R) :
x.verschiebung_fun.coeff 0 = 0
@[simp]
theorem
witt_vector.verschiebung_fun_coeff_succ
{p : ℕ}
{R : Type u_1}
[comm_ring R]
(x : witt_vector p R)
(n : ℕ) :
x.verschiebung_fun.coeff n.succ = x.coeff n
theorem
witt_vector.ghost_component_zero_verschiebung_fun
{p : ℕ}
{R : Type u_1}
[hp : fact (nat.prime p)]
[comm_ring R]
(x : witt_vector p R) :
theorem
witt_vector.ghost_component_verschiebung_fun
{p : ℕ}
{R : Type u_1}
[hp : fact (nat.prime p)]
[comm_ring R]
(x : witt_vector p R)
(n : ℕ) :
⇑(witt_vector.ghost_component (n + 1)) x.verschiebung_fun = ↑p * ⇑(witt_vector.ghost_component n) x
The 0th Verschiebung polynomial is 0. For n > 0, the nth Verschiebung polynomial is the
variable X (n-1).
Equations
- witt_vector.verschiebung_poly n = ite (n = 0) 0 (mv_polynomial.X (n - 1))
theorem
witt_vector.aeval_verschiebung_poly'
{p : ℕ}
{R : Type u_1}
[comm_ring R]
(x : witt_vector p R)
(n : ℕ) :
theorem
witt_vector.verschiebung_fun_is_poly
(p : ℕ) :
witt_vector.is_poly p (λ (R : Type u_1) (_Rcr : comm_ring R), witt_vector.verschiebung_fun)
witt_vector.verschiebung has polynomial structure given by witt_vector.verschiebung_poly.
@[instance]
def
witt_vector.verschiebung_fun_is_poly.comp₂_i
(p : ℕ)
(f : Π ⦃R : Type u_1⦄ [_inst_3 : comm_ring R], witt_vector p R → witt_vector p R → witt_vector p R)
[hf : witt_vector.is_poly₂ p f] :
witt_vector.is_poly₂ p (λ (R : Type u_1) (_Rcr : comm_ring R) (x y : witt_vector p R), (λ (R : Type u_1) (_Rcr : comm_ring R), witt_vector.verschiebung_fun) R _Rcr (f x y))
@[instance]
def
witt_vector.verschiebung_fun_is_poly.comp_i
(p : ℕ)
(f : Π ⦃R : Type u_1⦄ [_inst_3 : comm_ring R], witt_vector p R → witt_vector p R)
[hf : witt_vector.is_poly p f] :
witt_vector.is_poly p (λ (R : Type u_1) (_Rcr : comm_ring R), (λ (R : Type u_1) (_Rcr : comm_ring R), witt_vector.verschiebung_fun) R _Rcr ∘ f)
def
witt_vector.verschiebung
{p : ℕ}
{R : Type u_1}
[hp : fact (nat.prime p)]
[comm_ring R] :
witt_vector p R →+ witt_vector p 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 a additive monoid hom with underlying function verschiebung_fun.
Equations
- witt_vector.verschiebung = {to_fun := witt_vector.verschiebung_fun _inst_1, map_zero' := _, map_add' := _}
theorem
witt_vector.verschiebung_is_poly
{p : ℕ}
[hp : fact (nat.prime p)] :
witt_vector.is_poly p (λ (R : Type u_1) (_Rcr : comm_ring R), ⇑witt_vector.verschiebung)
witt_vector.verschiebung is a polynomial function.
@[instance]
def
witt_vector.verschiebung_is_poly.comp_i
{p : ℕ}
[hp : fact (nat.prime p)]
(f : Π ⦃R : Type u_1⦄ [_inst_3 : comm_ring R], witt_vector p R → witt_vector p R)
[hf : witt_vector.is_poly p f] :
witt_vector.is_poly p (λ (R : Type u_1) (_Rcr : comm_ring R), (λ (R : Type u_1) (_Rcr : comm_ring R), ⇑witt_vector.verschiebung) R _Rcr ∘ f)
@[instance]
def
witt_vector.verschiebung_is_poly.comp₂_i
{p : ℕ}
[hp : fact (nat.prime p)]
(f : Π ⦃R : Type u_1⦄ [_inst_3 : comm_ring R], witt_vector p R → witt_vector p R → witt_vector p R)
[hf : witt_vector.is_poly₂ p f] :
witt_vector.is_poly₂ p (λ (R : Type u_1) (_Rcr : comm_ring R) (x y : witt_vector p R), (λ (R : Type u_1) (_Rcr : comm_ring R), ⇑witt_vector.verschiebung) R _Rcr (f x y))
@[simp]
theorem
witt_vector.map_verschiebung
{p : ℕ}
{R : Type u_1}
{S : Type u_2}
[hp : fact (nat.prime p)]
[comm_ring R]
[comm_ring S]
(f : R →+* S)
(x : witt_vector p R) :
verschiebung is a natural transformation
theorem
witt_vector.ghost_component_zero_verschiebung
{p : ℕ}
{R : Type u_1}
[hp : fact (nat.prime p)]
[comm_ring R]
(x : witt_vector p R) :
theorem
witt_vector.ghost_component_verschiebung
{p : ℕ}
{R : Type u_1}
[hp : fact (nat.prime p)]
[comm_ring R]
(x : witt_vector p R)
(n : ℕ) :
⇑(witt_vector.ghost_component (n + 1)) (⇑witt_vector.verschiebung x) = ↑p * ⇑(witt_vector.ghost_component n) x
@[simp]
theorem
witt_vector.verschiebung_coeff_zero
{p : ℕ}
{R : Type u_1}
[hp : fact (nat.prime p)]
[comm_ring R]
(x : witt_vector p R) :
(⇑witt_vector.verschiebung x).coeff 0 = 0
theorem
witt_vector.verschiebung_coeff_add_one
{p : ℕ}
{R : Type u_1}
[hp : fact (nat.prime p)]
[comm_ring R]
(x : witt_vector p R)
(n : ℕ) :
@[simp]
theorem
witt_vector.verschiebung_coeff_succ
{p : ℕ}
{R : Type u_1}
[hp : fact (nat.prime p)]
[comm_ring R]
(x : witt_vector p R)
(n : ℕ) :
theorem
witt_vector.aeval_verschiebung_poly
{p : ℕ}
{R : Type u_1}
[hp : fact (nat.prime p)]
[comm_ring R]
(x : witt_vector p R)
(n : ℕ) :
@[simp]
theorem
witt_vector.bind₁_verschiebung_poly_witt_polynomial
{p : ℕ}
[hp : fact (nat.prime p)]
(n : ℕ) :
⇑(mv_polynomial.bind₁ witt_vector.verschiebung_poly) (witt_polynomial p ℤ n) = ite (n = 0) 0 (↑p * witt_polynomial p ℤ (n - 1))