WittVector.iterate_verschiebung_mul_coeff
theorem WittVector.iterate_verschiebung_mul_coeff :
∀ {p : ℕ} {R : Type u_1} [hp : Fact p.Prime] [inst : CommRing R] [inst_1 : CharP R p] (x y : WittVector p R)
(i j : ℕ),
((⇑WittVector.verschiebung)^[i] x * (⇑WittVector.verschiebung)^[j] y).coeff (i + j) =
x.coeff 0 ^ p ^ j * y.coeff 0 ^ p ^ i
This theorem is a specialized form of an equation found in Hazewinkel's work on Witt Vectors. Given a prime number `p` and a commutative ring `R` with characteristic `p`, the theorem establishes a relationship between the coefficients of Witt vectors `x` and `y` under repeated applications of the Verschiebung operation. Specifically, for any non-negative integers `i` and `j`, the coefficient at index `i + j` of the product of `x` and `y` after `i` and `j` iterations of Verschiebung, respectively, equals the `i`-th power of the `j`-th power of the 0th coefficient of `x` times the `j`-th power of the `i`-th power of the 0th coefficient of `y`. In mathematical notation, if $V$ denotes the Verschiebung operation, then this theorem states that
$(V^i x)(V^j y)_{i + j} = x_0^{p^j} y_0^{p^i}$.
More concisely: Given a prime number `p` and commutative rings `R` with characteristic `p`, for all non-negative integers `i` and `j`, the `(i + j)`-th coefficient of the product of Witt vectors `x` and `y` after `i` and `j` applications of the Verschiebung operation, respectively, equals the `i`-th power of the zero coefficient of `x` raised to the power of `p^j`, multiplied by the `j`-th power of the zero coefficient of `y` raised to the power of `p^i`.
|
WittVector.frobenius_verschiebung
theorem WittVector.frobenius_verschiebung :
∀ {p : ℕ} {R : Type u_1} [hp : Fact p.Prime] [inst : CommRing R] (x : WittVector p R),
WittVector.frobenius (WittVector.verschiebung x) = x * ↑p
The theorem `WittVector.frobenius_verschiebung` states that for every natural number `p` that is prime, and for any commutative ring `R`, the composition of the Frobenius and Verschiebung operations on any Witt vector `x` from `R` with `p` components, is equivalent to multiplying the Witt vector `x` by `p`. In other words, applying the Frobenius operation to the result of the Verschiebung operation on `x` gives the same result as multiplying `x` by `p`.
More concisely: For any prime number p and commutative ring R, the composition of the Verschiebung and Frobenius operations on a Witt vector x of length p over R equals x multiplied by p.
|
WittVector.verschiebung_zmod
theorem WittVector.verschiebung_zmod :
∀ {p : ℕ} [hp : Fact p.Prime] (x : WittVector p (ZMod p)), WittVector.verschiebung x = x * ↑p
The theorem `WittVector.verschiebung_zmod` states that, for any prime number `p` and any Witt vector `x` over the ring of integers modulo `p`, the operation of Verschiebung (which shifts the coefficients of `x` up by one, inserting 0 as the 0th coefficient) is equivalent to multiplying `x` by `p`. In other words, the result of applying the Verschiebung operation to `x` is the same as the result of multiplying `x` by `p` in the ring of Witt vectors of integers modulo `p`.
More concisely: For any prime number p and Witt vector x over the ring of integers modulo p, Verschiebung(x) = p * x in the ring of Witt vectors.
|
WittVector.verschiebung_mul_frobenius
theorem WittVector.verschiebung_mul_frobenius :
∀ {p : ℕ} {R : Type u_1} [hp : Fact p.Prime] [inst : CommRing R] (x y : WittVector p R),
WittVector.verschiebung (x * WittVector.frobenius y) = WittVector.verschiebung x * y
This theorem, termed as the "projection formula" for Frobenius and Verschiebung, states that for any natural number 'p' which is prime, any type 'R' that forms a commutative ring, and any two Witt vectors 'x' and 'y' of type 'R' with 'p' coefficients, the Verschiebung (which shifts coefficients upwards by one) of the product of 'x' and the Frobenius (which raises each coefficient to the power 'p') of 'y' is equal to the product of the Verschiebung of 'x' and 'y'. In other words, Verschiebung and Frobenius operations distribute over multiplication in Witt vectors.
More concisely: For any prime number p and commutative ring R, the Verschiebung and Frobenius operations distribute over multiplication in Witt vectors, i.e., (Frobenius x)∘Verschiebung y = Verschiebung x∘Frobenius y.
|