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] - refactor(field_theory/is_alg_closed/basic): Generalize alg closures to commutative rings #11703

Closed
wants to merge 47 commits into from
Closed

[Merged by Bors] - refactor(field_theory/is_alg_closed/basic): Generalize alg closures to commutative rings #11703

wants to merge 47 commits into from

Conversation

ChrisHughes24
Copy link
Member

@ChrisHughes24 ChrisHughes24 commented Jan 27, 2022 •
edited by github-actions bot

This PR generalizes the is_alg_closure predicate and some of the results about it to algebraic closures of commutative rings, defined as an algebraically closed algebraic extension with an injective map.

@ChrisHughes24 ChrisHughes24 added the WIP Work in progress label Jan 27, 2022
ericrbg
ericrbg reviewed Jan 27, 2022
View reviewed changes
src/field_theory/is_alg_closed/basic.lean Outdated
(alg_closed : is_alg_closed K)
(algebraic : algebra.is_algebraic k K)
(algebraic : algebra.is_algebraic R K)
(injective : function.injective (algebra_map R K))
Copy link
Collaborator

Choose a reason for hiding this comment

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

it may be worth making this a TC argument with no_zero_smul_divisors R K instead an injective algebra_map. (they're equivalent)

@riccardobrasca
Copy link
Member

Can you add that, for a domain R with fraction field K, an algebraic closure of R is the integral closure of R inside an algebraic closure of K? It shouldn't be hard and it seems a natural thing to have.

@ChrisHughes24
Copy link
Member Author

Can you add that, for a domain R with fraction field K, an algebraic closure of R is the integral closure of R inside an algebraic closure of K? It shouldn't be hard and it seems a natural thing to have.

For the definition I have, an algebraic closure of R is isomorphic to an algebraic closure of K. An algebraic closure of a ring to me is adding roots to all non-constant polynomials, not just the monic ones. This makes sense with our definition of algebraic extensions, which says that every element is a root of some not necessarily monic polynomial.

@riccardobrasca
Copy link
Member

Can you add that, for a domain R with fraction field K, an algebraic closure of R is the integral closure of R inside an algebraic closure of K? It shouldn't be hard and it seems a natural thing to have.

For the definition I have, an algebraic closure of R is isomorphic to an algebraic closure of K. An algebraic closure of a ring to me is adding roots to all non-constant polynomials, not just the monic ones. This makes sense with our definition of algebraic extensions, which says that every element is a root of some not necessarily monic polynomial.

Sorry, I missed that it must be a field. Your point makes perfectly sense.

@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Feb 1, 2022
@leanprover-community-bot-assistant
Copy link
Collaborator

This PR/issue depends on:

jcommelin
jcommelin reviewed Feb 2, 2022
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.

bors d+

src/field_theory/is_alg_closed/basic.lean Outdated Show resolved Hide resolved
src/field_theory/is_alg_closed/basic.lean Outdated Show resolved Hide resolved
src/field_theory/is_alg_closed/basic.lean Outdated Show resolved Hide resolved
@bors
Copy link

bors bot commented Feb 2, 2022

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

@leanprover-community-bot-assistant leanprover-community-bot-assistant added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Feb 2, 2022
ChrisHughes24 and others added 3 commits February 2, 2022 11:53
@ChrisHughes24 @jcommelin
Update src/field_theory/is_alg_closed/basic.lean
c1f7568 
Co-authored-by: Johan Commelin <johan@commelin.net>
@ChrisHughes24 @jcommelin
Update src/field_theory/is_alg_closed/basic.lean
908d4a9 
Co-authored-by: Johan Commelin <johan@commelin.net>
@ChrisHughes24 @jcommelin
Update src/field_theory/is_alg_closed/basic.lean
12fedba 
Co-authored-by: Johan Commelin <johan@commelin.net>
@ChrisHughes24
Copy link
Member Author

bors r+

@github-actions github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Feb 2, 2022
@ChrisHughes24
Copy link
Member Author

bors r-

merge conflict

@bors
Copy link

bors bot commented Feb 2, 2022

Canceled.

@ChrisHughes24 ChrisHughes24 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 Feb 2, 2022
@ChrisHughes24
Copy link
Member Author

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 Feb 2, 2022
bors bot pushed a commit that referenced this pull request Feb 2, 2022
@ChrisHughes24
refactor(field_theory/is_alg_closed/basic): Generalize alg closures t…
07d6d17 
…o commutative rings (#11703)

Co-authored-by: chughes <christopher.hughes@inria.fr>
Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
@bors
Copy link

bors bot commented Feb 2, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title refactor(field_theory/is_alg_closed/basic): Generalize alg closures to commutative rings [Merged by Bors] - refactor(field_theory/is_alg_closed/basic): Generalize alg closures to commutative rings Feb 2, 2022
@bors bors bot closed this Feb 2, 2022
@bors bors bot deleted the generalize_alg_closure branch February 2, 2022 14:51
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

@ericrbg ericrbg ericrbg left review comments

Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions. ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@ChrisHughes24 @riccardobrasca @leanprover-community-bot-assistant @jcommelin @ericrbg