Witt vectors as the unique strict p-ring with residue ring k
ProvedWittVector.exists_ringEquiv_comp_eq_constantCoeff_of_isAdicCompleteLet be a prime and let be a commutative ring in which the image of lies in the submonoid of non-zero-divisors, so that multiplication by on is injective. Let be a commutative ring of characteristic which is perfect in the sense that the Frobenius endomorphism of is bijective, and suppose is given the structure of an -algebra whose structure map is surjective with kernel exactly the ideal generated by ; assume further that is complete and separated for the adic topology defined by the ideal generated by . Then there exists a ring isomorphism from the ring of -typical Witt vectors of onto such that followed by the structure map is the zeroth Witt coordinate , and is unique with this property even as a ring homomorphism: any ring homomorphism whose composite with is the zeroth Witt coordinate coincides with .
This is the classical structure theorem for strict -rings with perfect residue ring: such a ring is determined, up to a unique isomorphism compatible with reduction, by its residue ring, and the Witt vectors realise it. In this development it is used to identify an abstractly given -adically complete base ring with or with , in the two Čerednik–Drinfeld statements that cite it.
import Mathlib set_option maxHeartbeats 4000000 set_option synthInstance.maxHeartbeats 400000 set_option backward.isDefEq.respectTransparency.types false universe u v
theorem WittVector.exists_ringEquiv_comp_eq_constantCoeff_of_isAdicComplete
{𝓞 : Type u} [CommRing 𝓞] (p : ℕ) [Fact p.Prime] (hp : (p : 𝓞) ∈ nonZeroDivisors 𝓞)
{k : Type v} [CommRing k] [CharP k p] [PerfectRing k p] [Algebra 𝓞 k]
(hk : Function.Surjective (algebraMap 𝓞 k))
(hker : RingHom.ker (algebraMap 𝓞 k) = Ideal.span {(p : 𝓞)})
[IsAdicComplete (Ideal.span {(p : 𝓞)}) 𝓞] :
∃ e : WittVector p k ≃+* 𝓞,
(algebraMap 𝓞 k).comp e.toRingHom = WittVector.constantCoeff ∧
∀ g : WittVector p k →+* 𝓞,
(algebraMap 𝓞 k).comp g = WittVector.constantCoeff → g = e.toRingHom := by sorry