WittVector.lift_unique
theorem WittVector.lift_unique :
∀ {p : ℕ} [hp : Fact p.Prime] {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : Semiring S]
{f : (k : ℕ) → S →+* TruncatedWittVector p k R}
(f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁)
(g : S →+* WittVector p R),
(∀ (k : ℕ), (WittVector.truncate k).comp g = f k) → WittVector.lift (fun k₂ => f k₂) f_compat = g
The theorem `WittVector.lift_unique` states the uniqueness part of the universal property of Witt vectors. Specifically, for a given prime number `p`, suppose we have a commutative ring `R`, a semiring `S`, and a compatible system of ring homomorphisms `f` from `S` to the truncated Witt vectors of varying lengths over `R`. If we have another ring homomorphism `g` from `S` to the Witt vectors over `R` such that its truncations agree with `f` at every length, then `g` is uniquely determined by the lift of `f` through the universal property of Witt vectors.
More concisely: Given a prime number `p`, a commutative ring `R`, a semiring `S`, and compatible ring homomorphisms `f` from `S` to the truncated Witt vectors over `R`, if another homomorphism `g` from `S` to the Witt vectors over `R` agrees with `f` on all truncations, then `g` is equal to the unique lift of `f` to the Witt vectors.
|
WittVector.truncate_surjective
theorem WittVector.truncate_surjective :
∀ (p : ℕ) [hp : Fact p.Prime] (n : ℕ) (R : Type u_1) [inst : CommRing R],
Function.Surjective ⇑(WittVector.truncate n)
This theorem states that for any prime number `p`, any natural number `n`, and any commutative ring `R`, the function `WittVector.truncate n` is surjective. In more mathematical terminology, given any `TruncatedWittVector` over the ring `R` with base `p` and length `n`, there exists a `WittVector` over the ring `R` with base `p` whose truncation to the first `n` entries equals the given `TruncatedWittVector`. This means that `WittVector.truncate n` maps onto the entire set of `n`-length `TruncatedWittVector`s.
More concisely: For any prime number `p`, any natural number `n`, and any commutative ring `R`, the function `WittVector.truncate n` maps every `n`-length `TruncatedWittVector` over `R` with base `p` to some `WittVector` over `R` with base `p`.
|
WittVector.coeff_truncateFun
theorem WittVector.coeff_truncateFun :
∀ {p n : ℕ} {R : Type u_1} (x : WittVector p R) (i : Fin n),
TruncatedWittVector.coeff i (WittVector.truncateFun n x) = x.coeff ↑i
This theorem states that for any given prime number `p`, any nonnegative integer `n`, any type `R`, any Witt vector `x` of type `R` and base `p`, and any index `i` which is less than `n`, the `i`th coefficient of the truncated Witt vector obtained from `x` by the function `WittVector.truncateFun` is equal to the `i`th coefficient of the original Witt vector `x`. In other words, the truncation operation preserves the `i`th coefficient of the Witt vector.
More concisely: For any prime number `p`, type `R`, Witt vector `x` of type `WittVector R p`, and index `i` less than the length of `x`, the `i`th coefficient of `WittVector.truncateFun x` equals the `i`th coefficient of `x`.
|
TruncatedWittVector.truncate_wittVector_truncate
theorem TruncatedWittVector.truncate_wittVector_truncate :
∀ {p : ℕ} [hp : Fact p.Prime] {n : ℕ} {R : Type u_1} [inst : CommRing R] {m : ℕ} (hm : n ≤ m) (x : WittVector p R),
(TruncatedWittVector.truncate hm) ((WittVector.truncate m) x) = (WittVector.truncate n) x
The theorem `TruncatedWittVector.truncate_wittVector_truncate` states that for any natural number `p` which is prime, a natural number `n`, a type `R` that forms a commutative ring, and a natural number `m` such that `n` is less than or equal to `m`, the operation of truncating a Witt vector `x` to `m` entries and then applying `TruncatedWittVector.truncate` operation with respect to `m` is equivalent to directly truncating the Witt vector `x` to `n` entries. In other words, it doesn't matter whether we truncate a Witt vector to `m` entries first and then truncate it to `n` entries or if we directly truncate it to `n` entries; both operations yield the same result.
More concisely: For any prime number p, commutative ring R, and natural numbers m (≥ n), the operation of truncating a Witt vector in R to m entries and then truncating it to n entries is equal to directly truncating it to n entries.
|
TruncatedWittVector.truncateFun_out
theorem TruncatedWittVector.truncateFun_out :
∀ {p n : ℕ} {R : Type u_1} [inst : CommRing R] (x : TruncatedWittVector p n R),
WittVector.truncateFun n x.out = x
The theorem `TruncatedWittVector.truncateFun_out` states that for any natural number `p` and `n` and any type `R` that forms a commutative ring, if we take any truncated Witt vector `x`, convert it into a full Witt vector using the `out` function, and then truncate it back to the original size using the `truncateFun` function, we will end up with the original truncated Witt vector `x`. This theorem shows that the operations of truncating and extending Witt vectors commute with each other.
More concisely: For any natural numbers `p` and `n`, and commutative ring `R`, the truncation and extension functions for truncated Witt vectors commute: `TruncatedWittVector.truncateFun (TruncatedWittVector.out R p n x) = x`.
|
TruncatedWittVector.out_injective
theorem TruncatedWittVector.out_injective :
∀ {p n : ℕ} {R : Type u_1} [inst : CommRing R], Function.Injective TruncatedWittVector.out
The theorem `TruncatedWittVector.out_injective` states that for all natural numbers `p` and `n`, and for any type `R` with a commutative ring structure, the function `TruncatedWittVector.out` is injective. In other words, if we have two truncated Witt vectors and applying the `out` function to both of them gives the same Witt vector, then the original truncated Witt vectors must have been the same. This function `out` turns a truncated Witt vector into a Witt vector by setting all coefficients after the vector to be 0.
More concisely: For all natural numbers `p` and `n` and commutative rings `R`, the function `TruncatedWittVector.out` maps distinct truncated Witt vectors of length `n` in `R` to distinct Witt vectors.
|
TruncatedWittVector.ext
theorem TruncatedWittVector.ext :
∀ {p n : ℕ} {R : Type u_1} {x y : TruncatedWittVector p n R},
(∀ (i : Fin n), TruncatedWittVector.coeff i x = TruncatedWittVector.coeff i y) → x = y
The theorem `TruncatedWittVector.ext` states that for any two truncated Witt vectors `x` and `y` of the same parameters `p`, `n`, and `R`, if all their corresponding coefficients are equal (i.e., for each index `i` within the bounds of `n`, the `i`th coefficient of `x` equals the `i`th coefficient of `y`), then the two truncated Witt vectors `x` and `y` are indeed the same. This theorem is essentially about the equality of truncated Witt vectors in terms of their coefficients.
More concisely: If two truncated Witt vectors of the same parameters and equal coefficients correspondently indexed within their bounds are given, then they are equal.
|
TruncatedWittVector.truncate_comp_wittVector_truncate
theorem TruncatedWittVector.truncate_comp_wittVector_truncate :
∀ {p : ℕ} [hp : Fact p.Prime] {n : ℕ} {R : Type u_1} [inst : CommRing R] {m : ℕ} (hm : n ≤ m),
(TruncatedWittVector.truncate hm).comp (WittVector.truncate m) = WittVector.truncate n
This theorem, `TruncatedWittVector.truncate_comp_wittVector_truncate`, states that for any natural number `p` that is prime, any natural number `n`, any commutative ring `R`, and any natural number `m` such that `n` is less than or equal to `m`, the composition of the ring homomorphism that truncates a truncated Witt vector of length `m` to a truncated Witt vector of length `n` and the ring homomorphism that truncates a Witt vector to its first `m` entries to obtain a truncated Witt vector is equal to the ring homomorphism that truncates a Witt vector to its first `n` entries to obtain a truncated Witt vector. In other words, truncating a Witt vector to length `m` and then truncating the result to length `n` is the same as directly truncating the original Witt vector to length `n`.
More concisely: For any prime number p, commutative ring R, and natural numbers n ≤ m, the truncation map of Witt vectors of length m followed by the truncation map of length n is equal to the truncation map of length n.
|
WittVector.truncate_comp_lift
theorem WittVector.truncate_comp_lift :
∀ {p : ℕ} [hp : Fact p.Prime] (n : ℕ) {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : Semiring S]
{f : (k : ℕ) → S →+* TruncatedWittVector p k R}
(f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁),
(WittVector.truncate n).comp (WittVector.lift (fun k₂ => f k₂) f_compat) = f n
The theorem `WittVector.truncate_comp_lift` states that for a given prime number `p`, a natural number `n`, a commutative ring `R`, a semiring `S`, and a family of ring homomorphisms `f` from `S` to the set of truncated Witt vectors of `R` with varying lengths, if the homomorphisms `f` are compatible (i.e., composing `f` at length `k₂` with the truncation function from length `k₂` to `k₁` yields `f` at length `k₁`), then composing the function that lifts the family `f` to a ring homomorphism on the Witt vectors of `R` with the truncation function to length `n` is equivalent to the ring homomorphism `f` at length `n`. This theorem essentially states the compatibility of the lift operation with the truncation operation in the context of Witt vectors.
More concisely: Given a prime number `p`, a natural number `n`, a commutative ring `R`, a semiring `S`, and a family of ring homomorphisms `f` from `S` to the truncated Witt vectors of `R` with compatible lengths, the lift of `f` to a ring homomorphism on the Witt vectors of `R` and the truncation function to length `n` are equal.
|
WittVector.out_truncateFun
theorem WittVector.out_truncateFun :
∀ {p n : ℕ} {R : Type u_1} [inst : CommRing R] (x : WittVector p R),
(WittVector.truncateFun n x).out = WittVector.init n x
The theorem `WittVector.out_truncateFun` states that for any natural numbers `p` and `n`, and any commutative ring `R`, for any Witt vector `x` with base `p` and coefficients from `R`, if we first truncate `x` to its first `n` entries using the `truncateFun` to get a truncated Witt vector, and then convert this truncated Witt vector back to a normal Witt vector using `TruncatedWittVector.out`, we will end up with the same result as if we had just directly initialized a new Witt vector with the first `n` coefficients of `x` and all other coefficients set to zero, using `WittVector.init`. In other words, it proves the equivalence between the sequence of truncation and out operations and the initialization of a Witt vector, when dealing with the first `n` entries of a Witt vector.
More concisely: For any commutative ring R, natural numbers p, n, and Witt vector x with base p and coefficients from R, the result of truncating x to its first n entries using `truncateFun` and then converting back to a Witt vector is equal to the Witt vector initialized with the first n coefficients of x and all other coefficients set to zero.
|
WittVector.coeff_truncate
theorem WittVector.coeff_truncate :
∀ {p : ℕ} [hp : Fact p.Prime] {n : ℕ} {R : Type u_1} [inst : CommRing R] (x : WittVector p R) (i : Fin n),
TruncatedWittVector.coeff i ((WittVector.truncate n) x) = x.coeff ↑i
The theorem `WittVector.coeff_truncate` states that for any natural number `p` which is a prime, any natural number `n`, any type `R` that is a commutative ring, any `x` which is a Witt vector over `R` with base `p`, and any `i` which is a finite ordinal less than `n`, the `i`th coefficient of the truncated Witt vector obtained by truncating `x` to its first `n` entries is equal to the `i`th coefficient of `x`. This essentially says that the truncation operation properly preserves the coefficients of the Witt vector up to the truncation index `n`.
More concisely: For any prime number p, natural number n, commutative ring R, Witt vector x over R with base p, and finite ordinal i < n, the i-th coefficient of the truncated Witt vector of x to length n equals the i-th coefficient of x.
|