
//	This loads a list of all the possibil 2-adic images associated to an elliptic curve defined over Q. Taken from RZB
load "~/gl2data";

//	Verifiation of the group theoretic computations in Propisition 3.4
Gsup := DirectProduct(DihedralGroup(4),CyclicGroup(4));
f := Gsup.1;
g := Gsup.2;
r := Gsup.3;
N1 := sub<Gsup | f^2,g,r>;
N2 := sub<Gsup | g*f^2,g,r>;
M := sub<Gsup | f,g,r^2>;
i :=0;
for g in Subgroups(Gsup : IndexEqual:=2) do
	G := g`subgroup;
	if N1 meet G eq M meet G and Index(G,N1 meet G) eq 2 then
		assert IdentifyGroup(G) eq <16,3>;
		i := i+1;
		printf "Found %o!\n",i;
	end if;
	if N2 meet G eq M meet G and Index(G,N2 meet G) eq 2 then
		assert IdentifyGroup(G) eq <16,3>;
		i := i+1;
		printf "Found %o!\n",i;
	end if;
end for;





//	Verifiation of the group theoretic computations in Lemma 3.5

for g in SmallGroups(16) do
	Quos := [IdentifyGroup(g/n`subgroup) : n in NormalSubgroups(g)];
	if <8,3> in Quos and <8,4> in Quos then
		assert IdentifyGroup(g) eq <16,4>;
	end if;
end for;

G := SmallGroup(16,4);
N := [h`subgroup : h in NormalSubgroups(G) | IdentifyGroup(G/h`subgroup) in [<2,1>, <4,1>, <8,3>]];
assert &meet N eq sub<G|G.0>;


//	Verifiation of the group theoretic computations in Lemma 3.6
Gsup := DirectProduct(Smallgroup(16,13),SmallGroup(4,1));
a := Gsup.3;
b := Gsup.2;
c := Gsup.1;
r := Gsup.5;
assert Gsup eq sub<Gsup |a,b,c,r>;
N := sub<Gsup | a^2,b,c,r>;
M := sub<Gsup | a,b,c,r^2>;
i :=0;
for g in Subgroups(Gsup : IndexEqual:=2) do
	G := g`subgroup;
	if N meet G eq M meet G and Index(G,N meet G) eq 2 then
		assert IdentifyGroup(G) eq <32,25>;
		i := i+1;
		printf "Found %o!\n",i;
	end if;
end for;


G := SmallGroup(32,25);
N := [h`subgroup : h in NormalSubgroups(G) | IdentifyGroup(G/h`subgroup) in [<2,1>, <4,1>, <8,3>]];
assert &meet N eq sub<G|G.0>;


//	Verifiation of the group theoretic computations in Lemma 3.7
Gsup := DirectProduct(SmallGroup(32,49),SmallGroup(8,3));
a := Gsup.1;
b := Gsup.2;
c := Gsup.3;
d := Gsup.4;
f := Gsup.6;
g := Gsup.7;
assert Gsup eq sub<Gsup |a,b,c,d,f,g>;

M := sub<Gsup | a,b,c,d,(f*g)^2>;
GroupName(Gsup/M);
listN := [n`subgroup : n in NormalSubgroups(Gsup) | GroupName(n`subgroup) eq "D4*Q8"]; //These groups fix the two possible biuquadratic subfields that we could embedd into a D4 extension.
for g in Subgroups(Gsup : IndexEqual:=4) do
	G := g`subgroup;
		for N in listN do
			if G meet N eq M meet G then
				assert IdentifyGroup(G) eq <64,231>;
			end if;
		end for;
end for;

G := SmallGroup(64,231);
N := [h`subgroup : h in NormalSubgroups(G) | IdentifyGroup(G/h`subgroup) in [<2,1>, <4,1>, <8,3>, <16,13>]];
assert &meet N eq sub<G|G.0>;


//	Verifiation of the group theoretic computations in Lemma 3.7
G := SmallGroup(64,206);
N1list := [n`subgroup : n in NormalSubgroups(G) | IsIsomorphic(G/n`subgroup,DirectProduct([DihedralGroup(4),CyclicGroup(2),CyclicGroup(2)])) ];
N2list := [n`subgroup : n in NormalSubgroups(G) | IsIsomorphic(G/n`subgroup,DirectProduct(SmallGroup(16,13),SmallGroup(2,1)))];
for N1 in N1list do
	for N2 in N2list do
		assert #(N1 meet N2) eq 1;
	end for;
end for;

for G in [SmallGroup(64,215), SmallGroup(64,216)] do
	N1list := [n`subgroup : n in NormalSubgroups(G) | IsIsomorphic(G/n`subgroup,DirectProduct([DihedralGroup(4),CyclicGroup(2),CyclicGroup(2)])) ];
	N2list := [n`subgroup : n in NormalSubgroups(G) | IsIsomorphic(G/n`subgroup,SmallGroup(32,49))];
	for N1 in N1list do
		for N2 in N2list do
			assert #(N1 meet N2) eq 1;
		end for;
	end for;
end for;

//***********************************************//
//	Verification for the proof of Theorem 1.3.   //
//***********************************************//

//	A list of groups (using small group ids) for which Q_{D_4} is known to be G-complete.
//	See Lemmas 3.5, 3.6, 3.7, and Proposition 3.11.
GRPS := [ <2,1>, <4,1>, <8,3>, <64, 206>, <64,215>, <64,216>];

print "\n\nTo verify the main theorem simply run Verify2Torsion()";
print "This groups used in this search are:\n";
GRPS;






//	The name and level  (first pair in each entry) along with the corresponding 2-torsion (the second pair) of each of the RZB groups in
//	Table 2 of the original D4 paper.
Table2 := [ [[ 6, 4 ], [ 4, 4 ]], [[ 8, 8 ], [ 8, 8 ]], [[ 11, 8 ], [ 8, 8 ]], [[ 12, 8 ], [ 4, 8 ]], [[ 13, 8 ], [ 4, 8 ]], [[ 25, 16 ], [ 8, 16 ]], [[ 36, 16 ], [ 4, 16 ]], [[ 58, 16 ], [ 16, 16 ]], [[ 92, 16 ], [ 8, 16 ]], [[ 193, 32 ], [ 8, 32 ]], [[ 235, 32 ], [ 4, 32 ]] ];



//	Checks to see if there is a set of normal subgroups { Ni } st G/Ni is in GRPS
//	and &meet { Ni }= { Id }.
function IsInF(G,GRPS)
	NS := [n`subgroup : n in NormalSubgroups(G) | Index(G,n`subgroup) le Max([s[1] : s in GRPS])];
    H := [N : N in NS | IdentifyGroup(G/N) in GRPS];
	if #H eq 0 then return false; end if;
	return #(&meet H) eq 1;
end function;


//	 Compute the invariant factors of a finite Z/nZ-module of rank at most 2
function ModuleInvariants(V)
    if Dimension(V) eq 0 then return []; end if;
    if Dimension(V) eq 1 then return [#V]; end if;
    assert Dimension(V) le 2;
    r1:=#sub<V|V.1>;  r2:=#sub<V|V.2>;
    return [GCD(r1,r2),LCM(r1,r2)];
end function;
   
//	 Given a subgroup of GL(2,Z/nZ), computes the invariants of the sub-module of Z/nZ x Z/nZ fixed by G (returns a list [], [a], or [a,b] with a|b|n)
function FixModule(H)
	V := Eigenspace(Identity(H),1);
	for h in Generators(H) do V:= V meet Eigenspace(Transpose(h),1); end for;	//	 take transpose to work with right eigenspaces
	return ModuleInvariants(V);
end function;

//	Given a subgroup G go GL(2,Integers(m)) lifts or reduces it to a subgroup of GL(2,Integers(n))
//	subject to the obvious divisibility conditions on m and n.
function ChangeLevel(G,n)
    I := BaseRing(G);
    if #I ge n then
    H := ChangeRing(G,Integers(n));
    end if;
    if not #I ge n then
    GL2n := GL(2,Integers(n));
    _,pi  := ChangeRing(GL(2,Integers(n)),I);
    H := sub<GL2n | Inverse(pi)(G),Kernel(pi) >;
    end if;
    return H;
end function;

//	Given a subgroup G go GL(2,Integers(m)), returns it transpose.
function MatrixGroupTranspose(H)
	G := GL(2,BaseRing(H));
    return sub<G| [Transpose(A) : A in Generators(H) ]>;
end function;

procedure Verify2Torsion()
	for object in Table2 do
		printf "Checking that G_%o yields torsion subgroup %o over Q_D4..\n", object[1][1],object[2];
		H := MatrixGroupTranspose(newsublist[object[1][1]][3]);
		G := ChangeLevel(H,2*object[1][2]);
		Ns := [ n`subgroup : n in NormalSubgroups(G) | #(n`subgroup) ge #G/64 ];
		if #Ns ne 0 then
		NG := &meet [ n : n in Ns | IdentifyGroup(G/n) in GRPS];
		assert FixModule(NG) eq object[2];
		print "confirmed!\n";
	end if;
	end for;
	print "******************************";
	print "****  Verified All Cases  ****";
	print "******************************";
end procedure;



