An example


Bisecting diagonals
The diagonals of a rectangle cross each other at their midpoint.

[Maple Metafile]

Hypotheses
x_4x_1-x_3x_2, x_1x_2-x_2x_3-x_1x_4


Theses
x_1^2+x_2^2-2x_1x_3-2x_2x_4, x_1^2-x_2^2-2x_1x_3+2x_2x_4,

The theorem is not algebraically true:


Use R::= Q[x[1..4]t]


NF(1, Ideal(x[4]x[1]-x[3]x[2], x[1]x[2]-x[2]x[3]-x[1]x[4],
(x[1]^2+x[2]^2-2x[1]x[3]-2x[2]x[4])t-1))

1
-------------------------------
NF(1, Ideal(x[4]x[1]-x[3]x[2], x[1]x[2]-x[2]x[3]-x[1]x[4],
(x[1]^2-x[2]^2-2x[1]x[3]+2x[2]x[4])t-1))

1
-------------------------------

Now we search for non-degeneracy conditions:



Saturation(H, Ideal(x[1]^2+x[2]^2-2x[1]x[3]-2x[2]x[4]))

Ideal(x[3]x[4], x[1]x[4], x[2]x[3], x[1]x[2])
-------------------------------


Saturation(H, Ideal(x[1]^2-x[2]^2-2x[1]x[3]+2x[2]x[4]))

Ideal(x[3]x[4], x[1]x[4], x[2]x[3], x[1]x[2])
-------------------------------

so the theorem is true just over the components of I given by

SS:=Saturation(H,
Saturation(H, Ideal(x[1]^2-x[2]^2-2x[1]x[3]+2x[2]x[4],
x[1]^2+x[2]^2-2x[1]x[3]-2x[2]x[4])))

SS
Ideal(x[1]^2 - 2x[1]x[3], x[1]x[2] - 2x[1]x[4], x[2]^2 - 2x[2]x[4], x[2]x[3] - x[1]x[4])
-------------------------------

In fact

P1:=Ideal(x[1]-2x[3],x[2]-2x[4])

P2:=Ideal(x[2],x[4])

P3:=Ideal(x[1],x[3])

P4:=Ideal(x[1],x[2])

Intersection(P1,P4)

Ideal(x[2]x[3] - x[1]x[4], x[2]^2 - 2x[2]x[4], x[1]x[2] - 2x[1]x[4],
x[1]^2 - 2x[1]x[3])
-------------------------------