English
Let f be a compatible family of ring homomorphisms f_k: S → 𝕎R/k truncated Witt rings, with compatibility f_{k1 ≤ k2}. Then there exists a unique ring homomorphism g: S → 𝕎R such that for every k, the truncation map composed with g equals f_k. In symbols: if f and f_compat satisfy the compatibility relation, then lift f f_compat is the unique g with (truncate k) ∘ g = f_k for all k.
Русский
Пусть задана совместимая семья кольцевых гомоморфизмов f_k: S → 𝕎R_k (задаётся через соответствующие ограничители), удовлетворяющая условиям совместимости. Тогда существует единственный кольцевой гомоморфизм g: S → 𝕎R такой, что для каждого k композиция с ограничения равна f_k: (truncate k) ∘ g = f_k.
LaTeX
$$$\\\\forall g : S \\\\rightarrow^+ 𝕎 R,\\\\ \\bigl(\\\\forall k, (\\\\operatorname{truncate}(k)) \\\\circ g = f k\\\\bigr) \\\\Rightarrow \\\\operatorname{lift} f f_{\\\\mathrm{compat}} = g.$$$
Lean4
/-- The uniqueness part of the universal property of `𝕎 R`. -/
theorem lift_unique (g : S →+* 𝕎 R) (g_compat : ∀ k, (WittVector.truncate k).comp g = f k) : lift _ f_compat = g :=
by
ext1 x
rw [← sub_eq_zero, ← Ideal.mem_bot, ← iInf_ker_truncate, Ideal.mem_iInf]
intro i
simp only [RingHom.mem_ker, g_compat, ← RingHom.comp_apply, truncate_comp_lift, RingHom.map_sub, sub_self]
