[Merged by Bors] - chore: refactor perfect rings / fields

[ocfnash]

The main changes are:

• we replace the data-bearing PerfectRing typeclass with a Prop-valued (non-constructive) version,
• we introduce a new typeclass PerfectField,
• we add a proof that a perfect field of positive characteristic has surjective Frobenius map,
• we add some basic facts such as perfection of finite rings / fields and products of perfect rings.

---

[acmepjz]

Would you like to add the equivalent definition that a field is perfect if and only if every (finite) algebraic extension is surjective?

[ocfnash]

Would you like to add the equivalent definition that a field is perfect if and only if every (finite) algebraic extension is surjective?

I don't plan to do this, but I encourage you to do it in a follow-up PR if you're interested!

[eric-wieser]

• we replace the data-bearing PerfectRing typeclass with a Prop-valued (non-constructive) version,

What do we gain by removing the data here? Is the problem that the class would not be subsingleton?

[ocfnash]

Is the problem that the class would not be subsingleton?

In fact the existing class is subsingleton:

-- Using old definition of `PerfectRing` (which I propose to remove):
example : Subsingleton (PerfectRing R p) := by
  constructor
  rintro ⟨f, -, hfr⟩ ⟨g, hgl, -⟩
  congr
  exact LeftInverse.eq_rightInverse hfr hgl

so this is not the problem.

What do we gain by removing the data here?

I claim the advantages are:

1. We get a type-theoretic expression of the above uniqueness.
2. Our formalisation becomes classical as opposed to constructive. [Albeit you might argue this begs your question.]
3. The sociological advantage that proposed new definition is what most mathematicians would expect.
4. We cannot author lemmas which depend on a particular instance of PerfectRing (e.g., stemming from finiteness) that might fail in a rewrite when PerfectRing is available some other way. [I admit, slightly speculative.]

[jcommelin]

bors d+

[bors]

✌️ ocfnash can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[ocfnash]

bors merge

[bors]

This PR was included in a batch that was canceled, it will be automatically retried

[bors]

Build failed (retrying...):

• Build

[bors]

Build failed (retrying...):

• Build

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style