Proj.openCoverOfISupEqTop

Stream: mathlib4

[Kenny Lau]

@Joël Riou @Christian Merten #30072 renamed AlgebraicGeometry.Scheme.openCoverOfISupEqTop to docs#AlgebraicGeometry.Scheme.openCoverOfIsOpenCover with deprecation but it also moved AlgebraicGeometry.Proj.openCoverOfISupEqTop to docs#AlgebraicGeometry.Proj.openCoverOfIsOpenCover perhaps by accident, and without deprecation.

Should I revert the change on Proj, or add a deprecation?

[Kenny Lau]

image.png

also this is when I realised that the declaration diff does not include namespace

[Christian Merten]

Oh this is indeed an oversight.

[Christian Merten]

But also the old name does not make sense to me.

[Kenny Lau]

hmm i always thought that they generate the unit ideal, but apparently this is not true (they only generate the irrelevant ideal)

[Christian Merten]

Maybe it should be called AlgebraicGeometry.Proj.affineOpenCoverOfLESpan

[Kenny Lau]

actually if you inspect the conditions in the statement, the generators are required to be homogeneous, so in fact the LE is an Eq, so maybe we can call it Proj.affineOpenCoverOfSpanIrrelevant...

[Kenny Lau]

idk maybe i just want irrelevant in the name, maybe what i really want is Proj.affineOpenCoverOfIrrelevantLESpan

[Christian Merten]

I would approve a PR that does this rename.

[Kenny Lau]

#30288 @Christian Merten