[Merged by Bors] - feat(field_theory): define the field of rational functions `ratfunc` #9563

Vierkantor · 2021-10-05T13:20:42Z

This PR defines ratfunc K as the field of rational functions over a field K, in terms of fraction_ring (polynomial K). I have been careful to use structures and @[irreducible] defs. Not only does that make for a nicer API, it also helps quite a bit with unification since the check can stop at ratfunc and doesn't have to start unfolding along the lines of fraction_field.field → localization.comm_ring → localization.comm_monoid → localization.has_mul and/or polynomial.integral_domain → polynomial.comm_ring → polynomial.ring → polynomial.semiring.

Most of the API is automatically derived from the (components of the) is_fraction_ring instance: the map polynomial K → ratpoly K is algebra_map, the isomorphism to fraction_ring (polynomial K) is is_localization.alg_equiv, ...

As a first application to verify that the definitions work, I rewrote function_field in terms of ratfunc.

It turned into a big PR, so you might like to review the individual commits instead:

src/field_theory/ratpoly.lean

alexjbest · 2021-10-05T14:17:05Z

/bikeshed: I would call this rational_functions or even function_field instead of ratpoly, as this matches the conventions in magma and sage respectively.

bryangingechen · 2021-10-06T17:18:44Z

I've also only ever seen these as referred to as rational functions; Wikipedia agrees as well https://en.wikipedia.org/wiki/Rational_function

Vierkantor · 2021-10-07T16:15:40Z

I've also only ever seen these as referred to as rational functions; Wikipedia agrees as well https://en.wikipedia.org/wiki/Rational_function

I've searched-and-replaced everything from ratpoly to ratfunc and [Rr]ational polynomial to [Rr]ational function. 👍

jcommelin · 2021-10-20T04:31:01Z

@Vierkantor I think this PR can also update the undergrad file:
https://github.com/leanprover-community/mathlib/blob/master/docs/undergrad.yaml#L189

Vierkantor · 2021-10-20T07:04:52Z

@Vierkantor I think this PR can also update the undergrad file: https://github.com/leanprover-community/mathlib/blob/master/docs/undergrad.yaml#L189

Good point, almost forgot!

…ials (#9600) This PR provides a couple of lemmas involving the division and gcd operators of polynomials that I needed for #9563. The ones that generalized to `euclidean_domain` and/or `gcd_monoid` are provided in the respective files. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

github-actions · 2021-11-11T21:26:44Z

🎉 Great news! Looks like all the dependencies have been resolved:

~~[Merged by Bors] - feat(algebra/gcd_monoid): trivial gcd on comm_group_with_zeros #9602~~
~~[Merged by Bors] - feat(data/polynomial): assorted lemmas on division and gcd of polynomials #9600~~

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

src/ring_theory/witt_vector/frobenius.lean

src/number_theory/function_field.lean

src/field_theory/ratfunc.lean

jcommelin · 2021-11-12T11:46:26Z

CI isn't happy

Vierkantor · 2021-11-16T08:44:30Z

Pretty sure it was one of the CI runners that failed/timed out - it worked on my machine. After restarting, it looks like it's building correctly again.

jcommelin

Thanks 🎉

bors merge

…9563) This PR defines `ratfunc K` as the field of rational functions over a field `K`, in terms of `fraction_ring (polynomial K)`. I have been careful to use `structure`s and `@[irreducible] def`s. Not only does that make for a nicer API, it also helps quite a bit with unification since the check can stop at `ratfunc` and doesn't have to start unfolding along the lines of `fraction_field.field → localization.comm_ring → localization.comm_monoid → localization.has_mul` and/or `polynomial.integral_domain → polynomial.comm_ring → polynomial.ring → polynomial.semiring`. Most of the API is automatically derived from the (components of the) `is_fraction_ring` instance: the map `polynomial K → ratpoly K` is `algebra_map`, the isomorphism to `fraction_ring (polynomial K)` is `is_localization.alg_equiv`, ... As a first application to verify that the definitions work, I rewrote `function_field` in terms of `ratfunc`. Co-authored-by: Johan Commelin <johan@commelin.net>

eric-wieser · 2021-11-16T12:48:39Z

bors merge

(bors crashed)

…9563) This PR defines `ratfunc K` as the field of rational functions over a field `K`, in terms of `fraction_ring (polynomial K)`. I have been careful to use `structure`s and `@[irreducible] def`s. Not only does that make for a nicer API, it also helps quite a bit with unification since the check can stop at `ratfunc` and doesn't have to start unfolding along the lines of `fraction_field.field → localization.comm_ring → localization.comm_monoid → localization.has_mul` and/or `polynomial.integral_domain → polynomial.comm_ring → polynomial.ring → polynomial.semiring`. Most of the API is automatically derived from the (components of the) `is_fraction_ring` instance: the map `polynomial K → ratpoly K` is `algebra_map`, the isomorphism to `fraction_ring (polynomial K)` is `is_localization.alg_equiv`, ... As a first application to verify that the definitions work, I rewrote `function_field` in terms of `ratfunc`. Co-authored-by: Johan Commelin <johan@commelin.net>

bors · 2021-11-16T14:42:42Z

Pull request successfully merged into master.

Build succeeded:

Vierkantor added the awaiting-review The author would like community review of the PR label Oct 5, 2021

Vierkantor requested a review from jcommelin October 5, 2021 13:20

Vierkantor commented Oct 5, 2021

View reviewed changes

src/field_theory/ratpoly.lean Outdated Show resolved Hide resolved

jcommelin reviewed Oct 5, 2021

View reviewed changes

src/field_theory/ratpoly.lean Outdated Show resolved Hide resolved

src/field_theory/ratpoly.lean Outdated Show resolved Hide resolved

jcommelin added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Oct 5, 2021

Vierkantor mentioned this pull request Oct 7, 2021

[Merged by Bors] - feat(data/polynomial): assorted lemmas on division and gcd of polynomials #9600

Closed

Vierkantor force-pushed the ratpoly branch from 91d9f18 to 6973999 Compare October 7, 2021 16:09

Vierkantor changed the title ~~feat(field_theory): define the field of rational polynomials ratpoly~~ feat(field_theory): define the field of rational functions ratfunc Oct 7, 2021

github-actions bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Oct 7, 2021

Vierkantor added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Oct 7, 2021

Vierkantor force-pushed the ratpoly branch from 1d5078d to 817ffb1 Compare October 8, 2021 09:19

Vierkantor mentioned this pull request Oct 8, 2021

[Merged by Bors] - feat(number_theory): define the class number #9071

Closed

5 tasks

Vierkantor force-pushed the ratpoly branch from 817ffb1 to 5e4f2f4 Compare October 11, 2021 15:39

github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 25, 2021

Vierkantor force-pushed the ratpoly branch from be6317f to 86ae99a Compare November 8, 2021 12:43

github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Nov 8, 2021

github-actions bot added merge-conflict Please `git merge origin/master` then a bot will remove this label. and removed blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. labels Nov 11, 2021

Vierkantor added 3 commits November 11, 2021 23:11

feat(field_theory): define the field of rational polynomials

db7bc35

Use ratpoly in function_field

8bbb2b8

Define num, denom, C, X and eval; basic results

e710f61

Vierkantor added 5 commits November 11, 2021 23:11

Fix

02005d9

Rename ratpoly to ratfunc

18fed3c

Update to newer polynomial-div-gcd-lemmas

d003a4a

Update undergrad.yaml

f97fa60

Update to latest mathlib (renames, elaboration changes)

a92ab55

Vierkantor force-pushed the ratpoly branch from 7b2fa9b to a92ab55 Compare November 11, 2021 23:11

github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Nov 11, 2021

jcommelin reviewed Nov 12, 2021

View reviewed changes

src/ring_theory/witt_vector/frobenius.lean Outdated Show resolved Hide resolved

src/number_theory/function_field.lean Outdated Show resolved Hide resolved

src/field_theory/ratfunc.lean Outdated Show resolved Hide resolved

Update src/ring_theory/witt_vector/frobenius.lean

001e7aa

jcommelin added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Nov 12, 2021

Typo fix: funcion → function

8456a91

Vierkantor added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Nov 12, 2021

jcommelin added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Nov 12, 2021

Vierkantor added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Nov 16, 2021

jcommelin approved these changes Nov 16, 2021

View reviewed changes

github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Nov 16, 2021

bors bot changed the title ~~feat(field_theory): define the field of rational functions ratfunc~~ [Merged by Bors] - feat(field_theory): define the field of rational functions ratfunc Nov 16, 2021

bors bot closed this Nov 16, 2021

bors bot deleted the ratpoly branch November 16, 2021 14:42

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(field_theory): define the field of rational functions `ratfunc` #9563

[Merged by Bors] - feat(field_theory): define the field of rational functions `ratfunc` #9563

Vierkantor commented Oct 5, 2021 •

edited

Loading

alexjbest commented Oct 5, 2021

bryangingechen commented Oct 6, 2021

Vierkantor commented Oct 7, 2021

jcommelin commented Oct 20, 2021

Vierkantor commented Oct 20, 2021

github-actions bot commented Nov 11, 2021

jcommelin commented Nov 12, 2021

Vierkantor commented Nov 16, 2021

jcommelin left a comment

eric-wieser commented Nov 16, 2021

bors bot commented Nov 16, 2021

[Merged by Bors] - feat(field_theory): define the field of rational functions ratfunc #9563

[Merged by Bors] - feat(field_theory): define the field of rational functions ratfunc #9563

Conversation

Vierkantor commented Oct 5, 2021 • edited Loading

alexjbest commented Oct 5, 2021

bryangingechen commented Oct 6, 2021

Vierkantor commented Oct 7, 2021

jcommelin commented Oct 20, 2021

Vierkantor commented Oct 20, 2021

github-actions bot commented Nov 11, 2021

jcommelin commented Nov 12, 2021

Vierkantor commented Nov 16, 2021

jcommelin left a comment

Choose a reason for hiding this comment

eric-wieser commented Nov 16, 2021

bors bot commented Nov 16, 2021

[Merged by Bors] - feat(field_theory): define the field of rational functions `ratfunc` #9563

[Merged by Bors] - feat(field_theory): define the field of rational functions `ratfunc` #9563

Vierkantor commented Oct 5, 2021 •

edited

Loading