feat(RingTheory/AdicCompletion): AdicCompletion of Noetherian ring is Noetherian#38331
feat(RingTheory/AdicCompletion): AdicCompletion of Noetherian ring is Noetherian#38331Thmoas-Guan wants to merge 67 commits into
Conversation
mathlib-dependent-issues
Bot
removed
the
blocked-by-other-PR
|
This PR/issue depends on:
|
Thmoas-Guan
temporarily deployed
to
cache-upload-forks
GitHub Actions
Inactive
|
|
||
| variable {R : Type u} [CommRing R] (I : Ideal R) | ||
|
|
||
| section |
There was a problem hiding this comment.
I think that this section should rather live in Mathlib.Topology.Algebra.Ring.Ideal, no?
There was a problem hiding this comment.
This is also what I am not very sure about, should I add adic completion of Noetherian ring is Noetherian here?
| · simp [degle, coeff'] | ||
| · simp [coeff', hi] | ||
|
|
||
| lemma isNoetherianRing_of_isAdicComplete_of_fg [IsNoetherianRing (R ⧸ I)] (fg : I.FG) |
There was a problem hiding this comment.
These are almost 70 lines of proof, can't you factor some results?
There was a problem hiding this comment.
I'll try, but I probably need to explain about the proof itself first: by the lemma above using associated graded, it finds series of coefficients forming Cauchy sequence to approximate the final element step by step, this is just complicated by itself, or else we might need some auxilary defs...
There was a problem hiding this comment.
OK, thanks!! You might have a look at the proof of LaurentSeries.Cauchy.limit (or friends around there) because it might give you an idea both on how to conceptualise the proof and on how to factor it.
| @@ -1,3 +1,3 @@ | |||
| /- | |||
| Copyright (c) 2024 Andrew Yang. All rights reserved. | |||
| Released under Apache 2.0 license as described in the file LICENSE. | |||
There was a problem hiding this comment.
I guess you need to add your name here.
faenuccio
left a comment
faenuccio
left a comment
There was a problem hiding this comment.
I added two more stylistic comments
faenuccio
added
the
awaiting-author
Thmoas-Guan
removed
the
awaiting-author
mathlib-dependent-issues
Bot
added
the
blocked-by-other-PR
|
Also, can I ask why you removed the |
3 participants
For
Ian ideal ofR, ifR/Iis Noetherian andIis finitely generated, the the completion ofRwrtIis Noetherian.reesAlgebra#41556