English
The perfect closure is a perfect ring of characteristic p; equivalently Frobenius is bijective on PerfectClosure(K,p).
Русский
Перфектное замыкание является совершенным кольцом характеристик p; эквивалентно биекция Фробениуса на PerfectClosure(K,p).
LaTeX
$$$\mathrm{PerfectRing}(\mathrm{PerfectClosure}(K,p),p).$$$
Lean4
instance instPerfectRing : PerfectRing (PerfectClosure K p) p where
bijective_frobenius :=
by
let f : PerfectClosure K p → PerfectClosure K p := fun e ↦
liftOn e (fun x => mk K p (x.1 + 1, x.2)) fun x y H =>
match x, y, H with
| _, _, R.intro n x => Quot.sound (R.intro _ _)
refine
bijective_iff_has_inverse.mpr
⟨f, fun e ↦ induction_on e fun ⟨n, x⟩ ↦ ?_, fun e ↦ induction_on e fun ⟨n, x⟩ ↦ ?_⟩ <;>
simp only [f, liftOn_mk, frobenius_mk, mk_succ_pow]
