A homogeneous prime that is homogeneously prime but not prime #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In src/ring_theory/graded_algebra/radical.lean, we assumed that the underline grading is indexed by a linear_ordered_cancel_add_comm_monoid to prove that a homogeneous ideal is prime if and only if it is homogeneously prime. This file is aimed to show that even if this assumption isn't strictly necessary, the assumption of "being cancellative" is. We construct a counterexample where the underlying indexing set is a linear_ordered_add_comm_monoid but is not cancellative and the statement is false.

We achieve this by considering the ring R=ℤ/4ℤ. We first give the two element set ι = {0, 1} a structure of linear ordered additive commutative monoid by setting 0 + 0 = 0 and _ + _ = 1 and 0 < 1. Then we use ι to grade R² by setting {(a, a) | a ∈ R} to have grade 0; and {(0, b) | b ∈ R} to have grade 1. Then the ideal I = span {(0, 2)} ⊆ ℤ/4ℤ is homogeneous and not prime. But it is homogeneously prime, i.e. if (a, b), (c, d) are two homogeneous elements then (a, b) * (c, d) ∈ I implies either (a, b) ∈ I or (c, d) ∈ I.

Tags #

homogeneous, prime