Solvability of orbit-finite systems of linear equations
This work addresses a foundational problem in theoretical computer science for researchers studying infinite structures, offering a novel decision procedure with potential broader applications.
The paper tackles the problem of determining solvability for orbit-finite systems of linear equations in sets with atoms, presenting a decision procedure that reduces such systems to finite ones, with exponential complexity in general but polynomial when atom dimension is fixed.
We study orbit-finite systems of linear equations, in the setting of sets with atoms. Our principal contribution is a decision procedure for solvability of such systems. The procedure works for every field (and even commutative ring) under mild effectiveness assumptions, and reduces a given orbit-finite system to a number of finite ones: exponentially many in general, but polynomially many when atom dimension of input systems is fixed. Towards obtaining the procedure we push further the theory of vector spaces generated by orbit-finite sets, and show that each such vector space admits an orbit-finite basis. This fundamental property is a key tool in our development, but should be also of wider interest.