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
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
- Counterexample.CounterexampleNotPrimeButHomogeneousPrime.submoduleZ R = { 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.