English
The reverse composition holds: Frobenius ∘ pthRoot = id on Ring.Perfection.
Русский
Обратная композиция: Фробениус ∘ pthRoot = id на Ring.Perfection.
LaTeX
$$$(\\mathrm{frobenius}_{p}) \\circ (\\mathrm{pthRoot}~R~p) = \\mathrm{id}_{\\mathrm{Ring.Perfection}(R,p)}$$$
Lean4
/-- For a perfect ring, it itself is the perfection. -/
theorem id [PerfectRing R p] : PerfectionMap p (RingHom.id R) :=
{ injective := fun _ _ hxy => hxy 0
surjective := fun f hf =>
⟨f 0, fun n =>
show ((frobeniusEquiv R p).symm)^[n] (f 0) = f n from
Nat.recOn n rfl fun n ih =>
injective_pow_p R p <| by rw [Function.iterate_succ_apply', frobeniusEquiv_symm_pow_p, ih, hf]⟩ }
