Zulip Chat Archive

Stream: Is there code for X?

Topic: Krull dimension, regular rings


view this post on Zulip Jon Eugster (Feb 15 2021 at 10:33):

Is there an implementation of regular (local) rings?

This would likely import ring_theory.noetherian or have some mentioning of "Krull dimension", both searches didn't lead anywhere. Krull dimension seems only been used in cases where it's 1\le 1 (e.g. dedekin domain, PID).

view this post on Zulip Johan Commelin (Feb 15 2021 at 10:55):

I don't think this is in mathlib yet. @Filippo A. E. Nuccio @Anne Baanen did you define Krull dimension in your project?

view this post on Zulip Johan Commelin (Feb 15 2021 at 10:55):

It would certainly be a natural and welcome addition to mathlib at this point

view this post on Zulip Filippo A. E. Nuccio (Feb 15 2021 at 10:56):

No, we just say what it means to have Krull dimension less or equal to one (every non-zero prime is maximal). But we don't speak about chains of ideals.

view this post on Zulip Jon Eugster (Feb 15 2021 at 11:55):

thank you!
@Johan Commelin Out of interest (to get more familiar with the mathlib structure), where would you put this? Are you generally making new files for each property a ring can have, like regular, normal, complete intersection etc. or are you bundling those as they kinda form a hierarchy of properties?

view this post on Zulip Johan Commelin (Feb 15 2021 at 11:56):

There is not a very strict rule here. Files >1000 tend to get split up. Files with <100 lines are not a problem at all.

view this post on Zulip Johan Commelin (Feb 15 2021 at 11:56):

So if it's really a new topic, I would start a new file

view this post on Zulip Johan Commelin (Feb 15 2021 at 11:56):

src/ring_theory/regular.lean looks good to me


Last updated: May 17 2021 at 16:26 UTC