Projection of twisted cubic using Gröbner bases+Macaulay2

Stream: general

[Riyaz Ahuja]

Hi, I've been working on making a basic Macaulay2 interface for Lean, and currently have a tactic that proves questions on ideal membership using Gröbner bases. Here's an example:

image.png

And a more complex one as well:

image.png

Now, I'm trying to make a demo of this for my algebraic geometry project, and concurrently find out what additional functionality I should start integrating into the tactic beyond ideal membership. Towards this, I was planning on formalize and prove a problem we discussed in class using my tactic:

"Consider the projection of the twisted cubic curve (i.e. Veronese embedding $\nu_3 : \mathbb{P}^1 \to \mathbb{P}^3$) from the point [1:0:0:1]. Find the defining equation."

Now, this question is more than reasonable to solve using M2, but I'm firstly curious how one would even go about formalizing this in Lean (I don't have much experience in formalization of Alggeo problems...)? Is there the necessary infrastructure for this already in Mathlib, or is this all things that I would need to construct myself?

Then, is there a nice way to reduce this problem to an ideal membership problem, and if not, what kind of functionality would be needed in this lean_m2 tactic to be able to solve this kind of problem?

[Kevin Buzzard]

We can make projective n-space over a field (or even a commutative ring) but I am not sure that we have any API for writing down maps between projective spaces. However I would argue that the M2 code you link to also doesn't do this, it just writes down the homogeneous ideal corresponding to the image and we can also do this. However IIRC the statement that the quotient of a graded ring by a homogeneous ideal can also be given a grading is I think an open PR, so that's where we are now.

[Andrew Yang]

I think the algorithm you described outputs a set of generators $S$ such that $\langle S \rangle = I \cap J$ (given the generators of $I$ and $J$), but your demo only gives $\subseteq$.

[Riyaz Ahuja]

Good to know, thanks :)

I agree that the M2 example doesn't use a full projective map and for the purposes of the demo is to just use $\langle −x_1^2​+x_0​x_2, ​​−x_1​x_2​+x_0​x_3​, ​−x^2_2​+x_1​x_3​​\rangle$ to represent the twisted cubic. But in regards to an actual statement of the theorem, how would you suggest I go about representing projecting this curve from the point [1:0:0:1] (likely also represented as an ideal $\langle x_0+x_3,x_1,x_2\rangle$) in a way that let's me more or less adapt the structure of the M2 argument above to prove it?

[Riyaz Ahuja]

Andrew Yang said:

I think the algorithm you described outputs a set of generators $S$ such that $\langle S \rangle = I \cap J$ (given the generators of $I$ and $J$), but your demo only gives $\subseteq$.

What do you mean?

[Michał Mrugała]

This is a side point: do you think that with your API you could determine minimal generating sets defining Veronese and Segre surfaces? Could you prove that the generating sets usually cited in the literature are generating?

[Riyaz Ahuja]

With the current tactic

Michał Mrugała said:

This is a side point: do you think that with your API you could determine minimal generating sets defining Veronese and Segre surfaces? Could you prove that the generating sets usually cited in the literature are generating?

With the current tactic, I don't think its possible yet (tactic only is able to do ideal membership over "nice" polynomial rings), but I think as I extend the functionality to be able to handle more of M2's, it should be more than possible. I don't have that deep of alggeo experience yet to fully know yet though, so take that with a grain of salt.