# A homogeneous ideal that is homogeneously prime but not prime #

In Ideal.IsHomogeneous.isPrime_of_homogeneous_mem_or_mem, we assumed that the underlying grading is indexed by a LinearOrderedCancelAddCommMonoid to prove that a homogeneous ideal is prime if and only if it is homogeneously prime. This file shows 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 LinearOrderedAddCommMonoid 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 {(2, 2)} ⊆ ℤ/4ℤ × ℤ/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

@[reducible, inline]
Equations
Instances For
Equations
• One or more equations did not get rendered due to their size.

The grade 0 part of R² is {(a, a) | a ∈ R}.

Equations
• = { carrier := {zz : R × R | zz.1 = zz.2}, add_mem' := , zero_mem' := , smul_mem' := }
Instances For

The grade 1 part of R² is {(0, b) | b ∈ R}.

Equations
Instances For

Given the above grading (see submoduleZ and submoduleO), we turn R² into a graded ring.

Equations
• One or more equations did not get rendered due to their size.
Instances For

R² ≅ {(a, a) | a ∈ R} ⨁ {(0, b) | b ∈ R} by (x, y) ↦ (x, x) + (0, y - x).

Equations
• One or more equations did not get rendered due to their size.
Instances For

The counterexample is the ideal I = span {(2, 2)}.

Equations
Instances For