English
If two ring homomorphisms g1, g2: S → 𝕎R agree after composing with every truncation map, then g1 = g2. In other words, the collection of truncations determines a Witt-vector map uniquely.
Русский
Если два кольцевых гомоморфизма g1, g2: S → 𝕎R совпадают после композиции с каждой огранительной отображающей функцией, то они равны. То есть совокупность ограничителей однозначно определяет гомоморфизм Witt.
LaTeX
$$$$\\forall g_1,g_2 : S \\to^+ 𝕎 R,\\ \\bigl(\\forall k, (\\\\operatorname{truncate}(k)) \\circ g_1 = (\\\\operatorname{truncate}(k)) \\circ g_2\\bigr) \\Rightarrow g_1 = g_2.$$$$
Lean4
theorem hom_ext (g₁ g₂ : S →+* 𝕎 R) (h : ∀ k, (truncate k).comp g₁ = (truncate k).comp g₂) : g₁ = g₂ :=
liftEquiv.symm.injective <| Subtype.ext <| funext h
