[Merged by Bors] - feat(number_theory): fundamental identity of ramification index and inertia degree #12287

Vierkantor · 2022-02-25T16:33:32Z

This PR proves the fundamental identity of ramification index and inertia degree:

Let p be a prime in a Dedekind domain R, S the integral closure of R in some finite field extension L of K = Frac(R), then for P ranging over the primes lying over p, Σ P, e P * f P = [L : K].

depends on: [Merged by Bors] - feat(number_theory): [S/P^e : R/p] = e * [S/P : R/p], where e is ramification index #15316
depends on: [Merged by Bors] - feat(number_theory): degree [Frac(S):Frac(R)] is degree [S/pS:R/p] #15315

…ules These are, like #12178, split off from #12287

…ules (#12401) These are, like #12178, split off from #12287

We define ramification index `ramification_idx` and inertia degree `inertia_deg` for `P : ideal S` over `p : ideal R` given a ring extension `f : R →+* S`. The literature generally assumes `p` is included in `P`, both are maximal, `R` is the ring of integers of a number field `K` and `S` is the integral closure of `R` in `L`, a finite separable extension of `K`; we relax these assumptions as much as is practical. This PR was split off from #12287.

Two little lemmas on the set of factors which I needed for #12287.

…#14333) Two little lemmas on the set of factors which I needed for #12287. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

kbuzzard · 2022-05-26T14:47:20Z

It's really exciting that we're moving towards this; I have only just seen this PR! Thanks to Oliver for directing my attention towards it.

src/number_theory/ramification_inertia.lean

kbuzzard · 2022-05-26T14:46:00Z

src/number_theory/ramification_inertia.lean

+/-- The **fundamental identity** of ramification index `e` and inertia degree `f`:
+for `P` ranging over the primes lying over `p`, `∑ P, e P * f P = [Frac(S) : Frac(R)]`;
+if `Frac(S) : Frac(R)` is a finite extension, `p` is maximal
+and `S` is the integral closure of `R` in `L`. -/


As it stands this docstring isn't quite true (I was very confused by this for a minute or two!). The issue is that if Frac(S)/Frac(R) is finite then in this generality it's not enough to deduce that S is a Noetherian R-module. Here https://arxiv.org/abs/2102.10481 is a recent paper discussing a statement which is true in the generality of the docstring; however I am certainly suggesting we should be formalising it! The result proved is exactly what I need for several applications; all the applications to arithmetic have S a Noetherian (or equivalently finitely-generated, as R is Noetherian) R-module. For applications beyond arithmetic, I'm very happy to be worrying about them later :-) Note that S f.g. as R-module implies Frac(S) is finite over Frac(R).

(for a Dedekind domain `R` and its integral closure `S` and maximal ideal `p`) This is the first step in showing the fundamental identity of inertia degree and ramification index (#12287). The next step is to factor `pS` into coprime factors `P` and use the Chinese remainder theorem.

src/number_theory/ramification_inertia.lean

#15315) (for a Dedekind domain `R` and its integral closure `S` and maximal ideal `p`) This is the first step in showing the fundamental identity of inertia degree and ramification index (#12287). The next step is to factor `pS` into coprime factors `P` and use the Chinese remainder theorem. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: Anne Baanen <t.baanen@vu.nl>

…fication index (#15316) Let `S` be a Dedekind domain extending the commutative ring `R`, `p` a maximal ideal of `R`, `P` a prime ideal of `S`, and `e` the (nonzero) ramification index of `P` over `p`. Because the ramification index is nonzero, we get an inclusion `R/p → S/P` and we can compute that the degree of the field extension `[S/(P^e) : R/p]` is exactly `e` times `[S/P : R/p]`. This is the next step in showing the fundamental identity of inertia degree and ramification index (#12287). Setting up the ingredients for the proof is quite complicated because it involves taking `(P^(i+1) / P^e)` as a `R/p`-subspace of `P^i / P^e` and basically each part of this structure would produce free metavariables if we naïvely assigned it an instance. In the end, the important parts are an instance for `S/(P^e)` as `R/p`-algebra and replacing subspaces with the image of inclusion maps. Co-authored-by: Anne Baanen <t.baanen@vu.nl> Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

mathlib-dependent-issues-bot · 2022-08-04T15:09:51Z

This PR/issue depends on:

~~[Merged by Bors] - feat(number_theory): [S/P^e : R/p] = e * [S/P : R/p], where e is ramification index #15316~~
~~[Merged by Bors] - feat(number_theory): degree [Frac(S):Frac(R)] is degree [S/pS:R/p] #15315~~
By Dependent Issues (🤖). Happy coding!

…nertia degree

Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>

riccardobrasca

LGTM!

src/number_theory/ramification_inertia.lean

jcommelin

Thanks 🎉

bors merge

…nertia degree (#12287) This PR proves the fundamental identity of ramification index and inertia degree: Let `p` be a prime in a Dedekind domain `R`, `S` the integral closure of `R` in some finite field extension `L` of `K = Frac(R)`, then for `P` ranging over the primes lying over `p`, `Σ P, e P * f P = [L : K]`. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

bors · 2022-08-17T20:40:06Z

Pull request successfully merged into master.

Build succeeded:

Vierkantor added the WIP Work in progress label Feb 25, 2022

Vierkantor force-pushed the ramification-inertia branch from 2d31d7f to 8b38f8d Compare March 1, 2022 11:24

Vierkantor added a commit that referenced this pull request Mar 2, 2022

feat(ring_theory/ideal): more lemmas on ideals multiplied with submod…

fa8c9d0

…ules These are, like #12178, split off from #12287

Vierkantor mentioned this pull request Mar 2, 2022

[Merged by Bors] - feat(ring_theory/ideal): more lemmas on ideals multiplied with submodules #12401

Closed

bors bot pushed a commit that referenced this pull request Mar 3, 2022

feat(ring_theory/ideal): more lemmas on ideals multiplied with submod…

9deac65

…ules (#12401) These are, like #12178, split off from #12287

Vierkantor force-pushed the ramification-inertia branch from 8b38f8d to 6399123 Compare March 30, 2022 08:29

leanprover-community-bot-assistant added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Apr 8, 2022

Vierkantor force-pushed the ramification-inertia branch from 5090ff2 to c7091c3 Compare April 11, 2022 13:36

leanprover-community-bot-assistant 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 Apr 11, 2022

Vierkantor force-pushed the ramification-inertia branch from fd9e9b5 to c4d8cc4 Compare May 2, 2022 12:40

leanprover-community-bot-assistant removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label May 2, 2022

kim-em added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label May 2, 2022

Vierkantor force-pushed the ramification-inertia branch from c4d8cc4 to b2d98d4 Compare May 23, 2022 10:20

Vierkantor mentioned this pull request May 23, 2022

[Merged by Bors] - feat(number_theory): define ramification index and inertia degree #14332

Closed

Vierkantor added a commit that referenced this pull request May 23, 2022

feat(ring_theory/unique_factorization_domain): misc lemmas on factors

88b9aeb

Two little lemmas on the set of factors which I needed for #12287.

Vierkantor mentioned this pull request May 23, 2022

[Merged by Bors] - feat(ring_theory/unique_factorization_domain): misc lemmas on factors #14333

Closed

kbuzzard reviewed May 26, 2022

View reviewed changes

Vierkantor mentioned this pull request Jul 13, 2022

[Merged by Bors] - feat(number_theory): degree [Frac(S):Frac(R)] is degree [S/pS:R/p] #15315

Closed

Vierkantor force-pushed the ramification-inertia branch from b2d98d4 to 5901013 Compare July 13, 2022 16:09

Vierkantor mentioned this pull request Jul 13, 2022

[Merged by Bors] - feat(number_theory): [S/P^e : R/p] = e * [S/P : R/p], where e is ramification index #15316

Closed

1 task

Vierkantor changed the title ~~feat(number_theory): fundamental identity of ramification index and inertia degree [WIP]~~ feat(number_theory): fundamental identity of ramification index and inertia degree Jul 13, 2022

Vierkantor commented Jul 13, 2022

View reviewed changes

src/number_theory/ramification_inertia.lean Outdated Show resolved Hide resolved

mathlib-dependent-issues-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 4, 2022

Vierkantor force-pushed the ramification-inertia branch from cebab99 to f1cb8aa Compare August 8, 2022 13:37

Vierkantor and others added 5 commits August 16, 2022 12:38

feat(number_theory): fundamental identity of ramification index and i…

92a5296

…nertia degree

Clarify docstring

0fbdbd1

Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>

Fix docstring

5385b2d

Lint fix: overlong line

174ef58

Bump mathlib, fix

00a6bad

Vierkantor force-pushed the ramification-inertia branch from cee9e2b to 00a6bad Compare August 16, 2022 12:56

riccardobrasca self-assigned this Aug 17, 2022

riccardobrasca approved these changes Aug 17, 2022

View reviewed changes

src/number_theory/ramification_inertia.lean Show resolved Hide resolved

riccardobrasca reviewed Aug 17, 2022

View reviewed changes

src/number_theory/ramification_inertia.lean Show resolved Hide resolved

Add instances for rings of integers so the theorem applies immediately

f5aa1ce

jcommelin approved these changes Aug 17, 2022

View reviewed changes

leanprover-community-bot-assistant 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 Aug 17, 2022

bors bot changed the title ~~feat(number_theory): fundamental identity of ramification index and inertia degree~~ [Merged by Bors] - feat(number_theory): fundamental identity of ramification index and inertia degree Aug 17, 2022

bors bot closed this Aug 17, 2022

bors bot deleted the ramification-inertia branch August 17, 2022 20:40

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(number_theory): fundamental identity of ramification index and inertia degree #12287

[Merged by Bors] - feat(number_theory): fundamental identity of ramification index and inertia degree #12287

Vierkantor commented Feb 25, 2022 •

edited by github-actions bot

Loading

kbuzzard commented May 26, 2022

kbuzzard May 26, 2022

mathlib-dependent-issues-bot commented Aug 4, 2022

riccardobrasca left a comment

jcommelin left a comment

bors bot commented Aug 17, 2022

[Merged by Bors] - feat(number_theory): fundamental identity of ramification index and inertia degree #12287

[Merged by Bors] - feat(number_theory): fundamental identity of ramification index and inertia degree #12287

Conversation

Vierkantor commented Feb 25, 2022 • edited by github-actions bot Loading

kbuzzard commented May 26, 2022

kbuzzard May 26, 2022

Choose a reason for hiding this comment

mathlib-dependent-issues-bot commented Aug 4, 2022

riccardobrasca left a comment

Choose a reason for hiding this comment

jcommelin left a comment

Choose a reason for hiding this comment

bors bot commented Aug 17, 2022

Vierkantor commented Feb 25, 2022 •

edited by github-actions bot

Loading