-
Notifications
You must be signed in to change notification settings - Fork 299
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(ring_theory/localization): order embedding of ideals, local ring instance #3287
Conversation
101damnations
commented
Jul 4, 2020
sorry for the long break in PRs. This is the order embedding of ideals in a localization & the local ring instance on the localization at the complement of a prime ideal. |
The linter says I am not sure what to do about this - the local ring instance added in this PR compiles - should I increase |
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.
Looks good to me! Maybe the instance is tripping up because codomain
is reducible? I have no idea. @gebner could you please take a look?
src/ring_theory/localization.lean
Outdated
namespace ideal | ||
|
||
/-- The complement of a prime ideal `I ⊆ R` is a submonoid of `R`. -/ | ||
def prime_submonoid : |
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.
def prime_submonoid : | |
def prime_complement : |
Otherwise it sounds like you're turning the prime ideal itself into a submonoid.
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.
good point... What about prime_compl
, to be in keeping with set.compl
etc?
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.
yup, sounds good to me
src/ring_theory/localization.lean
Outdated
@[nolint unused_arguments has_inhabited_instance] | ||
def codomain (f : localization_map M S) := S | ||
|
||
instance : comm_ring f.codomain := _inst_2 |
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.
instance : comm_ring f.codomain := _inst_2 | |
instance : comm_ring f.codomain := by apply_instance |
_inst_2
doesn't seem like a very stable name. If someone adds a variable we might suddenly need _inst_3
here.
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.
fair point! by apply_instance
doesn't work but I've just found out you can use by assumption
for instances... awesome
Also thank you for the irreducible codomain appeasing the linter :)
src/ring_theory/localization.lean
Outdated
def codomain (f : localization_map M S) := S | ||
|
||
instance : comm_ring f.codomain := _inst_2 | ||
instance {K : Type*} [field K] (f : localization_map M K) : field f.codomain := _inst_4 |
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.
instance {K : Type*} [field K] (f : localization_map M K) : field f.codomain := _inst_4 | |
instance {K : Type*} [field K] (f : localization_map M K) : field f.codomain := by apply_instance |
Thanks 🎉 bors merge |
Pull request successfully merged into master. Build succeeded: |