[Merged by Bors] - feat(FieldTheory/IsSepClosed): add some results on separable closure and perfect field #9522

acmepjz · 2024-01-07T17:05:03Z

IsSepClosure.isAlgClosure_of_perfectField, IsSepClosure.of_isAlgClosure_of_perfectField: if k is a perfect field, then its separable closure coincides with its algebraic closure.
IsSepClosed.isAlgClosed_of_perfectField: a separably closed perfect field is also algebraically closed.
Algebra.IsAlgebraic.[isSeparable_of_]perfectField: if L / K is an algebraic extension, K is a perfect field, then L / K is separable and L is perfect.

Mathlib/FieldTheory/IsSepClosed.lean

alreadydone · 2024-01-07T23:16:53Z

Mathlib/FieldTheory/Perfect.lean

+  have h2 := isIntegral_trans halg.isIntegral _ (AdjoinRoot.isIntegral_root h)
+  have h3 := (AdjoinRoot.minpoly_root h) ▸ minpoly.dvd_map_of_isScalarTower K L (AdjoinRoot.root f)
+  (PerfectField.separable_of_irreducible (minpoly.irreducible h2)).map |>.of_dvd h3 |>.of_mul_left⟩


Can you extract the lemma that says if L/K is integral with L a field and K a CommRing, then any irreducible polynomial in L[X] divides some monic irreducible polynomial in K[X]?

(Side comment: I think we can also prove it for an integrally closed domain L if we assume Monic because we have minpoly.isIntegrallyClosed_dvd and IsIntegrallyClosed.minpoly.unique. For L/K free maybe we can use Algebra.norm, but I'm not sure whether every element divides its norm in a general algebra; even though we can factor into irreducibles in a Noetherian domain, we probably need to start with a prime (not just irreducible) polynomial in L[X] in order for it to divide some factor ... there could be a version that assumes IsAlgebraic instead of IsIntegral too. But not for this PR ...)

Sure, let me check later.

Can you extract the lemma that says if L/K is integral with L a field and K a CommRing, then any irreducible polynomial in L[X] divides some monic irreducible polynomial in K[X]?

Need IsDomain K (used in minpoly.irreducible). Can it be deduced from existing conditions?

[EDIT] If let K' be the image of K in L, then it is a domain, so at least we can find a monic irreducible polynomial in K'[X]. The question is if its preimage in K[X] is still irreducible.

I see. There's no obvious way to remove IsDomain as far as I can see. If K is not a domain, it's possible that the minpoly has higher degree factors that become units in L[X].
Let's move this lemma to the file where AdjoinRoot is defined and call it a day!

Can you extract the lemma that says if L/K is integral with L a field and K a CommRing, then any irreducible polynomial in L[X] divides some monic irreducible polynomial in K[X]?

Need IsDomain K (used in minpoly.irreducible).

This result is incorrect, at least when K is not connected (i.e. can be written as a product of two rings), see https://math.stackexchange.com/a/4849403/235999. In fact, it's easy to prove that for such case, any monic polynomial in K[X] of degree ≥ 1 is NOT irreducible (a non-trivial factorization is obtained by applying Chinese Remainder Theorem on f * 1 and 1 * f).

On the other hand, it's true if K is irreducible (i.e. only one minimal prime ideal), see https://math.stackexchange.com/a/4843432/235999.

alreadydone · 2024-01-07T23:30:35Z

!bench

leanprover-bot · 2024-01-07T23:55:14Z

Here are the benchmark results for commit f858a9e.
There were significant changes against commit a7c1abf:

  Benchmark                                                           Metric         Change
  =========================================================================================
- ~Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit   instructions    16.4%

(discussion here. This slowed-down file doesn't import any file that is changed. - Junyan)

…hlib.RingTheory.AdjoinRoot`

alreadydone · 2024-01-08T03:12:28Z

Thanks 🎉
maintainer merge

github-actions · 2024-01-08T03:12:41Z

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

erdOne · 2024-01-08T04:24:03Z

Mathlib/RingTheory/AdjoinRoot.lean

+/-- If `L / K` is an integral extension, `K` is a domain, `L` is a field, then any irreducible
+polynomial over `L` divides some monic irreducible polynomial over `K`. -/
+theorem Irreducible.exists_dvd_monic_irreducible_of_isIntegral {K L : Type*}
+    [CommRing K] [IsDomain K] [Field L] [Algebra K L] (H : Algebra.IsIntegral K L) {f : L[X]}


Doesn't this imply that $\text{Frac} K$ is integral over $K$, i.e. $K$ is actually a field?

K to L isn't necessarily injective (K could be L[X] and algebraMap K L could be evaluation at 0, for example). That said, I think this is still true if IsIntegral is replaced by IsAlgebraic ...

riccardobrasca

Thanks!

bors d+

riccardobrasca · 2024-01-08T09:14:20Z

Mathlib/FieldTheory/Perfect.lean

@@ -218,3 +218,14 @@ instance toPerfectRing (p : ℕ) [hp : Fact p.Prime] [CharP K p] : PerfectRing K
  exact minpoly.degree_pos ha

 end PerfectField
+
+/-- If `L / K` is an algebraic extension, `K` is a perfect field, then `L / K` is separable. -/
+theorem Algebra.IsAlgebraic.isSeparable_of_perfectField {K L : Type*} [Field K] [Field L]


Can you add this to the docstring at the beginning of the file?

Also, can this be an instance?

Can you add this to the docstring at the beginning of the file?

Sure.

Also, can this be an instance?

No, it's not possible I think, since Algebra.IsAlgebraic is not a typeclass, so this condition must be provided manually.

mathlib-bors · 2024-01-08T09:15:49Z

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

acmepjz · 2024-01-08T13:46:06Z

bors r+

…and perfect field (#9522) - `IsSepClosure.isAlgClosure_of_perfectField`, `IsSepClosure.of_isAlgClosure_of_perfectField`: if `k` is a perfect field, then its separable closure coincides with its algebraic closure. - `IsSepClosed.isAlgClosed_of_perfectField`: a separably closed perfect field is also algebraically closed. - `Algebra.IsAlgebraic.[isSeparable_of_]perfectField`: if `L / K` is an algebraic extension, `K` is a perfect field, then `L / K` is separable and `L` is perfect.

mathlib-bors · 2024-01-08T15:43:54Z

Pull request successfully merged into master.

Build succeeded:

acmepjz added 2 commits January 8, 2024 00:50

add some results on separable closure and perfect field

41b421b

Merge branch 'master' into acmepjz_perfect_1

79117c0

acmepjz added awaiting-review awaiting-CI t-algebra Algebra (groups, rings, fields, etc) labels Jan 7, 2024

github-actions bot removed the awaiting-CI label Jan 7, 2024

erdOne reviewed Jan 7, 2024

View reviewed changes

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

lower the priority of the instances

f858a9e

alreadydone reviewed Jan 7, 2024

View reviewed changes

acmepjz added a commit that referenced this pull request Jan 8, 2024

still depends on #9522

159cb72

acmepjz mentioned this pull request Jan 8, 2024

[Merged by Bors] - feat(FieldTheory/PurelyInseparable): definition and basic results of purely inseparable extensions #9488

Closed

11 tasks

acmepjz added 2 commits January 8, 2024 08:53

add Irreducible.exists_dvd_monic_irreducible_of_isIntegral and golf

6892f11

move Irreducible.exists_dvd_monic_irreducible_of_isIntegral to `Mat…

7b222e5

…hlib.RingTheory.AdjoinRoot`

erdOne reviewed Jan 8, 2024

View reviewed changes

riccardobrasca approved these changes Jan 8, 2024

View reviewed changes

leanprover-community-mathlib4-bot added delegated and removed awaiting-review labels Jan 8, 2024

add docstring

40ad921

mathlib-bors bot changed the title ~~feat(FieldTheory/IsSepClosed): add some results on separable closure and perfect field~~ [Merged by Bors] - feat(FieldTheory/IsSepClosed): add some results on separable closure and perfect field Jan 8, 2024

mathlib-bors bot closed this Jan 8, 2024

mathlib-bors bot deleted the acmepjz_perfect_1 branch January 8, 2024 15:44

alreadydone mentioned this pull request Jan 11, 2024

[Merged by Bors] - perf (Subalgebra.Basic): de-prioritize Subalgebra.module' #9655

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(FieldTheory/IsSepClosed): add some results on separable closure and perfect field #9522

[Merged by Bors] - feat(FieldTheory/IsSepClosed): add some results on separable closure and perfect field #9522

acmepjz commented Jan 7, 2024

alreadydone Jan 7, 2024 •

edited

Loading

acmepjz Jan 7, 2024

acmepjz Jan 8, 2024 •

edited

Loading

alreadydone Jan 8, 2024

acmepjz Jan 26, 2024 •

edited

Loading

alreadydone commented Jan 7, 2024

leanprover-bot commented Jan 7, 2024 •

edited by alreadydone

Loading

alreadydone commented Jan 8, 2024

github-actions bot commented Jan 8, 2024

erdOne Jan 8, 2024

alreadydone Jan 8, 2024 •

edited

Loading

riccardobrasca left a comment

riccardobrasca Jan 8, 2024

riccardobrasca Jan 8, 2024

acmepjz Jan 8, 2024

mathlib-bors bot commented Jan 8, 2024

acmepjz commented Jan 8, 2024

mathlib-bors bot commented Jan 8, 2024

[Merged by Bors] - feat(FieldTheory/IsSepClosed): add some results on separable closure and perfect field #9522

[Merged by Bors] - feat(FieldTheory/IsSepClosed): add some results on separable closure and perfect field #9522

Conversation

acmepjz commented Jan 7, 2024

alreadydone Jan 7, 2024 • edited Loading

Choose a reason for hiding this comment

acmepjz Jan 7, 2024

Choose a reason for hiding this comment

acmepjz Jan 8, 2024 • edited Loading

Choose a reason for hiding this comment

alreadydone Jan 8, 2024

Choose a reason for hiding this comment

acmepjz Jan 26, 2024 • edited Loading

Choose a reason for hiding this comment

alreadydone commented Jan 7, 2024

leanprover-bot commented Jan 7, 2024 • edited by alreadydone Loading

alreadydone commented Jan 8, 2024

github-actions bot commented Jan 8, 2024

erdOne Jan 8, 2024

Choose a reason for hiding this comment

alreadydone Jan 8, 2024 • edited Loading

Choose a reason for hiding this comment

riccardobrasca left a comment

Choose a reason for hiding this comment

riccardobrasca Jan 8, 2024

Choose a reason for hiding this comment

riccardobrasca Jan 8, 2024

Choose a reason for hiding this comment

acmepjz Jan 8, 2024

Choose a reason for hiding this comment

mathlib-bors bot commented Jan 8, 2024

acmepjz commented Jan 8, 2024

mathlib-bors bot commented Jan 8, 2024

alreadydone Jan 7, 2024 •

edited

Loading

acmepjz Jan 8, 2024 •

edited

Loading

acmepjz Jan 26, 2024 •

edited

Loading

leanprover-bot commented Jan 7, 2024 •

edited by alreadydone

Loading

alreadydone Jan 8, 2024 •

edited

Loading