Perfect field

Stream: maths

[Kenny Lau]

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)

[Kenny Lau]

Do you guys have a better suggestion?

[Kenny Lau]

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

[Kenny Lau]

And go with this definition for now.

[Mario Carneiro]

use discrete_field

[Mario Carneiro]

field is deprecated

[Jz Pan]

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)

[Jz Pan]

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$
• Any finite algebraic extension of K is separable.

Do we have codes for them?

[Johan Commelin]

@Jz Pan I agree with you.

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Kenny Lau]

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

[Jz Pan]

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

[Jz Pan]

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.

[Jz Pan]

Sorry to bump this thread again. I tried to define PerfecField in lean4:

import Mathlib.FieldTheory.Separable
import Mathlib.FieldTheory.PerfectClosure

universe u

class PerfectField (R : Type u) [CommSemiring R] : Prop where
  separable : ∀ {f : Polynomial R}, (hf : Irreducible f) → f.Separable

instance PerfectField.ofCharZero (F : Type u) [Field F] [CharZero F] : PerfectField F where
  separable := Irreducible.separable

section

variable (F : Type u) [Field F] (p : ℕ) [hp : Fact p.Prime] [CharP F p] [PerfectRing F p]

lemma separable_of_perfect_ring {f : Polynomial F} (hf : Irreducible f) : f.Separable := by
  rcases Polynomial.separable_or p hf with h | ⟨_, g, _, h⟩
  · exact h
  · exfalso
    have hcomp : RingHom.comp (frobenius F p) (pthRoot F p) = RingHom.id F :=
      RingHom.ext <| fun x => by
        simp only [RingHom.coe_comp, Function.comp_apply, frobenius_pthRoot, RingHom.id_apply]
    have := (g.map (pthRoot F p)).expand_char p
    rw [Polynomial.map_expand, Polynomial.map_map, hcomp, Polynomial.map_id, h] at this
    rw [this] at hf
    exact Irreducible.not_unit hf <| IsUnit.pow p <|
      of_irreducible_pow (Nat.Prime.ne_one <| Fact.out (self := hp)) hf

/-
cannot find synthesization order for instance ofCharP with type
  ∀ (F : Type u) [inst : Field F] (p : ℕ) [hp : Fact (Nat.Prime p)] [inst_1 : CharP F p] [inst_2 : PerfectRing F p],
    PerfectField F
all remaining arguments have metavariables:
  Fact (Nat.Prime ?p)
  @CharP F AddGroupWithOne.toAddMonoidWithOne ?p
  @PerfectRing F Semifield.toCommSemiring ?p ?hp ?inst✝
-/
instance PerfectField.ofCharP : PerfectField F where
  separable := separable_of_perfect_ring F p

end

It basically works except for the last instance for char p. I got error which I don't understand.

[Jz Pan]

Johan Commelin said:

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

I check this again, it looks like things concerning on perfect complex.

[Jz Pan]

So maybe it could be protected class HomologicalAlgebra.PerfectRing.

[Eric Wieser]

Using class CharPOut (R) [Ring R] (p : outParam ℕ) extends CharP R p instead of CharP works

[Eric Wieser]

What's going on here is that Lean can't work out p for CharP; this is by design because Lean doesn't know if you want to find p = 3 or p = ringChar F.

[Eric Wieser]

By using outParam, you're saying "I don't care what p is, just pick one"

[Eric Wieser]

That being said, I'm not sure if CharPOut is actually a good idea; it just happens to be a workaround to your issue

[Kevin Buzzard]

Perfect complexes have nothing to do with perfect rings BTW. That's just the cool mathematician naming style, designed to confuse newcomers and keep them out of our patch.

[Ruben Van de Velde]

Perfect naming

[Jz Pan]

Eric Wieser said:

What's going on here is that Lean can't work out p for CharP; this is by design because Lean doesn't know if you want to find p = 3 or p = ringChar F.

But why in https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/Perfection.html#Perfection.perfectRing the p can be worked out? I'm confused.

[Eric Wieser]

In that example the p appears on the right of the colon (or more importantly, in the final conclusion)

[Oliver Nash]

Is our definition of docs#PerfectRing correct?

My understanding is that this should be a Prop-valued class and should not contain data.

[Riccardo Brasca]

I also think it should be prop valued.

[Adam Topaz]

I think this is wrong in more than one way. I can't write PerfectRing \Q which is silly.

[Kevin Buzzard]

What even is a perfect ring? Probably we should stick to perfect fields? (:= all finite extensions are separable)

[Adam Topaz]

Ugh, it's even worse than you think: https://en.wikipedia.org/wiki/Perfect_ring

[Adam Topaz]

But I think a "perfect ring" is perfectly ( :smile: ) well defined by saying that all the residue fields are perfect fields.

[Adam Topaz]

at least that should work for reduced rings.

[Adam Topaz]

I don't know what the definition should be (or should be equivalent to) in the non-reduced case.

[Kevin Buzzard]

o_O we have docs#IsSeparable for ring extensions! So we could define perfect to mean that any integral extension is separable?

[Adam Topaz]

what's the minimal polynomial over a ring that's not a field?

[Jz Pan]

Adam Topaz said:

Ugh, it's even worse than you think: https://en.wikipedia.org/wiki/Perfect_ring

I checked that page again, found that there is a line of text barely noticeable:

This article is about perfect rings as introduced by Hyman Bass. For perfect rings of characteristic p generalizing perfect fields, see https://en.wikipedia.org/wiki/Perfect_field.

So I think such perfect ring should be BassRing :rolling_on_the_floor_laughing:

But I think a "perfect ring" is perfectly ( :smile: ) well defined by saying that all the residue fields are perfect fields.

Oops, then Z is also a prefect ring? :thinking:

[Adam Topaz]

Should $\mathbb{Z}$ not be perfect?

[Kevin Buzzard]

Yes, the Wikipedia page for perfect ring is about a completely different concept (typically used in the non-commutative case).

[Kevin Buzzard]

The Wikipedia page for perfect fields says

"More generally, a ring of characteristic p (p a prime) is called perfect if the Frobenius endomorphism is an automorphism.[1] (When restricted to integral domains, this is equivalent to the above condition "every element of k is a pth power".)"

so if that is used in the literature it should probably be the mathlib definition. Note that the page for fields says "see also" and links (incorrectly, in my opinion) to the page for rings.

[Kevin Buzzard]

@Oliver Nash Kenny Lau was going through a huge constructivist phase in 2018, this is probably what's behind it all.

[Adam Topaz]

Ok, maybe there isn't a good definition for arbitrary rings. I think the thing I said about residue fields is probably not the best def (e.g. maybe $\mathbb{Z}$ shouldn't be considered as perfect? E.g. $\mathbb{Z}_p$ is not perfectoid).

[Eric Wieser]

What's wrong with the data-carrying version?

[Kevin Buzzard]

For fields of characteristic p, if something has a pth root then the pth root is unique. For general rings of characteristic p this isn't true (e.g. $\Z/p\Z[X]/(X^2)$ has both the solutions $0$ and $X$ to $x^p=0$) so there's more than one PerfectRing structure on a given ring, which is mathematically not correct.

[Johan Commelin]

Wait, but in that case Frobenius is not an automorphism...

[Kevin Buzzard]

Oh you're right: the current mathlib definition implies this, so my example is no good. So in fact this is a subsingleton.

BTW I only just noticed that if you scroll up to the top of this thread you see Kenny's discussion with Mario about this; the issue was that he wanted perfect fields but we didn't have separable extensions yet.

[Johan Commelin]

But, if I understand correctly, it is still an open (mathlib) question how to unify the definition of perfect ring in char p with the definition of perfect field in char 0...

[Kevin Buzzard]

Our definition is PerfectRing R p and typeclass inference has to find CharP R p. In particular right now we have to supply p. Is that what we want?

[Eric Wieser]

We could have a variant of the typeclass that bundles p

[Eric Wieser]

For when you need the ring to be perfect but your statement doesn't mention p

[Kevin Buzzard]

The definition in Wikipedia for fields doesn't have a p because all fields of characteristic zero are perfect; currently we can't say this (although we can say that all finite extensions are separable). I think that Kenny's definition shouldn't be taken too seriously. Around that time he got very interested in constructivism and so he's just given a constructive definition, it's finset v finite all over again, but the combinatorics people seem to appreciate constructive finsets; I don't think anyone appreciates constructive perfect fields (and if you want to invert pth power in a situation where it's constructive you can just do it yourself)

[Jz Pan]

I use PerfectField R p instead of PerfectField R as a workaround, similar to CharP R p:

import Mathlib.FieldTheory.Separable
import Mathlib.FieldTheory.PerfectClosure

universe u

/- ad-hoc workaround: `PerfectField R p` means `R` is of characteristic `p` and any irreducible
polynomial on `R` is separable (i.e. coprime with its derivative)
FIXME: currently the `p` need to be provided in the type class -/
class PerfectField (R : Type u) [CommSemiring R] (p : ℕ) extends CharP R p where
  separable : ∀ {f : Polynomial R}, (hf : Irreducible f) → f.Separable

instance PerfectField.ofCharZero (F : Type u) [Field F] [CharZero F] : PerfectField F 0 where
  separable := Irreducible.separable

section

variable (F : Type u) [Field F] (p : ℕ) [hp : Fact p.Prime] [CharP F p] [PerfectRing F p]

lemma separable_of_perfect_ring {f : Polynomial F} (hf : Irreducible f) : f.Separable := by
  rcases Polynomial.separable_or p hf with h | ⟨_, g, _, h⟩
  · exact h
  · exfalso
    have hcomp : RingHom.comp (frobenius F p) (pthRoot F p) = RingHom.id F :=
      RingHom.ext <| fun x => by
        simp only [RingHom.coe_comp, Function.comp_apply, frobenius_pthRoot, RingHom.id_apply]
    have := (g.map (pthRoot F p)).expand_char p
    rw [Polynomial.map_expand, Polynomial.map_map, hcomp, Polynomial.map_id, h] at this
    rw [this] at hf
    exact Irreducible.not_unit hf <| IsUnit.pow p <|
      of_irreducible_pow (Nat.Prime.ne_one <| Fact.out (self := hp)) hf

instance PerfectField.ofCharP : PerfectField F p where
  separable := separable_of_perfect_ring F p

end

[Oliver Nash]

Is the following an accurate summary of this thread:

1. We currently have no way to state that a field of characteristic zero is perfect?
2. We currently can only state that a field is perfect if we already know its characteristic?
3. We are not sure if the concept of being perfect should extend from fields to rings. In particular we're not even sure if ℤ should be perfect, to say nothing of non-reduced rings.
4. There is a totally distinct concept which already owns the terminology "Perfect Ring".
5. We should have a Prop-valued typeclass to state that a field is perfect (with no assumptions on characteristic).
6. The following is a correct definition which could replace docs#PerfectRing

class IsPerfectField (K : Type _) [Field K] : Prop where
  separable_of_irreducible : ∀ {f : Polynomial K}, Irreducible f → f.Separable

[Oliver Nash]

One last comment: I have just pulled Serre's "Local Fields" off my bookshelf and on page 35 he says:

We will say that a ring $\Lambda$ of characteristic $p$ is perfect if the endomorphism $x \mapsto x^p$ is an automorphism (i.e., is surjective). Every element $x \in \Lambda$ then hsa a unique $p$ th root, denoted $x^{p^{-1}}$. When $\Lambda$ is a field, this is the usual definition of a perfect field.

[Kevin Buzzard]

So then we have two definitions of perfect ring in the literature :-/

[Kevin Buzzard]

BTW I've noticed before on Zulip that $$p$$th doesn't render as LaTeX because of no space after the closing dollars. You have to write $$p$$ th (which makes a little space after the $p$)

[Eric Wieser]

Does $p$\ th work to eliminate the space? (edit: no)

[Yaël Dillies]

$p$-th works, I believe

[Johan Commelin]

I think it would be good to cover Serre's definition of perfect ring (i.e., not restrict to just fields) because this shows up in p-adic geometry/cohomology kind of stuff. E.g. I think prisms need perfect rings, not just fields.

[Oliver Nash]

I guess we could always ask some expert if there is a characteristic-zero generalisation of Serre's perfect rings. Failing that, how about we switch to the following:

/-- A perfect field.

See also `IsPerfectRing` for a generalisation in positive characteristic. -/
class PerfectField (K : Type _) [Field K] : Prop where
  separable_of_irreducible : ∀ {f : Polynomial K}, Irreducible f → f.Separable

/-- A perfect ring in the sense of Serre.

NB: This is not related to the concept with the same name introduced by Bass (related to projective
covers of modules). -/
class PerfectRing (R : Type _) (p : ℕ) [CommRing R] [Fact p.Prime] [CharP R p] : Prop where
  bijective_frobenius : Bijective $ frobenius R p

instance PerfectField.perfectRing (K : Type _) (p : ℕ)
  [Field K] [Fact p.Prime] [CharP K p] [PerfectField K] : PerfectRing K p :=
  sorry

[Adam Topaz]

Serre’s definition only really makes sense when the characteristic of the ring is prime

[Jz Pan]

how about we switch to the following:

Looks good to me. The only problem is that currently we cannot make an instance of PerfectRing -> PerfectField (unless we remove the requirement p from PerfectRing); we can only make a lemma and asks the user to call it manually everytime they need to use it.

[Oliver Nash]

Right, you're saying this lemma cannot be an instance because p underdetermined.

lemma PerfectRing.toPerfectField (K : Type _) (p : ℕ)
    [Field K] [Fact p.Prime] [CharP K p] [PerfectRing K p] : PerfectField K :=
  sorry

I agree. We could of course solve this by instead making the definition:

class PerfectRing' (R : Type _) [CommRing R] : Prop where
  exists_bijective_frobenius :
    ∃ (p : ℕ) (_ : Fact p.Prime) (_ : CharP R p), Bijective $ frobenius R p

but I think the same problem will arise elsewhere. Indeed since PerfectRing' is a prime characteristic phenomenon, users will need to use the fact that a ring satisfying PerfectRing' R has prime characteristic in their proofs, and to do so we'll have to write lemmas which cannot be instances for the same reason: p will be underdetermined.

[Niels Feld]

Adam Topaz said:

Serre’s definition only really makes sense when the characteristic of the ring is prime

I did not read the whole conversation, so you may already know this: Serre's definition could make sense in characteristic zero if one uses the "characteristic exponent" instead of the usual characteristic. In this case, the Frobenius is the identity map and thus trivially a bijection. I am not sure if this definition is useful in general, though.

[Johan Commelin]

That's a nice idea!

[Oliver Nash]

Does this mean we think ℤ should be perfect after all? Adam had some doubts ?

[Kevin Buzzard]

Oh wait -- we probably don't want all char 0 rings to be perfect, right?

[Adam Topaz]

For example, should $W(\mathbb{F}_p(t))$ be considered as perfect? Probably not.

[Adam Topaz]

Anyway, this is a mathematical discussion, not really about formalization of existing concepts. I think Oliver's code above is the right approach right now.

[Oliver Nash]

I made some time to define / refactor perfect fields this afternoon and I now have a WIP PR #6182 I probably won't have time to return to this till tomorrow afternoon so if someone wants to take it further while I'm busy with other things, that would be great!

[Jz Pan]

I have some code https://github.com/acmepjz/my-lean-test/blob/fd1bb144adc9ccd23794a867a2dd2cf57648b089/myhelper/separable_closed.lean#L40 which should be relevant to your half-finished PerfectField.toPerfectRing.

[Jz Pan]

Oh by the way, are there separable closed field and separable closure available in mathlib4?

[Kevin Buzzard]

I don't think that they are. They would be a very welcome addition! For separable closure a simple approach would be to define it as a subfield of the algebraic closure.

[Oliver Nash]

The PR #6182 with the new definitions is now ready for review.

[Jz Pan]

Kevin Buzzard said:

I don't think that they are. They would be a very welcome addition! For separable closure a simple approach would be to define it as a subfield of the algebraic closure.

I have just made a work-in-progress at https://github.com/leanprover-community/mathlib4/pull/6285

[Jz Pan]

Currently it is mostly a copy-and-paste of IsAlgClosed, though.

[Kevin Buzzard]

I've left a review.

[Jz Pan]

Currently in the file Mathlib/FieldTheory/IsAlgClosed/Basic.lean there is a namespace lift (line 196) defined globally. I think maybe it's better to move this namespace inside IsAlgClosed since this is used to prove IsAlgClosed.lift? I assume that there will be other namespace lift in a lot of irrelevant files. Do you think it's a good idea?

[Maarten Derickx]

Johan Commelin said:

But, if I understand correctly, it is still an open (mathlib) question how to unify the definition of perfect ring in char p with the definition of perfect field in char 0...

P.S. for me perfect fields are very intimately related to separable field extensions. So if there is a definition of a commutative ring R being perfect that would work nicely regardless of the characteristic and in larger generality, then we would first make sure that we have the right definition of separability of R algebras. For me it is a priori not clear wether the definition docs#IsSeparable we have now in lean is equivalent to the notion that is quite standard in the literature: https://projecteuclid.org/journals/osaka-journal-of-mathematics/volume-4/issue-2/On-separable-algebras-over-a-commutative-ring/ojm/1200691953.full .
I.e. one could try to take as definition of a commutative ring $R$ being perfect that $R$ is reduced and for $R$ algebra's $A$ one has that $A$ is reduced implies that $A$ is a separable $R$ algebra.

[Maarten Derickx]

I also wouldn't be surprised that there are different notions of being perfect that will be the correct one depending on the context. For example if one cares more about embedding your ring into a perfect ring (perfect closure) or cares more about having having map from a perfect ring to your ring (perfection).

[Maarten Derickx]

ps. I am fairly certain that we have the wrong definition of docs#IsSeparable for greater generality. The current definition:

class IsSeparable : Prop where
  isIntegral' (x : K) : IsIntegral F x
  separable' (x : K) : (minpoly F x).Separable

However if $F$ is not a domain (which is allowed by the generality of the defintion) then minpoly F x~ is not unique and (minpoly F x).Separable actually depends on the choice of minimal polynomial. Indeed let $F := \mathbb Q \times \mathbb Q$ and $K := \mathbb Q(\sqrt{37}) \times \mathbb Q$ then both $f_1 := x^2 - (37,0)$ and $f_2 := x^2 + (0,1)x - (37,0)$ are minimal polynomials of $(\sqrt{37},0)$, however $f_1$ is not separable while $f_2$ is separable.

However, now I do not know what interpretation to attach to instances class IsSeparable. Does it mean that
1) There exists a minimal polynomial of f of x such that f is separable.
2) For all minimal polynomials f of x one has that f is separable?

[Junyan Xu]

However, now I do not know what interpretation to attach to instances class IsSeparable. Does it mean that
1) There exists a minimal polynomial of f of x such that f is separable.
2) For all minimal polynomials f of x one has that f is separable?

I think: if you have a IsSeparable as a hypothesis, you effectively can only use 1), while if you need to prove IsSeparable, you effectively must prove 2).

[Antoine Chambert-Loir]

If you want a good and general definition, I'd say it should guarantee that for a ring extension R to S, an element s of S which is separable over R leads to a separable algebra R[s].
It also needs to agree with the definition for field which encompasses transcendental extensions.

[Joël Riou]

I would think it is sufficient to cover the case of field extensions (including transcendental ones). Otherwise, this is more an algebraic geometry matter: defining (formally) étale/mooth morphisms. (Anyway, before we have a good definition for the transcendental case, a quick patch could be to rename the current IsSeparable as IsAlgebraicSeparable.)

[Johan Commelin]

We have formal smoothness in mathlib, right?

[Joël Riou]

Yes, in RingTheory.Etale.