-
Notifications
You must be signed in to change notification settings - Fork 331
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
chore(RingTheory/Ideal): add new file Ideal.IsPrincipal
#13175
Conversation
Ideal.IsPrincipal
Ideal.IsPrincipal
@@ -0,0 +1,299 @@ | |||
/- | |||
Copyright (c) 2018 Kenny Lau. All rights reserved. |
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.
Is this copyright correct?
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.
Well, that's what I did in my previous splits: just copy the copyright of the original file. I am not sure it is the best way to proceed but, well, that's the only one I know...
|
||
/-! | ||
# Principal Ideals | ||
-/ |
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.
Do we want a small list of the principal results? Also, perhaps, a couple of words about what is what (i.e. in the whole file R
is a semiring, sometimes supposed to be a ring...)
variable [Semiring R] | ||
|
||
@[simp] | ||
theorem zero_eq_bot : (0 : Ideal R) = ⊥ := |
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 could stay in Basic
no? EDIT It was actually in Operation
but Basic
seems more appropriate.
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.
Yes, it was in Operations
. I moved it here because I need it here and, after all, zero is a principal ideal. It cannot be in Basic
because of imports and I don't want to change Basic
imports.
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 think this can go under Submodule.zero_eq_bot
?
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.
Okay after reading the remaining of the file, maybe add a new file RingTheory/Ideal/Lattice
?
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.
Yeah, I think I'm going to put this PR on hold. There is first a need to split Operations
into several smaller files first for this to work.
open Submodule Set | ||
|
||
@[simp] | ||
theorem one_eq_top : (1 : Ideal R) = ⊤ := by erw [Submodule.one_eq_range, LinearMap.range_id] |
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 could remain in Basic
, I think.
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 the same as above
(mul_dvd_mul_iff_left h₁).1 <| by rwa [mul_one, ← Ideal.span_singleton_le_span_singleton] | ||
#align ideal.factors_decreasing Ideal.factors_decreasing | ||
|
||
lemma Ideal.isPrime_of_maximally_disjoint [CommSemiring R] (I : Ideal R) (S : Submonoid R) |
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.
Why has this been moved 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.
As I mentioned in the description, a certain number of results could not stay in Basic
since they depend on results that have been moved to IsPrincipal
. For the moment, I moved those results to IsPrincipal
as a temporary solution (in the misc
section). I could put these results in Operations
but the file is already quite big so I am not sure it's the best way to proceed. I welcome any suggestions on what to do with those...
rw [← hr₁, ← hr₂] | ||
ring | ||
|
||
theorem Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top [CommSemiring R] [Nontrivial R] : |
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.
Why 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.
(Same as above)
exact lt_top (I.mul_mem_right _ mem) | ||
#align ring.not_is_field_iff_exists_ideal_bot_lt_and_lt_top Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top | ||
|
||
theorem Ring.not_isField_iff_exists_prime [CommSemiring R] [Nontrivial R] : |
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.
Once more... why 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.
(Same as above)
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 was all in favour of creating this new file, and so of course this PR looks very good to me. I wonder why many lemmas about prime/maximal ideals ended up in the IsPrincipal
one although they do not have anything to do with principality, AFAICT.
Well, I think I am going to close this PR. I do not think into possible to put everything about |
This PR adds a new file
RingTheory.Ideal.IsPrincipal
and moves most of the (basic) results aboutIdeal.IsPrincipal
andIdeal.span_singleton
fromIdeal.Basic
andIdeal.Operations
to this file. (Some very basic results or results related toSubmodule.span_singleton
are left in place.)The need for this PR comes from a discussion in #12780 about where to put the proof that the equivalence between principal ideals and associates is actually a
MulEquiv
(#13177).Some remarks:
no_lost_declarations.sh
saysthis is due to some renames in the variables and also
namespace
changes. I have checked that the added declarations correspond exactly to the removed declarationsIdeal.Basic
but are not really related to principal ideals have been moved (for the moment?) to the end ofIdeal.IsPrincipal
(see themisc
section). I thought about putting them inIdeal.Operations
but the file is already quite large (about 1400 lines). Note thatIdeal.Operations
importsIdeal.IsPrincipal
and these additional results do not add any extra import toIdeal.IsPrincipal
. Still, they should probably go somewhere else...