Skip to content

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

Closed
ocfnash wants to merge 21 commits intomasterfrom
ocfnash/perfect_fields
Closed

[Merged by Bors] - chore: refactor perfect rings / fields#6182
ocfnash wants to merge 21 commits intomasterfrom
ocfnash/perfect_fields

Conversation

@ocfnash
Copy link
Copy Markdown
Contributor

@ocfnash ocfnash commented Jul 27, 2023 •
edited
Loading

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.

Open in Gitpod

@ocfnash ocfnash added WIP Work in progress t-algebra Algebra (groups, rings, fields, etc) labels Jul 27, 2023
eric-wieser
eric-wieser reviewed Jul 27, 2023
View reviewed changes
acmepjz
acmepjz reviewed Jul 27, 2023
View reviewed changes
acmepjz
acmepjz reviewed Jul 27, 2023
View reviewed changes
acmepjz
acmepjz reviewed Jul 28, 2023
View reviewed changes
@acmepjz
Copy link
Copy Markdown
Collaborator

acmepjz commented Jul 30, 2023

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

@ocfnash
Copy link
Copy Markdown
Contributor Author

ocfnash commented Jul 30, 2023

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!

@ocfnash ocfnash added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed WIP Work in progress labels Jul 30, 2023
@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented Jul 30, 2023

  • 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?

@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jul 30, 2023
@ocfnash
Copy link
Copy Markdown
Contributor Author

ocfnash commented Jul 31, 2023

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

@ocfnash ocfnash removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 10, 2023
jcommelin
jcommelin reviewed Aug 14, 2023
View reviewed changes
jcommelin
jcommelin approved these changes Aug 14, 2023
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

bors d+

@bors
Copy link
Copy Markdown

bors bot commented Aug 14, 2023

✌️ 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.

@ghost ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Aug 14, 2023
@ocfnash
Copy link
Copy Markdown
Contributor Author

ocfnash commented Aug 14, 2023

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Aug 14, 2023
bors bot pushed a commit that referenced this pull request Aug 14, 2023
@ocfnash
chore: refactor perfect rings / fields (#6182)
0543638 
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.
@bors
Copy link
Copy Markdown

bors bot commented Aug 14, 2023

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

bors bot pushed a commit that referenced this pull request Aug 14, 2023
@ocfnash
chore: refactor perfect rings / fields (#6182)
98f1c92 
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.
bors bot pushed a commit that referenced this pull request Aug 14, 2023
@ocfnash
chore: refactor perfect rings / fields (#6182)
77a83cf 
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.
bors bot pushed a commit that referenced this pull request Aug 14, 2023
@ocfnash
chore: refactor perfect rings / fields (#6182)
998681c 
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.
bors bot pushed a commit that referenced this pull request Aug 14, 2023
@ocfnash
chore: refactor perfect rings / fields (#6182)
9388a3e 
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.
bors bot pushed a commit that referenced this pull request Aug 14, 2023
@ocfnash
chore: refactor perfect rings / fields (#6182)
99ef1b1 
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.
bors bot pushed a commit that referenced this pull request Aug 14, 2023
@ocfnash
chore: refactor perfect rings / fields (#6182)
e266692 
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.
bors bot pushed a commit that referenced this pull request Aug 14, 2023
@ocfnash
chore: refactor perfect rings / fields (#6182)
b480d31 
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.
bors bot pushed a commit that referenced this pull request Aug 14, 2023
@ocfnash
chore: refactor perfect rings / fields (#6182)
7106407 
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.
@bors
Copy link
Copy Markdown

bors bot commented Aug 14, 2023

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Aug 14, 2023
@ocfnash
chore: refactor perfect rings / fields (#6182)
9fcddd8 
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.
@bors
Copy link
Copy Markdown

bors bot commented Aug 14, 2023

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Aug 14, 2023
@ocfnash
chore: refactor perfect rings / fields (#6182)
75bcb18 
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.
@bors
Copy link
Copy Markdown

bors bot commented Aug 14, 2023

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.

@bors bors bot changed the title chore: refactor perfect rings / fields [Merged by Bors] - chore: refactor perfect rings / fields Aug 14, 2023
@bors bors bot closed this Aug 14, 2023
@bors bors bot deleted the ocfnash/perfect_fields branch August 14, 2023 22:04
kim-em pushed a commit that referenced this pull request Aug 15, 2023
@ocfnash @kim-em
chore: refactor perfect rings / fields (#6182)
a7429dd 
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.
kim-em pushed a commit that referenced this pull request Aug 15, 2023
@ocfnash @kim-em
chore: refactor perfect rings / fields (#6182)
9c29532 
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.
kim-em pushed a commit that referenced this pull request Aug 15, 2023
@ocfnash @kim-em
chore: refactor perfect rings / fields (#6182)
282c9ff 
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.
kim-em pushed a commit that referenced this pull request Aug 17, 2023
@ocfnash @kim-em
chore: refactor perfect rings / fields (#6182)
75e0ce9 
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

@jcommelin jcommelin jcommelin approved these changes

@kbuzzard kbuzzard kbuzzard approved these changes

+1 more reviewer

@acmepjz acmepjz acmepjz left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@ocfnash @acmepjz @eric-wieser @jcommelin @kbuzzard