Book Description
An n-ary Steiner law f(x[sub 1], x[sub 2], [hor-ellipsis], x[sub n]) on a projective curve[Gamma] over an algebraically closed field k is a totally symmetric n-ary morphism f from[Gamma][sup n] to[Gamma] satisfying the universal identity f(x[sub 1], x[sub 2], [hor-ellipsis], x[sub n-1], f(x[sub 1], x[sub 2], [hor-ellipsis], x[sub n]))= x[sub n]. An element e in[Gamma] is called an idempotent for f if f(e, e, [hor-ellipsis], e)= e. The binary morphism x* y of the classical chord-tangent construction on a nonsingular cubic curve is an example of a binary Steiner law on the curve, and the idempotents of* are precisely the inflection points of the curve. In this paper, the authors prove that if f and g are two 5-ary Steiner laws on an elliptic curve[Gamma] sharing a common idempotent, then f= g. They use a new rule of inference rule=(gL)[implies], extracted from a powerful local-to-global principal in algebraic geometry. This rule is implemented in the theorem-proving program OTTER. Then they use OTTER to automatically prove the uniqueness of the 5-ary Steiner law on an elliptic curve. Very much like the binary case, this theorem provides an algebraic characterization of a geometric construction process involving conics and cubics. The well-known theorem of the uniqueness of the group law on such a curve is shown to be a consequence of this result.