/* ABELIAN GROUP STRUCTURE abgrp[1] = A; matrix of generators abgrp[2] = DA; diagonal matrix of orders of generators abgrp[3] = id; identity element abgrp[4] = add / mul; binary operation abgrp[5] = mul / pow; optional: repeated binary operation abgrp[6] = red; optional: element reduction abgrp[7] = dlg; optional: dlog abgrp[8] = iselt; optional: iselt SUBGROUP STRUCTURE subgrp[1] = HNF HNF of subgroup subgrp[2] = Gr; group containing the subgroup */ /* SECTION: STRUCTURE */ is_ag(Gr, flag) = { my(G, DG, id, mul, pow, red, dlg, iselt, c); if( type(Gr) != "t_VEC", if(flag, error("Gr must be a vector")); return(0) ); if( #Gr < 9, if(flag, error("Gr has less than eight entries")); return(0) ); [G, DG, id, mul, pow, red, dlg, iselt] = Gr[1..8]; if( #Gr > 8 , c = Gr[9]); if( type(G) != "t_MAT", if(flag, error("G is not a matrix")); return(0) ); if( matsize(G)[1] != 1, if(flag, error("#(rows of G) != 1")); return(0) ); if( type(DG) != "t_MAT", if(flag, error("DG is not a matrix")); return(0) ); if( matsize(DG)[1] != matsize(DG)[2], if(flag, error("DG is a matrix but not square")); return(0) ); if( !matisdiagonal(DG), if(flag, error("DG is a matrix but not diagonal")); return(0) ); if( type(iselt) != "t_CLOSURE", if( iselt != 0, if(flag, error("invalid entry for optional entry iselt")); return(0)) ); if( iselt != 0, if( iselt(c, id) != 1, if(flag, error("identity element does not pass iselt test")); return(0) )); if( type(mul) != "t_CLOSURE", if(flag, error("type error for mul")); return(0) ); if( type(pow) != "t_CLOSURE", if(flag, error("type error for pow")); return(0) ); if( type(red) != "t_CLOSURE", if( iselt != 0, if(flag, error("invalid entry for optional entry red")); return(0)) ); my( withdlg ); withdlg = 1; if( dlg == 0 , withdlg = 0 ); if( type(dlg) != "t_CLOSURE", if( iselt != 0, if(flag, error("invalid entry for optional entry dlg")); return(0)) ); my(E); iferr( apply( x->iselt(c,x), G ), E, if(flag, error("given generators do not satisfy iselt"), return(0)) ); if( withdlog, if( G != matid(1), if( matid(#G) != matconcat(apply(x->ag_dlg(Gr,x), G)), if(flag, error("detected incompatibility between generators and dlg"), return(0)) ) )); return(1); } ag_G(Gr) = { return(Gr[1]) }; ag_DG(Gr) = { return(Gr[2]) }; ag_gen(Gr) = { return(vector(matsize(ag_G(Gr))[2], i, ag_G(Gr)[1,i])) }; ag_cyc(Gr) = { return(vector(matsize(ag_DG(Gr))[1], i, ag_DG(Gr)[i,i])) }; ag_id(Gr) = { return(Gr[3]) }; ag_funmul(Gr) = { return(Gr[4]) }; ag_funpow(Gr) = { return(Gr[5]) }; ag_funred(Gr) = { return(Gr[6]) }; ag_fundlg(Gr) = { return(Gr[7]) }; ag_funiselt(Gr) = { return(Gr[8]) }; ag_context(Gr) = { return(Gr[9]) }; ag_card(Gr) = { my(r);r=matdet(Gr[2]);if(r==0, return(+oo), return(r)) }; ag_mul(Gr, x, y) = { return(ag_funmul(Gr)(ag_context(Gr), x, y)) }; ag_pow(Gr, x, n) = { return(ag_funpow(Gr)(ag_context(Gr), x, n)) }; ag_red(Gr, x) = { return(ag_funred(Gr)(ag_context(Gr), x)) }; ag_dlg(Gr, x) = { return(ag_fundlg(Gr)(ag_context(Gr), x)) }; ag_iselt(Gr, x) = { return(ag_funiselt(Gr)(ag_context(Gr), x)) }; /* SECTION: SNFs and ALMOST SNFs */ ag_mulbasis(Gr, B, M) = { my(id, add, mul, red, c); id = ag_id(Gr); mul = ag_funmul(Gr); pow = ag_funpow(Gr); red = ag_funred(Gr); c = ag_context(Gr); if(type(B) == "t_VEC", B = Mat(B)); my(nB, mB, nM, mM, ret); [nB, mB] = matsize(B); [nM, mM] = matsize(M); if( mB != nM, error("dimension error", str) ); ret = matrix(nB, mM, i, j, id); for(i = 1, nB, for(j = 1, mM, for(k = 1, mB, ret[i,j] = mul( c, ret[i,j], pow( c, B[i,k], M[k, j] ) ); ret[i,j] = red( c, ret[i,j] ); ); ); ); return(ret); } fag_snf( GM, Gr ) = { my(G, M); [G, M] = GM; my(id, add, mul, red, dlg, iselt, context); id = ag_id(Gr); mul = ag_funmul(Gr); pow = ag_funpow(Gr); red = ag_funred(Gr); dlg = ag_fundlg(Gr); iselt = ag_funiselt(Gr); context = ag_context(Gr); my(H); H = mathnf(M); my(nH, mH); [nH, mH] = matsize(H); if( nH != mH, error("H is not a square matrix / M is not of maximal rank OR the group is infinite", str) ); my(U, V, D); [U, V, D] = matsnf(H, 1); my(nD, mD); [nD, mD] = matsize(D); if( nD != mD, error("D is not a square matrix", str) ); my(Ap); Ap = ag_mulbasis(Gr, G, U^-1); my(n); for(i=1, nD, if(D[i,i] == 1, break()); n = i; ); my(A, DA, Ua); A = Mat(Ap)[,1..n]; DA = D[1..n,1..n]; Ua = U[1..n,]; if(matsize(A) == [0,0], return([A, DA, Ua] = [Mat([ag_id(Gr)]), Mat(1), Mat(0)])); my(newdlg); newdlg = agoper_newdlg(dlg, Ua, DA); my(ret); ret = [A, DA, id, mul, pow, red, newdlg, iselt, context]; is_ag(ret, 1); return(ret); } /* SECTION: SUBGROUPS */ is_subgrp(SubGr, flag) = { my(HNF, Gr); [HNF, Gr] = SubGr; Grisag = is_ag(Gr, flag); if(!Grisag, return(0)); my(HinvDG, nHinvDG, mHinvDG); HinvDG = HNF^-1*ag_DG(Gr); [nHinvDG, mHinvDG] = matsize(HinvDG); for(i = 1, nHinvDG, for(j = 1, mHinvDG, if(type(HinvDG[i,j]) != "t_INT", if(flag, error("H^-1 * DG is not integral"), return(0))) ); ); return(1); } agoper_newdlg(dlg, Ua, DG) = { return ( (c,x)-> d=Ua*dlg(c,x); for(i = 1, #DG, if(DG[i,i] != 0, d[i] = lift(Mod(d[i], DG[i,i])); ); ); return(d); ) }; ag_almostsnfofsubgrp(SubGr) = { my(Gr, HG, DG); [HG, Gr] = SubGr; DG = ag_DG(Gr); my(id, add, mul, red, dlg, iselt, context); id = ag_id(Gr); mul = ag_funmul(Gr); pow = ag_funpow(Gr); red = ag_funred(Gr); dlg = ag_fundlg(Gr); iselt = ag_funiselt(Gr); context = ag_context(Gr); my(GHG); GHG = ag_mulbasis( Gr, ag_G(Gr), HG ); my(almostSNF); almostSNF = [GHG, HG^-1*DG ]; my(newdlg); newdlg = (agoper_newdlg(dlg, HG^-1, DG)); return( [GHG, HG^-1*DG, id, mul, pow, red, newdlg, iselt, context] ); } fag_snfofsubgrp(SubGr) = { my(GM, GrG); GM = ag_almostsnfofsubgrp(SubGr); /* not yet tested if works ... apparently it does */ GrG = concat(SubGr[2][1..2], GM[3..9]); if(ag_card(GrG) == +oo, error("group is not finite") ); my(SNF); SNF = fag_snf( GM[1..2], GrG ); return(SNF); } fag_subgrptogroup(SubGr) = { error("not implemented"); } ag_intsumofsubgrps(Gr, H1, H2) = { my(B, DB); [B, DB] = [ag_G(Gr), ag_DG(Gr)]; my(H1H2, H12, U12); H1H2 = matconcat([H1, H2]); [H12, U12] = mathnf(H1H2, 1); my(U1, U3); U1 = U12[1..#B, 1..#B]; U3 = U12[(#B+1)..#U12, 1..#B]; my(H3, H); H3 = mathnf(matconcat([H1*U1, DB])); /* intersection */ H = mathnf(matconcat([H2*U3, DB])); /* sum */ return([H3, H]); } ag_intofsubgrps(Gr, H1, H2) = { return([ag_intsumofsubgrps(Gr, H1, H2)[1], Gr]); } ag_sumofsubgrps(Gr, H1, H2) = { return([ag_intsumofsubgrps(Gr, H1, H2)[2], Gr]); } /* Given two subgrps, determines if one is the subset of the other. H1 cap H2 = H1 iff H1 subgrp of H2 */ ag_issubgrp(Gr, H1, H2) = { my(A, DA); [A, DA] = ADA; my(Hint); Hint = ag_intofsubgrps(Gr, H1, H2); if(Hint == H1, return(1)); return(0); } /* SECTION: MORPHISMS AS INPUT */ /* Quotient group of two subgroups A and B of a group G */ /* Assuming A is a subgrp of B */ /* Thus psi = identity */ ag_quogrp_oftwosubgroups(SubGrA, SubGrB, Gr) = { if(Gr == 0, /* Gr is given */ is_subgrp(SubGrA, 1); is_subgrp(SubGrB, 2), /* Gr is given */ SubGrA = [SubGrA, Gr]; SubGrB = [SubGrB, Gr]; ); my(HA, GrA); my(HB, GrB); [HA, GrA] = SubGrA; [HB, GrB] = SubGrB; if(GrA != GrB, error("the groups containing these subgroups are not equal")); my(GrQuo, BH, HinvDB, id, mul, pow, red, dlg, iselt, context); GrQuo = ag_almostsnfofsubgrp(SubGrB); [BH, HinvDB, id, mul, pow, red, dlg, iselt, context] = GrQuo; my(G, M); G = BH; M = HA*HB^-1; my(SNF); SNF = fag_snf([G, M], GrQuo); return( SNF ); } ag_quogrp(GrA, GrB, fsi, phi) = { error("not implemented"); my(A, DA); my(B, DB); [A, DA] = [ag_G(GrA), ag_DG(GrA)]; [B, DB] = [ag_G(GrB), ag_DG(GrB)]; my(id, add, mul, red); id = ag_id(Gr); add = ag_funmul(Gr); mul = ag_funpow(Gr); red = ag_funred(Gr); my(P); P = Mat( apply(fsi, A) ); my(phiB, PDB); phiB = apply(phi, B); PDB = matconcat([P, DB]); my(C, DC, Ua); [C, DC, Ua] = fag_snf( [phiB, PDB], GrB ); my(Gr); Gr = [C, DC, id, add, mul, red, 0, Ua, matdet(DC)]; return(Gr); } agc_grpext_GrA(c) = { return(c[1]) }; agc_grpext_GrC(c) = { return(c[2]) }; agc_grpext_GrB(c) = { return(c[3]) }; agc_grpext_GrB_id(c) = { return(c[3][1]) }; agc_grpext_GrB_mul(c) = { return(c[3][2]) }; agc_grpext_GrB_pow(c) = { return(c[3][3]) }; agc_grpext_GrB_red(c) = { return(c[3][4]) }; agc_grpext_GrB_dlg(c) = { return(c[3][5]) }; agc_grpext_GrB_iselt(c) = { return(c[3][6]) }; agc_grpext_GrB_effinv(c) = { return(c[3][7]) }; agc_grpext_GrB_gee(c) = { return(c[3][8]) }; agc_grpext_GrB_Bp(c) = { return(c[3][9]) }; agoper_dlogwrtGM_grpext() = { return( ( (c, x)-> my(id, mul, pow, red, gee, effinv, Bp); id = agc_grpext_GrB_id(c); mul = agc_grpext_GrB_mul(c); pow = agc_grpext_GrB_pow(c); red = agc_grpext_GrB_red(c); gee = agc_grpext_GrB_gee(c); effinv = agc_grpext_GrB_effinv(c); Bp = agc_grpext_GrB_Bp(c); my(Y); Y = ag_dlg(agc_grpext_GrC(c), gee(c, x)); my(BpY); /* BpY is an element of B. */ BpY = ag_mulbasis([0, 0, id, mul, pow, red, 0, 0, c], Bp, Mat(Y)); if(matsize(BpY) != [1,1], error("error")); BpY = BpY[1,1]; my(xdivBpY); xdivBpY = mul(c, x, pow(c, BpY, -1)); /* reduction */ xdivBpY = red(c, xdivBpY); my(X); X = ag_dlg(agc_grpext_GrA(c), effinv(c, xdivBpY)); return(concat([X~,Y~])~); ) ); } ag_grpext(c, eff, effinv, gee, geeinv) = { my(GrA, GrC); GrA = c[1]; GrC = c[2]; my(id, mul, pow, red, predlg, iselt); [id, mul, pow, red, predlg, iselt] = c[3]; my(A, DA); my(C, DC); [A, DA] = [ag_G(GrA), ag_DG(GrA)]; [C, DC] = [ag_G(GrC), ag_DG(GrC)]; /* Find Bp such that gee(Bp) = C. */ my(Bp); Bp = apply( x->geeinv(c,x), C); /* Find effA. */ my(effA); effA = apply( x->eff(c,x), A); /* Set Bpp = Bp*DC. */ my(Bpp); Bpp = ag_mulbasis([0, 0, id, mul, pow, red, 0, 0, c], Bp, DC); /* Find App such that eff(App) = Bpp. */ my(App); App = apply( x->effinv(c,x), Bpp); /* Compute P such that App = AP. */ my(P); P = matconcat( apply( (A_elt)->ag_dlg(GrA, A_elt), App ) ); my(G, M); /* G = [ f(A) | Bp ] */ G = matconcat([effA, Bp]); M = matconcat([DA, -P; 0, DC]); c[3] = concat(c[3], [effinv, gee, Bp]); my(dlgwrtGM); dlgwrtGM = agoper_dlogwrtGM_grpext(); my(SNF); SNF = fag_snf([G, M], [0, 0, id, mul, pow, red, dlgwrtGM, iselt, c]); my(retGr); retGr = SNF; return(retGr); } /* inverse image */ agmor_inverseimageofsubgrp(GrB, GrC, morBtoC, HC) = { if(HC == 0, error("must specify subgrp. if you want kernel, use grpmor_kernel")); my(B, DB); my(C, DC); [B, DB] = [ag_G(GrB), ag_DG(GrB)]; [C, DC] = [ag_G(GrC), ag_DG(GrC)]; my(morBtoCdlog); morBtoCdlog = morBtoC; if( type(morBtoC(ag_id(GrB))) != "t_COL", morBtoCdlog = ((x)->ag_dlg(GrC, morBtoC(x))) ); my(P); P = matconcat(apply(morBtoCdlog, B)); my(HC); if(HC == 0, HC = DC); my(nP, mP, nHC, mHC); [nP, mP] = matsize(P); [nHC, mHC] = matsize(HC); /* sanity check */ if(nP != nHC, error("incompatible size for P and HC", str) ); my(PHC); PHC = matconcat([P, HC]); my(H, U); [H, U] = mathnf(PHC, 1); /* U1 is a square matrix with dimensions nP x mP */ my(U1); U1 = U[1..mP,1..mP]; my(U1DB, HB); U1DB = matconcat( [U1, DB] ); HB = mathnf(U1DB); return( [ HB, GrB ] ); } agmor_imageofsubgrp(GrB, GrC, morBtoC, HB) = { if(HB == 0, error("must specify subgrp. if you want image, use grpmor_image")); my(B, DB); my(C, DC); [B, DB] = [ag_G(GrB), ag_DG(GrB)]; [C, DC] = [ag_G(GrC), ag_DG(GrC)]; my(morBtoCdlog); morBtoCdlog = morBtoC; if( type(morBtoC(ag_id(GrB))) != "t_COL", morBtoCdlog = ((x)->ag_dlg(GrC, morBtoC(x))) ); my(P); P = matconcat(apply(morBtoCdlog, B)); my(PHB, M); PHB = P*HB; M = matconcat([PHB, DC]); my(HC); HC = mathnf(M); return( [ HC, GrC ] ); } agmor_kernel(GrB, GrC, morBtoC) = { return( agmor_inverseimageofsubgrp(GrB, GrC, morBtoC, ag_DG(GrC)) ); } agmor_image(GrB, GrC, morBtoC) = { return( agmor_imageofsubgrp(GrB, GrC, morBtoC, matid(#ag_gen(GrB)) ) ); } agoper_mul_clgp() = { return( ( (c, x, y)->idealmul(c[1], x, y)) ); } agoper_pow_clgp() = { return( ( (c, x, n)->idealpow(c[1], x, n)) ); } agoper_red_clgp() = { return( ( (c, x)->idealhnf(c[1], x)) ); } agoper_dlg_clgp() = { return( ( (c, x)->bnrispr=bnrisprincipal(c[1], x)[1]; if(#bnrispr == 0, return([1]~), return(bnrispr))) ); } agoper_iselt_clgp() = { return( ( (c, x)->return(1)) ); } /* SAMPLE GROUP STRUCTURES */ ag_clgp_of(bnr) = { if(#bnr==10, bnr=bnrinit(bnr, 1, 1)); my(opers); opers = [ agoper_mul_clgp(), agoper_pow_clgp(), agoper_red_clgp(), agoper_dlg_clgp(), agoper_iselt_clgp() ]; my(K, clgp); K = bnr; clgp = K.clgp; my(G, DG); G = Mat(clgp[3]); DG = matdiagonal(clgp[2]); if(matsize(G) == [0, 0], G = Mat(1); DG = matdiagonal([1]); ); my(ret); ret = [G, DG, 1, opers[1], opers[2], opers[3], opers[4], opers[5], [K]]; is_ag(ret, 1); return(ret); } agoper_mul_OKstar() = { return( ((c, x, y)->nfeltmul(c[1], x, y)) ); } agoper_pow_OKstar() = { return( ((c, x, n)->nfeltpow(c[1], x, n)) ); } agoper_red_OKstar() = { return( ((c, x)->if(type(x)=="t_POL",x,nfbasistoalg(c[1], x))) ); } agoper_dlg_OKstar() = { return( ((c, x)->tmp=bnfisunit(c[1], x);tmp=concat([tmp[#tmp], tmp[1..(#tmp-1)]]);lift(tmp)) ); } agoper_iselt_OKstar() = { return( ((c, x)->if(#bnfisunit(c[1],x) == 0, return(0)); return(1)) ); } ag_OKstar_of(K:bnf) = { my(opers); opers = [ agoper_mul_OKstar(), agoper_pow_OKstar(), agoper_red_OKstar(), agoper_dlg_OKstar(), agoper_iselt_OKstar() ]; my(G, DG); G = Mat(concat([K.tu[2], K.fu])); DG = matdiagonal(concat([K.tu[1], vector(#K.fu)])); if(matsize(G) == [0, 0], G = Mat(1); DG = matdiagonal([1]); ); my(ret); ret = [G, DG, 1, opers[1], opers[2], opers[3], opers[4], opers[5], [K]]; is_ag(ret, 1); return(ret); } agoper_mul_OKmstar() = { return( ((c, x, y)->nfeltmul(c[1], x, y)) ); } agoper_pow_OKmstar() = { return( ((c, x, n)->nfeltpow(c[1], x, n)) ); } agoper_red_OKmstar() = { return( ((c, x)->if(type(x)=="t_POL",x,nfbasistoalg(c[1], x))) ); } agoper_dlg_OKmstar() = { return( ((c, x)->lift(ideallog(c[1], x, c[2]))) ); } agoper_iselt_OKmstar() = { return( ((c, x)->return(1)) ); } ag_OKmstar_of(bnf, m) = { my(opers); opers = [ agoper_mul_OKmstar(), agoper_pow_OKmstar(), agoper_red_OKmstar(), agoper_dlg_OKmstar(), agoper_iselt_OKmstar() ]; my(K); K = bnf; my(bid); bid = idealstar(K, m, 2); my(G, DG); G = Mat( apply( x->nfbasistoalg(K, x), bid.gen) ); DG = matdiagonal(bid.cyc); if(matsize(G) == [0, 0], G = Mat(1); DG = matdiagonal([1]); ); my(ret); ret = [G, DG, 1, opers[1], opers[2], opers[3], opers[4], opers[5], [K, bid]]; is_ag(ret, 1); return(ret); }