irrelevant ideal cannot be generalised

Stream: mathlib4

[Kenny Lau]

3 years ago, the following text appeared in the docstring of HomogeneousIdeal.irrelevant:

Future work

Here in the definition, ι is assumed to be canonically_ordered_add_monoid. However, the notion of irrelevant ideal makes sense in a more general setting by defining it as the ideal of elements with 0 as i-th coordinate for all i ≤ 0, i.e. {a | ∀ (i : ι), i ≤ 0 → aᵢ = 0}.

But I don't think this generalisation is possible, because if x is grade 1 and y is grade -1 then x is in the irrelevant ideal but xy is not.

[Matthew Ballard]

For your example (with a couple of more variables and regraded) k[x,y,z,w] with degrees 1,1,-1,-1 it makes sense to take (x,y) or (w,z) to be “the irrelevant” ideal. The difference between the two when you pass to Proj on the nonpositive or nonnegative parts yield what is called an Atiyah flop. You can even get the common contraction using 0 as another choice of ideal.

Main point: changing the locus removed before quotienting by a group is rich in geometry and there should not be a default choice.

[Kenny Lau]

what about x^3 * z^2?

[Kenny Lau]

what you say may make sense geometrically, but the given expression in that docstring does not.

[Matthew Ballard]

I am agreeing with you. I would delete that TODO unless it scoped to something narrower than we have here. The definition, even if you force it work, is not going to be useful as an “irrelevant ideal”.

[Kenny Lau]

@Matthew Ballard #30337

[Matthew Ballard]

On second thought, let’s replace it by something better.

Generalize the definition of irrelevantIdeal to encompass at least toric irrelevant ideals.

[Kenny Lau]

do you have a formula for it?

[Matthew Ballard]

I am just suggesting new language for the # Future work paragraph not any implementation.

[Kenny Lau]

I'm saying I literally don't know what you mean by that, because I've never seen it, mainly because I haven't touched toric a lot.

[Kenny Lau]

I tried to find it online, and I came across this: is this what you mean?

image.png

[Matthew Ballard]

Ah ok. Sorry. Chapter 5 Cox Little Schenk.

[Matthew Ballard]

That image looks ok from what I can see.

[Kenny Lau]

@Matthew Ballard thanks, but I must say, what you suggested doesn't seem to be a "generalisation", because this is not a special case, because the toric definition doesn't seem to be independent of all the other background data, or in other words, you can't recover it from just the grading, because it depends on the generators.