-
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
feat(ring_theory/ideals): quotient rings #196
feat(ring_theory/ideals): quotient rings #196
Conversation
@@ -3,15 +3,44 @@ Copyright (c) 2018 Kenny Lau. All rights reserved. | |||
Released under Apache 2.0 license as described in the file LICENSE. | |||
Authors: Kenny Lau |
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.
add Chris Hughes.
Thanks Chris by the way -- I need this for perfectoids!
ring_theory/ideals.lean
Outdated
|
||
lemma mul_left {S : set α} [is_ideal S] : b ∈ S → a * b ∈ S := @is_submodule.smul α α _ _ _ _ a _ | ||
|
||
lemma mul_right {S : set α} [is_ideal S] : a ∈ S → a * b ∈ S := mul_comm b a ▸ mul_left |
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.
At least zero
, add
and sub
should be protected here.
ring_theory/ideals.lean
Outdated
|
||
/- quotient by maximal ideal is a field. def rather than instance, since users will have | ||
computable inverses in some applications -/ | ||
noncomputable def field (S : set α) [is_maximal_ideal S] : field (quotient S) := |
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.
this should also be protected
Quotient rings are a ring, quotient by prime ideal is an integral domain, and quotient by maximal ideal is a field (noncomputable).