Conversation
PR summary 7b42e25396Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
github-actions
Bot
added
the
t-number-theory
xroblot
added
blocked-by-other-PR
…icates # Conflicts: # Mathlib/RingTheory/Algebraic/Integral.lean
mathlib-dependent-issues
Bot
removed
the
blocked-by-other-PR
|
This PR/issue depends on: |
mathlib-merge-conflicts
Bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
…icates # Conflicts: # Mathlib/RingTheory/Ideal/Pointwise.lean
github-actions
Bot
removed
the
merge-conflict
| ramification index and the inertia degree of `p` in `B`. -/ | ||
| theorem IsDecompositionRing.finrank_top [FaithfulSMul C B] [P.IsPrime] [P.IsDecompositionRing G C] : | ||
| Module.finrank C B = p.ramificationIdxIn B * p.inertiaDegIn B := by | ||
| by_cases hp : p = ⊥ |
There was a problem hiding this comment.
I think if we had a predicate for separable residue fields, then we might not need this casework on p.
There was a problem hiding this comment.
(Oh, I guess I already said this earlier, but I think it's probably worth doing at this stage since it's now materially affecting the proofs, so a future refactor wouldn't just be a simple cut and paste from finite quotients to separable residue fields).
There was a problem hiding this comment.
I guess you're right but I am not really sure what it would look like. Is it something like:
class Ring.HasSeparableResidueFields (A : Type*) [CommRing A] : Prop where
perfectField (p : Ideal A) [p.IsMaximal] : PerfectField (A ⧸ p)There was a problem hiding this comment.
Why not just ask for Algebra.IsSpearable p.ResidueField q.ResidueField for all prime ideals q/p?
There was a problem hiding this comment.
I guess there's also the option of fixing p and defining Ring.HasSeparableResidueFieldsAt since that's probably what's needed in practice.
There was a problem hiding this comment.
(The corresponding refactor is on my TODO list)
There was a problem hiding this comment.
@tb65536 Now that class Algebra.HasSeparableResidueFieldsAt has been added, I am thinking about how to use it in this file. The thing is to be able to use the new class, we need to have p.IsPrime and, in many results, this fact is derived from other hypothesis. Thus we will need to add this hypothesis p.IsPrime at several places to make use of the new class. Mathematically, this is not a problem, but still it will make the lemmas less easy to use. In my opinion, this is the right move, but I wanted to make sure first that you're okay with that.
There was a problem hiding this comment.
Probably ok. The other option would be to junk-ify Algebra.HasSeparableResidueFieldsAt at non-primes, but it's not immediately clear to me what the best choice would be for the junk.
There was a problem hiding this comment.
I quite agree. I'll refactor first what's already there to see what that looks like.
tb65536
added
the
awaiting-author
4 participants
Refactor of the decomposition/inertia infrastructure in Hilbert Theory to the level of rings with two new predicates
Ideal.IsDecompositionRing G P CandIdeal.IsInertiaRing G P C: for a groupGacting on a commutative ringBwith primeP, they state thatBis Galois over the ringCwith Galois group the decomposition group, resp. the inertia group of P.The old field-level classes and their whole API are deprecated in favor of the ring versions.