Should prime ideals be a class

Stream: maths

[Chris Hughes]

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

[Reid Barton]

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

[Mario Carneiro]

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

[Mario Carneiro]

I would prefer that these things are local instances

[Reid Barton]

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?

[Mario Carneiro]

yes, it's just that

[Chris Hughes]

is_primary is a class

[Mario Carneiro]

but it's not in brackets in the instance

[Reid Barton]

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

[Reid Barton]

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")

[Johan Commelin]

@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: