Basic results about purely inseparable extensions

This file contains basic definitions and results about purely inseparable extensions.

Main definitions

• IsPurelyInseparable: typeclass for purely inseparable field extensions: an algebraic extension E / F is purely inseparable if and only if the minimal polynomial of every element of E ∖ F is not separable.

Main results

• IsPurelyInseparable.surjective_algebraMap_of_isSeparable, IsPurelyInseparable.bijective_algebraMap_of_isSeparable, IntermediateField.eq_bot_of_isPurelyInseparable_of_isSeparable: if E / F is both purely inseparable and separable, then algebraMap F E is surjective (hence bijective). In particular, if an intermediate field of E / F is both purely inseparable and separable, then it is equal to F.

• isPurelyInseparable_iff_pow_mem: a field extension E / F of exponential characteristic q is purely inseparable if and only if for every element x of E, there exists a natural number n such that x ^ (q ^ n) is contained in F.

• IsPurelyInseparable.trans: if E / F and K / E are both purely inseparable extensions, then K / F is also purely inseparable.

• isPurelyInseparable_iff_natSepDegree_eq_one: E / F is purely inseparable if and only if for every element x of E, its minimal polynomial has separable degree one.

• isPurelyInseparable_iff_minpoly_eq_X_pow_sub_C: a field extension E / F of exponential characteristic q is purely inseparable if and only if for every element x of E, the minimal polynomial of x over F is of form X ^ (q ^ n) - y for some natural number n and some element y of F.

• isPurelyInseparable_iff_minpoly_eq_X_sub_C_pow: a field extension E / F of exponential characteristic q is purely inseparable if and only if for every element x of E, the minimal polynomial of x over F is of form (X - x) ^ (q ^ n) for some natural number n.

• isPurelyInseparable_iff_finSepDegree_eq_one: an extension is purely inseparable if and only if it has finite separable degree (Field.finSepDegree) one.

• IsPurelyInseparable.normal: a purely inseparable extension is normal.

• separableClosure.isPurelyInseparable: if E / F is algebraic, then E is purely inseparable over the separable closure of F in E.

• separableClosure_le_iff: if E / F is algebraic, then an intermediate field of E / F contains the separable closure of F in E if and only if E is purely inseparable over it.

• eq_separableClosure_iff: if E / F is algebraic, then an intermediate field of E / F is equal to the separable closure of F in E if and only if it is separable over F, and E is purely inseparable over it.

• IsPurelyInseparable.injective_comp_algebraMap: if E / F is purely inseparable, then for any reduced ring L, the map (E →+* L) → (F →+* L) induced by algebraMap F E is injective. In particular, a purely inseparable field extension is an epimorphism in the category of fields.

• IsPurelyInseparable.of_injective_comp_algebraMap: if L is an algebraically closed field containing E, such that the map (E →+* L) → (F →+* L) induced by algebraMap F E is injective, then E / F is purely inseparable. As a corollary, epimorphisms in the category of fields must be purely inseparable extensions.

• Field.finSepDegree_eq: if E / F is algebraic, then the Field.finSepDegree F E is equal to Field.sepDegree F E as a natural number. This means that the cardinality of Field.Emb F E and the degree of (separableClosure F E) / F are both finite or infinite, and when they are finite, they coincide.

• Field.finSepDegree_mul_finInsepDegree: the finite separable degree multiply by the finite inseparable degree is equal to the (finite) field extension degree.

Tags

separable degree, degree, separable closure, purely inseparable

class IsPurelyInseparable (F : Type u_1) (E : Type u_2) [CommRing F] [Ring E] [Algebra F E] : Prop

Typeclass for purely inseparable field extensions: an algebraic extension E / F is purely inseparable if and only if the minimal polynomial of every element of E ∖ F is not separable.

We define this for general (commutative) rings and only assume F and E are fields if this is needed for a proof.

• isIntegral : Algebra.IsIntegral F E
• inseparable' (x : E) : IsSeparable F x → x ∈ (algebraMap F E).range

theorem IsPurelyInseparable.isIntegral' (F : Type u_1) {E : Type u_2} [CommRing F] [Ring E] [Algebra F E] [IsPurelyInseparable F E] (x : E) : IsIntegral F x

theorem IsPurelyInseparable.isAlgebraic (F : Type u_1) (E : Type u_2) [CommRing F] [Ring E] [Algebra F E] [Nontrivial F] [IsPurelyInseparable F E] : Algebra.IsAlgebraic F E

theorem IsPurelyInseparable.inseparable (F : Type u_1) {E : Type u_2} [CommRing F] [Ring E] [Algebra F E] [IsPurelyInseparable F E] (x : E) : IsSeparable F x → x ∈ (algebraMap F E).range

theorem isPurelyInseparable_iff {F : Type u_1} {E : Type u_2} [CommRing F] [Ring E] [Algebra F E] : IsPurelyInseparable F E ↔ ∀ (x : E), IsIntegral F x ∧ (IsSeparable F x → x ∈ (algebraMap F E).range)

theorem AlgEquiv.isPurelyInseparable {F : Type u_1} {E : Type u_2} [CommRing F] [Ring E] [Algebra F E] {K : Type u_3} [Ring K] [Algebra F K] (e : K ≃ₐ[F] E) [IsPurelyInseparable F K] : IsPurelyInseparable F E

Transfer IsPurelyInseparable across an AlgEquiv.

theorem AlgEquiv.isPurelyInseparable_iff {F : Type u_1} {E : Type u_2} [CommRing F] [Ring E] [Algebra F E] {K : Type u_3} [Ring K] [Algebra F K] (e : K ≃ₐ[F] E) : IsPurelyInseparable F K ↔ IsPurelyInseparable F E

instance Algebra.IsAlgebraic.isPurelyInseparable_of_isSepClosed {F : Type u} {E : Type v} [Field F] [Ring E] [IsDomain E] [Algebra F E] [Algebra.IsAlgebraic F E] [IsSepClosed F] : IsPurelyInseparable F E

If E / F is an algebraic extension, F is separably closed, then E / F is purely inseparable.

theorem IsPurelyInseparable.surjective_algebraMap_of_isSeparable (F : Type u_1) (E : Type u_2) [CommRing F] [Ring E] [Algebra F E] [IsPurelyInseparable F E] [Algebra.IsSeparable F E] : Function.Surjective ⇑(algebraMap F E)

If E / F is both purely inseparable and separable, then algebraMap F E is surjective.

theorem IsPurelyInseparable.bijective_algebraMap_of_isSeparable (F : Type u_1) (E : Type u_2) [CommRing F] [Ring E] [Algebra F E] [Nontrivial E] [IsDomain F] [Module.IsTorsionFree F E] [IsPurelyInseparable F E] [Algebra.IsSeparable F E] : Function.Bijective ⇑(algebraMap F E)

If E / F is both purely inseparable and separable, then algebraMap F E is bijective.

theorem Subalgebra.eq_bot_of_isPurelyInseparable_of_isSeparable {F : Type u_1} {E : Type u_2} [CommRing F] [Ring E] [Algebra F E] (L : Subalgebra F E) [IsPurelyInseparable F ↥L] [Algebra.IsSeparable F ↥L] : L = ⊥

If a subalgebra of E / F is both purely inseparable and separable, then it is equal to F.

theorem IntermediateField.eq_bot_of_isPurelyInseparable_of_isSeparable {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (L : IntermediateField F E) [IsPurelyInseparable F ↥L] [Algebra.IsSeparable F ↥L] : L = ⊥

If an intermediate field of E / F is both purely inseparable and separable, then it is equal to F.

theorem separableClosure.eq_bot_of_isPurelyInseparable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [IsPurelyInseparable F E] : separableClosure F E = ⊥

If E / F is purely inseparable, then the separable closure of F in E is equal to F.

theorem separableClosure.eq_bot_iff {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] [Algebra.IsAlgebraic F E] : separableClosure F E = ⊥ ↔ IsPurelyInseparable F E

If E / F is an algebraic extension, then the separable closure of F in E is equal to F if and only if E / F is purely inseparable.

instance isPurelyInseparable_self (F : Type u_1) [CommRing F] : IsPurelyInseparable F F

theorem isPurelyInseparable_iff_pow_mem (F : Type u) {E : Type v} [Field F] [Ring E] [IsDomain E] [Algebra F E] (q : ℕ) [ExpChar F q] : IsPurelyInseparable F E ↔ ∀ (x : E), ∃ (n : ℕ), x ^ q ^ n ∈ (algebraMap F E).range

A field extension E / F of exponential characteristic q is purely inseparable if and only if for every element x of E, there exists a natural number n such that x ^ (q ^ n) is contained in F.

theorem IsPurelyInseparable.pow_mem (F : Type u) {E : Type v} [Field F] [Ring E] [IsDomain E] [Algebra F E] (q : ℕ) [ExpChar F q] (x : E) [IsPurelyInseparable F E] : ∃ (n : ℕ), x ^ q ^ n ∈ (algebraMap F E).range

theorem IsPurelyInseparable.tower_bot (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type w) [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] [IsPurelyInseparable F K] : IsPurelyInseparable F E

If K / E / F is a field extension tower such that K / F is purely inseparable, then E / F is also purely inseparable.

theorem IsPurelyInseparable.tower_top (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type w) [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] [h : IsPurelyInseparable F K] : IsPurelyInseparable E K

If K / E / F is a field extension tower such that K / F is purely inseparable, then K / E is also purely inseparable.

theorem IsPurelyInseparable.trans (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type w) [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] [h1 : IsPurelyInseparable F E] [h2 : IsPurelyInseparable E K] : IsPurelyInseparable F K

If E / F and K / E are both purely inseparable extensions, then K / F is also purely inseparable.

instance IntermediateField.isPurelyInseparable_tower_bot (F : Type u) [Field F] (K : Type w) [Field K] [Algebra F K] (M : IntermediateField F K) [IsPurelyInseparable F K] : IsPurelyInseparable F ↥M

instance IntermediateField.isPurelyInseparable_tower_top (F : Type u) [Field F] (K : Type w) [Field K] [Algebra F K] (M : IntermediateField F K) [IsPurelyInseparable F K] : IsPurelyInseparable (↥M) K

theorem isPurelyInseparable_iff_natSepDegree_eq_one (F : Type u) {E : Type v} [Field F] [Field E] [Algebra F E] : IsPurelyInseparable F E ↔ ∀ (x : E), (minpoly F x).natSepDegree = 1

A field extension E / F is purely inseparable if and only if for every element x of E, its minimal polynomial has separable degree one.

theorem IsPurelyInseparable.natSepDegree_eq_one (F : Type u) {E : Type v} [Field F] [Field E] [Algebra F E] [IsPurelyInseparable F E] (x : E) : (minpoly F x).natSepDegree = 1

theorem isPurelyInseparable_iff_minpoly_eq_X_pow_sub_C (F : Type u) {E : Type v} [Field F] [Field E] [Algebra F E] (q : ℕ) [hF : ExpChar F q] : IsPurelyInseparable F E ↔ ∀ (x : E), ∃ (n : ℕ) (y : F), minpoly F x = Polynomial.X ^ q ^ n - Polynomial.C y

A field extension E / F of exponential characteristic q is purely inseparable if and only if for every element x of E, the minimal polynomial of x over F is of form X ^ (q ^ n) - y for some natural number n and some element y of F.

theorem IsPurelyInseparable.minpoly_eq_X_pow_sub_C (F : Type u) {E : Type v} [Field F] [Field E] [Algebra F E] (q : ℕ) [ExpChar F q] [IsPurelyInseparable F E] (x : E) : ∃ (n : ℕ) (y : F), minpoly F x = Polynomial.X ^ q ^ n - Polynomial.C y

theorem isPurelyInseparable_iff_minpoly_eq_X_sub_C_pow (F : Type u) {E : Type v} [Field F] [Field E] [Algebra F E] (q : ℕ) [hF : ExpChar F q] : IsPurelyInseparable F E ↔ ∀ (x : E), ∃ (n : ℕ), Polynomial.map (algebraMap F E) (minpoly F x) = (Polynomial.X - Polynomial.C x) ^ q ^ n

A field extension E / F of exponential characteristic q is purely inseparable if and only if for every element x of E, the minimal polynomial of x over F is of form (X - x) ^ (q ^ n) for some natural number n.

theorem IsPurelyInseparable.minpoly_eq_X_sub_C_pow (F : Type u) {E : Type v} [Field F] [Field E] [Algebra F E] (q : ℕ) [ExpChar F q] [IsPurelyInseparable F E] (x : E) : ∃ (n : ℕ), Polynomial.map (algebraMap F E) (minpoly F x) = (Polynomial.X - Polynomial.C x) ^ q ^ n

theorem IsPurelyInseparable.finrank_eq_pow (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (q : ℕ) [ExpChar F q] [IsPurelyInseparable F E] [FiniteDimensional F E] : ∃ (n : ℕ), Module.finrank F E = q ^ n

theorem isPurelyInseparable_of_finSepDegree_eq_one {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (hdeg : Field.finSepDegree F E = 1) : IsPurelyInseparable F E

If an extension has finite separable degree one, then it is purely inseparable.

theorem IsPurelyInseparable.injective_comp_algebraMap (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [IsPurelyInseparable F E] (L : Type u_2) [CommRing L] [IsReduced L] : Function.Injective fun (f : E →+* L) => f.comp (algebraMap F E)

If E / F is purely inseparable, then for any reduced ring L, the map (E →+* L) → (F →+* L) induced by algebraMap F E is injective. In particular, a purely inseparable field extension is an epimorphism in the category of fields.

theorem IsPurelyInseparable.injective_restrictDomain (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [IsPurelyInseparable F E] (R : Type u_1) (L : Type u_2) [CommSemiring R] [Algebra R F] [Algebra R E] [CommRing L] [IsReduced L] [Algebra R L] [IsScalarTower R F E] : Function.Injective (AlgHom.restrictDomain F)

instance IsPurelyInseparable.instNonemptyAlgHomOfPerfectField (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [IsPurelyInseparable F E] (L : Type u_2) [Field L] [PerfectField L] [Algebra F L] : Nonempty (E →ₐ[F] L)

theorem IsPurelyInseparable.bijective_comp_algebraMap (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [IsPurelyInseparable F E] (L : Type u_2) [Field L] [PerfectField L] : Function.Bijective fun (f : E →+* L) => f.comp (algebraMap F E)

theorem IsPurelyInseparable.bijective_restrictDomain (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [IsPurelyInseparable F E] (R : Type u_1) (L : Type u_2) [CommSemiring R] [Algebra R F] [Algebra R E] [Field L] [PerfectField L] [Algebra R L] [IsScalarTower R F E] : Function.Bijective (AlgHom.restrictDomain F)

instance instSubsingletonAlgHomOfIsPurelyInseparable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [IsPurelyInseparable F E] (L : Type w) [CommRing L] [IsReduced L] [Algebra F L] : Subsingleton (E →ₐ[F] L)

If E / F is purely inseparable, then for any reduced F-algebra L, there exists at most one F-algebra homomorphism from E to L.

@[implicit_reducible]

instance instUniqueAlgHomOfIsPurelyInseparable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [IsPurelyInseparable F E] (L : Type w) [CommRing L] [IsReduced L] [Algebra F L] [Algebra E L] [IsScalarTower F E L] : Unique (E →ₐ[F] L)

@[implicit_reducible]

noncomputable instance instUniqueEmbOfIsPurelyInseparable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [IsPurelyInseparable F E] : Unique (Field.Emb F E)

If E / F is purely inseparable, then Field.Emb F E has exactly one element.

theorem IsPurelyInseparable.finSepDegree_eq_one (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [IsPurelyInseparable F E] : Field.finSepDegree F E = 1

A purely inseparable extension has finite separable degree one.

theorem IsPurelyInseparable.sepDegree_eq_one (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [IsPurelyInseparable F E] : Field.sepDegree F E = 1

A purely inseparable extension has separable degree one.

theorem IsPurelyInseparable.insepDegree_eq (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [IsPurelyInseparable F E] : Field.insepDegree F E = Module.rank F E

A purely inseparable extension has inseparable degree equal to degree.

theorem IsPurelyInseparable.finInsepDegree_eq (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [IsPurelyInseparable F E] : Field.finInsepDegree F E = Module.finrank F E

A purely inseparable extension has finite inseparable degree equal to degree.

theorem isPurelyInseparable_iff_finSepDegree_eq_one (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] : IsPurelyInseparable F E ↔ Field.finSepDegree F E = 1

An extension is purely inseparable if and only if it has finite separable degree one.

theorem isSeparable_iff_finInsepDegree_eq_one (F : Type u) [Field F] (K : Type w) [Field K] [Algebra F K] : Algebra.IsSeparable F K ↔ Field.finInsepDegree F K = 1

theorem isPurelyInseparable_iff_fd_isPurelyInseparable {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] [Algebra.IsAlgebraic F E] : IsPurelyInseparable F E ↔ ∀ (L : IntermediateField F E), FiniteDimensional F ↥L → IsPurelyInseparable F ↥L

An algebraic extension is purely inseparable if and only if all of its finite-dimensional subextensions are purely inseparable.

instance IsPurelyInseparable.normal (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [IsPurelyInseparable F E] : Normal F E

A purely inseparable extension is normal.

instance separableClosure.isPurelyInseparable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [Algebra.IsAlgebraic F E] : IsPurelyInseparable (↥(separableClosure F E)) E

If E / F is algebraic, then E is purely inseparable over the separable closure of F in E.

theorem Field.Emb.cardinal_separableClosure (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [Algebra.IsAlgebraic F E] : Cardinal.mk (Emb F ↥(separableClosure F E)) = Cardinal.mk (Emb F E)

theorem finInsepDegree_eq_pow (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (q : ℕ) [ExpChar F q] [FiniteDimensional F E] : ∃ (n : ℕ), Field.finInsepDegree F E = q ^ n

theorem separableClosure_le (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (L : IntermediateField F E) [h : IsPurelyInseparable (↥L) E] : separableClosure F E ≤ L

An intermediate field of E / F contains the separable closure of F in E if E is purely inseparable over it.

theorem separableClosure_le_iff (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [Algebra.IsAlgebraic F E] (L : IntermediateField F E) : separableClosure F E ≤ L ↔ IsPurelyInseparable (↥L) E

If E / F is algebraic, then an intermediate field of E / F contains the separable closure of F in E if and only if E is purely inseparable over it.

theorem eq_separableClosure (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (L : IntermediateField F E) [Algebra.IsSeparable F ↥L] [IsPurelyInseparable (↥L) E] : L = separableClosure F E

If an intermediate field of E / F is separable over F, and E is purely inseparable over it, then it is equal to the separable closure of F in E.

theorem eq_separableClosure_iff (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [Algebra.IsAlgebraic F E] (L : IntermediateField F E) : L = separableClosure F E ↔ Algebra.IsSeparable F ↥L ∧ IsPurelyInseparable (↥L) E

If E / F is algebraic, then an intermediate field of E / F is equal to the separable closure of F in E if and only if it is separable over F, and E is purely inseparable over it.

theorem IsPurelyInseparable.of_injective_comp_algebraMap (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (L : Type w) [Field L] [IsAlgClosed L] [Nonempty (E →+* L)] (h : Function.Injective fun (f : E →+* L) => f.comp (algebraMap F E)) : IsPurelyInseparable F E

If L is an algebraically closed field containing E, such that the map (E →+* L) → (F →+* L) induced by algebraMap F E is injective, then E / F is purely inseparable. As a corollary, epimorphisms in the category of fields must be purely inseparable extensions.

instance IntermediateField.isPurelyInseparable_bot (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] : IsPurelyInseparable F ↥⊥

theorem isSepClosed_iff_isPurelyInseparable_algebraicClosure (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [IsAlgClosure F E] : IsSepClosed F ↔ IsPurelyInseparable F E

If E is an algebraic closure of F, then F is separably closed if and only if E / F is purely inseparable.

theorem Algebra.IsAlgebraic.isSepClosed {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] [Algebra.IsAlgebraic F E] [IsSepClosed F] : IsSepClosed E

If E / F is an algebraic extension, F is separably closed, then E is also separably closed.

theorem Field.finSepDegree_eq (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [Algebra.IsAlgebraic F E] : finSepDegree F E = Cardinal.toNat (sepDegree F E)

If E / F is algebraic, then the Field.finSepDegree F E is equal to Field.sepDegree F E as a natural number. This means that the cardinality of Field.Emb F E and the degree of (separableClosure F E) / F are both finite or infinite, and when they are finite, they coincide.

theorem Field.finSepDegree_mul_finInsepDegree (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] : finSepDegree F E * finInsepDegree F E = Module.finrank F E

The finite separable degree multiply by the finite inseparable degree is equal to the (finite) field extension degree.

theorem separableClosure.adjoin_eq_of_isAlgebraic_of_isSeparable {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (K : Type w) [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] [Algebra.IsAlgebraic F E] [Algebra.IsSeparable E K] : IntermediateField.adjoin E ↑(separableClosure F K) = ⊤

If K / E / F is a field extension tower, such that E / F is algebraic and K / E is separable, then E adjoin separableClosure F K is equal to K. It is a special case of separableClosure.adjoin_eq_of_isAlgebraic, and is an intermediate result used to prove it.

theorem separableClosure.adjoin_eq_of_isAlgebraic {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (K : Type w) [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] [Algebra.IsAlgebraic F E] : IntermediateField.adjoin E ↑(separableClosure F K) = separableClosure E K

If K / E / F is a field extension tower, such that E / F is algebraic, then E adjoin separableClosure F K is equal to separableClosure E K.

def Subalgebra.perfectClosure (R : Type u_1) (A : Type u_2) [CommSemiring R] [CommSemiring A] [Algebra R A] (p : ℕ) [ExpChar A p] : Subalgebra R A

The perfect closure of R in A are the elements x : A such that x ^ p ^ n is in R for some n, where p is the exponential characteristic of R.

theorem Subalgebra.mem_perfectClosure_iff {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] {p : ℕ} [ExpChar A p] {x : A} : x ∈ perfectClosure R A p ↔ ∃ (n : ℕ), x ^ p ^ n ∈ (algebraMap R A).rangeS

theorem IsPurelyInseparable.exists_pow_pow_mem_range_tensorProduct_of_expChar {k : Type u_1} {K : Type u_2} {R : Type u_3} [Field k] [Field K] [Algebra k K] [CommRing R] [Algebra k R] [IsPurelyInseparable k K] (q : ℕ) [ExpChar k q] (x : TensorProduct k R K) : ∃ (n : ℕ), x ^ q ^ n ∈ (algebraMap R (TensorProduct k R K)).range

theorem IsPurelyInseparable.exists_pow_mem_range_tensorProduct {k : Type u_1} {K : Type u_2} {R : Type u_3} [Field k] [Field K] [Algebra k K] [CommRing R] [Algebra k R] [IsPurelyInseparable k K] (x : TensorProduct k R K) : ∃ n > 0, x ^ n ∈ (algebraMap R (TensorProduct k R K)).range