-
Notifications
You must be signed in to change notification settings - Fork 298
[Merged by Bors] - feat(number_theory/kummer_dedekind): define conductor and add basic API plus theorem #16833
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
These are mostly superficial comments without actually opening the branch in VSCode, and I may or may not take another look later ...
|
||
open ideal polynomial double_quot unique_factorization_monoid algebra ring_hom | ||
|
||
local notation R `[` x `]` := adjoin R ({x} : set S) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I am not sure, but since we now have R[X]
for polynomials (even if it's not opened here), this can be a little confusing. But I agree we need a good notation for adjoin
.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'll try and find something else!
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
|
||
/-- The canonical morphism of rings from `R[x] ⧸ (I*R[x])` to `S ⧸ (I*S)` is an isomorphism | ||
when `I` and `(conductor R x) ∩ R` are coprime. -/ | ||
noncomputable def quot_adjoin_equiv_quot_map (hx : (conductor R x).comap (algebra_map R S) ⊔ I = ⊤) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Maybe a simps
tag? It depends on what you want to do with this map, but we probably want at least a minimal API around it.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The I tried adding simps apply
but it gave the "wrong" projection lemma so I added a projection lemma manually.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
In a later PR - possibly #16870 - I'll prove the usual criterion for the Dedekind-Kummer theorem in terms of the divisibility of the index [O_K : Z[a] ]
by the prime ideal I
so I'll probably end up adding more API to do that.
Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
Thanks! bors merge |
Pull request successfully merged into master. Build succeeded: |
In this PR we define the conductor ideal and prove some basic results about it.
In a later PR (#16870), these will be used to prove the Dedekind-Kummer theorem in full generality.