Commit 2024-03-12 11:06 d4243447

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.