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(field_theory): Prove the Galois correspondence #4786

Closed
wants to merge 223 commits into from
Closed

[Merged by Bors] - feat(field_theory): Prove the Galois correspondence #4786

wants to merge 223 commits into from

Conversation

tb65536
Copy link
Collaborator

@tb65536 tb65536 commented Oct 26, 2020 •
edited by github-actions bot
Loading

The proof leverages existing results from field_theory/fixed.lean and field_theory/primitive_element.lean.
We define Galois as normal + separable. Proving the various equivalent characterizations of Galois extensions is yet to be done.

@tb65536 tb65536 added the awaiting-review The author would like community review of the PR label Oct 26, 2020
@bryangingechen bryangingechen changed the title Galois definition feat(field_theory): Prove the Galois correspondence Oct 26, 2020
jcommelin
jcommelin reviewed Oct 26, 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.

This is a great milestone. But it would be good to split things into smaller PRs.

src/algebra/algebra/subalgebra.lean Outdated Show resolved Hide resolved
src/data/polynomial/degree/basic.lean Outdated Show resolved Hide resolved
src/linear_algebra/finite_dimensional.lean Outdated Show resolved Hide resolved
@hrmacbeth
Copy link
Member

Can you update docs/overview.yaml (in the same PR)?

This was referenced Oct 26, 2020
Closed
Closed
Closed
@bryangingechen bryangingechen added 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 Oct 26, 2020
bors bot pushed a commit that referenced this pull request Oct 26, 2020
@tb65536
feat(degree/basic.lean): degree_lt_iff_coeff_zero (#4792)
c76c3c5 
Changes to degree/basic.lean from #4786



Co-authored-by: tb65536 <tb65536@users.noreply.github.com>
bors bot pushed a commit that referenced this pull request Oct 27, 2020
@tb65536
feat(algebra/algebra/subalgebra): algebra equalizer (#4791)
c737996 
Changes to subalgebra.lean from #4786



Co-authored-by: tb65536 <tb65536@users.noreply.github.com>
bors bot pushed a commit that referenced this pull request Oct 29, 2020
@tb65536
feat(linear_algebra/finite_dimensional): finite dimensional algebra_h…
d510a63 
…om of fields is bijective (#4793)

Changes to finite_dimensional.lean from #4786



Co-authored-by: tb65536 <tb65536@users.noreply.github.com>
tb65536 and others added 19 commits November 25, 2020 10:32
@tb65536 @Vierkantor
Update src/field_theory/adjoin.lean
e5ea39b 
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
@tb65536 @Vierkantor
Update src/field_theory/galois.lean
668f672 
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
@tb65536 @Vierkantor
Update src/field_theory/galois.lean
eddbecd 
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
@tb65536
fix errors
2027344
@tb65536 @Vierkantor
Update src/field_theory/galois.lean
9ff9405 
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
@tb65536 @Vierkantor
Update src/field_theory/galois.lean
a1ab282 
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
@tb65536 @Vierkantor
Update src/field_theory/galois.lean
6f5a4c2 
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
@tb65536 @Vierkantor
Update src/field_theory/galois.lean
2745ee4 
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
@tb65536 @Vierkantor
Update src/field_theory/galois.lean
88adfca 
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
@tb65536 @Vierkantor
Update src/field_theory/galois.lean
149f786 
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
@tb65536 @Vierkantor
Update src/field_theory/galois.lean
c1925a4 
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
@tb65536 @Vierkantor
Update src/field_theory/galois.lean
7adf5e8 
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
@tb65536
fix errors
50b8762
@tb65536
galois_(co)insertion
936ad13
@tb65536
fix long lines
52afaa3
@tb65536
move group instance
f8ff50f
@tb65536
fix long line
a75c413
@tb65536
fix overview.yaml
78fa561
@tb65536
remove hypothesis
f69a3e5
Vierkantor
Vierkantor approved these changes Nov 26, 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.

It's looking ready to merge to me, thanks for all the work! @jcommelin, what do you think?

jcommelin
jcommelin approved these changes Nov 27, 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.

Fantastic work! This is a true milestone. Thanks so much for all your efforts 🎉

bors merge

@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-review The author would like community review of the PR labels Nov 27, 2020
bors bot pushed a commit that referenced this pull request Nov 27, 2020
@tb65536
feat(field_theory): Prove the Galois correspondence (#4786)
2bda184 
The proof leverages existing results from field_theory/fixed.lean and field_theory/primitive_element.lean.
We define Galois as normal + separable. Proving the various equivalent characterizations of Galois extensions is yet to be done.
@bors
Copy link

bors bot commented Nov 27, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(field_theory): Prove the Galois correspondence [Merged by Bors] - feat(field_theory): Prove the Galois correspondence Nov 27, 2020
@bors bors bot closed this Nov 27, 2020
@bors bors bot deleted the galois_definition branch November 27, 2020 11:58
@eric-wieser eric-wieser mentioned this pull request Jan 29, 2021
Closed
eric-wieser
eric-wieser reviewed Jan 29, 2021
View reviewed changes
src/data/fintype/basic.lean
Comment on lines +234 to +236
noncomputable instance subtype_of_fintype [fintype α] (p : α → Prop) : fintype (subtype p) :=
fintype.of_injective coe subtype.coe_injective

Copy link
Member

Choose a reason for hiding this comment

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

xref #5943 - this instance is a duplicate of subtype.fintype (in the presence of classical.dec_pred anyway)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

@pglutz pglutz pglutz left review comments

@Vierkantor Vierkantor Vierkantor approved these changes

@jcommelin jcommelin jcommelin approved these changes

@kckennylau kckennylau Awaiting requested review from kckennylau

Assignees
No one assigned
Labels
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
7 participants
@tb65536 @hrmacbeth @jcommelin @Vierkantor @bryangingechen @eric-wieser @pglutz