-
Notifications
You must be signed in to change notification settings - Fork 234
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat: port Algebra.Category.Group.Injective #3908
Conversation
mattrobball
commented
May 11, 2023
•
edited by github-actions
bot
edited by github-actions
bot
- depends on: [Merged by Bors] - feat: port Algebra.Module.Injective #3873
Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean
commit 3ff5641 Author: Matthew Ballard <matt@mrb.email> Date: Wed May 10 10:39:49 2023 -0400 misc commit a148357 Author: Matthew Ballard <matt@mrb.email> Date: Wed May 10 10:31:51 2023 -0400 capitalize import file commit 6aab7dd Author: Matthew Ballard <matt@mrb.email> Date: Wed May 10 10:29:52 2023 -0400 lint commit 9d3e55d Author: Matthew Ballard <matt@mrb.email> Date: Wed May 10 10:27:38 2023 -0400 fix last errors, rename commit 5aa6268 Author: Matthew Ballard <matt@mrb.email> Date: Tue May 9 17:06:18 2023 -0400 fix more commit df92a44 Author: Matthew Ballard <matt@mrb.email> Date: Tue May 9 14:33:09 2023 -0400 automated fixes Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean commit 88161ad Author: Matthew Ballard <matt@mrb.email> Date: Tue May 9 14:33:09 2023 -0400 Initial file copy from mathport commit c7d31f2 Author: Matthew Ballard <matt@mrb.email> Date: Tue May 9 14:33:09 2023 -0400 feat: port Algebra.Module.Injective
This PR/issue depends on:
|
ext | ||
convert FunLike.congr_fun (injective.comp_factor_thru G F) x } | ||
convert map_zero (M := Y) (N := A) (F := Y →+ A) _ | ||
-- Porting note: hell of non-defeq instances; somehow this worked |
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.
Will this improve after Scott's refactor of concrete categories?
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.
Alas, no. The problem is that M : ModuleCat \Z
has the two fields isCommAddGroup
and isModule
so we immediately get a non-defeq diamond with isCommAddGroup.intModule
and isModule
. The ML3 version is clearly doing some work to dance around this. Things don't translate directly to ML4.
But it does look like #3900 let me drop a re-declaration of an instance.
Or at least I think that is why
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 🎉
bors merge
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. If you want to switch to GitHub's built-in merge queue, visit their help page. |