Zulip Chat Archive

Stream: maths

Topic: Difference between is_prime and normal


view this post on Zulip Chris Hughes (Jun 06 2020 at 10:47):

Why does this work for prime ideals, but not normal subgroups?

import group_theory.subgroup ring_theory.ideal_operations

example {R : Type} [comm_ring R] (P : ideal R) (hP : P.is_prime) : P.is_prime :=
by apply_instance --works

example {G : Type} [group G] (N : subgroup G) (hN : N.normal) : N.normal :=
by apply_instance --fails

view this post on Zulip Chris Hughes (Jun 07 2020 at 08:49):

So it seems that the difference is that is_prime is a structure (and), but normal is not. The class attribute doesn't seem to work on defs defined to start with two pis, one pi is fine for some reason. Making normal irreducible also works.

This also doesn't work, so the fact idea might be slightly flawed.

example {P Q R : Prop} [fact (P  Q  R)] : fact (P  Q  R) := by apply_instance

view this post on Zulip Kevin Buzzard (Jun 07 2020 at 08:55):

This is the main reason that 1 isn't prime

view this post on Zulip Chris Hughes (Jun 07 2020 at 08:56):

Maybe top shouldn't be normal either and then everything will be fine

view this post on Zulip Mario Carneiro (Jun 07 2020 at 09:21):

That sounds like a bug in typeclass inference

view this post on Zulip Kevin Buzzard (Jun 07 2020 at 09:26):

top isn't prime but I'm afraid it's normal

view this post on Zulip Gabriel Ebner (Jun 07 2020 at 10:31):

lean#300

view this post on Zulip Kevin Buzzard (Jun 07 2020 at 11:00):

Lean is now about five times less relaxed

view this post on Zulip Reid Barton (Jun 07 2020 at 12:52):

Oh huh, I wonder whether this would fix some of the odd errors we used to get with limits in category theory as well.

view this post on Zulip Chris Hughes (Jun 07 2020 at 13:23):

Gabriel Ebner said:

lean#300

If this is released I can fix my PR.


Last updated: May 10 2021 at 07:15 UTC