English
The absolute perfect closure is a p-radical extension over the base ring: IsPRadical (PerfectClosure.of K p) p.
Русский
Полное совершенное замыкание является p-радикальным расширением над основанием: IsPRadical (PerfectClosure.of K p) p.
LaTeX
$$$ \operatorname IsPRadical(\mathrm{PerfectClosure.of}\ K\ p)\ p $$$
Lean4
/-- The absolute perfect closure `PerfectClosure` is a `p`-radical extension over the base ring.
In particular, it is a perfect closure of the base ring, that is,
`IsPerfectClosure (PerfectClosure.of K p) p`. -/
instance isPRadical : IsPRadical (PerfectClosure.of K p) p
where
pow_mem'
x := PerfectClosure.induction_on x fun x ↦ ⟨x.1, x.2, by rw [← iterate_frobenius, iterate_frobenius_mk K p x.1 x.2]⟩
ker_le' x
h := by
rw [RingHom.mem_ker, of_apply, zero_def, mk_eq_iff] at h
obtain ⟨n, h⟩ := h
simp_rw [zero_add, ← coe_iterateFrobenius, map_zero] at h
exact mem_pNilradical.2 ⟨n, h⟩
