## "\Teichmuller curves in genus three and \\ just likely intersections in $\IG_m^n\times\IG_a^n$." ## by Matt Bainbridge, Philipp Habegger, Martin M\"oller ## ## File: g3fin_ch6.sage ## ## Description: Sage code to verify various computational claims in Section 6 of ## the paper. Any failure leads to an assertion fault. ## ## Usage: run "sage g3fin.sage" ## Works successfully with sage 5.8, 5.10, 6.0, 6.2 ## ## Comments: Running "time sage g3fin.sage" succeeds and returns ## real 3m27.851s ## user 3m27.687s ## sys 0m0.363s ## on a Lenovo X1 Carbon notebook (sage 5.10) with an i7-3667U 2Ghz CPU ## (turbo at 3.17Ghz) and ## real 2m46.940s ## user 2m27.923s ## sys 0m1.539s ## on a Dell desktop (sage 5.8) with an i7-4770 3.4Ghz CPU ## ## Lemmas covered by this script start_time = walltime() str_lem_cYgeomirred = "6.6 (label lem:cYgeomirred)" str_lem_SoODD = "6.8 (label lem:soODD)" str_lem_irred = "6.11 (label lem:irred)" str_lem_cong1 = "6.12 (label lem:cong1)" str_lem_cong2 = "6.13 (label lem:cong2)" str_lem_projirred = "6.14 (label lem:projirred)" str_lem_3264 = "6.16 (label lem:3264)" B4. = PolynomialRing(QQ) P1 = (y1-x2)*(y1-y2)*(y1^2-1) - (x1-x2)*(x1-y2)*(x1^2-1) P2 = (y2-x1)*(y2-y1)*(y2^2-1) - (x2-x1)*(x2-y1)*(x2^2-1) B. = PolynomialRing(QQ) sigma1 = B.hom([x2, y2, x1, y1, c2, c1]) sigma2 = B.hom([y1, x1, y2, x2, -c1, -c2]) f1 = x1*x2+y1*x2-x2^2+x1*y2+y1*y2-y2^2+2 f2 = x1^2+y1^2-x2^2-y2^2 f = 2*c1*(x2 - y2) + 2*c2*(x1 - y1) + (x1 - y1)*(x2 - y2) ## Hardcoded polynomial to be used further down fx1y1 = x1^6 + 2*x1^5*y1 - 5*x1^4*y1^2 + 4*x1^3*y1^3 - 5*x1^2*y1^4 + 2*x1*y1^5 + y1^6 + 4*x1^5*c1 + 12*x1^4*y1*c1 - 8*x1^3*y1^2*c1 + 8*x1^2*y1^3*c1 - 12*x1*y1^4*c1 - 4*y1^5*c1 + 4*x1^4*c1^2 + 16*x1^3*y1*c1^2 + 8*x1^2*y1^2*c1^2 + 16*x1*y1^3*c1^2 + 4*y1^4*c1^2 - 4*x1^4*c2^2 + 8*x1^2*y1^2*c2^2 - 4*y1^4*c2^2 + 4*x1^4 - 8*x1^3*y1 + 8*x1^2*y1^2 - 8*x1*y1^3 + 4*y1^4 + 16*x1^3*c1 - 16*x1^2*y1*c1 + 16*x1*y1^2*c1 - 16*y1^3*c1 + 16*x1^2*c1^2 + 16*y1^2*c1^2 - 4*x1^2 + 8*x1*y1 - 4*y1^2 - 16*x1*c1 + 16*y1*c1 - 16*c1^2 ## Hardcoded polynomial to be used further down fx1y2 = -2*x1^6*y2^2 - 2*x1^5*y2^3 + 9*x1^4*y2^4 - 2*x1^3*y2^5 - 2*x1^2*y2^6 - 8*x1^5*y2^2*c1 - 4*x1^4*y2^3*c1 + 24*x1^3*y2^4*c1 - 2*x1^2*y2^5*c1 - 4*x1*y2^6*c1 - 12*x1^4*y2^2*c1^2 - 4*x1^3*y2^3*c1^2 + 26*x1^2*y2^4*c1^2 + 4*x1*y2^5*c1^2 - 2*y2^6*c1^2 - 8*x1^3*y2^2*c1^3 + 12*x1*y2^4*c1^3 + 4*y2^5*c1^3 + 4*x1^6*y2*c2 + 2*x1^5*y2^2*c2 - 24*x1^4*y2^3*c2 + 4*x1^3*y2^4*c2 + 8*x1^2*y2^5*c2 + 12*x1^5*y2*c1*c2 - 48*x1^3*y2^3*c1*c2 + 12*x1*y2^5*c1*c2 + 8*x1^4*y2*c1^2*c2 - 8*x1^3*y2^2*c1^2*c2 - 24*x1^2*y2^3*c1^2*c2 - 4*x1*y2^4*c1^2*c2 + 4*y2^5*c1^2*c2 - 2*x1^6*c2^2 + 4*x1^5*y2*c2^2 + 26*x1^4*y2^2*c2^2 - 4*x1^3*y2^3*c2^2 - 12*x1^2*y2^4*c2^2 - 4*x1^5*c1*c2^2 + 4*x1^4*y2*c1*c2^2 + 24*x1^3*y2^2*c1*c2^2 + 8*x1^2*y2^3*c1*c2^2 - 8*x1*y2^4*c1*c2^2 - 4*x1^5*c2^3 - 12*x1^4*y2*c2^3 + 8*x1^2*y2^3*c2^3 - 2*x1^5*y2 - 6*x1^4*y2^2 + 16*x1^3*y2^3 - 6*x1^2*y2^4 - 2*x1*y2^5 - 8*x1^4*y2*c1 - 12*x1^3*y2^2*c1 + 32*x1^2*y2^3*c1 - 8*x1*y2^4*c1 - 2*y2^5*c1 - 12*x1^3*y2*c1^2 - 12*x1^2*y2^2*c1^2 + 28*x1*y2^3*c1^2 - 8*x1^2*y2*c1^3 + 8*y2^3*c1^3 + 2*x1^5*c2 + 8*x1^4*y2*c2 - 32*x1^3*y2^2*c2 + 12*x1^2*y2^3*c2 + 8*x1*y2^4*c2 + 8*x1^4*c1*c2 + 8*x1^3*y2*c1*c2 - 56*x1^2*y2^2*c1*c2 + 8*x1*y2^3*c1*c2 + 8*y2^4*c1*c2 + 8*x1^3*c1^2*c2 - 8*x1^2*y2*c1^2*c2 - 24*x1*y2^2*c1^2*c2 - 8*y2^3*c1^2*c2 + 28*x1^3*y2*c2^2 - 12*x1^2*y2^2*c2^2 - 12*x1*y2^3*c2^2 + 8*x1^3*c1*c2^2 + 24*x1^2*y2*c1*c2^2 + 8*x1*y2^2*c1*c2^2 - 8*y2^3*c1*c2^2 - 8*x1^3*c2^3 + 8*x1*y2^2*c2^3 - x1^4 - 6*x1^3*y2 + 12*x1^2*y2^2 - 6*x1*y2^3 - y2^4 - 4*x1^3*c1 - 14*x1^2*y2*c1 + 16*x1*y2^2*c1 - 4*y2^3*c1 - 6*x1^2*c1^2 - 16*x1*y2*c1^2 + 10*y2^2*c1^2 - 4*x1*c1^3 - 4*y2*c1^3 + 4*x1^3*c2 - 16*x1^2*y2*c2 + 14*x1*y2^2*c2 + 4*y2^3*c2 + 8*x1^2*c1*c2 - 24*x1*y2*c1*c2 + 8*y2^2*c1*c2 - 4*x1*c1^2*c2 - 4*y2*c1^2*c2 + 10*x1^2*c2^2 - 16*x1*y2*c2^2 - 6*y2^2*c2^2 + 4*x1*c1*c2^2 + 4*y2*c1*c2^2 + 4*x1*c2^3 + 4*y2*c2^3 - 2*x1^2 + 4*x1*y2 - 2*y2^2 - 4*x1*c1 + 2*y2*c1 - 4*c1^2 - 2*x1*c2 + 4*y2*c2 - 8*c1*c2 - 4*c2^2 + 1 ## Hardcoded polynomial to be used further down fx1x2 = -2*x1^6*x2^2 - 2*x1^5*x2^3 + 9*x1^4*x2^4 - 2*x1^3*x2^5 - 2*x1^2*x2^6 - 8*x1^5*x2^2*c1 - 4*x1^4*x2^3*c1 + 24*x1^3*x2^4*c1 - 2*x1^2*x2^5*c1 - 4*x1*x2^6*c1 - 12*x1^4*x2^2*c1^2 - 4*x1^3*x2^3*c1^2 + 26*x1^2*x2^4*c1^2 + 4*x1*x2^5*c1^2 - 2*x2^6*c1^2 - 8*x1^3*x2^2*c1^3 + 12*x1*x2^4*c1^3 + 4*x2^5*c1^3 - 4*x1^6*x2*c2 - 2*x1^5*x2^2*c2 + 24*x1^4*x2^3*c2 - 4*x1^3*x2^4*c2 - 8*x1^2*x2^5*c2 - 12*x1^5*x2*c1*c2 + 48*x1^3*x2^3*c1*c2 - 12*x1*x2^5*c1*c2 - 8*x1^4*x2*c1^2*c2 + 8*x1^3*x2^2*c1^2*c2 + 24*x1^2*x2^3*c1^2*c2 + 4*x1*x2^4*c1^2*c2 - 4*x2^5*c1^2*c2 - 2*x1^6*c2^2 + 4*x1^5*x2*c2^2 + 26*x1^4*x2^2*c2^2 - 4*x1^3*x2^3*c2^2 - 12*x1^2*x2^4*c2^2 - 4*x1^5*c1*c2^2 + 4*x1^4*x2*c1*c2^2 + 24*x1^3*x2^2*c1*c2^2 + 8*x1^2*x2^3*c1*c2^2 - 8*x1*x2^4*c1*c2^2 + 4*x1^5*c2^3 + 12*x1^4*x2*c2^3 - 8*x1^2*x2^3*c2^3 - 2*x1^5*x2 - 6*x1^4*x2^2 + 16*x1^3*x2^3 - 6*x1^2*x2^4 - 2*x1*x2^5 - 8*x1^4*x2*c1 - 12*x1^3*x2^2*c1 + 32*x1^2*x2^3*c1 - 8*x1*x2^4*c1 - 2*x2^5*c1 - 12*x1^3*x2*c1^2 - 12*x1^2*x2^2*c1^2 + 28*x1*x2^3*c1^2 - 8*x1^2*x2*c1^3 + 8*x2^3*c1^3 - 2*x1^5*c2 - 8*x1^4*x2*c2 + 32*x1^3*x2^2*c2 - 12*x1^2*x2^3*c2 - 8*x1*x2^4*c2 - 8*x1^4*c1*c2 - 8*x1^3*x2*c1*c2 + 56*x1^2*x2^2*c1*c2 - 8*x1*x2^3*c1*c2 - 8*x2^4*c1*c2 - 8*x1^3*c1^2*c2 + 8*x1^2*x2*c1^2*c2 + 24*x1*x2^2*c1^2*c2 + 8*x2^3*c1^2*c2 + 28*x1^3*x2*c2^2 - 12*x1^2*x2^2*c2^2 - 12*x1*x2^3*c2^2 + 8*x1^3*c1*c2^2 + 24*x1^2*x2*c1*c2^2 + 8*x1*x2^2*c1*c2^2 - 8*x2^3*c1*c2^2 + 8*x1^3*c2^3 - 8*x1*x2^2*c2^3 - x1^4 - 6*x1^3*x2 + 12*x1^2*x2^2 - 6*x1*x2^3 - x2^4 - 4*x1^3*c1 - 14*x1^2*x2*c1 + 16*x1*x2^2*c1 - 4*x2^3*c1 - 6*x1^2*c1^2 - 16*x1*x2*c1^2 + 10*x2^2*c1^2 - 4*x1*c1^3 - 4*x2*c1^3 - 4*x1^3*c2 + 16*x1^2*x2*c2 - 14*x1*x2^2*c2 - 4*x2^3*c2 - 8*x1^2*c1*c2 + 24*x1*x2*c1*c2 - 8*x2^2*c1*c2 + 4*x1*c1^2*c2 + 4*x2*c1^2*c2 + 10*x1^2*c2^2 - 16*x1*x2*c2^2 - 6*x2^2*c2^2 + 4*x1*c1*c2^2 + 4*x2*c1*c2^2 - 4*x1*c2^3 - 4*x2*c2^3 - 2*x1^2 + 4*x1*x2 - 2*x2^2 - 4*x1*c1 + 2*x2*c1 - 4*c1^2 + 2*x1*c2 - 4*x2*c2 + 8*c1*c2 - 4*c2^2 + 1 Bt. = PolynomialRing(QQ) ## Hardcoded polynomial to be used further down fx2t = x2^6*c1^2*t^6 - 2*x2^5*c1^3*t^6 + 2*x2^5*c1^2*c2*t^6 + 4*x2^6*c1^2*t^5 - 8*x2^5*c1^3*t^5 - 4*x2^4*c1^4*t^5 + 8*x2^5*c1^2*c2*t^5 + 4*x2^4*c1^2*c2^2*t^5 - 2*x2^6*c1*t^6 + 2*x2^5*c1^2*t^6 + 6*x2^4*c1^3*t^6 - 6*x2^5*c1*c2*t^6 + 2*x2^4*c1^2*c2*t^6 - 4*x2^4*c1*c2^2*t^6 - x2^6*c1^2*t^4 - 2*x2^5*c1^3*t^4 - 16*x2^4*c1^4*t^4 - 2*x2^5*c1^2*c2*t^4 - 4*x2^6*c1*t^5 + 16*x2^5*c1^2*t^5 + 4*x2^4*c1^3*t^5 + 8*x2^3*c1^4*t^5 - 12*x2^5*c1*c2*t^5 + 20*x2^4*c1^2*c2*t^5 + 16*x2^3*c1^3*c2*t^5 - 16*x2^4*c1*c2^2*t^5 - 8*x2^3*c1*c2^3*t^5 + x2^6*t^6 + 2*x2^5*c1*t^6 - 13*x2^4*c1^2*t^6 - 4*x2^3*c1^3*t^6 + 4*x2^5*c2*t^6 + 4*x2^4*c1*c2*t^6 - 16*x2^3*c1^2*c2*t^6 + 6*x2^4*c2^2*t^6 + 4*x2^3*c2^3*t^6 - 8*x2^6*c1^2*t^3 - 8*x2^4*c1^4*t^3 - 16*x2^5*c1^2*c2*t^3 - 8*x2^4*c1^2*c2^2*t^3 + 14*x2^6*c1*t^4 - 10*x2^5*c1^2*t^4 + 22*x2^4*c1^3*t^4 - 16*x2^3*c1^4*t^4 + 42*x2^5*c1*c2*t^4 - 2*x2^4*c1^2*c2*t^4 + 16*x2^3*c1^3*c2*t^4 + 44*x2^4*c1*c2^2*t^4 + 16*x2^3*c1^2*c2^2*t^4 + 16*x2^3*c1*c2^3*t^4 - 20*x2^5*c1*t^5 + 12*x2^4*c1^2*t^5 - 8*x2^3*c1^3*t^5 - 40*x2^4*c1*c2*t^5 - 24*x2^3*c1^2*c2*t^5 - 24*x2^2*c1^3*c2*t^5 + 4*x2^4*c2^2*t^5 - 16*x2^3*c1*c2^2*t^5 - 32*x2^2*c1^2*c2^2*t^5 + 8*x2^3*c2^3*t^5 + 8*x2^2*c2^4*t^5 - 2*x2^5*t^6 + 8*x2^4*c1*t^6 + 12*x2^3*c1^2*t^6 - 4*x2^2*c1^3*t^6 - 6*x2^4*c2*t^6 + 20*x2^3*c1*c2*t^6 + 16*x2^2*c1^2*c2*t^6 - 8*x2^3*c2^2*t^6 + 16*x2^2*c1*c2^2*t^6 - 4*x2^2*c2^3*t^6 - x2^6*c1^2*t^2 + 2*x2^5*c1^3*t^2 - 16*x2^4*c1^4*t^2 - 2*x2^5*c1^2*c2*t^2 - 16*x2^5*c1^2*t^3 + 16*x2^3*c1^4*t^3 - 40*x2^4*c1^2*c2*t^3 - 32*x2^3*c1^2*c2^2*t^3 - 9*x2^6*t^4 + 34*x2^5*c1*t^4 - 11*x2^4*c1^2*t^4 + 12*x2^3*c1^3*t^4 - 16*x2^2*c1^4*t^4 - 36*x2^5*c2*t^4 + 68*x2^4*c1*c2*t^4 + 48*x2^3*c1^2*c2*t^4 + 16*x2^2*c1^3*c2*t^4 - 70*x2^4*c2^2*t^4 + 32*x2^3*c1*c2^2*t^4 + 48*x2^2*c1^2*c2^2*t^4 - 68*x2^3*c2^3*t^4 - 32*x2^2*c2^4*t^4 + 12*x2^5*t^5 - 16*x2^4*c1*t^5 - 16*x2^3*c1^2*t^5 + 16*x2^2*c1^3*t^5 - 8*x2*c1^4*t^5 + 36*x2^4*c2*t^5 - 16*x2^3*c1*c2*t^5 - 16*x2^2*c1^2*c2*t^5 + 48*x2^3*c2^2*t^5 + 16*x2^2*c1*c2^2*t^5 + 32*x2*c1^2*c2^2*t^5 + 24*x2^2*c2^3*t^5 + 24*x2*c1*c2^3*t^5 - x2^4*t^6 - 12*x2^3*c1*t^6 + 7*x2^2*c1^2*t^6 + 6*x2*c1^3*t^6 - 4*x2^3*c2*t^6 - 24*x2^2*c1*c2*t^6 - 2*x2*c1^2*c2*t^6 - 4*x2^2*c2^2*t^6 - 16*x2*c1*c2^2*t^6 - 4*x2*c2^3*t^6 + 4*x2^6*c1^2*t + 8*x2^5*c1^3*t - 4*x2^4*c1^4*t + 8*x2^5*c1^2*c2*t + 4*x2^4*c1^2*c2^2*t - 14*x2^6*c1*t^2 - 10*x2^5*c1^2*t^2 - 22*x2^4*c1^3*t^2 - 16*x2^3*c1^4*t^2 - 42*x2^5*c1*c2*t^2 - 2*x2^4*c1^2*c2*t^2 - 16*x2^3*c1^3*c2*t^2 - 44*x2^4*c1*c2^2*t^2 + 16*x2^3*c1^2*c2^2*t^2 - 16*x2^3*c1*c2^3*t^2 + 16*x2^6*t^3 + 24*x2^4*c1^2*t^3 + 64*x2^5*c2*t^3 - 16*x2^3*c1^2*c2*t^3 + 120*x2^4*c2^2*t^3 - 32*x2^2*c1^2*c2^2*t^3 + 112*x2^3*c2^3*t^3 + 48*x2^2*c2^4*t^3 - 30*x2^5*t^4 + 8*x2^4*c1*t^4 + 4*x2^3*c1^2*t^4 + 12*x2^2*c1^3*t^4 + 16*x2*c1^4*t^4 - 90*x2^4*c2*t^4 - 28*x2^3*c1*c2*t^4 + 16*x2^2*c1^2*c2*t^4 + 16*x2*c1^3*c2*t^4 - 120*x2^3*c2^2*t^4 - 80*x2^2*c1*c2^2*t^4 - 48*x2*c1^2*c2^2*t^4 - 60*x2^2*c2^3*t^4 - 48*x2*c1*c2^3*t^4 + 4*x2^4*t^5 + 40*x2^3*c1*t^5 - 44*x2^2*c1^2*t^5 + 4*c1^4*t^5 + 8*x2^3*c2*t^5 + 80*x2^2*c1*c2*t^5 + 16*x2*c1^2*c2*t^5 + 8*c1^3*c2*t^5 - 8*x2^2*c2^2*t^5 + 32*x2*c1*c2^2*t^5 - 4*c1^2*c2^2*t^5 - 8*x2*c2^3*t^5 - 16*c1*c2^3*t^5 - 8*c2^4*t^5 + 4*x2^3*t^6 - 2*x2^2*c1*t^6 - 14*x2*c1^2*t^6 - 2*c1^3*t^6 + 8*x2^2*c2*t^6 + 2*x2*c1*c2*t^6 - 2*c1^2*c2*t^6 + 8*x2*c2^2*t^6 + 4*c1*c2^2*t^6 + 4*c2^3*t^6 + x2^6*c1^2 + 2*x2^5*c1^3 + 2*x2^5*c1^2*c2 + 4*x2^6*c1*t + 16*x2^5*c1^2*t - 4*x2^4*c1^3*t + 8*x2^3*c1^4*t + 12*x2^5*c1*c2*t + 20*x2^4*c1^2*c2*t - 16*x2^3*c1^3*c2*t + 16*x2^4*c1*c2^2*t + 8*x2^3*c1*c2^3*t - 9*x2^6*t^2 - 34*x2^5*c1*t^2 - 11*x2^4*c1^2*t^2 - 12*x2^3*c1^3*t^2 - 16*x2^2*c1^4*t^2 - 36*x2^5*c2*t^2 - 68*x2^4*c1*c2*t^2 + 48*x2^3*c1^2*c2*t^2 - 16*x2^2*c1^3*c2*t^2 - 70*x2^4*c2^2*t^2 - 32*x2^3*c1*c2^2*t^2 + 48*x2^2*c1^2*c2^2*t^2 - 68*x2^3*c2^3*t^2 - 32*x2^2*c2^4*t^2 + 40*x2^5*t^3 - 16*x2*c1^4*t^3 + 120*x2^4*c2*t^3 - 32*x2^2*c1^2*c2*t^3 + 160*x2^3*c2^2*t^3 + 32*x2*c1^2*c2^2*t^3 + 80*x2^2*c2^3*t^3 - 7*x2^4*t^4 - 44*x2^3*c1*t^4 + 41*x2^2*c1^2*t^4 - 10*x2*c1^3*t^4 + 4*x2^3*c2*t^4 - 88*x2^2*c1*c2*t^4 - 94*x2*c1^2*c2*t^4 - 16*c1^3*c2*t^4 + 68*x2^2*c2^2*t^4 - 16*x2*c1*c2^2*t^4 - 16*c1^2*c2^2*t^4 + 68*x2*c2^3*t^4 + 32*c1*c2^3*t^4 + 32*c2^4*t^4 - 24*x2^3*t^5 + 28*x2^2*c1*t^5 + 32*x2*c1^2*t^5 - 4*c1^3*t^5 - 48*x2^2*c2*t^5 + 12*x2*c1*c2*t^5 - 4*c1^2*c2*t^5 - 48*x2*c2^2*t^5 - 16*c1*c2^2*t^5 - 24*c2^3*t^5 - x2^2*t^6 + 10*x2*c1*t^6 + 5*c1^2*t^6 + 4*c1*c2*t^6 - 2*c2^2*t^6 + 2*x2^6*c1 + 2*x2^5*c1^2 - 6*x2^4*c1^3 + 6*x2^5*c1*c2 + 2*x2^4*c1^2*c2 + 4*x2^4*c1*c2^2 + 20*x2^5*c1*t + 12*x2^4*c1^2*t + 8*x2^3*c1^3*t + 40*x2^4*c1*c2*t - 24*x2^3*c1^2*c2*t + 24*x2^2*c1^3*c2*t + 4*x2^4*c2^2*t + 16*x2^3*c1*c2^2*t - 32*x2^2*c1^2*c2^2*t + 8*x2^3*c2^3*t + 8*x2^2*c2^4*t - 30*x2^5*t^2 - 8*x2^4*c1*t^2 + 4*x2^3*c1^2*t^2 - 12*x2^2*c1^3*t^2 + 16*x2*c1^4*t^2 - 90*x2^4*c2*t^2 + 28*x2^3*c1*c2*t^2 + 16*x2^2*c1^2*c2*t^2 - 16*x2*c1^3*c2*t^2 - 120*x2^3*c2^2*t^2 + 80*x2^2*c1*c2^2*t^2 - 48*x2*c1^2*c2^2*t^2 - 60*x2^2*c2^3*t^2 + 48*x2*c1*c2^3*t^2 + 8*x2^4*t^3 - 8*x2^2*c1^2*t^3 + 8*c1^4*t^3 - 16*x2^3*c2*t^3 + 160*x2*c1^2*c2*t^3 - 112*x2^2*c2^2*t^3 + 40*c1^2*c2^2*t^3 - 112*x2*c2^3*t^3 - 48*c2^4*t^3 + 60*x2^3*t^4 - 50*x2^2*c1*t^4 - 26*x2*c1^2*t^4 - 2*c1^3*t^4 + 120*x2^2*c2*t^4 - 30*x2*c1*c2*t^4 + 34*c1^2*c2*t^4 + 120*x2*c2^2*t^4 + 20*c1*c2^2*t^4 + 60*c2^3*t^4 - 36*x2*c1*t^5 - 4*c1^2*t^5 - 8*x2*c2*t^5 - 24*c1*c2*t^5 + 4*c2^2*t^5 - 2*x2*t^6 - 4*c1*t^6 - 2*c2*t^6 + x2^6 - 2*x2^5*c1 - 13*x2^4*c1^2 + 4*x2^3*c1^3 + 4*x2^5*c2 - 4*x2^4*c1*c2 - 16*x2^3*c1^2*c2 + 6*x2^4*c2^2 + 4*x2^3*c2^3 + 12*x2^5*t + 16*x2^4*c1*t - 16*x2^3*c1^2*t - 16*x2^2*c1^3*t - 8*x2*c1^4*t + 36*x2^4*c2*t + 16*x2^3*c1*c2*t - 16*x2^2*c1^2*c2*t + 48*x2^3*c2^2*t - 16*x2^2*c1*c2^2*t + 32*x2*c1^2*c2^2*t + 24*x2^2*c2^3*t - 24*x2*c1*c2^3*t - 7*x2^4*t^2 + 44*x2^3*c1*t^2 + 41*x2^2*c1^2*t^2 + 10*x2*c1^3*t^2 + 4*x2^3*c2*t^2 + 88*x2^2*c1*c2*t^2 - 94*x2*c1^2*c2*t^2 + 16*c1^3*c2*t^2 + 68*x2^2*c2^2*t^2 + 16*x2*c1*c2^2*t^2 - 16*c1^2*c2^2*t^2 + 68*x2*c2^3*t^2 - 32*c1*c2^3*t^2 + 32*c2^4*t^2 - 80*x2^3*t^3 + 16*x2*c1^2*t^3 - 160*x2^2*c2*t^3 - 56*c1^2*c2*t^3 - 160*x2*c2^2*t^3 - 80*c2^3*t^3 + 9*x2^2*t^4 + 42*x2*c1*t^4 + 3*c1^2*t^4 + 32*x2*c2*t^4 + 36*c1*c2*t^4 + 2*c2^2*t^4 + 12*x2*t^5 + 8*c1*t^5 + 12*c2*t^5 + t^6 - 2*x2^5 - 8*x2^4*c1 + 12*x2^3*c1^2 + 4*x2^2*c1^3 - 6*x2^4*c2 - 20*x2^3*c1*c2 + 16*x2^2*c1^2*c2 - 8*x2^3*c2^2 - 16*x2^2*c1*c2^2 - 4*x2^2*c2^3 + 4*x2^4*t - 40*x2^3*c1*t - 44*x2^2*c1^2*t + 4*c1^4*t + 8*x2^3*c2*t - 80*x2^2*c1*c2*t + 16*x2*c1^2*c2*t - 8*c1^3*c2*t - 8*x2^2*c2^2*t - 32*x2*c1*c2^2*t - 4*c1^2*c2^2*t - 8*x2*c2^3*t + 16*c1*c2^3*t - 8*c2^4*t + 60*x2^3*t^2 + 50*x2^2*c1*t^2 - 26*x2*c1^2*t^2 + 2*c1^3*t^2 + 120*x2^2*c2*t^2 + 30*x2*c1*c2*t^2 + 34*c1^2*c2*t^2 + 120*x2*c2^2*t^2 - 20*c1*c2^2*t^2 + 60*c2^3*t^2 - 16*x2^2*t^3 - 8*c1^2*t^3 - 48*x2*c2*t^3 - 8*c2^2*t^3 - 30*x2*t^4 - 4*c1*t^4 - 30*c2*t^4 - 4*t^5 - x2^4 + 12*x2^3*c1 + 7*x2^2*c1^2 - 6*x2*c1^3 - 4*x2^3*c2 + 24*x2^2*c1*c2 - 2*x2*c1^2*c2 - 4*x2^2*c2^2 + 16*x2*c1*c2^2 - 4*x2*c2^3 - 24*x2^3*t - 28*x2^2*c1*t + 32*x2*c1^2*t + 4*c1^3*t - 48*x2^2*c2*t - 12*x2*c1*c2*t - 4*c1^2*c2*t - 48*x2*c2^2*t + 16*c1*c2^2*t - 24*c2^3*t + 9*x2^2*t^2 - 42*x2*c1*t^2 + 3*c1^2*t^2 + 32*x2*c2*t^2 - 36*c1*c2*t^2 + 2*c2^2*t^2 + 40*x2*t^3 + 40*c2*t^3 + 7*t^4 + 4*x2^3 + 2*x2^2*c1 - 14*x2*c1^2 + 2*c1^3 + 8*x2^2*c2 - 2*x2*c1*c2 - 2*c1^2*c2 + 8*x2*c2^2 - 4*c1*c2^2 + 4*c2^3 + 36*x2*c1*t - 4*c1^2*t - 8*x2*c2*t + 24*c1*c2*t + 4*c2^2*t - 30*x2*t^2 + 4*c1*t^2 - 30*c2*t^2 - 8*t^3 - x2^2 - 10*x2*c1 + 5*c1^2 - 4*c1*c2 - 2*c2^2 + 12*x2*t - 8*c1*t + 12*c2*t + 7*t^2 - 2*x2 + 4*c1 - 2*c2 - 4*t + 1 ######################################## ## ## We verify Lemma lem:cYgeomirred ## print("Verifying Lemma "+str_lem_cYgeomirred) B. = PolynomialRing(QQ) I = Ideal(B4(f1),B4(f2)) ## Assert that f1 and f2 generate a prime ideal I of Q[x1,y1,x2,y2]. assert(I.is_prime()) ## Assert that P1 vanishes on zero set of I by asserting that it is contained in I assert(I.reduce(P1)==0) ## Assert that P2 vanishes on zero set of I by asserting that it is contained in I assert(I.reduce(P2)==0) ## Assert that dimension is 2 assert(I.dimension() == 2) ## Now assert that a common zero of P1 and P2 at which (x1-y1)*(y1-y2)*(x1-y2)*(x2-y2)*(x1+y1) do not, is a common zero of f1 and f2 tmpI = Ideal(P1,P2) assert(tmpI.reduce(B4((x1-y1)*(y1-y2)*(x1-y2)*(x2-y2)*(x1+y1)*f1)^2) == 0) assert(tmpI.reduce(B4((x1-y1)*(y1-y2)*(x1-y2)*(x2-y2)*(x1+y1)*f2)^2) == 0) ## Assert that (1,-1,1,-1) is a common zero of f1 and f2 assert(f1.substitute({x1:1,y1:-1,x2:1,y2:-1}) == 0) assert(f2.substitute({x1:1,y1:-1,x2:1,y2:-1}) == 0) ## Now we apply the Jacobian criterion to verify that (1,-1,1,-1) is a smooth point a=f1.derivative(y1).substitute({x1:1,y1:-1,x2:1,y2:-1}) b=f1.derivative(y2).substitute({x1:1,y1:-1,x2:1,y2:-1}) c=f2.derivative(y1).substitute({x1:1,y1:-1,x2:1,y2:-1}) d=f2.derivative(y2).substitute({x1:1,y1:-1,x2:1,y2:-1}) assert(a*d-b*c) print("Done.") ## ## Finished verifying Lemma lem:cYgeomirred ## ## ## Assert that h vanishes von R(\mathcal Y) ## print("Verifying that h vanishes von R(\mathcal Y) ") R. = PolynomialRing(QQ) ## Here's the polynomial h that should cut out R(\cY). It was constructed elsewhere, we only check the necessary properties. h = X^6*Y^6*Z^2 - 4*X^6*Y^5*Z^3 - 4*X^5*Y^6*Z^3 + 6*X^6*Y^4*Z^4 - 124*X^5*Y^5*Z^4 + 6*X^4*Y^6*Z^4 - 4*X^6*Y^3*Z^5 - 124*X^5*Y^4*Z^5 - 124*X^4*Y^5*Z^5 - 4*X^3*Y^6*Z^5 + X^6*Y^2*Z^6 - 4*X^5*Y^3*Z^6 + 6*X^4*Y^4*Z^6 - 4*X^3*Y^5*Z^6 + X^2*Y^6*Z^6 + 336*X^5*Y^5*Z^3 + 864*X^5*Y^4*Z^4 + 864*X^4*Y^5*Z^4 + 336*X^5*Y^3*Z^5 + 864*X^4*Y^4*Z^5 + 336*X^3*Y^5*Z^5 - 2*X^6*Y^5*Z - 2*X^5*Y^6*Z + 8*X^6*Y^4*Z^2 - 246*X^5*Y^5*Z^2 + 8*X^4*Y^6*Z^2 - 12*X^6*Y^3*Z^3 - 1672*X^5*Y^4*Z^3 - 1672*X^4*Y^5*Z^3 - 12*X^3*Y^6*Z^3 + 8*X^6*Y^2*Z^4 - 1672*X^5*Y^3*Z^4 - 4800*X^4*Y^4*Z^4 - 1672*X^3*Y^5*Z^4 + 8*X^2*Y^6*Z^4 - 2*X^6*Y*Z^5 - 246*X^5*Y^2*Z^5 - 1672*X^4*Y^3*Z^5 - 1672*X^3*Y^4*Z^5 - 246*X^2*Y^5*Z^5 - 2*X*Y^6*Z^5 - 2*X^5*Y*Z^6 + 8*X^4*Y^2*Z^6 - 12*X^3*Y^3*Z^6 + 8*X^2*Y^4*Z^6 - 2*X*Y^5*Z^6 + 72*X^5*Y^5*Z + 1088*X^5*Y^4*Z^2 + 1088*X^4*Y^5*Z^2 + 2800*X^5*Y^3*Z^3 + 8288*X^4*Y^4*Z^3 + 2800*X^3*Y^5*Z^3 + 1088*X^5*Y^2*Z^4 + 8288*X^4*Y^3*Z^4 + 8288*X^3*Y^4*Z^4 + 1088*X^2*Y^5*Z^4 + 72*X^5*Y*Z^5 + 1088*X^4*Y^2*Z^5 + 2800*X^3*Y^3*Z^5 + 1088*X^2*Y^4*Z^5 + 72*X*Y^5*Z^5 + X^6*Y^4 - 2*X^5*Y^5 + X^4*Y^6 - 4*X^6*Y^3*Z - 246*X^5*Y^4*Z - 246*X^4*Y^5*Z - 4*X^3*Y^6*Z + 6*X^6*Y^2*Z^2 - 1672*X^5*Y^3*Z^2 - 5229*X^4*Y^4*Z^2 - 1672*X^3*Y^5*Z^2 + 6*X^2*Y^6*Z^2 - 4*X^6*Y*Z^3 - 1672*X^5*Y^2*Z^3 - 13532*X^4*Y^3*Z^3 - 13532*X^3*Y^4*Z^3 - 1672*X^2*Y^5*Z^3 - 4*X*Y^6*Z^3 + X^6*Z^4 - 246*X^5*Y*Z^4 - 5229*X^4*Y^2*Z^4 - 13532*X^3*Y^3*Z^4 - 5229*X^2*Y^4*Z^4 - 246*X*Y^5*Z^4 + Y^6*Z^4 - 2*X^5*Z^5 - 246*X^4*Y*Z^5 - 1672*X^3*Y^2*Z^5 - 1672*X^2*Y^3*Z^5 - 246*X*Y^4*Z^5 - 2*Y^5*Z^5 + X^4*Z^6 - 4*X^3*Y*Z^6 + 6*X^2*Y^2*Z^6 - 4*X*Y^3*Z^6 + Y^4*Z^6 + 336*X^5*Y^3*Z + 1088*X^4*Y^4*Z + 336*X^3*Y^5*Z + 864*X^5*Y^2*Z^2 + 8288*X^4*Y^3*Z^2 + 8288*X^3*Y^4*Z^2 + 864*X^2*Y^5*Z^2 + 336*X^5*Y*Z^3 + 8288*X^4*Y^2*Z^3 + 21888*X^3*Y^3*Z^3 + 8288*X^2*Y^4*Z^3 + 336*X*Y^5*Z^3 + 1088*X^4*Y*Z^4 + 8288*X^3*Y^2*Z^4 + 8288*X^2*Y^3*Z^4 + 1088*X*Y^4*Z^4 + 336*X^3*Y*Z^5 + 864*X^2*Y^2*Z^5 + 336*X*Y^3*Z^5 - 4*X^5*Y^3 + 8*X^4*Y^4 - 4*X^3*Y^5 - 124*X^5*Y^2*Z - 1672*X^4*Y^3*Z - 1672*X^3*Y^4*Z - 124*X^2*Y^5*Z - 124*X^5*Y*Z^2 - 4800*X^4*Y^2*Z^2 - 13532*X^3*Y^3*Z^2 - 4800*X^2*Y^4*Z^2 - 124*X*Y^5*Z^2 - 4*X^5*Z^3 - 1672*X^4*Y*Z^3 - 13532*X^3*Y^2*Z^3 - 13532*X^2*Y^3*Z^3 - 1672*X*Y^4*Z^3 - 4*Y^5*Z^3 + 8*X^4*Z^4 - 1672*X^3*Y*Z^4 - 4800*X^2*Y^2*Z^4 - 1672*X*Y^3*Z^4 + 8*Y^4*Z^4 - 4*X^3*Z^5 - 124*X^2*Y*Z^5 - 124*X*Y^2*Z^5 - 4*Y^3*Z^5 + 864*X^4*Y^2*Z + 2800*X^3*Y^3*Z + 864*X^2*Y^4*Z + 864*X^4*Y*Z^2 + 8288*X^3*Y^2*Z^2 + 8288*X^2*Y^3*Z^2 + 864*X*Y^4*Z^2 + 2800*X^3*Y*Z^3 + 8288*X^2*Y^2*Z^3 + 2800*X*Y^3*Z^3 + 864*X^2*Y*Z^4 + 864*X*Y^2*Z^4 + 6*X^4*Y^2 - 12*X^3*Y^3 + 6*X^2*Y^4 - 124*X^4*Y*Z - 1672*X^3*Y^2*Z - 1672*X^2*Y^3*Z - 124*X*Y^4*Z + 6*X^4*Z^2 - 1672*X^3*Y*Z^2 - 5229*X^2*Y^2*Z^2 - 1672*X*Y^3*Z^2 + 6*Y^4*Z^2 - 12*X^3*Z^3 - 1672*X^2*Y*Z^3 - 1672*X*Y^2*Z^3 - 12*Y^3*Z^3 + 6*X^2*Z^4 - 124*X*Y*Z^4 + 6*Y^2*Z^4 + 336*X^3*Y*Z + 1088*X^2*Y^2*Z + 336*X*Y^3*Z + 1088*X^2*Y*Z^2 + 1088*X*Y^2*Z^2 + 336*X*Y*Z^3 - 4*X^3*Y + 8*X^2*Y^2 - 4*X*Y^3 - 4*X^3*Z - 246*X^2*Y*Z - 246*X*Y^2*Z - 4*Y^3*Z + 8*X^2*Z^2 - 246*X*Y*Z^2 + 8*Y^2*Z^2 - 4*X*Z^3 - 4*Y*Z^3 + 72*X*Y*Z + X^2 - 2*X*Y + Y^2 - 2*X*Z - 2*Y*Z + Z^2 ## h is irreducible. assert(h.is_squarefree()==True and len(h.factor())==1) ## In the text we make grandious claims about h, let us assert them now. assert(len(h.coefficients()) == 199) assert(h.degree() == 14) R1 = (x2-1)*(y2+1)/(x2+1)/(y2-1) R2 = (x1-1)*(y1+1)/(x1+1)/(y1-1) R3 = (x2-x1)*(y1-y2)/(x1-y2)/(x2-y1) ## Now we assert that h vanishes on R(cY) by proving that h(R_1,R_2,R_3) is a member of I. The substitution takes some time. assert(I.reduce(h.substitute({X:R1,Y:R2,Z:R3}).numerator()) == 0) print("Done.") ######################################## ## ## We verify Lemma lem:SoODD. We need some subroutines for this. ## h_exp = h.exponents() def make_matrix2(v1,v2): return matrix(ZZ,2,3,[v1[0],v1[1],v1[2],v2[0],v2[1],v2[2]]) print("Verifying Lemma "+str_lem_SoODD) def tier1() : cand = Set([]) l1 = (X^6*Y^6*Z^2).exponents()[0] assert(l1 in h_exp) n=0 panic = false; for l1prime in h_exp: # print(n) n=n+1 if l1 != l1prime : v1 = l1.esub(l1prime) good = false for l2 in h_exp: spoiled=false for l2prime in h_exp: if l2!=l2prime: v2 = l2.esub(l2prime) M=make_matrix2(v1,v2) if M.rank() <= 1 : spoiled = true break if spoiled == false : for l2prime in h_exp: if l2!=l2prime: v2 = l2.esub(l2prime) M=make_matrix2(v1,v2) if M.rank() <= 1 : print("Something is wrong.") assert(false) v = M.transpose().kernel().basis()[0] cand = cand.union(Set([(v[0],v[1],v[2])])) good = true break assert(good); return cand def get_multiplicity(x,li): n = 0 for entry in li : if x==entry : n+=1 return n def get_min_multiplicity(li): mi = len(li) for entry in li : mi = min(mi,get_multiplicity(entry,li)) return mi def tier2(cand) : cand2 = list([]) for vec in cand : tmp_list = list() for ex in h_exp : tmp_list.append(vec[0]*ex[0]+vec[1]*ex[1]+vec[2]*ex[2]) if get_min_multiplicity(tmp_list) > 1 : cand2.append(vec) return cand2; def tier3(cand2): Ruvw. = PolynomialRing(QQ) S. = LaurentPolynomialRing(Ruvw) for expvec in cand2 : gens = h.substitute({X:u*t^expvec[0],Y:v*t^expvec[1],Z:w*t^expvec[2]}).coefficients() gens.append(u*uu-1) gens.append(v*vv-1) gens.append(w*ww-1) h_subs_ideal = Ideal(gens) if(h_subs_ideal.is_one() <> True) : print("Found coset") print(S(u)*S(t)^expvec[0],v*t^expvec[1],w*t^expvec[2]) print("parametrized by t with") if h_subs_ideal.reduce((u-1)^7) == 0 : print(" u=1") if h_subs_ideal.reduce((v-1)^7) == 0 : print(" v=1") if h_subs_ideal.reduce((w-1)^7) == 0 : print(" w=1") print("Tier 1 ") cand = tier1() print(str(len(cand))+ " candidates found.") print("Tier 2 ") cand2 = tier2(cand) print(str(len(cand2))+ " candidates remain:") print(cand2) print("Tier 3 ") tier3(cand2) print("Done.") ## ## Finished verifying Lemma lem:SoODD ## B. = PolynomialRing(QQ) #Define the ideal J J = Ideal(f1,f2,f) print("Verify that J is a prime ideal") #Verify that J is a prime ideal in QQ[c_1,c_2,x_1,y_1,x_2,y_2]. assert(J.is_prime()) #Verify that c_1 lies in the ideal J + (x_1+1,y_1+1). This means that (y_1+1)/(x_1+1) generates #the localization of B/J at x_1+1 as a subring of Frac(B/J). assert((J+Ideal(x1+1,y1+1)).reduce(c1) == 0) #Verify claim regarding action of ring automorphism on J assert(sigma1(f1) == f1 - f2) assert(sigma1(f2) == -f2) assert(sigma1(f) == f) assert(sigma2(f1) == f1) assert(sigma2(f2) == f2) assert(sigma2(f) == f) ################################# ## ## We verify Lemma lem:irred ## print("Verifying Lemma "+str_lem_irred) ## Returns the (n choose k) k\times k-minors of a matrix M. def get_dets(M,k): Scol = Subsets(range(M.ncols()),k) Srow = Subsets(range(M.nrows()),k) f_li = [] for col in Scol : for row in Srow : f_li.append(M.matrix_from_rows_and_columns(list(row),list(col)).det()) return(f_li) B_hom. = PolynomialRing(QQ) ## Polynomial ring for homogen. of f, f1, f2 ## C_c is cut out by f,f1,f2 ## Homogenize f manually (because c1,c2 count as variables and affect the total degree) f_hom = B_hom(2 * c1 * (x2-y2)*h + 2 * c2 * (x1-y1)*h + (x1-y1) * (x2-y2)) assert(f_hom.substitute(h=1) == B_hom(f)) f1_hom = B_hom(f1).homogenize('h') f2_hom = B_hom(f2).homogenize('h') ## Now we construct the Jacobian with respect to the homogenous coordinates x1,y1,x2,y2,h. It's a 3x5 matrix Jacobianf1_f2_f = matrix(3,5,[f1_hom.derivative(x1),f1_hom.derivative(y1),f1_hom.derivative(x2),f1_hom.derivative(y2),f1_hom.derivative(h), f2_hom.derivative(x1),f2_hom.derivative(y1),f2_hom.derivative(x2),f2_hom.derivative(y2),f2_hom.derivative(h), f_hom.derivative(x1),f_hom.derivative(y1),f_hom.derivative(x2),f_hom.derivative(y2),f_hom.derivative(h)]) ## Get all 3x3 minors of the Jacobian matrix Jacobian_minors=get_dets(Jacobianf1_f2_f,3) ## Add the definining equations for \mathcal{C}_c ... Jacobian_minors.append(f1_hom) Jacobian_minors.append(f2_hom) Jacobian_minors.append(f_hom) ##... and convert it into an ideal of B_hom. For fixed (c1,c2) any singular point must be a zero of f1_hom,f2_hom,f and the minors in Jacobian_minors. Jacobian_ideal = Ideal(Jacobian_minors) ## Now let's look at the 5 affine charts separately. x1chart=Ideal(Jacobian_minors)+Ideal(x1-1) y1chart=Ideal(Jacobian_minors)+Ideal(y1-1) x2chart=Ideal(Jacobian_minors)+Ideal(x2-1) y2chart=Ideal(Jacobian_minors)+Ideal(y2-1) hchart=Ideal(Jacobian_minors)+Ideal(h-1) RC1C2C3. = PolynomialRing(QQ) ## The polynomial appearing in Lemma lem:irred in the variables C1,C2,C3 is C1C2C3_hom = RC1C2C3(C1^12 - 3*C1^10*C2^2 + 6*C1^8*C2^4 - 7*C1^6*C2^6 + 6*C1^4*C2^8 - 3*C1^2*C2^10 + C2^12 - 3*C1^10*C3^2 - 51*C1^8*C2^2*C3^2 + 78*C1^6*C2^4*C3^2 + 78*C1^4*C2^6*C3^2 - 51*C1^2*C2^8*C3^2 - 3*C2^10*C3^2 + 6*C1^8*C3^4 + 78*C1^6*C2^2*C3^4 + 414*C1^4*C2^4*C3^4 + 78*C1^2*C2^6*C3^4 + 6*C2^8*C3^4 - 7*C1^6*C3^6 + 78*C1^4*C2^2*C3^6 + 78*C1^2*C2^4*C3^6 - 7*C2^6*C3^6 + 6*C1^4*C3^8 - 51*C1^2*C2^2*C3^8 + 6*C2^4*C3^8 - 3*C1^2*C3^10 - 3*C2^2*C3^10 + C3^12) phi = RC1C2C3.hom([B_hom('c1'),B_hom('c2'),1]) c1c2 = phi(C1 * C2 * (C1 + C2 + 1) * (- C1 + C2 + 1) * (C1 - C2 + 1) * (- C1 - C2 + 1) * C1C2C3_hom) ## Now we check that c1c2 is contained in each ideal coming from one of the 5 charts assert(x1chart.reduce(c1c2)==0) assert(y1chart.reduce(c1c2)==0) assert(x2chart.reduce(c1c2)==0) assert(y1chart.reduce(c1c2)==0) assert(hchart.reduce(c1c2)==0) ## Never send a human to do a machine's job. for x in range(2) : for y in range(2) : for z in range(2) : if x + y + z > 0 : assert((Integer(C1C2C3_hom.substitute({C1:x,C2:y,C3:z})) % 2) == 1) print("Done.") ## ## Finished verifying Lemma lem:irred ## ######################################## ## ## We verify Lemma lem:cong1 ## print("Verifying Lemma "+str_lem_cong1) B. = PolynomialRing(QQ) # We first construct fx1y1 assert(J.elimination_ideal([x2,y2]).is_principal()) #So fx1y1 lies in J assert(J.reduce(fx1y1) == 0) #fx1y1 is irreducible, so it generates J eliminated x2,y2 as an ideal assert(fx1y1.is_squarefree() and len(fx1y1.factor()) == 1) ##First equality assert(fx1y1.degree(x1) == 6) assert(fx1y1.coefficient({x1:6}) == 1) ##Second equality assert(fx1y1.degree(y1) == 6) assert(fx1y1.coefficient({y1:6}) == 1) ##Third equality assert(fx1y1.substitute(y1=1).degree(x1) == 6) assert(fx1y1.substitute(y1=1).coefficient({x1:6}) == 1) assert(fx1y1.substitute(y1=-1).degree(x1) == 6) assert(fx1y1.substitute(y1=-1).coefficient({x1:6}) == 1) ##Fourth equality assert(fx1y1.substitute(x1=1).degree(y1) == 6) assert(fx1y1.substitute(x1=1).coefficient({y1:6}) == 1) assert(fx1y1.substitute(x1=-1).degree(y1) == 6) assert(fx1y1.substitute(x1=-1).coefficient({y1:6}) == 1) #J eliminated x2,y1 is a principal ideal assert(J.elimination_ideal([x2,y1]).is_principal()) #fx1y2 lies in J assert(J.reduce(fx1y2) == 0) #fx1y2 is irreducible. So J eliminated x2,y1 is generated by fx1y2 as an ideal. assert(fx1y2.is_squarefree() and len(fx1y2.factor())==1) ## Check the fifth equality assert(fx1y2.substitute(y2=x1).degree(x1) == 8) assert(fx1y2.substitute(y2=x1).coefficient({x1:8}) == 1) ## Now check the final two fx2y1 = sigma1(fx1y2) assert(fx2y1.substitute({x2:1,y1:1}) == -64*c1*c2*(-c1+c2+1)) fx2y2 = sigma1(fx1y1) assert(fx2y2.substitute({x2:1,y2:1}) == 64*c2^2) print("Done.") ## ## Finished verifying Lemma lem:cong1 ## ######################################## ## ## We verify Lemma lem:cong2 ## print("Verifying Lemma "+str_lem_cong2) B. = PolynomialRing(QQ) # J eliminated y1,y2 is principal assert(J.elimination_ideal([y1,y2]).is_principal()) #fx1x2 lies in J assert(J.reduce(fx1x2) == 0) #fx1x2 is irreducible. So it generates J eliminated y1,y2 as an ideal. assert(fx1x2.is_squarefree() and len(fx1x2.factor())==1) #First equality assert(fx1x2.degree(x1) == 6) assert(fx1x2.coefficient({x1:6}) == -2*(B(x2)+B(c2))^2) #Second equality assert(fx1x2.degree(x2) == 6) assert(fx1x2.coefficient({x2:6}) == -2*(B(x1)+B(c1))^2) #Fifth equality assert(fx1x2.substitute(x2=x1).degree(x1) == 8) assert(fx1x2.substitute(x2=x1).coefficient({x1:8}) == 1) #Final equality assert(fx1x2.substitute({x1:1,x2:1}) == 64*c1*c2*(c1+c2+1)) print("Done.") ## ## Finished verifying Lemma lem:cong2 ## ######################################## ## ## We verify statements just before Lemma lem:projirred ## print("Verifying statements leading up to Lemma "+str_lem_projirred) B. = PolynomialRing(QQ) assert(Ideal(f1,f2,f,x1+1,y1+1).reduce(c1) == 0) print("Done.") ######################################## ## ## We verify Lemma lem:projirred ## print("Verifying Lemma "+str_lem_projirred) Bt. = PolynomialRing(QQ) K = Ideal(Bt(f1),Bt(f2),Bt(f),Bt(x1+1)*t-Bt(y1+1)) # Elimination x1,y1,y2 from K yields a principal ideal K.elimination_ideal([Bt(x1),Bt(y1),Bt(y2)]).is_principal() # fx2t is irreducible assert(fx2t.is_squarefree() and len(fx2t.factor()) == 1) # fx2t lies in K. Therefore, it generates K eliminated x1,y1,y2 assert(K.reduce(fx2t) == 0) assert(fx2t.degree(t) == 6) print(" Total degree of f_{x2 t} is "+str(fx2t.degree())+ " and f_{x2 t} has "+str(len(fx2t.coefficients()))+" terms.") # Equalities in (i) assert(fx2t.substitute(x2=1) == 32*c1^3*t^2 *((-c1 + c2 + 1)*t^2 - (c1 + c2 + 1))) assert(fx2t.substitute(x2=-1) == 32 * c1 * (t^2 - (c1+ c2 + 1)*t + c2) * (c2*t^2 + (c1-c2-1)*t + 1) * ((c1 + c2 - 1)*t^2 + c1 - c2 + 1)) T=var('T') F=NumberField(T^2-3,'x') # Check irreducibility over Q(sqrt(3)) of the two possible substitutions fx2tsub1 = fx2t.substitute(c2=c1+1).change_ring(F) assert(fx2tsub1.is_squarefree() and len(fx2tsub1.factor()) == 1) fx2tsub1_hom = fx2tsub1.homogenize('u') Rtmp = fx2tsub1_hom.parent() u = Rtmp.gens()[7] ## (1/sqrt(3),1,1) is a smooth zero of the homogenization of fx2t(c1+1) assert(fx2tsub1_hom.substitute({Rtmp(x2) : 1/F.gen(),Rtmp(t) : 1,u:1}) == 0) assert(fx2tsub1_hom.derivative(Rtmp(x2)).substitute({Rtmp(x2) : 1/F.gen(),Rtmp(t) : 1,u:1})) fx2tsub2 = fx2t.substitute(c2=-c1+1).change_ring(F) assert(fx2tsub2.is_squarefree() and len(fx2tsub2.factor()) == 1) fx2tsub2_hom = fx2tsub2.homogenize('u') Rtmp = fx2tsub2_hom.parent() u = Rtmp.gens()[7] ## (1/sqrt(3),1,1) is a smooth zero of the homogenization of fx2t(-c1+1) assert(fx2tsub2_hom.substitute({Rtmp(x2) : 1/F.gen(),Rtmp(t) : 1,u:1}) == 0) assert(fx2tsub2_hom.derivative(Rtmp(x2)).substitute({Rtmp(x2) : 1/F.gen(),Rtmp(t) : 1,u:1})) ## Check the three integrality properties mentioned in proof ## Get leading terms of a set of generators of Kx1x2t with respect to x1 Kx1x2t = K.elimination_ideal([y1,y2]) ltlist = [] for tmp in Kx1x2t.gens() : ltlist.append(tmp.coefficient({x1:tmp.degree(x1)})) assert(Ideal(ltlist).reduce(t^2+1) == 0) ## Get leading terms of a set of generators of Kx2y1t with respect to y1 Kx2y1t = K.elimination_ideal([x1,y2]) ltlist = [] for tmp in Kx2y1t.gens() : ltlist.append(tmp.coefficient({y1:tmp.degree(y1)})) assert(Ideal(ltlist).reduce(t^2+1) == 0) ## Get leading terms of a set of generators of Kx2y1t with respect to y2 Kx2y2t = K.elimination_ideal([x1,y1]) ltlist = [] for tmp in Kx2y2t.gens() : ltlist.append(tmp.coefficient({y2:tmp.degree(y2)})) assert(Ideal(ltlist).is_one()) print("Done.") ## ## Finished verifying Lemma lem:projirred ## ######################################## ## ## We verify Lemma lem:3264 ## print("Verifying Lemma "+str_lem_3264) def test1(): ## Check c1-c2+1=0 Q = 97 count = 0 for q in xrange(1,Q) : for p in range(-2*q,2*q+1) : if (p<>0) and (gcd(p,q)==1) and (p<>-q): count = count + 1 ## Use QQ(q)/QQ(p) instead of q/p as the second fraction is interpreted as an integer. ftmp = fx2t.subs(c1 = QQ(q)/QQ(p)).subs(c2=1+QQ(q)/QQ(p)) if (ftmp.is_squarefree() == False) or (len(ftmp.factor()) > 1): assert(False) #print('Triples checked: ',count) def test2(): ## Check -c1-c2+1=0 Q = 97 count = 0 for q in xrange(1,Q) : for p in range(-2*q,2*q+1) : if (p<>0) and (gcd(p,q)==1) and (p<>q): count = count + 1 ## Use QQ(q)/QQ(p) instead of q/p as the second fraction is interpreted as an integer. ftmp = fx2t.subs(c1 = QQ(q)/QQ(p)).subs(c2=1-QQ(q)/QQ(p)) if (ftmp.is_squarefree() == False) or (len(ftmp.factor()) > 1): assert(False) print(" case c1-c2+1=0") test1() print(" case -c1-c2+1=0") print("Done.") print("Finished verifying computational stuff in chapter 6") print("Wall time: "+str(walltime()-start_time)+"s") ## ## Finished verifying Lemma lem:3264 ##