# Zulip Chat Archive

## Stream: maths

### Topic: Should prime ideals be a class

#### 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

#### 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?

#### 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

#### Mario Carneiro (Jun 06 2019 at 22:28):

I would prefer that these things are local instances

#### 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?

#### Mario Carneiro (Jun 06 2019 at 22:29):

yes, it's just that

#### Chris Hughes (Jun 06 2019 at 22:44):

`is_primary`

is a class

#### Mario Carneiro (Jun 06 2019 at 22:45):

but it's not in brackets in the instance

#### Reid Barton (Jun 06 2019 at 22:51):

What I would suggest:

- Leave
`is_prime`

a class - Turn all the
`instance`

s in the file you linked to into`theorem`

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

#### 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