English
The equality of compositions translates to the equality of truncated coefficients under the appropriate isomorphisms.
Русский
Равенство композиции переводится в равенство коэффициентов усечения под соответствующими изоморфизмами.
LaTeX
$$$$ \\operatorname{truncate}_{hm} ( \\mathrm{WittVector.truncate} m (x) ) = \\mathrm{WittVector.truncate} n (x). $$$$
Lean4
/-- Given compatible ring homs from `S` into `TruncatedWittVector n` for each `n`, we can lift these
to a ring hom `S → 𝕎 R`.
`lift` defines the universal property of `𝕎 R` as the inverse limit of `TruncatedWittVector n`.
-/
def lift : S →+* 𝕎 R := by
refine
{ toFun := liftFun f
map_zero' := ?_
map_one' := ?_
map_add' := ?_
map_mul' := ?_ } <;>
( intros
rw [← sub_eq_zero, ← Ideal.mem_bot, ← iInf_ker_truncate, Ideal.mem_iInf]
simp [RingHom.mem_ker, f_compat])
