[Merged by Bors] - refactor(ring_theory/algebra): use bundled homs, allow semirings #2303

urkud · 2020-03-31T16:53:31Z

Fixes #2297

Build fails because of some class instance problems, asked on Zulip, no answer yet.

TO CONTRIBUTORS:

Make sure you have:

reviewed and applied the coding style: coding, naming
reviewed and applied the documentation requirements
for tactics:
- added or adapted documentation in the tactic doc entries
- write an example of use of the new feature in test/tactics.lean or another test file
make sure definitions and lemmas are put in the right files
make sure definitions and lemmas are not redundant

If this PR is related to a discussion on Zulip, please include a link in the discussion.

For reviewers: code review check list

jcommelin

LGTM

urkud · 2020-04-01T07:53:50Z

@jcommelin It fails to build, and I don't know how to fix this. I mean, I can supply arguments explicitly but this is a workaround, not a fix.

jcommelin · 2020-04-01T18:31:29Z

I see some type class resolution trace in the build logs, but I couldn't extract what failed exactly. Are you having trouble with coercing bundled homs to the underlying function?

urkud · 2020-04-01T19:33:47Z

The last line in lie_algebra.lean fails to find matrix_algebra instance, probably because of some semiring vs ring or semimodule vs module issues.

sgouezel · 2020-04-02T12:09:25Z

One thing I wanted to do is to get rid of modules, and replace them by semimodules everywhere. It used to fail in Lean 3.4 because of type class issues, but now that some problems have been solved in Lean 3.7 it might be the right time to try again. Would you mind if I tried to do this starting from your branch, and see if it fixes your problem?

urkud · 2020-04-02T13:48:10Z

One thing I wanted to do is to get rid of modules, and replace them by semimodules everywhere. It used to fail in Lean 3.4 because of type class issues, but now that some problems have been solved in Lean 3.7 it might be the right time to try again. Would you mind if I tried to do this starting from your branch, and see if it fixes your problem?

This would be awesome. Unfortunately I won't have time to participate in this for a couple of days.

sgouezel · 2020-04-03T15:26:33Z

I failed, again. The reason is that I am asking more from typeclass inference in usual situations (it should find a semiringinstance from a ring, and an add_comm_monoid from an add_comm_group), and it is simply not up to the task because there are way too many instances around. So, it becomes unbearably slow (and times out in some situations). Still, my time was not totally wasted as it uncovered a bug, see #2319.

urkud · 2020-04-03T16:56:22Z

@sgouezel Is your failed attempt somewhere on github?

sgouezel · 2020-04-04T09:16:47Z

I have put it in a branch remove_module. It already fails in linear_algebra/basic. There is also something fishy going on in dfinsupp, that I will investigate further. You are welcome to play with the branch (and push whatever you want to it) if you like.

sgouezel · 2020-04-04T09:24:59Z

In fact the dfinsupp is fixed by #2319, so I have merged #2319 and now the issue has disappeared.

sgouezel · 2020-04-04T10:37:11Z

It seems that your problem with lie_ring is also solved by #2319. I have merged the relevant bits in your branch, and now the instance is found. I have just pushed this to your branch.

urkud · 2020-04-07T01:11:33Z

merge master failed, so I rebased.

Some functions and lemmas in `polynomial` now take bundled homomorphisms as arguments.

sgouezel · 2020-04-08T19:02:19Z

I had done a mess when picking the relevant bits of #2319. Hopefully fixed.

urkud · 2020-04-08T19:51:35Z

Merge conflict was because of #2348

jcommelin

Thanks a lot for this major effort!!!
If you would rather ignore my comments and merge this before it breaks, that's fine with me.

src/ring_theory/algebra.lean

jcommelin · 2020-04-09T13:08:51Z

src/ring_theory/algebra.lean

@@ -26,55 +26,37 @@ ring is the under category R ↓ CRing. In the categorical
 setting we have a forgetful functor R-Alg ⥤ R-Mod.
 However here it extends module in order to preserve
 definitional equality in certain cases. -/
-class algebra (R : Type u) (A : Type v) [comm_ring R] [ring A] extends has_scalar R A :=
-(to_fun : R → A) [hom : is_ring_hom to_fun]
+@[nolint has_inhabited_instance]


If you want, you can mark the identity as default algebra (i.e. inhabited instance).

Probably a better choice is of_ring_hom 0 _ because it works for all R, A.

All ring homs are unital, so that won't work.

You're right. That's why I didn't add an inhabited instance in the first place. I don't want to add an inhabited sequence just to make the linter happy. For me this nolint says "there is no universal construction that turns a semiring into an algebra over a given comm_semiring".

Ok, I guess there's not really a consensus on what to do with this linter (-;
I like your point of view, but I also like @semorrison 's idea of using these instances to sprinkle examples into mathlib...

src/ring_theory/algebra.lean

sgouezel · 2020-04-10T10:06:22Z

Did I understand the new workflow? And is it working?
bors r+

gebner · 2020-04-10T10:19:40Z

bors r+

Fixes #2297 Build fails because of some class instance problems, asked [on Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Need.20help.20with.20class.20instance.20resolution), no answer yet.

bors · 2020-04-10T11:53:12Z

Build succeeded

Build mathlib

bors · 2020-04-10T11:53:12Z

Pull request successfully merged into master.

…nprover-community#2303) Fixes leanprover-community#2297 Build fails because of some class instance problems, asked [on Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Need.20help.20with.20class.20instance.20resolution), no answer yet.

urkud added the WIP Work in progress label Mar 31, 2020

jcommelin approved these changes Apr 1, 2020

View reviewed changes

urkud added the help-wanted The author needs attention to resolve issues label Apr 1, 2020

urkud and others added 2 commits April 6, 2020 21:08

Snapshot

e07521e

pick up relevant bits of #2319

8090a16

urkud force-pushed the algebra-bundled branch from 5e5e32a to 8090a16 Compare April 7, 2020 01:10

urkud added 2 commits April 7, 2020 15:40

Fix compile

411bc6c

Some functions and lemmas in `polynomial` now take bundled homomorphisms as arguments.

Fix lint

fbdd303

urkud added awaiting-review The author would like community review of the PR and removed WIP Work in progress help-wanted The author needs attention to resolve issues labels Apr 8, 2020

Use bundled ring_hom API

4abf5d2

sgouezel marked this pull request as ready for review April 8, 2020 18:49

merge master

a9c3176

urkud mentioned this pull request Apr 9, 2020

[Merged by Bors] - feat(data/monoid_algebra): algebra structure, lift of morphisms #2366

Closed

7 tasks

jcommelin reviewed Apr 9, 2020

View reviewed changes

Use extends ring_hom as suggested by @jcommelin

d58cfb4

urkud added 2 commits April 9, 2020 13:39

Add a rudimentary module docstring

9f864fd

Fix compile

9fb4bf0

bors bot changed the title ~~refactor(ring_theory/algebra): use bundled homs, allow semirings~~ [Merged by Bors] - refactor(ring_theory/algebra): use bundled homs, allow semirings Apr 10, 2020

bors bot closed this Apr 10, 2020

ChrisHughes24 deleted the algebra-bundled branch April 10, 2020 12:30

YaelDillies removed the awaiting-review The author would like community review of the PR label Nov 15, 2021

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - refactor(ring_theory/algebra): use bundled homs, allow semirings #2303

[Merged by Bors] - refactor(ring_theory/algebra): use bundled homs, allow semirings #2303

urkud commented Mar 31, 2020 •

edited

Loading

jcommelin left a comment

urkud commented Apr 1, 2020

jcommelin commented Apr 1, 2020

urkud commented Apr 1, 2020 •

edited

Loading

sgouezel commented Apr 2, 2020

urkud commented Apr 2, 2020

sgouezel commented Apr 3, 2020

urkud commented Apr 3, 2020

sgouezel commented Apr 4, 2020 •

edited

Loading

sgouezel commented Apr 4, 2020

sgouezel commented Apr 4, 2020

urkud commented Apr 7, 2020

sgouezel commented Apr 8, 2020

urkud commented Apr 8, 2020

jcommelin left a comment

jcommelin Apr 9, 2020

urkud Apr 9, 2020

jcommelin Apr 9, 2020

urkud Apr 9, 2020

jcommelin Apr 9, 2020

sgouezel commented Apr 10, 2020

gebner commented Apr 10, 2020

bors bot commented Apr 10, 2020

bors bot commented Apr 10, 2020

[Merged by Bors] - refactor(ring_theory/algebra): use bundled homs, allow semirings #2303

[Merged by Bors] - refactor(ring_theory/algebra): use bundled homs, allow semirings #2303

Conversation

urkud commented Mar 31, 2020 • edited Loading

jcommelin left a comment

Choose a reason for hiding this comment

urkud commented Apr 1, 2020

jcommelin commented Apr 1, 2020

urkud commented Apr 1, 2020 • edited Loading

sgouezel commented Apr 2, 2020

urkud commented Apr 2, 2020

sgouezel commented Apr 3, 2020

urkud commented Apr 3, 2020

sgouezel commented Apr 4, 2020 • edited Loading

sgouezel commented Apr 4, 2020

sgouezel commented Apr 4, 2020

urkud commented Apr 7, 2020

sgouezel commented Apr 8, 2020

urkud commented Apr 8, 2020

jcommelin left a comment

Choose a reason for hiding this comment

jcommelin Apr 9, 2020

Choose a reason for hiding this comment

urkud Apr 9, 2020

Choose a reason for hiding this comment

jcommelin Apr 9, 2020

Choose a reason for hiding this comment

urkud Apr 9, 2020

Choose a reason for hiding this comment

jcommelin Apr 9, 2020

Choose a reason for hiding this comment

sgouezel commented Apr 10, 2020

gebner commented Apr 10, 2020

bors bot commented Apr 10, 2020

Build succeeded

bors bot commented Apr 10, 2020

Pull request successfully merged into master.

urkud commented Mar 31, 2020 •

edited

Loading

urkud commented Apr 1, 2020 •

edited

Loading

sgouezel commented Apr 4, 2020 •

edited

Loading