Witt vectors over ̄ k as a Cohen ring with universal property
ProvedWittVector.exists_isDiscreteValuationRing_charZero_isAdicComplete_residueField_equiv_forall_existsUnique_ringHom_of_isAlgClosedLet be a prime and let be an algebraically closed field of characteristic . The assertion is that there exists a type carrying a commutative ring structure which is a domain, a discrete valuation ring and of characteristic zero, together with a -algebra structure on for which is adically complete with respect to the ideal generated by the image of and for which that ideal is maximal, a ring isomorphism from the residue field of onto , and a ring homomorphism from the ring of Witt vectors of the Galois field of order , such that the following holds: for every commutative local Artinian ring and every surjective ring homomorphism whose kernel is the maximal ideal of , there is a unique ring homomorphism with . No compatibility is imposed on beyond its existence; it is part of the data provided for later use, not constrained by the universal property.
This packages as a complete unramified discrete valuation ring of characteristic zero, with uniformiser and residue field , satisfying the universal property of a Cohen ring with respect to Artin local rings with residue field : it is the canonical coefficient ring for deformation-theoretic arguments. It is used in the construction of a two-dimensional regular tower with a versal pullback property for fake elliptic curves.
import Mathlib set_option maxHeartbeats 4000000 set_option synthInstance.maxHeartbeats 400000 set_option backward.isDefEq.respectTransparency.types false set_option autoImplicit false
theorem WittVector.exists_isDiscreteValuationRing_charZero_isAdicComplete_residueField_equiv_forall_existsUnique_ringHom_of_isAlgClosed
(q : ℕ) [Fact q.Prime] (kbar : Type) [Field kbar] [IsAlgClosed kbar] [CharP kbar q] :
∃ (O : Type) (_ : CommRing O) (_ : IsDomain O) (_ : IsDiscreteValuationRing O) (_ : CharZero O)
(_ : Algebra ℤ_[q] O) (_ : IsAdicComplete (Ideal.span {algebraMap ℤ_[q] O (q : ℤ_[q])}) O)
(_ : (Ideal.span {algebraMap ℤ_[q] O (q : ℤ_[q])}).IsMaximal)
(e : IsLocalRing.ResidueField O ≃+* kbar) (ι : WittVector q (GaloisField q 2) →+* O),
∀ (B : Type) [CommRing B] [IsLocalRing B] [IsArtinianRing B] (ρ : B →+* kbar),
Function.Surjective ρ → RingHom.ker ρ = IsLocalRing.maximalIdeal B →
∃! f : O →+* B, ρ.comp f = e.toRingHom.comp (IsLocalRing.residue O) := by sorry