Algebras over Witt vectors

Stream: Is there code for X?

[Kevin Buzzard]

Is it true that given an Artin local ring with perfect residue field k of characteristic p, this Artin ring inherits a canonical W(k)-algebra structure? Do we have this construction in mathlib?

I've got a student (@Sebastian Monnet) working on Mazur's deformation theory.

[Johan Commelin]

Nope, we don't have this. (I don't even know if it's true...)

[Johan Commelin]

We don't really have the universal property of Witt vectors in that direction.