Solvability of orbit-finite systems of linear equations

TL;DR

This paper introduces a decision procedure for determining the solvability of orbit-finite systems of linear equations within sets with atoms, applicable over various fields and rings, and advances the theory of orbit-finite vector spaces.

Contribution

It develops a decision procedure for orbit-finite linear systems, reducing them to finite systems, and proves the existence of orbit-finite bases for such vector spaces.

Findings

Decision procedure works for any field or ring under mild assumptions.

Reduces orbit-finite systems to exponentially many finite systems, polynomially when atom dimension is fixed.

Proves that orbit-finite vector spaces have orbit-finite bases.

Abstract

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.