Exponent of purely inseparable field extension

Stream: Is there code for X?

[Michał Staromiejski]

I can't find a definition of the exponent of a purely inseparable field extension (see for example here)? I'm aware of docs#isPurelyInseparable_iff_pow_mem and co. If we don't have the exponent definition, I'd like to add it and once it's there I'd like to add also the following:
For a purely inseparable field extension L/K with exponent e, the iterated Frobenius map x ↦ x ^ p ^ s (with s ≥ e) on L has range contained in (algebraMap K L).range so one can define both the ring homomorphism L →+* K and the semilinear map L →ₛₗ[iterateFrobenius F p s] K (for any subfield F of K) acting via x ↦ x ^ p ^ s.

Here is my attempt in my private project.

[Jz Pan]

I don't think this is in mathlib yet, although we have some dicsussions. Let me find.

[Jz Pan]

No we don't have this yet. I think we even don't have the following: if L/K is a finite purely inseparable extension of exponential characteristic p, then there exists a natural number n such that [L:K]=p^n.

I think such n is not the same as the exponent you mentioned, is it?

[Jz Pan]

When I was developing the theory of separable degree and purely inseparable extensions, I followed the Wikipedia article. So I'm not aware of the definition of exponent of purely inseparable extensions.

[Jz Pan]

Michał Staromiejski said:

... I'd like to add also the following:
For a purely inseparable field extension L/K with exponent e, the iterated Frobenius map x ↦ x ^ p ^ s (with s ≥ e) on L has range contained in (algebraMap K L).range so one can define both the ring homomorphism L →+* K and the semilinear map L →ₛₗ[iterateFrobenius F p s] K (for any subfield F of K) acting via x ↦ x ^ p ^ s.

But in order to define this, you don't need to define the exponent. You only require that s is such that L^(p^s) is contained in K. Just put it as a requirement in your definition, and I think it's OK.

[Jz Pan]

... and is it the same to say that for any x in L, x^(p^s) is in K?

[Michał Staromiejski]

@Jz Pan Thanks for the answer!

Jz Pan said:

No we don't have this yet. I think we even don't have the following: if L/K is a finite purely inseparable extension of exponential characteristic p, then there exists a natural number n such that [L:K]=p^n.

I think such n is not the same as the exponent you mentioned, is it?

It's not the exponent but it's a tight upper bound. I actually do have a proof that [L:K]=p^n for inseparable extensions so I might contribute it.

Talking about the exponent, I was thinking to define it this way:

import Mathlib.FieldTheory.PurelyInseparable

namespace IsPurelyInseparable

variable (K L) [Field K] [Field L] [Algebra K L]

/-- A predicate class on a purely inseparable extension saying that there is a natural number
    `e` such that `a ^ p ^ e ∈ K` for all `a ∈ L`. -/
class Exponent [IsPurelyInseparable K L] [ExpChar K p] : Prop :=
    exp : ∃ e, ∀ a, a ^ p ^ e ∈ (algebraMap K L).range

open Classical in
/-- The *exponent* of a purely inseparable extension, i.e., the smallest
    natural number `e` such that `a ^ p ^ e ∈ K` for all `a ∈ L`. -/
noncomputable def exponent [IsPurelyInseparable K L] [ExpChar K p] [Exponent K L p] : ℕ :=
  Nat.find ‹Exponent K L p›.exp

Or should IsPurelyInseparable K L be bundled? :thinking:

[Michał Staromiejski]

Jz Pan said:

Michał Staromiejski said:

... I'd like to add also the following:
For a purely inseparable field extension L/K with exponent e, the iterated Frobenius map x ↦ x ^ p ^ s (with s ≥ e) on L has range contained in (algebraMap K L).range so one can define both the ring homomorphism L →+* K and the semilinear map L →ₛₗ[iterateFrobenius F p s] K (for any subfield F of K) acting via x ↦ x ^ p ^ s.

But in order to define this, you don't need to define the exponent. You only require that s is such that L^(p^s) is contained in K. Just put it as a requirement in your definition, and I think it's OK.

This was my first approach but It's less general so I thought maybe adding definition of the exponent and make it more general would be of greater value. But I can start simply. The thing is, I do have proofs already, it's only to shape them correctly and add.

[Michał Staromiejski]

Jz Pan said:

... and is it the same to say that for any x in L, x^(p^s) is in K?

Yes, only that s has to be universal.
BTW, existence of such an s means that the exponent exists, see my proposed definition :smile:

[Jz Pan]

Michał Staromiejski said:

Talking about the exponent, I was thinking to define it this way:

import Mathlib.FieldTheory.PurelyInseparable

namespace IsPurelyInseparable

variable (K L) [Field K] [Field L] [Algebra K L]

/-- A predicate class on a purely inseparable extension saying that there is a natural number
    `e` such that `a ^ p ^ e ∈ K` for all `a ∈ L`. -/
class Exponent [IsPurelyInseparable K L] [ExpChar K p] : Prop :=
    exp : ∃ e, ∀ a, a ^ p ^ e ∈ (algebraMap K L).range

open Classical in
/-- The *exponent* of a purely inseparable extension, i.e., the smallest
    natural number `e` such that `a ^ p ^ e ∈ K` for all `a ∈ L`. -/
noncomputable def exponent [IsPurelyInseparable K L] [ExpChar K p] [Exponent K L p] : ℕ :=
  Nat.find ‹Exponent K L p›.exp

Or should IsPurelyInseparable K L be bundled? :thinking:

Personally I'd like to do the API design similar to Polynomial.IsSeparableContraction, Polynomial.HasSeparableContraction (both of them are only Prop but not class), and Polynomial.HasSeparableContraction.degree, in the file https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/Polynomial/SeparableDegree.html. But it's only my personal opinion. (@Junyan Xu what do you think?) The final decision is up to you.

Michał Staromiejski said:

Jz Pan said:

... But in order to define this, you don't need to define the exponent. You only require that s is such that L^(p^s) is contained in K. Just put it as a requirement in your definition, and I think it's OK.

This was my first approach but It's less general so I thought maybe adding definition of the exponent and make it more general would be of greater value. But I can start simply. The thing is, I do have proofs already, it's only to shape them correctly and add.

I think use L^(p^s) contained in K approach you need fewer additional definition to define your maps. Of course we can also have an iff theorem to convert this assumption to/from s ≥ e. Personally I think this is better.

Michał Staromiejski said:

Jz Pan said:

... and is it the same to say that for any x in L, x^(p^s) is in K?

Yes, only that s has to be universal.
BTW, existence of such an s means that the exponent exists, see my proposed definition :smile:

Thanks for the clarification. So we can have another iff theorem to give the exponent another characterization.

[Jz Pan]

More precisely, I think we can have IsPurelyInseparable.IsExponent, IsPurelyInseparable.HasExponent and IsPurelyInseparable.HasExponent.exponent.

Also, do you look at docs#IsPRadical which generalizes purely inseparable to non-field case? Do you think we should also define exponent for it?

[Michał Staromiejski]

I was thinking to go analogously to exponent of a monoid docs#Monoid.exponent, they first define similar predicate (but non-class). Do you mean you would avoid defining predicate class? Maybe better would be:

import Mathlib.FieldTheory.PurelyInseparable

namespace IsPurelyInseparable

variable (K L) [Field K] [Field L] [Algebra K L]

/-- A predicate class on a purely inseparable extension saying that there is a natural number
    `e` such that `a ^ p ^ e ∈ K` for all `a ∈ L`. -/
class WithExponent [ExpChar K p] : Prop :=
  isPurelyInseparable : IsPurelyInseparable K L
  hasExponent : ∃ e, ∀ a, a ^ p ^ e ∈ (algebraMap K L).range

open Classical in
/-- The *exponent* of a purely inseparable extension, i.e., the smallest
    natural number `e` such that `a ^ p ^ e ∈ K` for all `a ∈ L`. -/
noncomputable def exponent [ExpChar K p] [IsPurelyInseparable.WithExponent K L p] : ℕ :=
  Nat.find ‹Exponent K L p›.hasExponent

I think it is quite similar to Algebra.IsAlgebraic R A (but Algebra R A is not bundled). I have a feeling that it should be a class but no idea if IsPurelyInseparable should be bundled or not.

[Michał Staromiejski]

As for IsPRadical, it seems that the number is not universal? But once the exponent is defined for purely inseparable extensions, we could think to generalize.

[Michał Staromiejski]

If IsPRadical is generalization of IsPurelyInseparable, do we have

instance [IsPurelyInseparable K L] [ExpChar L p] : IsPRadical (algebraMap K L) p := sorry

?

[Jz Pan]

I think an unbundled version is better (just like your previous Exponent). If it is me, I'll call it HasExponent and make it just a def.

As for your second question, yes we have docs#IsPurelyInseparable.isPRadical.

Currently IsPRadical is not used in elsewhere. So if you think you don't need it, it's OK to just stick to IsPurelyInseparable.

[Michał Staromiejski]

Thanks, I think having an exponent is a property of a purely inseparable extension (just like having exp-char p), which is a typeclass parameter. In case of polynomials, it's different as polynomial parameters are not typeclass. That's why my feeling is it should be typeclass parameter. The only question is if we should write

example [IsPurelyInseparable K L] [ExpChar L p] [WithExponent K L p] : ... := ...

or

example [ExpChar L p] [WithExponent K L p] : ... := ...

because for WithExponent we need IsPurelyInseparable (for example in a similar way IsPurelyInseparable requires Algebra.IsIntegral and this one is bundled). But I'm not sure.

[Jz Pan]

I prefer this:

import Mathlib.FieldTheory.PurelyInseparable

namespace IsPurelyInseparable

variable (K L) [Field K] [Field L] [Algebra K L]

/-- A predicate class on a purely inseparable extension saying that there is a natural number
    `e` such that `a ^ p ^ e ∈ K` for all `a ∈ L`. -/
class HasExponent [ExpChar K p] : Prop where
  hasExponent : ∃ e, ∀ a, a ^ p ^ e ∈ (algebraMap K L).range

-- Note that `HasExponent` automatically implies `IsPurelyInseparable`, here we need an instance states it

open Classical in
/-- The *exponent* of a purely inseparable extension, i.e., the smallest
    natural number `e` such that `a ^ p ^ e ∈ K` for all `a ∈ L`. -/
noncomputable def exponent [ExpChar K p] [IsPurelyInseparable.HasExponent K L p] : ℕ :=
  Nat.find ‹HasExponent K L p›.hasExponent

Since you already assume that both of them are fields, the assumption of HasExponent automatically implies IsPurelyInseparable (via docs#isPurelyInseparable_iff_pow_mem), so I don't think we need to bundle IsPurelyInseparable into it.

Also, I think we can eliminate the p in the definition of HasExponent, just like in the definition of docs#perfectClosure, just use ringExpChar F to replace p.

[Jz Pan]

(deleted)

[Michał Staromiejski]

How HasExponent K L p implies IsPurelyInseparable K L in your code?

About [ExpChar K p], I think it might be necessary to have some defeqs maybe? If we can get rid of it, why is it necessary in other places?

[Jz Pan]

Michał Staromiejski said:

How HasExponent K L p implies IsPurelyInseparable K L in your code?

What about this:

import Mathlib.FieldTheory.PurelyInseparable

namespace IsPurelyInseparable

variable (K L : Type*)

section Ring

variable [CommRing K] [Ring L] [Algebra K L]

/-- A predicate class on a ring extension saying that there is a natural number
    `e` such that `a ^ ringExpChar K ^ e ∈ K` for all `a ∈ L`. -/
class HasExponent : Prop where
  hasExponent' : ∃ e, ∀ a, a ^ ringExpChar K ^ e ∈ (algebraMap K L).range

theorem HasExponent.hasExponent (p : ℕ) [ExpChar K p] [HasExponent K L] :
    ∃ e, ∀ a, a ^ p ^ e ∈ (algebraMap K L).range :=
  ringExpChar.eq K p ▸ hasExponent'

open scoped Classical in
/-- The *exponent* of a purely inseparable extension, i.e., the smallest
    natural number `e` such that `a ^ p ^ e ∈ K` for all `a ∈ L`. -/
noncomputable def exponent [HasExponent K L] : ℕ :=
  Nat.find ‹HasExponent K L›.hasExponent'

end Ring

section FieldAndDomain

variable [Field K] [Ring L] [IsDomain L] [Algebra K L]

instance [HasExponent K L] : IsPurelyInseparable K L := by
  obtain ⟨n, h⟩ := ‹HasExponent K L›.hasExponent'
  exact (isPurelyInseparable_iff_pow_mem K (ringExpChar K)).2 fun x ↦ ⟨n, h x⟩

end FieldAndDomain

About [ExpChar K p], I think it might be necessary to have some defeqs maybe? If we can get rid of it, why is it necessary in other places?

No, we don't need ExpChar in the definition of IsPurelyInseparable and perfectClosure. It only used in IsPRadical. We use ringExpChar in perfectClosure, so yes, docs#mem_perfectClosure_iff is rfl while docs#mem_perfectClosure_iff_pow_mem is not rfl. But I think it's not harmful.

[Michał Staromiejski]

Thanks, will follow this path then. Will prepare a PR with some basic results as well, and let's discuss it further then.

[Michał Staromiejski]

BTW, Mathlib.FieldTheory.PurelyInseparable is quite big already, should we split it? I'm thinking about Separability directory and all the related files inside, but could be also Separable and PurelyInseparable separately (thos a lot of results about separable extensions are in Mathlib.FieldTheory.PurelyInseparable now). Any suggestions?

[Jz Pan]

I'd like to made a correction: hasExponent['] should be has_exponent['] (since its type has type Prop) or exists_exponent['] if strictly following naming convention.

Michał Staromiejski said:

BTW, Mathlib.FieldTheory.PurelyInseparable is quite big already, should we split it? I'm thinking about Separability directory and all the related files inside, but could be also Separable and PurelyInseparable separately (thos a lot of results about separable extensions are in Mathlib.FieldTheory.PurelyInseparable now). Any suggestions?

I think it's reasonable. A possible approach is PurelyInseparable/(Basic,RelPerfectClosure,InsepDegree)? And your results could go PurelyInseparable/Exponent.

[Michał Staromiejski]

So you think that common Separability directory is not a good idea?

[Michał Staromiejski]

there is already:

Separable.lean
SeparableClosure.lean
SeparableDegree.lean
IsSepClosed.lean

[Jz Pan]

Michał Staromiejski said:

So you think that common Separability directory is not a good idea?

I have no idea on this. The definition of Separable is in mathlib long before my work on SeparableDegree (which contains some important properties of Separable).

[Michał Staromiejski]

Maybe some maintainer could comment here?

[Kevin Buzzard]

A Separable directory looks reasonable, but the PR that makes it should probably do nothing but move the files around without adding or removing any theorems or definitions.

[Michał Staromiejski]

@Kevin Buzzard that's clear, but how about PurelyInseparable? I was thinking that maybe Separability would be a common name for both, but if you think that Separable is ok, I could proceed with that.

[Michał Staromiejski]

Ok, I think I'll split just PurelyInseparable.

[Michał Staromiejski]

@Jz Pan Some seemingly basic results (for example IntermediateField.isPurelyInseparable_adjoin[_simple]_iff_pow_mem) use le_perfectClosure_iff which requires perfectClosure. Do you think there is proof not using perfectClosure?

[Junyan Xu]

Why do you want to avoid perfectClosure? Wouldn't you need to repeat the same proofs in the construction of perfectClosure if you want to prove isPurelyInseparable_adjoin[_simple]_iff_pow_mem directly?

[Kevin Buzzard]

If you want Separable and PurelyInseparable directories this sounds fine -- the more files and directories we have, the more modular the library is, and I think modularity is a good thing, especially here where we're splitting at concepts which are mathematically meaningful

[Jz Pan]

Michał Staromiejski said:

Some seemingly basic results (for example IntermediateField.isPurelyInseparable_adjoin[_simple]_iff_pow_mem) use le_perfectClosure_iff which requires perfectClosure. Do you think there is proof not using perfectClosure?

No, at least I'm not aware of.

[Jz Pan]

Also, the docstring of perfectClosure says "It is also the maximal purely inseparable subextension", so I think it's closely related to IsPurelyInseparable.

[Michał Staromiejski]

Alright, shall I keep it in Basic then?

[Jz Pan]

Michał Staromiejski said:

Alright, shall I keep it in Basic then?

Sure.

[Michał Staromiejski]

#21343 is ready, I split as initially suggested, with some results in RelPerfectClosure.

[Jz Pan]

@Junyan Xu Would you like to have a look at PR #21343? I think it's good to go.

[Michał Staromiejski]

Created PR #21372 introducing definitions and basic facts about exponent. @Jz Pan please have a look.

A remark from my side: the definition of the exponent for an element now is meaningful only when ringExpChar > 1 (so it is prime). In all the application I encountered that is enough but maybe we need to extend the definition to ringExpChar = 1 by setting the exponent of the element to 0. The question is how to do it in the cleanest possible way? Naive option is to just introduce if but is it the best option?

[Michał Staromiejski]

More general question: when working with exponential characteristic, is there any guideline as when to use instance parameter [ExpChar K p] and have p, and when to use ringExpChar K? It seems that with [ExpChar K p] the API is a bit more complicated (extra explicit parameter p) but OTOH, one can use rcases ‹ExpChar K p› with _ | ⟨hp⟩ and there is no need to constantly use ringExpChar.eq K p.

[Michał Staromiejski]

Created separate PR topic: #PR reviews > #21372 Exponent for (purely inseparable) field extensions

[Johan Commelin]

I would advise to use ExpChar K p almost always. It works much better when working with field extensions.

[Michał Staromiejski]

@Jz Pan could you comment here? I guess your opinion is not to use it. I stated most results in terms of ringExpChar K without much trouble and overuse of ringExpChar.eq K p and actually not having this p everywhere seems better. But I think we need some guideline...

@Johan Commelin I just want to understand in which sense it works better? I mean, there are pros and cons of course but maybe someone with more experience in formalizing results that make use of ringExpChar might guide here...

[Johan Commelin]

If you have a type like ZMod p, then it depends on the term p. If you have a field extension [Algebra K L], and K and L are both fields of characteristic p, then you might want to talk about their prime fields.
We now have 4 candidates:

• ZMod (ringChar K)
• ZMod (ringChar L)
• ZMod (ringExpChar K)
• ZMod (ringExpChar L)

However, if we use [CharP K p] and [CharP L p] (or the ExpChar variants), then all of those prime fields collapse into ZMod p.

We indeed have lemmas like ringExpChar.eq. But rewriting with those in types like ZMod _ will very often lead to problems with dependent types. (Motive is not type correct error, or heterogeneous equalities, etc)

[Michał Staromiejski]

Thanks a lot @Johan Commelin. And I guess there is no smart way to get rid of this extra explicit parameter p, so that I write for example exponent K L and not exponent K L p?

[Johan Commelin]

It very much depends on what you want to do. I think if you are making a new definition, then you might want to use ringExpChar. But in the API lemmas for the definition, you want to use [ExpChar K p].

[Johan Commelin]

I guess there is a more refined rule: if the statement doesn't need p, then it is fine to avoid it. In proofs you can start with let p := and then set up the instances [ExpChar K p] local to the proof.
But if a statement refers to the characteristic in any form, then it should be as a variable p, and not as ringExpChar K.

[Michał Staromiejski]

Thanks, that makes sense.

[Jz Pan]

I agree with Johan's comments.