English
Under suitable conditions, the Frobenius endomorphism on Witt vectors is part of a ring isomorphism of Witt vectors to itself; there is an inverse given by a related Frobenius-equivariant map.
Русский
При подходящих условиях операция Фробениуса на Witt-векторах входит в структуру кольцевого изоморства Witt-переходов к самим себе; существует обратное отображение, совместимое с Фробениусом.
LaTeX
$$$\operatorname{frobeniusEquiv}(p,R) : \mathrm{WittVector}_p(R) \cong_{\mathrm{ring}} \mathrm{WittVector}_p(R)$$$
Lean4
/-- `WittVector.frobenius` as an equiv. -/
@[simps -fullyApplied]
def frobeniusEquiv [PerfectRing R p] : WittVector p R ≃+* WittVector p R :=
{
(WittVector.frobenius :
WittVector p R →+* WittVector p R) with
toFun := WittVector.frobenius
invFun := map (_root_.frobeniusEquiv R p).symm
left_inv := fun f =>
ext fun n => by
rw [frobenius_eq_map_frobenius]
exact frobeniusEquiv_symm_apply_frobenius R p _
right_inv := fun f =>
ext fun n => by
rw [frobenius_eq_map_frobenius]
exact frobenius_apply_frobeniusEquiv_symm R p _ }
