English
There is a natural truncation homomorphism from longer truncated Witt vectors to shorter ones when n ≤ m: truncate hm: TruncatedWittVector p m R →+* TruncatedWittVector p n R.
Русский
Существует естественный гомоморфизм усечения от более длинного усечённого виттового вектора к более короткому при n ≤ m: truncate hm...
LaTeX
$$$$\\text{truncate}_{hm}: \\mathrm{TruncatedWittVector}_p^m R \\to+* \\mathrm{TruncatedWittVector}_p^n R, \\quad (n \\le m). $$$$
Lean4
/-- A ring homomorphism that truncates a truncated Witt vector of length `m` to
a truncated Witt vector of length `n`, for `n ≤ m`.
-/
def truncate {m : ℕ} (hm : n ≤ m) : TruncatedWittVector p m R →+* TruncatedWittVector p n R :=
RingHom.liftOfRightInverse (WittVector.truncate m) out truncateFun_out
⟨WittVector.truncate n, by
intro x
simp only [WittVector.mem_ker_truncate]
intro h i hi
exact h i (lt_of_lt_of_le hi hm)⟩
