Zulip Chat Archive

Stream: maths

Topic: Perfect field


view this post on Zulip Kenny Lau (Oct 17 2018 at 08:26):

Currently this is my definition:

/-- A perfect field is a field of characteristic p that has p-th root. -/
class perfect_field (α : Type u) [field α] (p : ) [char_p α p] : Type u :=
(pth_root : α  α)
(frobenius_pth_root :  x, frobenius α p (pth_root x) = x)

view this post on Zulip Kenny Lau (Oct 17 2018 at 08:26):

Do you guys have a better suggestion?

view this post on Zulip Kenny Lau (Oct 17 2018 at 08:27):

My idea is that we can change the definition once we have enough theory about separable polynomials.

view this post on Zulip Kenny Lau (Oct 17 2018 at 08:27):

And go with this definition for now.

view this post on Zulip Mario Carneiro (Oct 17 2018 at 18:16):

use discrete_field

view this post on Zulip Mario Carneiro (Oct 17 2018 at 18:16):

field is deprecated

view this post on Zulip Jz Pan (Dec 26 2020 at 07:36):

Sorry for bumping this thread, but I have two concerns:
(1) recently the perfect_field is removed from mathlib in favor of perfect_ring (in field_theory.perfect_closure).
(2) the current definition of perfect_ring (as well as the previous perfect_field) require that the characteristic is a prime and must be given in the definition.
This makes the following assertion tedious to write: "if the field K is of characteristic 2, moreover require that K is perfect". char_p K 2 → @perfect_field K _ 2 (by norm_num) (by assumption)

view this post on Zulip Jz Pan (Dec 26 2020 at 07:46):

And I think perfect field is not necessarily of characteristic p, and the correct definitions are the following three equivalent definitions:

  • K is of characteristic zero, or K is of characteristic p and the Frobenius map is surjective (equivalent to isomorphism).
  • Any irreducible polynomial f over K has no multiple roots, equivalently, (f,f)=1 (f,f')=1
  • Any finite algebraic extension of K is separable.

Do we have codes for them?

view this post on Zulip Johan Commelin (Dec 26 2020 at 07:52):

@Jz Pan I agree with you.

view this post on Zulip Johan Commelin (Dec 26 2020 at 07:52):

By now we have separable polynomials and separable extensions. So it makes sense to go with the second/third option.

view this post on Zulip Johan Commelin (Dec 26 2020 at 07:53):

I think by now mathlib even has the equivalence of points 2 and 3.

view this post on Zulip Johan Commelin (Dec 26 2020 at 07:59):

@Jz Pan Would you agree that the current definition of perfect_ring should stay the way it is? For general rings, I don't know of a definition that doesn't assume char_p R p from the start.

view this post on Zulip Johan Commelin (Dec 26 2020 at 08:00):

(Aside: I just learned that there is conflicting terminology. Apparently perfect ring also means https://en.wikipedia.org/wiki/Perfect_ring)

view this post on Zulip Kenny Lau (Dec 26 2020 at 08:46):

Maybe the thing in the wiki page can be perfect_ring' /s

view this post on Zulip Jz Pan (Dec 26 2020 at 09:11):

Yes, I think the definition of perfect ring should not be changed for now.

view this post on Zulip Jz Pan (Dec 26 2020 at 09:16):

For my usage I just use the following code

def nth_power_surjective (K : Type*) [field K] (n : ) :=
 x : K,  y : K, y ^ n = x

def my_perfect_field (K : Type*) [field K] :=
ring_char K = 0  nth_power_surjective K (ring_char K)

and I write ring_char K = 2 → my_perfect_field K.


Last updated: May 11 2021 at 15:12 UTC