Documentation

Mathlib.FieldTheory.IsPerfectClosure

IsPerfectClosure predicate #

This file contains IsPerfectClosure which asserts that L is a perfect closure of K under a ring homomorphism i : K →+* L, as well as its basic properties.

Main definitions #

Main results #

Tags #

perfect ring, perfect closure, purely inseparable

def pNilradical (R : Type u_1) [CommSemiring R] (p : ) :

Given a natural number p, the p-nilradical of a ring is defined to be the nilradical if p > 1 (pNilradical_eq_nilradical), and defined to be the zero ideal if p ≤ 1 (pNilradical_eq_bot'). Equivalently, it is the ideal consisting of elements x such that x ^ p ^ n = 0 for some n (mem_pNilradical).

Equations
theorem pNilradical_eq_nilradical {R : Type u_1} [CommSemiring R] {p : } (hp : 1 < p) :
theorem pNilradical_eq_bot {R : Type u_1} [CommSemiring R] {p : } (hp : ¬1 < p) :
theorem pNilradical_eq_bot' {R : Type u_1} [CommSemiring R] {p : } (hp : p 1) :
theorem pNilradical_prime {R : Type u_1} [CommSemiring R] {p : } (hp : Nat.Prime p) :
theorem mem_pNilradical {R : Type u_1} [CommSemiring R] {p : } {x : R} :
x pNilradical R p ∃ (n : ), x ^ p ^ n = 0
theorem sub_mem_pNilradical_iff_pow_expChar_pow_eq {R : Type u_1} [CommRing R] {p : } [ExpChar R p] {x y : R} :
x - y pNilradical R p ∃ (n : ), x ^ p ^ n = y ^ p ^ n
theorem pow_expChar_pow_inj_of_pNilradical_eq_bot (R : Type u_1) [CommRing R] (p : ) [ExpChar R p] (h : pNilradical R p = ) (n : ) :
Function.Injective fun (x : R) => x ^ p ^ n
class IsPRadical {K : Type u_1} {L : Type u_2} [CommSemiring K] [CommSemiring L] (i : K →+* L) (p : ) :

If i : K →+* L is a ring homomorphism of characteristic p rings, then it is called p-radical if the following conditions are satisfied:

  • For any element x of L there is n : ℕ such that x ^ (p ^ n) is contained in K.
  • The kernel of i is contained in the p-nilradical of K.

It is a generalization of purely inseparable extension for fields.

Instances
    theorem isPRadical_iff {K : Type u_1} {L : Type u_2} [CommSemiring K] [CommSemiring L] (i : K →+* L) (p : ) :
    IsPRadical i p (∀ (x : L), ∃ (n : ) (y : K), i y = x ^ p ^ n) RingHom.ker i pNilradical K p
    theorem IsPRadical.pow_mem {K : Type u_1} {L : Type u_2} [CommSemiring K] [CommSemiring L] (i : K →+* L) (p : ) [IsPRadical i p] (x : L) :
    ∃ (n : ) (y : K), i y = x ^ p ^ n
    theorem IsPRadical.ker_le {K : Type u_1} {L : Type u_2} [CommSemiring K] [CommSemiring L] (i : K →+* L) (p : ) [IsPRadical i p] :
    theorem IsPRadical.comap_pNilradical {K : Type u_1} {L : Type u_2} [CommSemiring K] [CommSemiring L] (i : K →+* L) (p : ) [IsPRadical i p] :
    instance IsPRadical.of_id (K : Type u_1) [CommSemiring K] (p : ) :
    theorem IsPRadical.trans {K : Type u_1} {L : Type u_2} {M : Type u_3} [CommSemiring K] [CommSemiring L] [CommSemiring M] (i : K →+* L) (f : L →+* M) (p : ) [IsPRadical i p] [IsPRadical f p] :

    Composition of p-radical ring homomorphisms is also p-radical.

    @[reducible, inline]
    abbrev IsPerfectClosure {K : Type u_1} {L : Type u_2} [CommSemiring K] [CommSemiring L] (i : K →+* L) (p : ) [ExpChar L p] [PerfectRing L p] :

    If i : K →+* L is a p-radical ring homomorphism, then it makes L a perfect closure of K, if L is perfect. In this case the kernel of i is equal to the p-nilradical of K (see IsPerfectClosure.ker_eq).

    Our definition makes it synonymous to IsPRadical if PerfectRing L p is present. A caveat is that you need to write [PerfectRing L p] [IsPerfectClosure i p]. This is similar to PerfectRing which has ExpChar as a prerequisite.

    Equations
    theorem RingHom.pNilradical_le_ker_of_perfectRing {K : Type u_1} {L : Type u_2} [CommSemiring K] [CommSemiring L] (i : K →+* L) (p : ) [ExpChar L p] [PerfectRing L p] :

    If i : K →+* L is a ring homomorphism of exponential characteristic p rings, such that L is perfect, then the p-nilradical of K is contained in the kernel of i.

    theorem IsPerfectClosure.ker_eq {K : Type u_1} {L : Type u_2} [CommSemiring K] [CommSemiring L] (i : K →+* L) (p : ) [ExpChar L p] [PerfectRing L p] [IsPerfectClosure i p] :
    theorem PerfectRing.lift_aux {K : Type u_1} {L : Type u_2} [CommSemiring K] [CommSemiring L] (i : K →+* L) (p : ) [IsPRadical i p] (x : L) :
    ∃ (y : × K), i y.2 = x ^ p ^ y.1
    def PerfectRing.liftAux {K : Type u_1} {L : Type u_2} {M : Type u_3} [CommSemiring K] [CommSemiring L] [CommSemiring M] (i : K →+* L) (j : K →+* M) (p : ) [ExpChar M p] [PerfectRing M p] [IsPRadical i p] (x : L) :
    M

    If i : K →+* L and j : K →+* M are ring homomorphisms of characteristic p rings, such that i is p-radical (in fact only the IsPRadical.pow_mem is required) and M is a perfect ring, then one can define a map L → M which maps an element x of L to y ^ (p ^ -n) if x ^ (p ^ n) is equal to some element y of K.

    Equations
    @[simp]
    theorem PerfectRing.liftAux_self_apply {K : Type u_1} {L : Type u_2} [CommSemiring K] [CommSemiring L] (i : K →+* L) (p : ) [IsPRadical i p] [ExpChar L p] [PerfectRing L p] (x : L) :
    liftAux i i p x = x
    @[simp]
    theorem PerfectRing.liftAux_self {K : Type u_1} {L : Type u_2} [CommSemiring K] [CommSemiring L] (i : K →+* L) (p : ) [IsPRadical i p] [ExpChar L p] [PerfectRing L p] :
    liftAux i i p = id
    @[simp]
    theorem PerfectRing.liftAux_id_apply {K : Type u_1} {M : Type u_3} [CommSemiring K] [CommSemiring M] (j : K →+* M) (p : ) [ExpChar M p] [PerfectRing M p] (x : K) :
    liftAux (RingHom.id K) j p x = j x
    @[simp]
    theorem PerfectRing.liftAux_id {K : Type u_1} {M : Type u_3} [CommSemiring K] [CommSemiring M] (j : K →+* M) (p : ) [ExpChar M p] [PerfectRing M p] :
    liftAux (RingHom.id K) j p = j
    theorem IsPRadical.injective_comp_of_pNilradical_eq_bot {K : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing K] [CommRing L] [CommRing M] (i : K →+* L) (p : ) [ExpChar M p] [IsPRadical i p] (h : pNilradical M p = ) :
    Function.Injective fun (f : L →+* M) => f.comp i

    If i : K →+* L is p-radical, then for any ring M of exponential charactistic p whose p-nilradical is zero, the map (L →+* M) → (K →+* M) induced by i is injective.

    theorem IsPRadical.injective_comp {K : Type u_1} {L : Type u_2} (M : Type u_3) [CommRing K] [CommRing L] [CommRing M] (i : K →+* L) (p : ) [ExpChar M p] [IsPRadical i p] [IsReduced M] :
    Function.Injective fun (f : L →+* M) => f.comp i

    If i : K →+* L is p-radical, then for any reduced ring M of exponential charactistic p, the map (L →+* M) → (K →+* M) induced by i is injective. A special case of IsPRadical.injective_comp_of_pNilradical_eq_bot and a generalization of IsPurelyInseparable.injective_comp_algebraMap.

    theorem IsPRadical.injective_comp_of_perfect {K : Type u_1} {L : Type u_2} (M : Type u_3) [CommRing K] [CommRing L] [CommRing M] (i : K →+* L) (p : ) [ExpChar M p] [IsPRadical i p] [PerfectRing M p] :
    Function.Injective fun (f : L →+* M) => f.comp i

    If i : K →+* L is p-radical, then for any perfect ring M of exponential charactistic p, the map (L →+* M) → (K →+* M) induced by i is injective. A special case of IsPRadical.injective_comp_of_pNilradical_eq_bot.

    theorem PerfectRing.liftAux_apply {K : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing K] [CommRing L] [CommRing M] (i : K →+* L) (j : K →+* M) (p : ) [ExpChar M p] [ExpChar K p] [PerfectRing M p] [IsPRadical i p] (x : L) (n : ) (y : K) (h : i y = x ^ p ^ n) :
    liftAux i j p x = (iterateFrobeniusEquiv M p n).symm (j y)

    If i : K →+* L and j : K →+* M are ring homomorphisms of characteristic p rings, such that i is p-radical, and M is a perfect ring, then PerfectRing.liftAux is well-defined.

    def PerfectRing.lift {K : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing K] [CommRing L] [CommRing M] (i : K →+* L) (j : K →+* M) (p : ) [ExpChar M p] [ExpChar K p] [PerfectRing M p] [IsPRadical i p] [ExpChar L p] :
    L →+* M

    If i : K →+* L and j : K →+* M are ring homomorphisms of characteristic p rings, such that i is p-radical, and M is a perfect ring, then PerfectRing.liftAux is a ring homomorphism. This is similar to IsAlgClosed.lift and IsSepClosed.lift.

    Equations
    theorem PerfectRing.lift_apply {K : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing K] [CommRing L] [CommRing M] (i : K →+* L) (j : K →+* M) (p : ) [ExpChar M p] [ExpChar K p] [PerfectRing M p] [IsPRadical i p] [ExpChar L p] (x : L) (n : ) (y : K) (h : i y = x ^ p ^ n) :
    (lift i j p) x = (iterateFrobeniusEquiv M p n).symm (j y)
    @[simp]
    theorem PerfectRing.lift_comp_apply {K : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing K] [CommRing L] [CommRing M] (i : K →+* L) (j : K →+* M) (p : ) [ExpChar M p] [ExpChar K p] [PerfectRing M p] [IsPRadical i p] [ExpChar L p] (x : K) :
    (lift i j p) (i x) = j x
    @[simp]
    theorem PerfectRing.lift_comp {K : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing K] [CommRing L] [CommRing M] (i : K →+* L) (j : K →+* M) (p : ) [ExpChar M p] [ExpChar K p] [PerfectRing M p] [IsPRadical i p] [ExpChar L p] :
    (lift i j p).comp i = j
    theorem PerfectRing.lift_self_apply {K : Type u_1} {L : Type u_2} [CommRing K] [CommRing L] (i : K →+* L) (p : ) [ExpChar K p] [IsPRadical i p] [ExpChar L p] [PerfectRing L p] (x : L) :
    (lift i i p) x = x
    @[simp]
    theorem PerfectRing.lift_self {K : Type u_1} {L : Type u_2} [CommRing K] [CommRing L] (i : K →+* L) (p : ) [ExpChar K p] [IsPRadical i p] [ExpChar L p] [PerfectRing L p] :
    lift i i p = RingHom.id L
    theorem PerfectRing.lift_id_apply {K : Type u_1} {M : Type u_3} [CommRing K] [CommRing M] (j : K →+* M) (p : ) [ExpChar M p] [ExpChar K p] [PerfectRing M p] (x : K) :
    (lift (RingHom.id K) j p) x = j x
    @[simp]
    theorem PerfectRing.lift_id {K : Type u_1} {M : Type u_3} [CommRing K] [CommRing M] (j : K →+* M) (p : ) [ExpChar M p] [ExpChar K p] [PerfectRing M p] :
    lift (RingHom.id K) j p = j
    @[simp]
    theorem PerfectRing.comp_lift {K : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing K] [CommRing L] [CommRing M] (i : K →+* L) (f : L →+* M) (p : ) [ExpChar M p] [ExpChar K p] [PerfectRing M p] [IsPRadical i p] [ExpChar L p] :
    lift i (f.comp i) p = f
    theorem PerfectRing.comp_lift_apply {K : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing K] [CommRing L] [CommRing M] (i : K →+* L) (f : L →+* M) (p : ) [ExpChar M p] [ExpChar K p] [PerfectRing M p] [IsPRadical i p] [ExpChar L p] (x : L) :
    (lift i (f.comp i) p) x = f x
    def PerfectRing.liftEquiv {K : Type u_1} {L : Type u_2} (M : Type u_3) [CommRing K] [CommRing L] [CommRing M] (i : K →+* L) (p : ) [ExpChar M p] [ExpChar K p] [PerfectRing M p] [IsPRadical i p] [ExpChar L p] :
    (K →+* M) (L →+* M)

    If i : K →+* L is a homomorphisms of characteristic p rings, such that i is p-radical, and M is a perfect ring of characteristic p, then K →+* M is one-to-one correspondence to L →+* M, given by PerfectRing.lift. This is a generalization to PerfectClosure.lift.

    Equations
    theorem PerfectRing.liftEquiv_apply {K : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing K] [CommRing L] [CommRing M] (i : K →+* L) (j : K →+* M) (p : ) [ExpChar M p] [ExpChar K p] [PerfectRing M p] [IsPRadical i p] [ExpChar L p] :
    (liftEquiv M i p) j = lift i j p
    theorem PerfectRing.liftEquiv_symm_apply {K : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing K] [CommRing L] [CommRing M] (i : K →+* L) (f : L →+* M) (p : ) [ExpChar M p] [ExpChar K p] [PerfectRing M p] [IsPRadical i p] [ExpChar L p] :
    (liftEquiv M i p).symm f = f.comp i
    theorem PerfectRing.liftEquiv_id_apply {K : Type u_1} {M : Type u_3} [CommRing K] [CommRing M] (j : K →+* M) (p : ) [ExpChar M p] [ExpChar K p] [PerfectRing M p] :
    (liftEquiv M (RingHom.id K) p) j = j
    @[simp]
    theorem PerfectRing.liftEquiv_id {K : Type u_1} {M : Type u_3} [CommRing K] [CommRing M] (p : ) [ExpChar M p] [ExpChar K p] [PerfectRing M p] :
    @[simp]
    theorem PerfectRing.lift_comp_lift {K : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing K] [CommRing L] [CommRing M] [CommRing N] (i : K →+* L) (j : K →+* M) (k : K →+* N) (p : ) [ExpChar M p] [ExpChar K p] [PerfectRing M p] [IsPRadical i p] [ExpChar L p] [ExpChar N p] [PerfectRing N p] [IsPRadical j p] :
    (lift j k p).comp (lift i j p) = lift i k p
    @[simp]
    theorem PerfectRing.lift_comp_lift_apply {K : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing K] [CommRing L] [CommRing M] [CommRing N] (i : K →+* L) (j : K →+* M) (k : K →+* N) (p : ) [ExpChar M p] [ExpChar K p] [PerfectRing M p] [IsPRadical i p] [ExpChar L p] [ExpChar N p] [PerfectRing N p] [IsPRadical j p] (x : L) :
    (lift j k p) ((lift i j p) x) = (lift i k p) x
    theorem PerfectRing.lift_comp_lift_apply_eq_self {K : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing K] [CommRing L] [CommRing M] (i : K →+* L) (j : K →+* M) (p : ) [ExpChar M p] [ExpChar K p] [PerfectRing M p] [IsPRadical i p] [ExpChar L p] [IsPRadical j p] [PerfectRing L p] (x : L) :
    (lift j i p) ((lift i j p) x) = x
    theorem PerfectRing.lift_comp_lift_eq_id {K : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing K] [CommRing L] [CommRing M] (i : K →+* L) (j : K →+* M) (p : ) [ExpChar M p] [ExpChar K p] [PerfectRing M p] [IsPRadical i p] [ExpChar L p] [IsPRadical j p] [PerfectRing L p] :
    (lift j i p).comp (lift i j p) = RingHom.id L
    @[simp]
    theorem PerfectRing.lift_lift {K : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing K] [CommRing L] [CommRing M] [CommRing N] (i : K →+* L) (j : K →+* M) (g : L →+* N) (p : ) [ExpChar M p] [ExpChar K p] [PerfectRing M p] [IsPRadical i p] [ExpChar L p] [ExpChar N p] [IsPRadical g p] [IsPRadical (g.comp i) p] :
    lift g (lift i j p) p = lift (g.comp i) j p
    theorem PerfectRing.lift_lift_apply {K : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing K] [CommRing L] [CommRing M] [CommRing N] (i : K →+* L) (j : K →+* M) (g : L →+* N) (p : ) [ExpChar M p] [ExpChar K p] [PerfectRing M p] [IsPRadical i p] [ExpChar L p] [ExpChar N p] [IsPRadical g p] [IsPRadical (g.comp i) p] (x : N) :
    (lift g (lift i j p) p) x = (lift (g.comp i) j p) x
    @[simp]
    theorem PerfectRing.liftEquiv_comp_apply {K : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing K] [CommRing L] [CommRing M] [CommRing N] (i : K →+* L) (j : K →+* M) (g : L →+* N) (p : ) [ExpChar M p] [ExpChar K p] [PerfectRing M p] [IsPRadical i p] [ExpChar L p] [ExpChar N p] [IsPRadical g p] [IsPRadical (g.comp i) p] :
    (liftEquiv M g p) ((liftEquiv M i p) j) = (liftEquiv M (g.comp i) p) j
    @[simp]
    theorem PerfectRing.liftEquiv_trans {K : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing K] [CommRing L] [CommRing M] [CommRing N] (i : K →+* L) (g : L →+* N) (p : ) [ExpChar M p] [ExpChar K p] [PerfectRing M p] [IsPRadical i p] [ExpChar L p] [ExpChar N p] [IsPRadical g p] [IsPRadical (g.comp i) p] :
    (liftEquiv M i p).trans (liftEquiv M g p) = liftEquiv M (g.comp i) p
    def IsPerfectClosure.equiv {K : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing K] [CommRing L] [CommRing M] (i : K →+* L) (j : K →+* M) (p : ) [ExpChar M p] [ExpChar K p] [ExpChar L p] [PerfectRing L p] [IsPerfectClosure i p] [PerfectRing M p] [IsPerfectClosure j p] :
    L ≃+* M

    If L and M are both perfect closures of K, then there is a ring isomorphism L ≃+* M. This is similar to IsAlgClosure.equiv and IsSepClosure.equiv.

    Equations
    theorem IsPerfectClosure.equiv_toRingHom {K : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing K] [CommRing L] [CommRing M] (i : K →+* L) (j : K →+* M) (p : ) [ExpChar M p] [ExpChar K p] [ExpChar L p] [PerfectRing L p] [IsPerfectClosure i p] [PerfectRing M p] [IsPerfectClosure j p] :
    @[simp]
    theorem IsPerfectClosure.equiv_symm {K : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing K] [CommRing L] [CommRing M] (i : K →+* L) (j : K →+* M) (p : ) [ExpChar M p] [ExpChar K p] [ExpChar L p] [PerfectRing L p] [IsPerfectClosure i p] [PerfectRing M p] [IsPerfectClosure j p] :
    (equiv i j p).symm = equiv j i p
    theorem IsPerfectClosure.equiv_symm_toRingHom {K : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing K] [CommRing L] [CommRing M] (i : K →+* L) (j : K →+* M) (p : ) [ExpChar M p] [ExpChar K p] [ExpChar L p] [PerfectRing L p] [IsPerfectClosure i p] [PerfectRing M p] [IsPerfectClosure j p] :
    theorem IsPerfectClosure.equiv_apply {K : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing K] [CommRing L] [CommRing M] (i : K →+* L) (j : K →+* M) (p : ) [ExpChar M p] [ExpChar K p] [ExpChar L p] [PerfectRing L p] [IsPerfectClosure i p] [PerfectRing M p] [IsPerfectClosure j p] (x : L) (n : ) (y : K) (h : i y = x ^ p ^ n) :
    (equiv i j p) x = (iterateFrobeniusEquiv M p n).symm (j y)
    theorem IsPerfectClosure.equiv_symm_apply {K : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing K] [CommRing L] [CommRing M] (i : K →+* L) (j : K →+* M) (p : ) [ExpChar M p] [ExpChar K p] [ExpChar L p] [PerfectRing L p] [IsPerfectClosure i p] [PerfectRing M p] [IsPerfectClosure j p] (x : M) (n : ) (y : K) (h : j y = x ^ p ^ n) :
    (equiv i j p).symm x = (iterateFrobeniusEquiv L p n).symm (i y)
    theorem IsPerfectClosure.equiv_self_apply {K : Type u_1} {L : Type u_2} [CommRing K] [CommRing L] (i : K →+* L) (p : ) [ExpChar K p] [ExpChar L p] [PerfectRing L p] [IsPerfectClosure i p] (x : L) :
    (equiv i i p) x = x
    @[simp]
    theorem IsPerfectClosure.equiv_self {K : Type u_1} {L : Type u_2} [CommRing K] [CommRing L] (i : K →+* L) (p : ) [ExpChar K p] [ExpChar L p] [PerfectRing L p] [IsPerfectClosure i p] :
    @[simp]
    theorem IsPerfectClosure.equiv_comp_apply {K : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing K] [CommRing L] [CommRing M] (i : K →+* L) (j : K →+* M) (p : ) [ExpChar M p] [ExpChar K p] [ExpChar L p] [PerfectRing L p] [IsPerfectClosure i p] [PerfectRing M p] [IsPerfectClosure j p] (x : K) :
    (equiv i j p) (i x) = j x
    @[simp]
    theorem IsPerfectClosure.equiv_comp {K : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing K] [CommRing L] [CommRing M] (i : K →+* L) (j : K →+* M) (p : ) [ExpChar M p] [ExpChar K p] [ExpChar L p] [PerfectRing L p] [IsPerfectClosure i p] [PerfectRing M p] [IsPerfectClosure j p] :
    (↑(equiv i j p)).comp i = j
    @[simp]
    theorem IsPerfectClosure.equiv_comp_equiv_apply {K : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing K] [CommRing L] [CommRing M] [CommRing N] (i : K →+* L) (j : K →+* M) (k : K →+* N) (p : ) [ExpChar M p] [ExpChar K p] [ExpChar L p] [PerfectRing L p] [IsPerfectClosure i p] [PerfectRing M p] [IsPerfectClosure j p] [ExpChar N p] [PerfectRing N p] [IsPerfectClosure k p] (x : L) :
    (equiv j k p) ((equiv i j p) x) = (equiv i k p) x
    @[simp]
    theorem IsPerfectClosure.equiv_comp_equiv {K : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing K] [CommRing L] [CommRing M] [CommRing N] (i : K →+* L) (j : K →+* M) (k : K →+* N) (p : ) [ExpChar M p] [ExpChar K p] [ExpChar L p] [PerfectRing L p] [IsPerfectClosure i p] [PerfectRing M p] [IsPerfectClosure j p] [ExpChar N p] [PerfectRing N p] [IsPerfectClosure k p] :
    (equiv i j p).trans (equiv j k p) = equiv i k p
    theorem IsPerfectClosure.equiv_comp_equiv_apply_eq_self {K : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing K] [CommRing L] [CommRing M] (i : K →+* L) (j : K →+* M) (p : ) [ExpChar M p] [ExpChar K p] [ExpChar L p] [PerfectRing L p] [IsPerfectClosure i p] [PerfectRing M p] [IsPerfectClosure j p] (x : L) :
    (equiv j i p) ((equiv i j p) x) = x
    theorem IsPerfectClosure.equiv_comp_equiv_eq_id {K : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing K] [CommRing L] [CommRing M] (i : K →+* L) (j : K →+* M) (p : ) [ExpChar M p] [ExpChar K p] [ExpChar L p] [PerfectRing L p] [IsPerfectClosure i p] [PerfectRing M p] [IsPerfectClosure j p] :
    (equiv i j p).trans (equiv j i p) = RingEquiv.refl L
    instance PerfectClosure.isPRadical (K : Type u_1) [CommRing K] (p : ) [Fact (Nat.Prime p)] [CharP K p] :
    IsPRadical (of K p) p

    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.

    theorem IsPRadical.isPurelyInseparable (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] (p : ) [ExpChar K p] [IsPRadical (algebraMap K L) p] :

    If L / K is a p-radical field extension, then it is purely inseparable.

    instance IsPurelyInseparable.isPRadical (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] (p : ) [ExpChar K p] [IsPurelyInseparable K L] :

    If L / K is a purely inseparable field extension, then it is p-radical. In particular, if L is perfect, then the (relative) perfect closure perfectClosure K L is a perfect closure of K, that is, IsPerfectClosure (algebraMap K (perfectClosure K L)) p.