Difference between is_prime and normal

Stream: maths

[Chris Hughes]

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

[Chris Hughes]

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

[Kevin Buzzard]

This is the main reason that 1 isn't prime

[Chris Hughes]

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

[Mario Carneiro]

That sounds like a bug in typeclass inference

[Kevin Buzzard]

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

[Gabriel Ebner]

lean#300

[Kevin Buzzard]

Lean is now about five times less relaxed

[Reid Barton]

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

[Chris Hughes]

Gabriel Ebner said:

lean#300

If this is released I can fix my PR.