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

• pNilradical: 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).

• 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: if i : K →+* L is p-radical ring homomorphism, then it makes L a perfect closure of K, if L is perfect.

  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.

• 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.isPRadical: 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.

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

• The (relative) perfect closure perfectClosure is a perfect closure (inferred from IsPurelyInseparable.isPRadical automatically by Lean).

Tags

perfect ring, perfect closure, purely inseparable

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

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

• pNilradical R p = if 1 < p then nilradical R else ⊥

theorem pNilradical_le_nilradical {R : Type u_1} [CommSemiring R] {p : ℕ} : pNilradical R p ≤ nilradical R

theorem pNilradical_eq_nilradical {R : Type u_1} [CommSemiring R] {p : ℕ} (hp : 1 < p) : pNilradical R p = nilradical R

theorem pNilradical_eq_bot {R : Type u_1} [CommSemiring R] {p : ℕ} (hp : ¬1 < p) : pNilradical R p = ⊥

theorem pNilradical_eq_bot' {R : Type u_1} [CommSemiring R] {p : ℕ} (hp : p ≤ 1) : pNilradical R p = ⊥

theorem pNilradical_prime {R : Type u_1} [CommSemiring R] {p : ℕ} (hp : Nat.Prime p) : pNilradical R p = nilradical R

theorem pNilradical_one {R : Type u_1} [CommSemiring R] : pNilradical R 1 = ⊥

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

theorem pNilradical_eq_bot_of_frobenius_inj (R : Type u_1) [CommSemiring R] (p : ℕ) [ExpChar R p] (h : Function.Injective ⇑(frobenius R p)) : pNilradical R p = ⊥

theorem PerfectRing.pNilradical_eq_bot (R : Type u_1) [CommSemiring R] (p : ℕ) [ExpChar R p] [PerfectRing R p] : pNilradical R p = ⊥

class IsPRadical {K : Type u_1} {L : Type u_2} [CommSemiring K] [CommSemiring L] (i : K →+* L) (p : ℕ) : Prop

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.

• pow_mem' (x : L) : ∃ (n : ℕ) (y : K), i y = x ^ p ^ n
• ker_le' : RingHom.ker i ≤ pNilradical K p

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] : RingHom.ker i ≤ pNilradical K p

theorem IsPRadical.comap_pNilradical {K : Type u_1} {L : Type u_2} [CommSemiring K] [CommSemiring L] (i : K →+* L) (p : ℕ) [IsPRadical i p] : Ideal.comap i (pNilradical L p) = pNilradical K p

instance IsPRadical.of_id (K : Type u_1) [CommSemiring K] (p : ℕ) : IsPRadical (RingHom.id 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] : 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] : Prop

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

• IsPerfectClosure i p = IsPRadical i p

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] : pNilradical K p ≤ ker i

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] : RingHom.ker i = pNilradical K 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

• PerfectRing.liftAux i j p x = (iterateFrobeniusEquiv M p (Classical.choose ⋯).1).symm (j (Classical.choose ⋯).2)

@[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

• PerfectRing.lift i j p = { toFun := PerfectRing.liftAux i j p, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

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

• PerfectRing.liftEquiv M i p = { toFun := fun (j : K →+* M) => PerfectRing.lift i j p, invFun := fun (f : L →+* M) => f.comp i, left_inv := ⋯, right_inv := ⋯ }

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] : liftEquiv M (RingHom.id K) p = Equiv.refl (K →+* M)

@[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

• IsPerfectClosure.equiv i j p = { toFun := (↑↑(PerfectRing.lift i j p)).toFun, invFun := PerfectRing.liftAux j i p, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }

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] : (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 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] : (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 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] : equiv i i p = RingEquiv.refl L

@[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] : IsPurelyInseparable K L

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] : IsPRadical (algebraMap K L) p

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.