Witt vectors

TheoremGhost components determine Witt vector coefficients#✓fully proved

Ghost components determine Witt vector coefficients when p is a non-zero-divisor.

theorem WittVector.coeff_eq_coeff_of_forall_ghostComponent_eq {R : Type u}
    [CommRing R] (p : ℕ) [Fact p.Prime] (hp : (p : R) ∈ nonZeroDivisors R)
    (n : ℕ) (x y : WittVector p R)
    (h : ∀ k < n, WittVector.ghostComponent k x = WittVector.ghostComponent k y) :
    ∀ k < n, x.coeff k = y.coeff k

TheoremGhost data compatible with a Frobenius lift come from a Witt vector#✓fully proved

Compatible ghost data with a Frobenius lift is realized by a Witt vector.

theorem WittVector.exists_forall_ghostComponent_eq_of_sub_frobeniusLift_mem
    {R : Type u} [CommRing R] (p : ℕ) [Fact p.Prime] (σ : R →+* R)
    (hσ : ∀ a : R, σ a - a ^ p ∈ Ideal.span {(p : R)})
    (n : ℕ) (g : ℕ → R)
    (hg : ∀ k : ℕ, k + 1 < n → g (k + 1) - σ (g k) ∈ Ideal.span {(p : R) ^ (k + 1)}) :
    ∃ x : WittVector p R, ∀ k < n, WittVector.ghostComponent k x = g k

TheoremHomomorphisms from Witt vectors over finite fields commute with Frobenius#✓fully proved

Ring homomorphisms out of Witt vectors over a finite field commute with Frobenius.

theorem WittVector.ringHom_map_frobenius_of_finite (p : ℕ) [Fact p.Prime]
    {F : Type u} [Field F] [Finite F] [CharP F p] {k : Type v} [CommRing k] [CharP k p]
    [PerfectRing k p] (ι : WittVector p F →+* WittVector p k) (x : WittVector p F) :
    ι (WittVector.frobenius x) = WittVector.frobenius (ι x)

TheoremDivisibility of Witt coefficients from divisible ghost components#✓fully proved

If a ghost component of a Witt vector is highly p-divisible and the reduction mod p is reduced, all lower coefficients lie in (p).

theorem WittVector.coeff_mem_span_of_ghostComponent_mem_span_pow_of_isReduced
    {S : Type u} [CommRing S] (p : ℕ) [Fact p.Prime] (hp : (p : S) ∈ nonZeroDivisors S)
    (hred : IsReduced (S ⧸ Ideal.span {(p : S)}))
    (z : WittVector p S) (N : ℕ)
    (hz : WittVector.ghostComponent (N - 1) z ∈ Ideal.span {(p : S) ^ N}) :
    ∀ j : ℕ, j < N → z.coeff j ∈ Ideal.span {(p : S)}

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.