using ArgParse using Nemo import SCS.SCSSolver using PropertyT using Groups Nemo.setpermstyle(:cycles) #= Note that the element α(i,j,k) = ϱ(i,j)*ϱ(i,k)*inv(ϱ(i,j))*inv(ϱ(i,k)), which surely belongs to ball of radius 4 in Aut(F₄) becomes trivial under the representation Aut(F₄) → GL₄(ℤ)⋉ℤ⁴ → GL₅(ℂ). Moreover, due to work of Potapchik and Rapinchuk [1] every real representation of Aut(Fₙ) into GLₘ(ℂ) (for m ≤ 2n-2) factors through GLₙ(ℤ)⋉ℤⁿ, so will have the same problem. We need a different approach: Here we actually compute in Aut(𝔽₄) =# ############################################################################### # # Generating set # ############################################################################### function SOutFN_generating_set(N::Int) SOutFN = AutGroup(FreeGroup(N), special=true, outer=true) S = gens(SOutFN); S = [S; [inv(s) for s in S]] return SOutFN, unique(S) end ############################################################################### # # Parsing command line # ############################################################################### function parse_commandline() s = ArgParseSettings() @add_arg_table s begin "--tol" help = "set numerical tolerance for the SDP solver" arg_type = Float64 default = 1e-6 "--iterations" help = "set maximal number of iterations for the SDP solver" arg_type = Int default = 50000 "--upper-bound" help = "Set an upper bound for the spectral gap" arg_type = Float64 default = Inf "--cpus" help = "Set number of cpus used by solver (default: auto)" arg_type = Int required = false "-N" help = "Consider automorphisms of free group on N generators" arg_type = Int default = 2 "--radius" help = "Radius of ball B_r(e,S) to find solution over" arg_type = Int default = 2 "--warmstart" help = "Use warmstart.jld as the initial guess for SCS" action = :store_true end return parse_args(s) end function main() include("CPUselect.jl") set_parallel_mthread(PARSEDARGS, workers=true) N = parsed_args["N"] radius = 2 tol = parsed_args["tol"] iterations = parsed_args["iterations"] upper_bound = parsed_args["upper-bound"] dirname = "SOutF$(N)_$(upper_bound)_r=$radius" logger = PropertyT.setup_logging(dirname) info(logger, "Group: $dirname") info(logger, "Iterations: $iterations") info(logger, "Precision: $tol") info(logger, "Upper bound: $upper_bound") G, S = SOutFN_generating_set(N) info(logger, G) info(logger, "Symmetric generating set of size $(length(S))") info(logger, S) Id = G() solver = SCSSolver(eps=tol, max_iters=iterations, linearsolver=SCS.Direct) @time PropertyT.check_property_T(dirname, S, Id, solver, upper_bound, tol, 2) return 0 end main()