Theorems · Definition · commutative algebra

TruncatedWittVector

ℕ → ℕ → Type u_2 → Type u_2

A truncated Witt vector over R is a vector of elements of R, i.e., the first n coefficients of a Witt vector. We will define operations on this type that are compatible with the (untruncated) Witt vector operations. TruncatedWittVector p n R takes a parameter p : ℕ that is not used in the definition. In practice, this number p is assumed to be a prime number, and under this assumption we construct a ring structure on TruncatedWittVector p n R. (TruncatedWittVector p₁ n R and TruncatedWittVector p₂ n R are definitionally equal as types but will have different ring operations.)

Defined in

Mathlib.RingTheory.WittVector.Truncated

Cited by

56 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms