[Merged by Bors] - feat(FieldTheory/SeparableDegree): further properties of separable degree of fields and polynomials #9041

acmepjz · 2023-12-13T23:38:49Z

Breaking changes:

remove Field.sepDegree since it is not quite correct for infinite case; will be added in later PR (see [Merged by Bors] - feat(FieldTheory/IsPerfectClosure): predicate IsPerfectClosure #8696)

New definitions (non-exhaustive):

Polynomial.natSepDegree: the separable degree of a polynomial is a natural number, defined to be the number of distinct roots of it over its splitting field.

New results (non-exhaustive):

Polynomial.natSepDegree_le_natDegree: the separable degree of a polynomial is smaller than its degree.
Polynomial.natSepDegree_eq_natDegree_iff: the separable degree of a non-zero polynomial is equal to its degree if and only if it is separable.
Polynomial.natSepDegree_dvd_natDegree_of_irreducible: the separable degree of an irreducible polynomial divides its degree.
Field.finSepDegree_adjoin_simple_eq_natSepDegree: the (finite) separable degree of F⟮α⟯ / F is equal to the separable degree of the minimal polynomial of α over F.
Field.finSepDegree_dvd_finrank: the separable degree of any field extension E / F divides the degree of E / F.
Field.finSepDegree_le_finrank: the separable degree of a finite extension E / F is smaller than the degree of E / F.
Field.finSepDegree_eq_finrank_iff: if E / F is a finite extension, then its separable degree is equal to its degree if and only if it is a separable extension.

Mathlib/FieldTheory/SeparableDegree.lean

alreadydone

From a brief skim up to Line 532:

Mathlib/FieldTheory/SeparableDegree.lean

alreadydone

okay I've now skimmed through the whole PR. Fantastic work! Next time I'll be trying to golf some proofs ...

Mathlib/FieldTheory/SeparableDegree.lean

Mathlib/Data/Polynomial/Expand.lean

Mathlib/FieldTheory/SeparableDegree.lean

riccardobrasca · 2023-12-19T15:44:17Z

Is it possible to split the PR? It is currently rather big...

alreadydone · 2023-12-19T16:11:52Z

I'm happy with the content, just haven't checked whether some proofs' lengths are justified :)

leanprover-community-mathlib4-bot · 2023-12-26T07:02:36Z

This PR/issue depends on:

~~[Merged by Bors] - feat(Algebra/CharP/ExpChar): add some results parallel to CharP #8860~~
~~[Merged by Bors] - feat(Mathlib/FieldTheory/Separable): add Polynomial.Separable.isIntegral and golf #9134~~
~~[Merged by Bors] - feat(Algebra/CharP/ExpChar): add expChar[_pow]_pos #9260~~
~~[Merged by Bors] - feat(Data/Polynomial/Expand): add leadingCoeff_expand and monic_expand_iff #9261~~
~~[Merged by Bors] - feat(FieldTheory/Adjoin): add exists_lt_finrank_of_infinite_dimensional #9262~~
~~[Merged by Bors] - feat(FieldTheory/Separable): add some results regarding separable and no repeated roots #9263~~
~~[Merged by Bors] - feat(FieldTheory/Perfect): add rootsExpand[Pow]EquivRoots[_apply] #9271~~
~~[Merged by Bors] - chore(RingTheory/Polynomial/SeparableDegree): add HasSeparableContraction.isSeparableContraction and ... #9272~~
By Dependent Issues (🤖). Happy coding!

riccardobrasca · 2023-12-26T08:38:28Z

Can you please fix the conflict?

alreadydone

Thanks, I think this is my final review on this PR!

Mathlib/FieldTheory/SeparableDegree.lean

alreadydone · 2023-12-26T23:33:34Z

Mathlib/FieldTheory/SeparableDegree.lean

+    (finSepDegree_adjoin_simple_eq_finrank_iff L E y halg' |>.2
+      (hy.map (f := algebraMap F F⟮x⟯) |>.of_dvd (minpoly.dvd_map_of_isScalarTower F L y)))
+  let M := L⟮y⟯
+  letI : Algebra L M := Subalgebra.algebra M.toSubalgebra


I opened #9291 to remove these manual instances.

Mathlib/FieldTheory/SeparableDegree.lean

…ield (#9291) Removes [manual letI/haveI](https://github.com/leanprover-community/mathlib4/blob/fe76ea7c2bb0c725ad161755ac158171aa9c545a/Mathlib/FieldTheory/SeparableDegree.lean#L568-L571) that appear in four proofs of #9041 Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

riccardobrasca · 2023-12-27T12:35:07Z

I also think this is almost ready! Since #9291 has been merged, can you see if you can golf some proof?

acmepjz · 2023-12-27T12:43:10Z

I also think this is almost ready! Since #9291 has been merged, can you see if you can golf some proof?

Sure. Let me try how many of them can be removed.

Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

alreadydone

Just a few more nits I missed ...

Mathlib/FieldTheory/SeparableDegree.lean

alreadydone · 2023-12-27T17:27:28Z

Mathlib/FieldTheory/SeparableDegree.lean

+- `Field.finSepDegree_eq_finrank_iff`: if `E / F` is a finite extension, then its separable degree
+  is equal to its degree if and only if it is a separable extension.
+
+- `IntermediateField.isSeparable_adjoin_simple_iff_separable`: `F⟮x⟯ / F` is a separable extension


Side comment: I think the phrase adjoin_simple is strange. It's a simple extension obtained by adjoining a singleton. Indeed similar constructions are called adjoin_singleton, but I think we could just use the shorthand simple here which also agrees with math terminology. I think we might open a PR to rename all adjoin_simple to simple.

But mem_adjoin_simple_self -> mem_simple_self sounds strange ...

Mathlib/FieldTheory/SeparableDegree.lean

alreadydone · 2023-12-27T22:32:29Z

Thanks 🎉
maintainer merge

github-actions · 2023-12-27T22:32:42Z

🚀 Pull request has been placed on the maintainer queue by alreadydone.

Mathlib/FieldTheory/SeparableDegree.lean

jcommelin · 2023-12-28T06:17:38Z

Thanks 🎉

bors merge

…gree of fields and polynomials (#9041) Breaking changes: - remove `Field.sepDegree` since it is not quite correct for infinite case; will be added in later PR (see #8696) New definitions (non-exhaustive): - `Polynomial.natSepDegree`: the separable degree of a polynomial is a natural number, defined to be the number of distinct roots of it over its splitting field. New results (non-exhaustive): - `Polynomial.natSepDegree_le_natDegree`: the separable degree of a polynomial is smaller than its degree. - `Polynomial.natSepDegree_eq_natDegree_iff`: the separable degree of a non-zero polynomial is equal to its degree if and only if it is separable. - `Polynomial.natSepDegree_dvd_natDegree_of_irreducible`: the separable degree of an irreducible polynomial divides its degree. - `Field.finSepDegree_adjoin_simple_eq_natSepDegree`: the (finite) separable degree of `F⟮α⟯ / F` is equal to the separable degree of the minimal polynomial of `α` over `F`. - `Field.finSepDegree_dvd_finrank`: the separable degree of any field extension `E / F` divides the degree of `E / F`. - `Field.finSepDegree_le_finrank`: the separable degree of a finite extension `E / F` is smaller than the degree of `E / F`. - `Field.finSepDegree_eq_finrank_iff`: if `E / F` is a finite extension, then its separable degree is equal to its degree if and only if it is a separable extension. Co-authored-by: Johan Commelin <johan@commelin.net>

mathlib-bors · 2023-12-28T06:40:40Z

Pull request successfully merged into master.

Build succeeded:

copy file from #8696

d722c09

acmepjz added awaiting-review awaiting-CI t-algebra Algebra (groups, rings, fields etc) labels Dec 13, 2023

acmepjz mentioned this pull request Dec 13, 2023

[Merged by Bors] - feat(FieldTheory/IsPerfectClosure): predicate IsPerfectClosure #8696

Closed

13 tasks

still depends on #8860

fcae884

leanprover-community-mathlib4-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib label Dec 13, 2023

github-actions bot removed the awaiting-CI label Dec 14, 2023

leanprover-community-mathlib4-bot added merge-conflict The PR has a merge conflict with master, and needs manual merging. and removed blocked-by-other-PR This PR depends on another PR to Mathlib labels Dec 14, 2023

acmepjz added 2 commits December 14, 2023 19:45

copy file from master

819465c

Merge branch 'master' into acmepjz_sep_degree_2a

b3b472a

leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Dec 14, 2023

move some functions to IntermediateField namespace

b24b3ca

alreadydone reviewed Dec 15, 2023

View reviewed changes

Mathlib/FieldTheory/SeparableDegree.lean Outdated Show resolved Hide resolved

alreadydone reviewed Dec 16, 2023

View reviewed changes

Mathlib/FieldTheory/SeparableDegree.lean Outdated Show resolved Hide resolved

acmepjz added 3 commits December 17, 2023 09:10

rephrase docstring

50ca9bc

add leadingCoeff_expand and monic_expand_iff for Polynomial

f847d75

various fixes according to suggestions

f9a5115

alreadydone reviewed Dec 17, 2023

View reviewed changes

Mathlib/Data/Polynomial/Expand.lean Outdated Show resolved Hide resolved

Mathlib/FieldTheory/SeparableDegree.lean Outdated Show resolved Hide resolved

Mathlib/FieldTheory/SeparableDegree.lean Outdated Show resolved Hide resolved

apply suggestions

19c30fd

leanprover-community-mathlib4-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib label Dec 18, 2023

remove some IsIntegral, depends on #9134

f22d777

leanprover-community-mathlib4-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib label Dec 18, 2023

acmepjz added 2 commits December 18, 2023 17:33

remove ad-hoc code

efe383b

Merge branch 'master' into acmepjz_sep_degree_2a

c5cc68c

acmepjz added a commit that referenced this pull request Dec 19, 2023

adapt #9041 and add more results

bbff0d9

leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Dec 26, 2023

acmepjz added 2 commits December 26, 2023 21:02

copy file from master

4b82b77

Merge branch 'master' into acmepjz_sep_degree_2a

fe76ea7

leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Dec 26, 2023

acmepjz added a commit that referenced this pull request Dec 26, 2023

copy file from #9041

e18e9a0

alreadydone mentioned this pull request Dec 26, 2023

[Merged by Bors] - chore: shortcut instances for IntermediateField over an IntermediateField #9291

Closed

alreadydone approved these changes Dec 27, 2023

View reviewed changes

riccardobrasca self-assigned this Dec 27, 2023

acmepjz and others added 3 commits December 27, 2023 20:45

Apply suggestions from code review

4088254

Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

Merge branch 'master' into acmepjz_sep_degree_2a

e642961

apply suggestions and golf

597382f

alreadydone approved these changes Dec 27, 2023

View reviewed changes

golf

a5d64c9

jcommelin approved these changes Dec 28, 2023

View reviewed changes

Mathlib/FieldTheory/SeparableDegree.lean Outdated Show resolved Hide resolved

Update Mathlib/FieldTheory/SeparableDegree.lean

0beb9e1

github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Dec 28, 2023

mathlib-bors bot changed the title ~~feat(FieldTheory/SeparableDegree): further properties of separable degree of fields and polynomials~~ [Merged by Bors] - feat(FieldTheory/SeparableDegree): further properties of separable degree of fields and polynomials Dec 28, 2023

mathlib-bors bot closed this Dec 28, 2023

mathlib-bors bot deleted the acmepjz_sep_degree_2a branch December 28, 2023 06:40

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(FieldTheory/SeparableDegree): further properties of separable degree of fields and polynomials #9041

[Merged by Bors] - feat(FieldTheory/SeparableDegree): further properties of separable degree of fields and polynomials #9041

acmepjz commented Dec 13, 2023 •

edited

Loading

alreadydone left a comment

alreadydone left a comment

riccardobrasca commented Dec 19, 2023

alreadydone commented Dec 19, 2023

leanprover-community-mathlib4-bot commented Dec 26, 2023

riccardobrasca commented Dec 26, 2023

alreadydone left a comment •

edited

Loading

alreadydone Dec 26, 2023

riccardobrasca commented Dec 27, 2023

acmepjz commented Dec 27, 2023

alreadydone left a comment

alreadydone Dec 27, 2023

acmepjz Dec 27, 2023

alreadydone commented Dec 27, 2023

github-actions bot commented Dec 27, 2023

jcommelin commented Dec 28, 2023

mathlib-bors bot commented Dec 28, 2023

[Merged by Bors] - feat(FieldTheory/SeparableDegree): further properties of separable degree of fields and polynomials #9041

[Merged by Bors] - feat(FieldTheory/SeparableDegree): further properties of separable degree of fields and polynomials #9041

Conversation

acmepjz commented Dec 13, 2023 • edited Loading

alreadydone left a comment

Choose a reason for hiding this comment

alreadydone left a comment

Choose a reason for hiding this comment

riccardobrasca commented Dec 19, 2023

alreadydone commented Dec 19, 2023

leanprover-community-mathlib4-bot commented Dec 26, 2023

riccardobrasca commented Dec 26, 2023

alreadydone left a comment • edited Loading

Choose a reason for hiding this comment

alreadydone Dec 26, 2023

Choose a reason for hiding this comment

riccardobrasca commented Dec 27, 2023

acmepjz commented Dec 27, 2023

alreadydone left a comment

Choose a reason for hiding this comment

alreadydone Dec 27, 2023

Choose a reason for hiding this comment

acmepjz Dec 27, 2023

Choose a reason for hiding this comment

alreadydone commented Dec 27, 2023

github-actions bot commented Dec 27, 2023

jcommelin commented Dec 28, 2023

mathlib-bors bot commented Dec 28, 2023

acmepjz commented Dec 13, 2023 •

edited

Loading

alreadydone left a comment •

edited

Loading