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
Instances For
    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 : R} {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
    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
    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.pow_mem' {K : Type u_1} {L : Type u_2} [CommSemiring K] [CommSemiring L] {i : K →+* L} {p : } [self : 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 : } [self : IsPRadical i 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 : ) :
      Equations
      • =
      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] :
      IsPRadical (f.comp i) 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
      Instances For

        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
        Instances For
          @[simp]
          theorem PerfectRing.liftAux_self_apply {K : Type u_1} {L : Type u_2} [CommSemiring K] [CommSemiring L] (i : K →+* L) (p : ) [ExpChar L p] [IsPRadical i p] [PerfectRing L p] (x : L) :
          @[simp]
          theorem PerfectRing.liftAux_self {K : Type u_1} {L : Type u_2} [CommSemiring K] [CommSemiring L] (i : K →+* L) (p : ) [ExpChar L p] [IsPRadical i p] [PerfectRing L p] :
          @[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) :
          @[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] :
          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 K p] [ExpChar M p] [PerfectRing M p] [IsPRadical i p] (x : L) (n : ) (y : K) (h : i y = x ^ p ^ n) :
          PerfectRing.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 K p] [ExpChar L p] [ExpChar M p] [PerfectRing M p] [IsPRadical i 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
          Instances For
            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 K p] [ExpChar L p] [ExpChar M p] [PerfectRing M p] [IsPRadical i p] (x : L) (n : ) (y : K) (h : i y = x ^ p ^ n) :
            (PerfectRing.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 K p] [ExpChar L p] [ExpChar M p] [PerfectRing M p] [IsPRadical i p] (x : K) :
            (PerfectRing.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 K p] [ExpChar L p] [ExpChar M p] [PerfectRing M p] [IsPRadical i p] :
            (PerfectRing.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] [ExpChar L p] [IsPRadical i p] [PerfectRing L p] (x : L) :
            (PerfectRing.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] [ExpChar L p] [IsPRadical i p] [PerfectRing L p] :
            theorem PerfectRing.lift_id_apply {K : Type u_1} {M : Type u_3} [CommRing K] [CommRing M] (j : K →+* M) (p : ) [ExpChar K p] [ExpChar M p] [PerfectRing M p] (x : K) :
            (PerfectRing.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 K p] [ExpChar M p] [PerfectRing M p] :
            @[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 K p] [ExpChar L p] [ExpChar M p] [PerfectRing M p] [IsPRadical i p] :
            PerfectRing.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 K p] [ExpChar L p] [ExpChar M p] [PerfectRing M p] [IsPRadical i p] (x : L) :
            (PerfectRing.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 K p] [ExpChar L p] [ExpChar M p] [PerfectRing M p] [IsPRadical i 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
            Instances For
              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 K p] [ExpChar L p] [ExpChar M p] [PerfectRing M p] [IsPRadical i 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 K p] [ExpChar L p] [ExpChar M p] [PerfectRing M p] [IsPRadical i p] :
              (PerfectRing.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 K p] [ExpChar M p] [PerfectRing M p] :
              @[simp]
              theorem PerfectRing.liftEquiv_id {K : Type u_1} {M : Type u_3} [CommRing K] [CommRing M] (p : ) [ExpChar K p] [ExpChar M 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 K p] [ExpChar L p] [ExpChar M p] [ExpChar N p] [PerfectRing M p] [IsPRadical i p] [PerfectRing N p] [IsPRadical j 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 K p] [ExpChar L p] [ExpChar M p] [ExpChar N p] [PerfectRing M p] [IsPRadical i p] [PerfectRing N p] [IsPRadical j p] (x : L) :
              (PerfectRing.lift j k p) ((PerfectRing.lift i j p) x) = (PerfectRing.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 K p] [ExpChar L p] [ExpChar M p] [PerfectRing M p] [IsPRadical i p] [IsPRadical j p] [PerfectRing L p] (x : L) :
              (PerfectRing.lift j i p) ((PerfectRing.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 K p] [ExpChar L p] [ExpChar M p] [PerfectRing M p] [IsPRadical i p] [IsPRadical j p] [PerfectRing L p] :
              @[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 K p] [ExpChar L p] [ExpChar M p] [ExpChar N p] [PerfectRing M p] [IsPRadical i p] [IsPRadical g p] [IsPRadical (g.comp i) 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 K p] [ExpChar L p] [ExpChar M p] [ExpChar N p] [PerfectRing M p] [IsPRadical i p] [IsPRadical g p] [IsPRadical (g.comp i) p] (x : N) :
              (PerfectRing.lift g (PerfectRing.lift i j p) p) x = (PerfectRing.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 K p] [ExpChar L p] [ExpChar M p] [ExpChar N p] [PerfectRing M p] [IsPRadical i p] [IsPRadical g p] [IsPRadical (g.comp i) p] :
              @[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 K p] [ExpChar L p] [ExpChar M p] [ExpChar N p] [PerfectRing M p] [IsPRadical i p] [IsPRadical g p] [IsPRadical (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 K p] [ExpChar L p] [ExpChar M 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
              • One or more equations did not get rendered due to their size.
              Instances For
                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 K p] [ExpChar L p] [ExpChar M p] [PerfectRing L p] [IsPerfectClosure i p] [PerfectRing M p] [IsPerfectClosure j p] :
                (IsPerfectClosure.equiv i j p).toRingHom = PerfectRing.lift i 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 K p] [ExpChar L p] [ExpChar M p] [PerfectRing L p] [IsPerfectClosure i p] [PerfectRing M p] [IsPerfectClosure j 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 K p] [ExpChar L p] [ExpChar M p] [PerfectRing L p] [IsPerfectClosure i p] [PerfectRing M p] [IsPerfectClosure j p] :
                (IsPerfectClosure.equiv i j p).symm.toRingHom = PerfectRing.lift j i 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 K p] [ExpChar L p] [ExpChar M p] [PerfectRing L p] [IsPerfectClosure i p] [PerfectRing M p] [IsPerfectClosure j p] (x : L) (n : ) (y : K) (h : i y = x ^ p ^ n) :
                (IsPerfectClosure.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 K p] [ExpChar L p] [ExpChar M p] [PerfectRing L p] [IsPerfectClosure i p] [PerfectRing M p] [IsPerfectClosure j p] (x : M) (n : ) (y : K) (h : j y = x ^ p ^ n) :
                (IsPerfectClosure.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) :
                @[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 K p] [ExpChar L p] [ExpChar M p] [PerfectRing L p] [IsPerfectClosure i p] [PerfectRing M p] [IsPerfectClosure j p] (x : K) :
                (IsPerfectClosure.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 K p] [ExpChar L p] [ExpChar M p] [PerfectRing L p] [IsPerfectClosure i p] [PerfectRing M p] [IsPerfectClosure j p] :
                ((IsPerfectClosure.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 K p] [ExpChar L p] [ExpChar M p] [ExpChar N p] [PerfectRing L p] [IsPerfectClosure i p] [PerfectRing M p] [IsPerfectClosure j p] [PerfectRing N p] [IsPerfectClosure k p] (x : L) :
                @[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 K p] [ExpChar L p] [ExpChar M p] [ExpChar N p] [PerfectRing L p] [IsPerfectClosure i p] [PerfectRing M p] [IsPerfectClosure j p] [PerfectRing N p] [IsPerfectClosure 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 K p] [ExpChar L p] [ExpChar M p] [PerfectRing L p] [IsPerfectClosure i p] [PerfectRing M p] [IsPerfectClosure j p] (x : L) :
                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 K p] [ExpChar L p] [ExpChar M p] [PerfectRing L p] [IsPerfectClosure i p] [PerfectRing M p] [IsPerfectClosure j p] :
                instance PerfectClosure.isPRadical (K : Type u_1) [CommRing K] (p : ) [Fact (Nat.Prime p)] [CharP K 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.

                Equations
                • =
                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.

                Equations
                • =