[Merged by Bors] - feat: IsNormalClosure predicate #8418

alreadydone · 2023-11-15T07:29:16Z

Main changes are to the file NormalClosure:

Introduce predicate IsNormalClosure to characterize normal closures L/F of a field extension K/F by the conditions that every minimal polynomial of an element of K over F splits in L, and that L is generated by roots of such polynomials. (When K/F is not necessarily algebraic, the conditions actually says L/F is a normal closure of the algebraic closure of F in K over F.
IsNormalClosure.normal: a normal closure is always normal.
isNormalClosure_iff : if K/F is algebraic, the "generated by roots" condition in IsNormalClosure can be replaced by "generated by images of embeddings". To prove it, we split out the two inclusions in restrictScalars_eq_iSup_adjoin and golf its proof. restrictScalars_eq_iSup_adjoin is renamed to normalClosure_eq_iSup_adjoin as it has nothing to do with restrictScalars.
IsNormalClosure.lift: a normal closure of K/F embeds into any L/F such that the minpolys of K/F splits in L/F.
IsNormalClosure.equiv: normal closures are unique up to F-algebra isomorphisms.
isNormalClosure_normalClosure: normalClosure F K L is a valid normal closure if K/F is algebraic and all minpolys of K/F splits in L/F; in particular, if there is at least one F-embedding of K into L, and L/F is normal.
Algebra.IsAlgebraic.cardinal_mk_algHom_le_of_splits: if every minpoly of K/F splits in L/F, then L is maximal w.r.t. F-embeddings of K, in the sense that K →ₐ[F] L achieves maximal cardinality.

In the file Normal:

splits_of_mem_adjoin: If a set of algebraic elements in a field extension K/F have minimal polynomials that split in another extension L/F, then all minimal polynomials in the intermediate field generated by the set also split in L/F. This is in preparation for connecting IsNormalClosure and IsSplittingField.

In the file IntermediateField:

Add comap and show it forms a Galois connection with map.

In the file FieldTheory/Adjoin:

Add map_sup/iSup lemmas that follow from the Galois connection, plus an additional convenience lemma.

In the file RingTheory/Algebraic: add a lemma AlgHom.isAlgebraic_of_injective.

Co-authored-by: Jz Pan acme_pjz@hotmail.com

tb65536 · 2023-11-15T07:40:17Z

Mathlib/FieldTheory/Adjoin.lean

+      adjoin_algebraic_toSubalgebra fun _ ↦ isAlgebraic_of_mem_rootSet]
+  exact ⟨fun ⟨spl, adj⟩ ↦ ⟨spl, adj⟩, fun ⟨spl, adj⟩ ↦ ⟨spl, adj⟩⟩
+
+-- Note: p.Splits (algebraMap F E) also works
 theorem isSplittingField_iff {p : F[X]} {K : IntermediateField F E} :
    p.IsSplittingField F K ↔ p.Splits (algebraMap F K) ∧ K = adjoin F (p.rootSet E) := by
  suffices _ → (Algebra.adjoin F (p.rootSet K) = ⊤ ↔ K = adjoin F (p.rootSet E)) by


Is it possible to use your new lemma to golf this proof?

It doesn't quite work because Polynomial.adjoin_rootSet_eq_range is about Subalgebras not IntermediateFields. I wonder whether we should change IsSplittingField to use IntermediateField.adjoin ...

This can be a good idea, but let's keep it for another PR.

tb65536 · 2023-11-15T07:47:20Z

Mathlib/FieldTheory/Normal.lean

+  have : ∀ x ∈ S, (minpoly F x).Splits (algebraMap F E) := fun x hx ↦ splits_of_splits
+    (splits x hx).2 fun y hy ↦ (le_iSup _ ⟨x, hx⟩ : _ ≤ E) (subset_adjoin F _ <| by exact hy)
+  obtain ⟨φ⟩ := nonempty_algHom_adjoin_of_splits fun x hx ↦ ⟨(splits x hx).1, this x hx⟩
+  convert splits_comp_of_splits _ E.val.toRingHom (normal.splits <| φ ⟨x, hx⟩)
+  rw [minpoly.algHom_eq _ φ.injective, ← minpoly.algHom_eq _ (adjoin F S).val.injective]
+  rfl


I haven't looked at this super closely, but it feels like this should all be easier. For instance, going from (minpoly F x).Splits (algebraMap F E) to (minpoly F x).Splits (algebraMap F L) feels like it should be a one-liner. Are there missing lemmas in the library perhaps?

going from (minpoly F x).Splits (algebraMap F E) to (minpoly F x).Splits (algebraMap F L) feels like it should be a one-liner.

I think it's Polynomial.splits_comp_of_splits

As @acmepjz said, if the two minpoly F x were defeq then convert splits_comp_of_splits would close the goal. However, the normal.splits only guarantees the splitting of minpolys of elements in E; since adjoin F S embeds in E (via φ), the minpolys of elements in adjoin F S also splits because they are equal to the minpolys of the images of the elements in E. This is what rw [minpoly.algHom_eq _ φ.injective] does, and then we need another rewrite to go between adjoin F S and K.
The whole proof is a bit nontrivial and uses Normal.of_isSplittingField essentially.

Mathlib/FieldTheory/NormalClosure.lean

alreadydone

Thanks for the review!

Mathlib/FieldTheory/NormalClosure.lean

alreadydone · 2023-11-16T07:07:15Z

Mathlib/FieldTheory/Adjoin.lean

+      adjoin_algebraic_toSubalgebra fun _ ↦ isAlgebraic_of_mem_rootSet]
+  exact ⟨fun ⟨spl, adj⟩ ↦ ⟨spl, adj⟩, fun ⟨spl, adj⟩ ↦ ⟨spl, adj⟩⟩
+
+-- Note: p.Splits (algebraMap F E) also works
 theorem isSplittingField_iff {p : F[X]} {K : IntermediateField F E} :
    p.IsSplittingField F K ↔ p.Splits (algebraMap F K) ∧ K = adjoin F (p.rootSet E) := by
  suffices _ → (Algebra.adjoin F (p.rootSet K) = ⊤ ↔ K = adjoin F (p.rootSet E)) by


It doesn't quite work because Polynomial.adjoin_rootSet_eq_range is about Subalgebras not IntermediateFields. I wonder whether we should change IsSplittingField to use IntermediateField.adjoin ...

alreadydone · 2023-11-16T07:26:06Z

Mathlib/FieldTheory/Normal.lean

+  have : ∀ x ∈ S, (minpoly F x).Splits (algebraMap F E) := fun x hx ↦ splits_of_splits
+    (splits x hx).2 fun y hy ↦ (le_iSup _ ⟨x, hx⟩ : _ ≤ E) (subset_adjoin F _ <| by exact hy)
+  obtain ⟨φ⟩ := nonempty_algHom_adjoin_of_splits fun x hx ↦ ⟨(splits x hx).1, this x hx⟩
+  convert splits_comp_of_splits _ E.val.toRingHom (normal.splits <| φ ⟨x, hx⟩)
+  rw [minpoly.algHom_eq _ φ.injective, ← minpoly.algHom_eq _ (adjoin F S).val.injective]
+  rfl


As @acmepjz said, if the two minpoly F x were defeq then convert splits_comp_of_splits would close the goal. However, the normal.splits only guarantees the splitting of minpolys of elements in E; since adjoin F S embeds in E (via φ), the minpolys of elements in adjoin F S also splits because they are equal to the minpolys of the images of the elements in E. This is what rw [minpoly.algHom_eq _ φ.injective] does, and then we need another rewrite to go between adjoin F S and K.
The whole proof is a bit nontrivial and uses Normal.of_isSplittingField essentially.

Mathlib/FieldTheory/NormalClosure.lean

Mathlib/RingTheory/Algebraic.lean

Mathlib/FieldTheory/IntermediateField.lean

riccardobrasca · 2023-11-17T11:17:53Z

Mathlib/FieldTheory/Adjoin.lean

+      adjoin_algebraic_toSubalgebra fun _ ↦ isAlgebraic_of_mem_rootSet]
+  exact ⟨fun ⟨spl, adj⟩ ↦ ⟨spl, adj⟩, fun ⟨spl, adj⟩ ↦ ⟨spl, adj⟩⟩
+
+-- Note: p.Splits (algebraMap F E) also works
 theorem isSplittingField_iff {p : F[X]} {K : IntermediateField F E} :
    p.IsSplittingField F K ↔ p.Splits (algebraMap F K) ∧ K = adjoin F (p.rootSet E) := by
  suffices _ → (Algebra.adjoin F (p.rootSet K) = ⊤ ↔ K = adjoin F (p.rootSet E)) by


This can be a good idea, but let's keep it for another PR.

Mathlib/FieldTheory/NormalClosure.lean

riccardobrasca · 2023-11-17T11:21:39Z

Mathlib/FieldTheory/NormalClosure.lean

@@ -31,62 +44,135 @@ lemma normalClosure_def : normalClosure F K L = ⨆ f : K →ₐ[F] L, f.fieldRa

 variable {F K L}

+/-- A normal closure is always normal. -/
+lemma IsNormalClosure.normal [h : IsNormalClosure F K L] : Normal F L :=


Can this be an instance?

No way to infer K, right? (Same in Normal.ofIsSplittingField, where there's no way to infer the polynomial.)

Ah yes, of course.

alreadydone · 2023-11-17T18:35:39Z

Mathlib/FieldTheory/NormalClosure.lean

@@ -31,62 +44,135 @@ lemma normalClosure_def : normalClosure F K L = ⨆ f : K →ₐ[F] L, f.fieldRa

 variable {F K L}

+/-- A normal closure is always normal. -/
+lemma IsNormalClosure.normal [h : IsNormalClosure F K L] : Normal F L :=


No way to infer K, right? (Same in Normal.ofIsSplittingField, where there's no way to infer the polynomial.)

Mathlib/FieldTheory/IntermediateField.lean

Mathlib/RingTheory/Algebraic.lean

Mathlib/FieldTheory/NormalClosure.lean

Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>

riccardobrasca · 2023-11-18T00:38:13Z

Thanks!

bors merge

Main changes are to the file NormalClosure: + Introduce predicate `IsNormalClosure` to characterize normal closures L/F of a field extension K/F by the conditions that every minimal polynomial of an element of K over F splits in L, and that L is generated by roots of such polynomials. (When K/F is not necessarily algebraic, the conditions actually says L/F is a normal closure of the algebraic closure of F in K over F. + `IsNormalClosure.normal`: a normal closure is always normal. + `isNormalClosure_iff `: if K/F is algebraic, the "generated by roots" condition in IsNormalClosure can be replaced by "generated by images of embeddings". To prove it, we split out the two inclusions in `restrictScalars_eq_iSup_adjoin` and golf its proof. `restrictScalars_eq_iSup_adjoin` is renamed to `normalClosure_eq_iSup_adjoin` as it has nothing to do with `restrictScalars`. + `IsNormalClosure.lift`: a normal closure of K/F embeds into any L/F such that the minpolys of K/F splits in L/F. + `IsNormalClosure.equiv`: normal closures are unique up to F-algebra isomorphisms. + `isNormalClosure_normalClosure`: `normalClosure F K L` is a valid normal closure if K/F is algebraic and all minpolys of K/F splits in L/F; in particular, if there is at least one F-embedding of K into L, and L/F is normal. + `Algebra.IsAlgebraic.cardinal_mk_algHom_le_of_splits`: if every minpoly of `K/F` splits in `L/F`, then `L` is maximal w.r.t. `F`-embeddings of `K`, in the sense that `K →ₐ[F] L` achieves maximal cardinality. In the file Normal: + `splits_of_mem_adjoin`: If a set of algebraic elements in a field extension `K/F` have minimal polynomials that split in another extension `L/F`, then all minimal polynomials in the intermediate field generated by the set also split in `L/F`. This is in preparation for connecting `IsNormalClosure` and `IsSplittingField`. In the file IntermediateField: + Add `comap` and show it forms a Galois connection with `map`. In the file FieldTheory/Adjoin: + Add `map_sup/iSup` lemmas that follow from the Galois connection, plus an additional convenience lemma. In the file RingTheory/Algebraic: add a lemma `AlgHom.isAlgebraic_of_injective`. Co-authored-by: Jz Pan <acme_pjz@hotmail.com> Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

mathlib-bors · 2023-11-18T01:08:58Z

Pull request successfully merged into master.

Build succeeded:

Main changes are to the file NormalClosure: + Introduce predicate `IsNormalClosure` to characterize normal closures L/F of a field extension K/F by the conditions that every minimal polynomial of an element of K over F splits in L, and that L is generated by roots of such polynomials. (When K/F is not necessarily algebraic, the conditions actually says L/F is a normal closure of the algebraic closure of F in K over F. + `IsNormalClosure.normal`: a normal closure is always normal. + `isNormalClosure_iff `: if K/F is algebraic, the "generated by roots" condition in IsNormalClosure can be replaced by "generated by images of embeddings". To prove it, we split out the two inclusions in `restrictScalars_eq_iSup_adjoin` and golf its proof. `restrictScalars_eq_iSup_adjoin` is renamed to `normalClosure_eq_iSup_adjoin` as it has nothing to do with `restrictScalars`. + `IsNormalClosure.lift`: a normal closure of K/F embeds into any L/F such that the minpolys of K/F splits in L/F. + `IsNormalClosure.equiv`: normal closures are unique up to F-algebra isomorphisms. + `isNormalClosure_normalClosure`: `normalClosure F K L` is a valid normal closure if K/F is algebraic and all minpolys of K/F splits in L/F; in particular, if there is at least one F-embedding of K into L, and L/F is normal. + `Algebra.IsAlgebraic.cardinal_mk_algHom_le_of_splits`: if every minpoly of `K/F` splits in `L/F`, then `L` is maximal w.r.t. `F`-embeddings of `K`, in the sense that `K →ₐ[F] L` achieves maximal cardinality. In the file Normal: + `splits_of_mem_adjoin`: If a set of algebraic elements in a field extension `K/F` have minimal polynomials that split in another extension `L/F`, then all minimal polynomials in the intermediate field generated by the set also split in `L/F`. This is in preparation for connecting `IsNormalClosure` and `IsSplittingField`. In the file IntermediateField: + Add `comap` and show it forms a Galois connection with `map`. In the file FieldTheory/Adjoin: + Add `map_sup/iSup` lemmas that follow from the Galois connection, plus an additional convenience lemma. In the file RingTheory/Algebraic: add a lemma `AlgHom.isAlgebraic_of_injective`. Co-authored-by: Jz Pan <acme_pjz@hotmail.com> Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

alreadydone added 8 commits November 6, 2023 15:59

refactor: golf IntermediateField.Lifts

9fa57b1

finer versions of algHom_mk_adjoin_splits

dbe017b

More convenience lemmas

8ee933e

systematic rename + 2 golfs

01d1707

wip

0dec893

Merge remote-tracking branch 'origin/master' into IsNormalClosure

d51dd7d

cardinal_mk_algHom_le_of_splits

7ff9b1b

Merge remote-tracking branch 'origin/master' into IsNormalClosure

dc2c368

alreadydone added awaiting-review The author would like community review of the PR t-algebra Algebra (groups, rings, fields etc) labels Nov 15, 2023

alreadydone requested review from acmepjz and tb65536 November 15, 2023 07:29

docstrings

67ada4f

alreadydone mentioned this pull request Nov 15, 2023

[Merged by Bors] - feat(FieldTheory/SeparableDegree): basic definition of separable degree of field extension #8117

Closed

2 tasks

tb65536 reviewed Nov 15, 2023

View reviewed changes

alreadydone 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 Nov 15, 2023

switch to Embedding

e5501e0

alreadydone commented Nov 16, 2023

View reviewed changes

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

alreadydone and others added 2 commits November 16, 2023 10:29

lemma -> def

e20fb8a

Merge branch 'master' into IsNormalClosure

f452e91

alreadydone added awaiting-review The author would like community review of the PR awaiting-CI and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. awaiting-author A reviewer has asked the author a question or requested changes awaiting-CI labels Nov 16, 2023

riccardobrasca self-assigned this Nov 17, 2023

riccardobrasca reviewed Nov 17, 2023

View reviewed changes

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

Merge branch 'master' into IsNormalClosure

b6791cd

alreadydone commented Nov 17, 2023

View reviewed changes

docstring

f500303

Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>

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

fix merge

e933aba

alreadydone 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 Nov 17, 2023

module doc: main definitions

126d083

alreadydone 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 Nov 17, 2023

github-actions 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 Nov 18, 2023

mathlib-bors bot changed the title ~~feat: IsNormalClosure predicate~~ [Merged by Bors] - feat: IsNormalClosure predicate Nov 18, 2023

mathlib-bors bot closed this Nov 18, 2023

mathlib-bors bot deleted the IsNormalClosure branch November 18, 2023 01:09

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

remove temporary lemma in favor of #8418

2e231b0

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat: IsNormalClosure predicate #8418

[Merged by Bors] - feat: IsNormalClosure predicate #8418

alreadydone commented Nov 15, 2023 •

edited

tb65536 Nov 15, 2023

alreadydone Nov 16, 2023

riccardobrasca Nov 17, 2023

tb65536 Nov 15, 2023

acmepjz Nov 15, 2023

alreadydone Nov 16, 2023

alreadydone left a comment

alreadydone Nov 16, 2023

alreadydone Nov 16, 2023

riccardobrasca Nov 17, 2023

riccardobrasca Nov 17, 2023

alreadydone Nov 17, 2023 •

edited

riccardobrasca Nov 18, 2023

alreadydone Nov 17, 2023 •

edited

riccardobrasca commented Nov 18, 2023

mathlib-bors bot commented Nov 18, 2023

[Merged by Bors] - feat: IsNormalClosure predicate #8418

[Merged by Bors] - feat: IsNormalClosure predicate #8418

Conversation

alreadydone commented Nov 15, 2023 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

alreadydone left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

alreadydone Nov 17, 2023 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

alreadydone Nov 17, 2023 • edited

Choose a reason for hiding this comment

riccardobrasca commented Nov 18, 2023

mathlib-bors bot commented Nov 18, 2023

alreadydone commented Nov 15, 2023 •

edited

alreadydone Nov 17, 2023 •

edited

alreadydone Nov 17, 2023 •

edited