Zulip Chat Archive

Stream: maths

Topic: Should prime ideals be a class


view this post on Zulip Chris Hughes (Jun 06 2019 at 22:13):

Currently is_prime is a class on ideals. This is so that the instance that says that quotienting by a prime ideal is an integral domain can be an instance. However we could do this differently, either by bundling prime ideals, or by making a quotient_ring function whose type is something like Π {α : Type*} (I : ideal α) (h : is_prime I), Type*. Would either of these be better? Stuff like this might be overusing type class inference a little I think https://github.com/leanprover-community/mathlib/pull/768/files#diff-210de6c3e5a3b7cf7ed5f3fe5352c9a7R547

view this post on Zulip Reid Barton (Jun 06 2019 at 22:26):

Using classes for theorem-type stuff is awkward in my experience.
What about leaving it a class, but just not writing any instances?

view this post on Zulip Mario Carneiro (Jun 06 2019 at 22:26):

I don't think that example can actually work, since is_primary is not a typeclass arg

view this post on Zulip Mario Carneiro (Jun 06 2019 at 22:28):

I would prefer that these things are local instances

view this post on Zulip Reid Barton (Jun 06 2019 at 22:29):

Is there a simple rule about that? Arguments of an instance to the left of a colon must be either inferrable from the result type or [] arguments?

view this post on Zulip Mario Carneiro (Jun 06 2019 at 22:29):

yes, it's just that

view this post on Zulip Chris Hughes (Jun 06 2019 at 22:44):

is_primary is a class

view this post on Zulip Mario Carneiro (Jun 06 2019 at 22:45):

but it's not in brackets in the instance

view this post on Zulip Reid Barton (Jun 06 2019 at 22:51):

What I would suggest:

  • Leave is_prime a class
  • Turn all the instances in the file you linked to into theorems
  • Leave instance (I : ideal α) [hI : I.is_prime] : integral_domain I.quotient unchanged
  • Expect the user to use letI or local attribute [instance] to connect the theorems about is_prime to integral_domain I.quotient as necessary

view this post on Zulip Reid Barton (Jun 06 2019 at 22:51):

and often it won't be necessary, e.g., if we just have an I.is_prime hypothesis floating around (to the "left of the colon")

view this post on Zulip Johan Commelin (Jun 07 2019 at 04:27):

@Chris Hughes Of course you can bundle prime ideals... it's a very good idea (-; Call the type of bundled prime ideals Spec R. :wink:


Last updated: May 14 2021 at 19:21 UTC