English
There is a natural bijection between compatible families of ring homomorphisms f_k: S → TruncatedWittVector p k R (compatible under truncation maps) and ring homomorphisms g: S → 𝕎R. The forward map sends (f, f_compat) to lift f f_compat; the inverse sends a morphism g to the family k ↦ (truncate k) ∘ g. This equivalence is natural in all variables.
Русский
Существует естественное биективное соответствие между совместимыми семьями гомоморфизмов f_k: S → TruncatedWittVector p k R и гомоморфизмами g: S → 𝕎R: g ↦ (truncate k) ∘ g образует семью; обратное отображение берет g к семейству f_k = (truncate k) ∘ g. Это эквивалентность между системами ограничений и гомоморфизмами в 𝕎R.
LaTeX
$$$$ \\text{liftEquiv} : \\{ f : \\forall k, S \\to^+ TruncatedWittVector(p,k,R) \\mid \\forall k_1,k_2, hk, (truncate hk) \\circ (f k_2) = f k_1 \\} \\cong (S \\to^+ 𝕎R). $$$$
Lean4
/-- The universal property of `𝕎 R` as projective limit of truncated Witt vector rings. -/
@[simps]
def liftEquiv :
{ f : ∀ k, S →+* TruncatedWittVector p k R //
∀ (k₁ k₂) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁ } ≃
(S →+* 𝕎 R)
where
toFun f := lift f.1 f.2
invFun
g :=
⟨fun k => (truncate k).comp g, by
intro _ _ h
simp only [← RingHom.comp_assoc, truncate_comp_wittVector_truncate]⟩
left_inv := by rintro ⟨f, hf⟩; simp only [truncate_comp_lift]
right_inv _ := lift_unique _ _ fun _ => rfl
