Skip to content
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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat(ring_theory/integral_closure): Explicitly define integral extensions #4164

Closed
wants to merge 10 commits into from
Closed

[Merged by Bors] - feat(ring_theory/integral_closure): Explicitly define integral extensions #4164

wants to merge 10 commits into from

Conversation

dtumad
Copy link
Collaborator

@dtumad dtumad commented Sep 15, 2020 •
edited

  • Defined ring_hom.is_integral_elem as a generalization of is_integral that takes a ring homomorphism rather than an algebra. The old version is is redefined to be (algebra_map R A).is_integral_elem x.

  • Create predicates ring_hom.is_integral and algebra.is_integral representing when the entire extension is integral over the base ring.

Note that is_integral no longer depends on aeval in its definition.

@dtumad
feat(ring_theory/integral_closure): Explicitly define integral extens…
23a7f22 
…ion and prove that is_jacobson transfers along them
@dtumad dtumad added the awaiting-review The author would like community review of the PR label Sep 15, 2020
jcommelin
jcommelin reviewed Sep 17, 2020
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for taking this on.

src/ring_theory/integral_closure.lean Outdated Show resolved Hide resolved
src/ring_theory/jacobson.lean Outdated Show resolved Hide resolved
@jcommelin jcommelin added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Sep 17, 2020
@dtumad dtumad added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Sep 18, 2020
jcommelin
jcommelin reviewed Sep 19, 2020
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggestion about names. Otherwise, this looks like a much needed refactor to me. Thanks!

src/ring_theory/integral_closure.lean Outdated Show resolved Hide resolved
src/ring_theory/integral_closure.lean Outdated Show resolved Hide resolved
@dtumad
Copy link
Collaborator Author

dtumad commented Sep 23, 2020

@jcommelin Is this code okay to merge at this point after the naming changes?

@Vierkantor Vierkantor self-requested a review September 25, 2020 08:56
Vierkantor
Vierkantor approved these changes Sep 25, 2020
View reviewed changes
Copy link
Collaborator

@Vierkantor Vierkantor left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks! Two style suggestions, otherwise looks good to me.

bors d+

src/ring_theory/integral_closure.lean
Comment on lines 50 to +51
def is_integral (x : A) : Prop :=
∃ p : polynomial R, monic p ∧ aeval x p = 0
(algebra_map R A).is_integral_elem x
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's a bit confusing that the split is made between ring_hom.is_integral_elem and ring_hom.is_integral one way, and between _root_.is_integral and algebra.is_integral another way. On the other hand, this way more closely matches existing mathematical terminology. I can't think of any better alternatives, so I guess let's keep it as is for now.

src/ring_theory/integral_closure.lean Outdated Show resolved Hide resolved
src/ring_theory/localization.lean Outdated Show resolved Hide resolved
@bors
Copy link

bors bot commented Sep 25, 2020

✌️ dtumad can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@robertylewis robertylewis added awaiting-author A reviewer has asked the author a question or requested changes delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Sep 25, 2020
dtumad and others added 2 commits September 25, 2020 12:14
@dtumad @Vierkantor
Update src/ring_theory/integral_closure.lean
e06f5c4 
Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>
@dtumad @Vierkantor
Update src/ring_theory/localization.lean
a4612ca 
Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>
@dtumad
Copy link
Collaborator Author

dtumad commented Sep 25, 2020

bors r+

@dtumad
Copy link
Collaborator Author

dtumad commented Sep 26, 2020

Have I caused an issue with bors somehow? it seems to be stuck pending in the queue, and I'm not really sure why?

@bryangingechen
Copy link
Collaborator

@dtumad ah, I think the "Details" link next to "bors: Pending - Waiting in queue" (which I'm guessing you don't have access to) shows that bors crashed on this batch.

Let's just try again.

bors r+

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-author A reviewer has asked the author a question or requested changes labels Sep 26, 2020
bors bot pushed a commit that referenced this pull request Sep 26, 2020
@dtumad
feat(ring_theory/integral_closure): Explicitly define integral extens…
158b676 
…ions (#4164)

* Defined `ring_hom.is_integral_elem` as a generalization of `is_integral` that takes a ring homomorphism rather than an algebra. The old version is is redefined to be `(algebra_map R A).is_integral_elem x`.

* Create predicates `ring_hom.is_integral` and `algebra.is_integral` representing when the entire extension is integral over the base ring.



Co-authored-by: Devon Tuma <dtumad@gmail.com>
@bors
Copy link

bors bot commented Sep 26, 2020

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Sep 26, 2020
@dtumad
feat(ring_theory/integral_closure): Explicitly define integral extens…
645592b 
…ions (#4164)

* Defined `ring_hom.is_integral_elem` as a generalization of `is_integral` that takes a ring homomorphism rather than an algebra. The old version is is redefined to be `(algebra_map R A).is_integral_elem x`.

* Create predicates `ring_hom.is_integral` and `algebra.is_integral` representing when the entire extension is integral over the base ring.



Co-authored-by: Devon Tuma <dtumad@gmail.com>
@bors
Copy link

bors bot commented Sep 26, 2020

Build failed:

@bryangingechen bryangingechen added awaiting-author A reviewer has asked the author a question or requested changes and removed ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) labels Sep 26, 2020
@bryangingechen
Copy link
Collaborator

Please merge master, fix the error and then try bors r+ again.

@jcommelin
Copy link
Member

@jcommelin Is this code okay to merge at this point after the naming changes?

@dtumad Sorry, I didn't receive a notification... please ping me on Zulip if I don't reply on Github.

@dtumad
Copy link
Collaborator Author

dtumad commented Sep 28, 2020

bors r+

bors bot pushed a commit that referenced this pull request Sep 28, 2020
@dtumad
feat(ring_theory/integral_closure): Explicitly define integral extens…
d8726bf 
…ions (#4164)

* Defined `ring_hom.is_integral_elem` as a generalization of `is_integral` that takes a ring homomorphism rather than an algebra. The old version is is redefined to be `(algebra_map R A).is_integral_elem x`.

* Create predicates `ring_hom.is_integral` and `algebra.is_integral` representing when the entire extension is integral over the base ring.



Co-authored-by: Devon Tuma <dtumad@gmail.com>
@bors
Copy link

bors bot commented Sep 28, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(ring_theory/integral_closure): Explicitly define integral extensions [Merged by Bors] - feat(ring_theory/integral_closure): Explicitly define integral extensions Sep 28, 2020
@bors bors bot closed this Sep 28, 2020
@bors bors bot deleted the is_integral_extension branch September 28, 2020 02:32
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jcommelin jcommelin jcommelin left review comments

@Vierkantor Vierkantor Vierkantor approved these changes

Assignees
No one assigned
Labels
awaiting-author A reviewer has asked the author a question or requested changes delegated The PR author may merge after reviewing final suggestions.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@dtumad @bryangingechen @jcommelin @Vierkantor @robertylewis