feat(FieldTheory/IsPerfectClosure): predicate IsPerfectClosure (#8696)

Main definitions

- `pNilradical`: the `p`-nilradical of a ring is an ideal consists of elements `x` such that
  `x ^ p ^ n = 0` for some `n` (`mem_pNilradical`). It is equal to the nilradical if `p > 1`
  (`pNilradical_eq_nilradical`), otherwise it is equal to zero (`pNilradical_eq_bot`).

- `IsPRadical`: a ring homomorphism `i : K →+* L` of characteristic `p` rings is called `p`-radical,
  if or any element `x` of `L` there is `n : ℕ` such that `x ^ (p ^ n)` is contained in `K`,
  and the kernel of `i` is contained in the `p`-nilradical of `K`.
  A generalization of purely inseparable extension for fields.

- `IsPerfectClosure`: a ring homomorphism `i : K →+* L` of characteristic `p` rings makes `L` a
  perfect closure of `K`, if `L` is perfect, and `i` is `p`-radical.

- `PerfectRing.lift`: if a `p`-radical ring homomorphism `K →+* L` is given, `M` is a perfect ring,
  then any ring homomorphism `K →+* M` can be lifted to `L →+* M`.
  This is similar to `IsAlgClosed.lift` and `IsSepClosed.lift`.

- `PerfectRing.liftEquiv`: `K →+* M` is one-to-one correspondence to `L →+* M`,
  given by `PerfectRing.lift`. This is a generalization to `PerfectClosure.lift`.

- `IsPerfectClosure.equiv`: perfect closures of a ring are isomorphic.

Main results

- `IsPRadical.trans`: composition of `p`-radical ring homomorphisms is also `p`-radical.

- `PerfectClosure.isPerfectClosure`: the absolute perfect closure `PerfectClosure` is a
  perfect closure.

- `IsPRadical.isPurelyInseparable`, `IsPurelyInseparable.isPRadical`: `p`-radical and
  purely inseparable are equivalent for fields.

- `perfectClosure.isPerfectClosure`: the (relative) perfect closure `perfectClosure` is a
  perfect closure.

Author: acmepjz

Mathlib.lean

@@ -2198,6 +2198,7 @@ import Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
 import Mathlib.FieldTheory.IsAlgClosed.Basic
 import Mathlib.FieldTheory.IsAlgClosed.Classification
 import Mathlib.FieldTheory.IsAlgClosed.Spectrum
+import Mathlib.FieldTheory.IsPerfectClosure
 import Mathlib.FieldTheory.IsSepClosed
 import Mathlib.FieldTheory.KrullTopology
 import Mathlib.FieldTheory.KummerExtension