English
The Teichmüller lift teichmuller p r defines a MonoidHom from R to WittVector p R.
Русский
Проведение Тейхмюллерова подъёма teichmuller p r задаёт моноид-одомо from R в WittVector p R.
LaTeX
$$$\\mathrm{teichmuller} : R \\to^{} \\mathbb{W}R \\quad\\text{is a MonoidHom}$$$
Lean4
/-- The Teichmüller lift of an element of `R` to `𝕎 R`.
The `0`-th coefficient of `teichmuller p r` is `r`, and all others are `0`.
This is a monoid homomorphism. -/
def teichmuller : R →* 𝕎 R where
toFun := teichmullerFun p
map_one' := by
ext ⟨⟩
· rw [one_coeff_zero]; rfl
· rw [one_coeff_eq_of_pos _ _ _ (Nat.succ_pos _)]; rfl
map_mul' := by
intro x y
rcases counit_surjective R x with ⟨x, rfl⟩
rcases counit_surjective R y with ⟨y, rfl⟩
simp only [← map_teichmullerFun, ← RingHom.map_mul, teichmuller_mul_aux₂]
