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: Kummer extensions are cyclic. #9119

Closed
wants to merge 22 commits into from
Closed

[Merged by Bors] - feat: Kummer extensions are cyclic. #9119

wants to merge 22 commits into from

Conversation

erdOne
Copy link
Member

@erdOne erdOne commented Dec 17, 2023

Open in Gitpod

github-actions[bot]
github-actions bot reviewed Dec 17, 2023
View reviewed changes
Mathlib/FieldTheory/KummerExtension.lean Outdated Show resolved Hide resolved
Mathlib/FieldTheory/KummerExtension.lean Outdated Show resolved Hide resolved
Mathlib/GroupTheory/Subgroup/Basic.lean Outdated Show resolved Hide resolved
Mathlib/GroupTheory/Subgroup/Basic.lean Outdated Show resolved Hide resolved
erdOne and others added 2 commits December 17, 2023 09:40
@erdOne
fix
c7359d4
@erdOne @github-actions
Apply suggestions from code review
37e480d 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
github-actions[bot]
github-actions bot reviewed Dec 17, 2023
View reviewed changes
Mathlib/FieldTheory/KummerExtension.lean Outdated Show resolved Hide resolved
Mathlib/GroupTheory/Subgroup/Basic.lean Outdated Show resolved Hide resolved
Mathlib/GroupTheory/Subgroup/Basic.lean Outdated Show resolved Hide resolved
@erdOne erdOne added awaiting-review The author would like community review of the PR t-algebra Algebra (groups, rings, fields etc) labels Dec 17, 2023
@riccardobrasca riccardobrasca self-assigned this Dec 19, 2023
riccardobrasca
riccardobrasca reviewed Dec 19, 2023
View reviewed changes
Copy link
Member

@riccardobrasca riccardobrasca left a comment

Choose a reason for hiding this comment

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

I will have a look at the juicy file tomorrow.

Mathlib/Data/Polynomial/RingDivision.lean Outdated Show resolved Hide resolved
Mathlib/RingTheory/RootsOfUnity/Basic.lean Outdated Show resolved Hide resolved
alreadydone
alreadydone reviewed Dec 19, 2023
View reviewed changes
Mathlib/FieldTheory/KummerExtension.lean Outdated
Comment on lines 33 to 36
Criteria for `X ^ n - C a` to be irreducible is given:
`X_pow_sub_C_irreducible_iff_of_prime`: `X ^ n - C a` is irreducible iff `a` is not a `p`-power.

TODO: criteria for general `n`.
Copy link
Contributor

Choose a reason for hiding this comment

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

Suggested change
Criteria for `X ^ n - C a` to be irreducible is given:
`X_pow_sub_C_irreducible_iff_of_prime`: `X ^ n - C a` is irreducible iff `a` is not a `p`-power.
TODO: criteria for general `n`.
Criteria for `X ^ p - C a` to be irreducible is given for `p` prime.
`X_pow_sub_C_irreducible_iff_of_prime`: `X ^ p - C a` is irreducible iff `a` is not a `p`-power.
TODO: criteria for general `n`.

Maybe add a reference to Serge Lang's Algebra:
image

Copy link
Member Author

Choose a reason for hiding this comment

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

I was planning to list the criteria provided and hence the wording.

riccardobrasca
riccardobrasca reviewed Dec 20, 2023
View reviewed changes
Copy link
Member

@riccardobrasca riccardobrasca left a comment

Choose a reason for hiding this comment

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

I think that some of the results at the beginning of KummerExtension.lean should be moved to more basic files.

Mathlib/FieldTheory/KummerExtension.lean
mk_ne_zero_of_natDegree_lt (monic_X_pow_sub_C _ (Nat.not_eq_zero_of_lt hn))
X_ne_zero <| by rwa [natDegree_X_pow_sub_C, natDegree_X]

lemma root_X_pow_sub_C_ne_zero' {n : ℕ} {a : K} (hn : 0 < n) (ha : a ≠ 0) :
Copy link
Member

Choose a reason for hiding this comment

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

The first three results can go in a more basic file (where AdjoinRoot is defined maybe?), and I guess that Field K is an overkill assumption.

Copy link
Member Author

Choose a reason for hiding this comment

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

I think it's fine to list everything we know about AdjoinRoot (X ^ n - C a) (i.e. K[n√a]) here?

Mathlib/FieldTheory/KummerExtension.lean Outdated Show resolved Hide resolved
Mathlib/FieldTheory/KummerExtension.lean Outdated Show resolved Hide resolved
Mathlib/FieldTheory/KummerExtension.lean Outdated Show resolved Hide resolved
Mathlib/FieldTheory/KummerExtension.lean Outdated Show resolved Hide resolved
Mathlib/FieldTheory/KummerExtension.lean Show resolved Hide resolved
Mathlib/FieldTheory/KummerExtension.lean Outdated Show resolved Hide resolved
@erdOne erdOne 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 Dec 20, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Dec 25, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Dec 25, 2023
@erdOne erdOne 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 Dec 25, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Dec 27, 2023
@riccardobrasca
Copy link
Member

Can you please fix the conflict?

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Dec 28, 2023
riccardobrasca
riccardobrasca reviewed Dec 30, 2023
View reviewed changes
Copy link
Member

@riccardobrasca riccardobrasca left a comment

Choose a reason for hiding this comment

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

Thanks!

bors merge

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Dec 30, 2023
mathlib-bors bot pushed a commit that referenced this pull request Dec 30, 2023
@erdOne
feat: Kummer extensions are cyclic. (#9119)
ba4be74 
Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
@mathlib-bors
Copy link

mathlib-bors bot commented Dec 30, 2023

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: Kummer extensions are cyclic. [Merged by Bors] - feat: Kummer extensions are cyclic. Dec 30, 2023
@mathlib-bors mathlib-bors bot closed this Dec 30, 2023
@mathlib-bors mathlib-bors bot deleted the erd1/kummerextension branch December 30, 2023 20:29
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@alexjbest alexjbest alexjbest left review comments

@alreadydone alreadydone alreadydone left review comments

@riccardobrasca riccardobrasca riccardobrasca left review comments

@github-actions github-actions[bot] github-actions left review comments

Assignees

@riccardobrasca riccardobrasca

Labels
ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields etc)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@erdOne @riccardobrasca @alexjbest @alreadydone @leanprover-community-mathlib4-bot