Zulip Chat Archive

Stream: maths

Topic: ACC/DCC


view this post on Zulip Aaron Anderson (Aug 20 2020 at 21:05):

I'm trying to prove that being a UFD is equivalent to (irreducible iff prime) and the ascending chain condition on principal ideals, or equivalently, descending chain condition/well-foundedness of < on associates.

view this post on Zulip Aaron Anderson (Aug 20 2020 at 21:08):

I notice that there aren't any typeclasses for ACC or DCC, so I have to talk about well-foundedness of < or > or (a | b and not b | a) a lot, and these ad-hoc descriptions are getting a little messy.

view this post on Zulip Aaron Anderson (Aug 20 2020 at 21:09):

Is there a good reason not to define ACC and DCC as classes (or just predicates) for pre-/partial orders, or has it just not been done because it wasn't needed?

view this post on Zulip Johan Commelin (Aug 20 2020 at 21:18):

I don't know why they aren't there yet, but I think it makes sense to add them.

view this post on Zulip Aaron Anderson (Aug 21 2020 at 04:43):

One possible reason is that there's already a typeclass related to well-foundedness called acc

view this post on Zulip Aaron Anderson (Aug 21 2020 at 04:43):

But I think it stands for accessible, and isn't just a property of an order/relation

view this post on Zulip Aaron Anderson (Aug 21 2020 at 04:49):

it still makes it awkward to write an abbreviation called ACC...


Last updated: May 06 2021 at 17:38 UTC