/*

Check the formula for P_3 (4th coord of product of Witt vectors)

*/

load 'witt_gen.m';
load 'sec_coord.m';

p:=17;

PR<x0,x1,x2,x3,y0,y1,y2,y3>:=PolynomialRing(GF(p),8);

P3a:=PR!WittProdPol(3,p)[4]; // using witt_gen.m

// using the formula!
P3b:=x0^(p^3)*y3 + x1^(p^2)*y2^p + x2^p*y1^(p^2) + x3*y0^(p^3) +
     fSpcFct(x0^(p^2)*y2,x2*y0^(p^2)) + 
     fSpcFct(x0^(p^2)*y2 + x2*y0^(p^2),fSpcFct(x0^p*y1,x1*y0^p)) +
     fSpcFct(x0^(p^2)*y2 + x2*y0^(p^2) + fSpcFct(x0^p*y1,x1*y0^p),x1^p*y1^p) +
     fSpc4Fct(x0^p*y1,x1*y0^p);

P3a eq P3b;


// CHECKED!!! (for 5<=p<=17)


/*

Now try to have some idea of GT...

*/

load 'witt_gen.m';
load 'sec_coord.m';

p:=3;

F<a0,a1,a2,a3>:=RationalFunctionField(GF(p),4);

n:=5;
m:=4;

PR<x0,x1,x2,x3,y0,y1,y2,y3>:=PolynomialRing(F,8);

a:=[a0,a1,a2,a3];
x:=[x0,x1,x2,x3];
y:=[y0,y1,y2,y3];


vecP:=WittProdPol(3,p);

mon:=WittProd(WittPwr(x,n : vecP:=vecP),WittPwr(y,m : vecP:=vecP) : vecP:=vecP);
mon:=WittProd(a,mon : vecP:=vecP);

