diff --git a/AutFN.jl b/AutFN.jl index 436c33a..d609ef4 100644 --- a/AutFN.jl +++ b/AutFN.jl @@ -1,37 +1,5 @@ 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 @@ -73,37 +41,61 @@ function parse_commandline() return parse_args(s) end +const PARSEDARGS = parse_commandline() -function main() include("CPUselect.jl") set_parallel_mthread(PARSEDARGS, workers=true) +#= +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_(n+1)(ℂ). +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. - N = parsed_args["N"] - radius = 2 +We need a different approach: Here we actually compute in (S)Aut(𝔽ₙ) +=# + +using Nemo +using SCS.SCSSolver +using PropertyT +using Groups + +Nemo.setpermstyle(:cycles) + +include("groups/autfreegroup.jl") + +function main(GROUP, parsed_args) + + radius = parsed_args["radius"] tol = parsed_args["tol"] iterations = parsed_args["iterations"] upper_bound = parsed_args["upper-bound"] + warm = parsed_args["warmstart"] - dirname = "SOutF$(N)_$(upper_bound)_r=$radius" + name, N = GROUP.groupname(parsed_args) + G, S = GROUP.generatingset(parsed_args) - logger = PropertyT.setup_logging(dirname) + name = "$(name)_r$radius" + isdir(name) || mkdir(name) - info(logger, "Group: $dirname") + logger = PropertyT.setup_logging(joinpath(name, "$(upper_bound)")) + + info(logger, "Group: $name") 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) + info(logger, "Threads: $(Threads.nthreads())") + info(logger, "Workers: $(workers())") + Id = G() - solver = SCSSolver(eps=tol, max_iters=iterations, linearsolver=SCS.Direct) + solver = SCSSolver(eps=tol, max_iters=iterations, linearsolver=SCS.Direct, alpha=1.95, acceleration_lookback=1) - @time PropertyT.check_property_T(dirname, S, Id, solver, upper_bound, tol, 2) + PropertyT.check_property_T(name, S, Id, solver, upper_bound, tol, radius, warm) return 0 end -main() +main(SpecialAutomorphisms, PARSEDARGS) diff --git a/AutFN_orbit.jl b/AutFN_orbit.jl index f42d251..25e63c3 100644 --- a/AutFN_orbit.jl +++ b/AutFN_orbit.jl @@ -48,7 +48,8 @@ include("CPUselect.jl") set_parallel_mthread(parsed_args, workers=true) -include("SAutFNs.jl") +include("groups/autfreegroup.jl") + include("Orbit.jl") -main(SAutFNs, parsed_args) +main(SpecialAutomorphisms, parsed_args) diff --git a/SL.jl b/SL.jl index a57d7f3..3a83231 100644 --- a/SL.jl +++ b/SL.jl @@ -53,12 +53,12 @@ const PARSEDARGS = parse_commandline() include("CPUselect.jl") set_parallel_mthread(PARSEDARGS, workers=true) -using SCS.SCSSolver using Nemo +using SCS.SCSSolver using PropertyT using Groups -include("SLNs.jl") +include("groups/speciallinear.jl") function main(GROUP, parsed_args) @@ -87,10 +87,10 @@ function main(GROUP, parsed_args) Id = one(G) - solver = SCSSolver(eps=tol, max_iters=iterations, linearsolver=SCS.Direct, alpha=1.9, acceleration_lookback=1) + solver = SCSSolver(eps=tol, max_iters=iterations, linearsolver=SCS.Direct, alpha=1.95, acceleration_lookback=1) - PropertyT.check_property_T(name, S, Id, solver, upper_bound, tol, radius) + PropertyT.check_property_T(name, S, Id, solver, upper_bound, tol, radius, warm) return 0 end -main(SLNs, PARSEDARGS) +main(SpecialLinear, PARSEDARGS) diff --git a/SL_orbit.jl b/SL_orbit.jl index 6668ee6..28ae2fe 100644 --- a/SL_orbit.jl +++ b/SL_orbit.jl @@ -55,7 +55,7 @@ include("CPUselect.jl") set_parallel_mthread(PARSEDARGS, workers=true) -include("SLNs.jl") +include("groups/speciallinear.jl") include("Orbit.jl") -main(SLNs, PARSEDARGS) +main(SpecialLinear, PARSEDARGS)