-
Notifications
You must be signed in to change notification settings - Fork 297
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/ideal/basic): define right ideals and show division rings are left and right Artinian #14399
base: master
Are you sure you want to change the base?
Conversation
…rings are left and right Artinian
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
/-- A right ideal is a left ideal of the opposite (semi)ring. -/ | ||
@[simps] def to_ideal : ideal αᵐᵒᵖ := |
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.
I can see this being more useful as an equiv or even order_iso between ideal αᵐᵒᵖ
and right_ideal α
. In particular, having things like to_ideal.injective
and to_ideal.map_bot
seem valuable.
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.
In the same vein, ideal.to_right_ideal : ideal α \equivo right_ideal αᵐᵒᵖ
would go in the other direction
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 with @eric-wieser's suggestion.
|
||
protected lemma zero_mem : (0 : α) ∈ I := I.zero_mem | ||
|
||
protected lemma add_mem : a ∈ I → b ∈ I → a + b ∈ I := I.add_mem |
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.
We should be able to safely delete these lemmas since there should already be an add_submonoid_class
instance.
protected lemma zero_mem : (0 : α) ∈ I := I.zero_mem | |
protected lemma add_mem : a ∈ I → b ∈ I → a + b ∈ I := I.add_mem |
zero_mem' := I.zero_mem, | ||
add_mem' := λ a b ha hb, I.add_mem ha hb, |
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.
zero_mem' := I.zero_mem, | |
add_mem' := λ a b ha hb, I.add_mem ha hb, | |
zero_mem' := zero_mem I, | |
add_mem' := λ a b ha hb, add_mem ha hb, |
intros h1, | ||
rw eq_bot_iff, | ||
intros r hr, | ||
by_cases H : r = 0, {simpa}, |
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.
by_cases H : r = 0, {simpa}, | |
by_cases H : r = 0, { simpa }, |
|
||
lemma sum_mem {ι : Type*} {t : finset ι} {f : ι → α} : | ||
(∀c∈t, f c ∈ I) → (∑ i in t, f i) ∈ I := submodule.sum_mem I |
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 is also provided by add_submonoid_class
.
lemma sum_mem {ι : Type*} {t : finset ι} {f : ι → α} : | |
(∀c∈t, f c ∈ I) → (∑ i in t, f i) ∈ I := submodule.sum_mem I |
See also comments on Zulip