Computational-Algebra/Verifying EC group at main · DTaufer/Computational-Algebra · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
// (0:0:1)
function AL1(A,B, P1, P2)
	local x1,y1,z1,x2,y2,z2,X1,Y1,Z1;
	x1 := P1[1]; y1 := P1[2]; z1 := P1[3];
	x2 := P2[1]; y2 := P2[2]; z2 := P2[3];

	X1 := ( (x1*y2 - x2*y1)*(y1*z2 + y2*z1) + (x1*z2 - x2*z1)*y1*y2 - A*(x1*z2 + x2*z1)*(x1*z2 - x2*z1) - 3*B*(x1*z2 -x2*z1)*z1*z2 );
	Y1 := ( -3*x1*x2*(x1*y2 - x2*y1) - y1*y2*(y1*z2 - y2*z1) - A*(x1*y2 - x2*y1)*z1*z2 + A*(x1*z2 + x2*z1)*(y1*z2 - y2*z1) + 3*B*(y1*z2 - y2*z1)*z1*z2 );
	Z1 := ( 3*x1*x2*(x1*z2 - x2*z1) - (y1*z2 + y2*z1)*(y1*z2 - y2*z1) + A*(x1*z2 - x2*z1)*z1*z2 );
	return [X1,Y1,Z1];
end function;

// (0:1:0)
function AL2(A,B, P1, P2)
	local x1,y1,z1,x2,y2,z2,X2,Y2,Z2;
	x1 := P1[1]; y1 := P1[2]; z1 := P1[3];
	x2 := P2[1]; y2 := P2[2]; z2 := P2[3];

	X2 := ( y1*y2*(x1*y2 + x2*y1) - A*x1*x2*(y1*z2 + y2*z1) - A*(x1*y2 + x2*y1)*(x1*z2 + x2*z1) - 3*B*(x1*y2 + x2*y1)*z1*z2 - 3*B*(x1*z2 + x2*z1)*(y1*z2 + y2*z1) + A^2 *(y1*z2 + y2*z1)*z1*z2 );
	Y2 := ( y1^2*y2^2 + 3*A*x1^2*x2^2 + 9*B*x1*x2*(x1*z2 + x2*z1) - A^2*x1*z2*(x1*z2 + 2*x2*z1) - A^2*x2*z1*(2*x1*z2 + x2*z1) - 3*A*B*z1*z2*(x1*z2 + x2*z1)- (A^3 + 9*B^2)*z1^2*z2^2 );
	Z2 := ( 3*x1*x2*(x1*y2 + x2*y1) + y1*y2*(y1*z2 + y2*z1) + A*(x1*y2 + x2*y1)*z1*z2 + A*(x1*z2 + x2*z1)*(y1*z2 + y2*z1) + 3*B*(y1*z2 + y2*z1)*z1*z2 );
return [X2,Y2,Z2];
end function;

function ProjEqual(P1, P2, J)
	local R,M;
	R := Parent(P1[1]);
	M := Matrix(R, [P1,P2]);
	if ideal<R|Minors(M,2)> subset J then
		return true;
	else
		return false;
	end if;
end function;

S< A,B, x1,y1,z1, x2,y2,z2, x3,y3,z3 > := PolynomialRing(Integers(),11);
J := ideal< S | y1^2*z1 - x1^3 - A*x1*z1^2 - B*z1^3, y2^2*z2 - x2^3 - A*x2*z2^2 - B*z2^3, y3^2*z3 - x3^3 - A*x3*z3^2 - B*z3^3 >;

P1 := [x1,y1,z1]; P2 := [x2,y2,z2]; P3 := [x3,y3,z3];

// Projectively equivalent
S1 := AL1(A,B, P1, P2);
S2 := AL2(A,B, P1, P2);
ProjEqual(S1,S2,J);

// The addition is closed
S1[2]^2*S1[3] - S1[1]^3 - A*S1[1]*S1[3]^2 - B*S1[3]^3 in J;
S2[2]^2*S2[3] - S2[1]^3 - A*S2[1]*S2[3]^2 - B*S2[3]^3 in J;

// The addition is symmetric
S1A := AL1(A,B, P1, P2);
S1B := AL1(A,B, P2, P1);
ProjEqual(S1A,S1B,ideal<S|0>);
S2A := AL2(A,B, P1, P2);
S2B := AL2(A,B, P2, P1);
ProjEqual(S2A,S2B,ideal<S|0>);

// Associativity
S1A := AL1(A,B, AL1(A,B, P1, P2), P3);
S1B := AL1(A,B, P1, AL1(A,B, P2, P3));
ProjEqual(S1A,S1B,J);
S2A := AL2(A,B, AL1(A,B, P1, P2), P3);
S2B := AL2(A,B, P1, AL1(A,B, P2, P3));
ProjEqual(S1A,S1B,J);

// Identity
P01 := AL1(A,B, P1, [0,1,0]);
ProjEqual(P1,P01,J);
P02 := AL2(A,B, P1, [0,1,0]);
ProjEqual(P1,P02,J);

// Inverses
O1 := AL1(A,B, P1, [x1,-y1,z1]);
ProjEqual(O1,[0,1,0],J);
O2 := AL2(A,B, P1, [x1,-y1,z1]);
ProjEqual(O2,[0,1,0],J);