WittVector.map_verschiebung
theorem WittVector.map_verschiebung :
∀ {p : ℕ} {R : Type u_1} {S : Type u_2} [hp : Fact p.Prime] [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S)
(x : WittVector p R),
(WittVector.map f) (WittVector.verschiebung x) = WittVector.verschiebung ((WittVector.map f) x)
The theorem `WittVector.map_verschiebung` is stating that for any prime number `p`, types `R` and `S` that form commutative rings, any ring homomorphism `f` from `R` to `S`, and any Witt vector `x` over `R`, the operation of first applying the `verschiebung` operation to `x` and then mapping the result using `f` is the same as first mapping `x` using `f` and then applying the `verschiebung` operation. In other words, the `verschiebung` operation is a natural transformation between the categories of Witt vectors over `R` and Witt vectors over `S`, where the functor is given by the `map` operation associated to `f`.
More concisely: For any prime number `p`, commutative rings `R` and `S`, ring homomorphism `f` from `R` to `S`, and Witt vectors `x` over `R`, the application of the `verschiebung` operation to `x` followed by mapping using `f` equals mapping `x` using `f` followed by applying the `verschiebung` operation.
|
WittVector.verschiebung_coeff_zero
theorem WittVector.verschiebung_coeff_zero :
∀ {p : ℕ} {R : Type u_1} [hp : Fact p.Prime] [inst : CommRing R] (x : WittVector p R),
(WittVector.verschiebung x).coeff 0 = 0
The theorem `WittVector.verschiebung_coeff_zero` states that for any prime number `p`, and any type `R` that is a commutative ring, the 0th coefficient of the verschiebung (or shift) of any Witt vector `x` with coefficients in `R` modulo `p` is always 0. In other words, when we apply the verschiebung operation, which shifts the coefficients of a Witt vector up by one, the new coefficient at position 0 is always 0.
More concisely: For any prime number p and commutative ring R, the 0th coefficient of the verschiebung of a Witt vector with coefficients in R modulo p is 0.
|
WittVector.verschiebung_coeff_succ
theorem WittVector.verschiebung_coeff_succ :
∀ {p : ℕ} {R : Type u_1} [hp : Fact p.Prime] [inst : CommRing R] (x : WittVector p R) (n : ℕ),
(WittVector.verschiebung x).coeff n.succ = x.coeff n
This theorem, `WittVector.verschiebung_coeff_succ`, states that for any natural number `p`, a type `R`, a Witt vector `x` of type `R` and `p` as its prime, and another natural number `n`, if `p` is a prime number and `R` is a commutative ring, then the coefficient of the (n+1)th term of the shifted Witt vector (achieved by the `verschiebung` operation on `x`) is equal to the coefficient of the nth term of the original Witt vector `x`. Essentially, this theorem captures how the `verschiebung` operation shifts coefficients up by one place in a Witt vector.
More concisely: For any prime number `p` and commutative ring `R`, the `(n+1)`th coefficient of the shifted Witt vector `verschiebung x` of Witt vector `x` over `R` with prime `p` equals the `n`th coefficient of `x`.
|
WittVector.verschiebung_isPoly
theorem WittVector.verschiebung_isPoly :
∀ {p : ℕ} [hp : Fact p.Prime], WittVector.IsPoly p fun R _Rcr => ⇑WittVector.verschiebung
The theorem `WittVector.verschiebung_isPoly` states that for every natural number `p` which is a prime number, the `verschiebung` operation on `WittVector` is a polynomial function. The `verschiebung` operation shifts the coefficients of a Witt vector up by one, by inserting 0 as the 0th coefficient, and is defined over all commutative rings.
More concisely: For every prime number `p`, the `verschiebung` operation on `WittVector` is a polynomial function.
|