-
Notifications
You must be signed in to change notification settings - Fork 299
[Merged by Bors] - refactor(ring_theory/algebra): use bundled homs, allow semirings #2303
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM
@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. |
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? |
The last line in |
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. |
I failed, again. The reason is that I am asking more from typeclass inference in usual situations (it should find a |
@sgouezel Is your failed attempt somewhere on github? |
I have put it in a branch |
It seems that your problem with |
|
Some functions and lemmas in `polynomial` now take bundled homomorphisms as arguments.
I had done a mess when picking the relevant bits of #2319. Hopefully fixed. |
Merge conflict was because of #2348 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
@@ -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] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
If you want, you can mark the identity as default algebra (i.e. inhabited
instance).
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Probably a better choice is of_ring_hom 0 _
because it works for all R
, A
.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
All ring homs are unital, so that won't work.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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
".
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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...
Did I understand the new workflow? And is it working? |
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.
Build succeeded |
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.
…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.
…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.
Fixes #2297
Build fails because of some class instance problems, asked on Zulip, no answer yet.
TO CONTRIBUTORS:
Make sure you have:
If this PR is related to a discussion on Zulip, please include a link in the discussion.
For reviewers: code review check list