[Merged by Bors] - feat(ring_theory/trace): Tr(x) is the sum of embeddings σ x into an algebraically closed field #8762

Vierkantor · 2021-08-19T12:17:12Z

The point of this PR is to provide the other formulation of "the trace of x is the sum of its conjugates", alongside trace_eq_sum_roots, namely trace_eq_sum_embeddings. We do so by exploiting the bijection between conjugate roots to x : L over K and embeddings of K(x), then counting the number of embeddings of x to go to the whole of L.

depends on: [Merged by Bors] - feat(ring_theory): the trace of an integral element is integral #8702
depends on: [Merged by Bors] - chore(field_theory): make is_separable an instance parameter #8741
depends on: [Merged by Bors] - feat(algebra/big_operators): the product over {x // x ∈ m} is the product over m.to_finset #8742
depends on: [Merged by Bors] - feat(field_theory/intermediate_field): generalize algebra instances #8761

The `algebra` and `is_scalar_tower` instances for `intermediate_field` are (again) as general as those for `subalgebra`.

Vierkantor · 2021-08-24T13:32:24Z

src/linear_algebra/free_module_pid.lean

-    use ϕ,
-    intros ψ hψ,
-    exact P_max _ ⟨_, rfl⟩ hψ },
+    exact ⟨ϕ, λ ψ hψ, P_max _ ⟨_, rfl⟩ hψ⟩ },


Not only is this slightly shorter, it runs noticeably faster which was useful when messing around with some instances. (See also #8761.)

Vierkantor · 2021-08-24T13:33:24Z

src/ring_theory/trace.lean

@@ -232,20 +233,29 @@ end

 end intermediate_field.adjoin_simple

-lemma trace_eq_sum_roots [finite_dimensional K L]


trace_eq_sum_roots still exists with the same statement, it's just that the first part of the proof was split off into trace_eq_trace_adjoin and the diff is having trouble showing that clearly.

Use a specialized instance for the common case `is_scalar_tower K S L`, which was the only instance in the old situation.

src/field_theory/adjoin.lean

…le extension

…lgebraically closed field

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

github-actions · 2021-08-26T13:30:59Z

🎉 Great news! Looks like all the dependencies have been resolved:

~~[Merged by Bors] - feat(ring_theory): the trace of an integral element is integral #8702~~
~~[Merged by Bors] - chore(field_theory): make is_separable an instance parameter #8741~~
~~[Merged by Bors] - feat(algebra/big_operators): the product over {x // x ∈ m} is the product over m.to_finset #8742~~
~~[Merged by Bors] - feat(field_theory/intermediate_field): generalize algebra instances #8761~~

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

jcommelin

Thanks 🎉 This is looking good. (Note that it is sufficient to consider an overfield E that contains a Galois closure of L/K. But I don't think we can express that in mathlib atm.)

bors d+

bors · 2021-08-26T13:39:47Z

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

Vierkantor · 2021-08-26T14:07:41Z

Note that it is sufficient to consider an overfield E that contains a Galois closure of L/K. But I don't think we can express that in mathlib atm.

Indeed, for the proof we really just need that minpoly K (pb : power_basis K L).gen splits in E for the pb that falls out of the primitive element theorem. But that's quite awkward to express.

Vierkantor · 2021-08-26T14:28:45Z

The build has actually finished correctly, it's just the dependent issues action that seems to have failed. Since all dependencies have actually been merged, I'll go ahead and hit the button.

bors merge

jcommelin · 2021-08-26T14:29:08Z

Right, so for now I would just merge this as it is (when CI is happy).

…lgebraically closed field (#8762) The point of this PR is to provide the other formulation of "the trace of `x` is the sum of its conjugates", alongside `trace_eq_sum_roots`, namely `trace_eq_sum_embeddings`. We do so by exploiting the bijection between conjugate roots to `x : L` over `K` and embeddings of `K(x)`, then counting the number of embeddings of `x` to go to the whole of `L`. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: Anne Baanen <t.baanen@vu.nl>

Vierkantor · 2021-08-26T15:16:15Z

CI is happy, it just doesn't realize it, is my point :)

bors · 2021-08-26T16:47:55Z

Build failed (retrying...):

Lint mathlib

…lgebraically closed field (#8762) The point of this PR is to provide the other formulation of "the trace of `x` is the sum of its conjugates", alongside `trace_eq_sum_roots`, namely `trace_eq_sum_embeddings`. We do so by exploiting the bijection between conjugate roots to `x : L` over `K` and embeddings of `K(x)`, then counting the number of embeddings of `x` to go to the whole of `L`. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: Anne Baanen <t.baanen@vu.nl>

bors · 2021-08-26T19:37:00Z

Pull request successfully merged into master.

Build succeeded:

This PR shows the determinant of the trace form is nonzero over a finite separable field extension. This is an important ingredient in showing the integral closure of a Dedekind domain in a finite separable extension is again a Dedekind domain, i.e. that rings of integers are Dedekind domains. We extend the results of #8762 to write the trace form as a Vandermonde matrix to get a nice expression for the determinant, then use separability to show this value is nonzero.

Vierkantor added WIP Work in progress blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. labels Aug 19, 2021

Vierkantor force-pushed the trace_eq_sum_embeddings branch from aa726e7 to a865d45 Compare August 20, 2021 10:24

github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Aug 20, 2021

Vierkantor mentioned this pull request Aug 20, 2021

[Merged by Bors] - feat(ring_theory/trace): the trace form is nondegenerate #8777

Closed

3 tasks

github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Aug 20, 2021

Vierkantor force-pushed the trace_eq_sum_embeddings branch from a865d45 to b1c4e1d Compare August 23, 2021 11:56

github-actions bot added merge-conflict Please `git merge origin/master` then a bot will remove this label. and removed merge-conflict Please `git merge origin/master` then a bot will remove this label. labels Aug 23, 2021

Vierkantor mentioned this pull request Aug 24, 2021

[Merged by Bors] - feat(ring_theory/dedekind_domain): the integral closure of a DD is a DD #8847

Closed

4 tasks

Vierkantor added 3 commits August 24, 2021 13:24

feat(field_theory/intermediate_field): generalize algebra instances

41c42fe

The `algebra` and `is_scalar_tower` instances for `intermediate_field` are (again) as general as those for `subalgebra`.

Lint fix

232d8b9

Fix the timeout by making some unifications fail fast

af3ffa7

Vierkantor force-pushed the trace_eq_sum_embeddings branch from b1c4e1d to 9dc4380 Compare August 24, 2021 13:29

Vierkantor added awaiting-review The author would like community review of the PR and removed WIP Work in progress merge-conflict Please `git merge origin/master` then a bot will remove this label. labels Aug 24, 2021

Vierkantor commented Aug 24, 2021

View reviewed changes

Specialize intermediate_field.is_scalar_tower_mid

fdad3dd

Use a specialized instance for the common case `is_scalar_tower K S L`, which was the only instance in the old situation.

Ruben-VandeVelde reviewed Aug 24, 2021

View reviewed changes

src/field_theory/adjoin.lean Outdated Show resolved Hide resolved

Vierkantor and others added 5 commits August 25, 2021 10:58

chore(ring_theory/power_basis): @[simps] lift_equiv'

a32df1c

feat(field_theory): cardinality of alg_homs out of a finite separab…

f166b33

…le extension

Golf/speedup

2691f0b

feat(ring_theory/trace): Tr(x) is the sum of embeddings σ x into an a…

2fde8df

…lgebraically closed field

More elegant proof

17ea68a

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

Vierkantor force-pushed the trace_eq_sum_embeddings branch from d351f4d to 17ea68a Compare August 25, 2021 10:58

Lint fix, by rearranging variables

91372ec

github-actions bot removed 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 Aug 26, 2021

jcommelin reviewed Aug 26, 2021

View reviewed changes

github-actions bot added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Aug 26, 2021

github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Aug 26, 2021

bors bot changed the title ~~feat(ring_theory/trace): Tr(x) is the sum of embeddings σ x into an algebraically closed field~~ [Merged by Bors] - feat(ring_theory/trace): Tr(x) is the sum of embeddings σ x into an algebraically closed field Aug 26, 2021

bors bot closed this Aug 26, 2021

bors bot deleted the trace_eq_sum_embeddings branch August 26, 2021 19:37

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(ring_theory/trace): Tr(x) is the sum of embeddings σ x into an algebraically closed field #8762

[Merged by Bors] - feat(ring_theory/trace): Tr(x) is the sum of embeddings σ x into an algebraically closed field #8762

Vierkantor commented Aug 19, 2021 •

edited by github-actions bot

Vierkantor Aug 24, 2021

Vierkantor Aug 24, 2021

github-actions bot commented Aug 26, 2021

jcommelin left a comment

bors bot commented Aug 26, 2021

Vierkantor commented Aug 26, 2021

Vierkantor commented Aug 26, 2021

jcommelin commented Aug 26, 2021

Vierkantor commented Aug 26, 2021

bors bot commented Aug 26, 2021

bors bot commented Aug 26, 2021

		@@ -232,20 +233,29 @@ end

		end intermediate_field.adjoin_simple

		lemma trace_eq_sum_roots [finite_dimensional K L]

[Merged by Bors] - feat(ring_theory/trace): Tr(x) is the sum of embeddings σ x into an algebraically closed field #8762

[Merged by Bors] - feat(ring_theory/trace): Tr(x) is the sum of embeddings σ x into an algebraically closed field #8762

Conversation

Vierkantor commented Aug 19, 2021 • edited by github-actions bot

Vierkantor Aug 24, 2021

Choose a reason for hiding this comment

Vierkantor Aug 24, 2021

Choose a reason for hiding this comment

github-actions bot commented Aug 26, 2021

jcommelin left a comment

Choose a reason for hiding this comment

bors bot commented Aug 26, 2021

Vierkantor commented Aug 26, 2021

Vierkantor commented Aug 26, 2021

jcommelin commented Aug 26, 2021

Vierkantor commented Aug 26, 2021

bors bot commented Aug 26, 2021

bors bot commented Aug 26, 2021

Vierkantor commented Aug 19, 2021 •

edited by github-actions bot