Linear groups and free groups are equationally Noetherian

Let R be a commutative Noetherian ring. Every subgroup of GL n R, and more generally every group H with an injective homomorphism into GL n R, is equationally Noetherian over any coefficients ι : G →* H: every system of equations in finitely many variables over G has a finite subsystem with the same solutions in H. This is Theorem B1 of Baumslag, Myasnikov and Remeslennikov, going back to Bryant and to Guba. Free groups of countable rank embed in SL(2, ℤ) (Sanov), so they are equationally Noetherian over any coefficients; for free groups of finite rank this is Guba's theorem.

Main results

• TauCeti.GroupAlgGeom.isEquationallyNoetherian_generalLinearGroup: GL n R is equationally Noetherian over any coefficients.
• TauCeti.GroupAlgGeom.isEquationallyNoetherian_of_injective_generalLinearGroup: so is every group with an injective homomorphism into GL n R.
• TauCeti.GroupAlgGeom.isEquationallyNoetherian_specialLinearGroup: in particular so is SL n R.
• TauCeti.GroupAlgGeom.isEquationallyNoetherian_of_freeGroupBasis, TauCeti.GroupAlgGeom.isEquationallyNoetherian_freeGroup: free groups of countable rank are equationally Noetherian over any coefficients.

Implementation notes

The proof turns equations over GL n R into polynomial equations over R. Fix a finite type of variables X. The coordinate ring of (GL n)^X is the quotient B of the polynomial ring over R in the entries of two matrices Mₓ and Nₓ per variable x by the entries of Mₓ Nₓ - 1. It is Noetherian by the Hilbert basis theorem, and the images of the Mₓ are invertible matrices over B. Evaluating an equation w at this generic point gives an invertible matrix w(M) over B. A point v : X → GL n R specializes B to R, and w(v) = 1 exactly when the specialization kills the entries of w(M) - 1. The ideal generated by these entries for all w ∈ S is finitely generated, so finitely many equations of S already generate it, and they form the required finite subsystem.

References

• G. Baumslag, A. Myasnikov, V. Remeslennikov, Algebraic geometry over groups I. Algebraic sets and ideal theory, J. Algebra 219 (1999), §2.2, Theorem B1.
• R. M. Bryant, The verbal topology of a group, J. Algebra 48 (1977).
• V. Guba, Equivalence of infinite systems of equations in free groups and semigroups to finite subsystems, Mat. Zametki 40 (1986).

The generic point of (GL n)^X

Linear groups

theorem TauCeti.GroupAlgGeom.isEquationallyNoetherian_generalLinearGroup {G : Type u_1} [Group G] {R : Type u_4} {n : Type u_5} [CommRing R] [IsNoetherianRing R] [Fintype n] [DecidableEq n] (ι : G →* GL n R) : IsEquationallyNoetherian ι

Linear groups are equationally Noetherian. Over a commutative Noetherian ring R, the general linear group GL n R is equationally Noetherian over any coefficients: every system of equations in finitely many variables has a finite subsystem with the same solutions in GL n R.

theorem TauCeti.GroupAlgGeom.isEquationallyNoetherian_of_injective_generalLinearGroup {G : Type u_1} {H : Type u_2} [Group G] [Group H] {R : Type u_4} {n : Type u_5} [CommRing R] [IsNoetherianRing R] [Fintype n] [DecidableEq n] (ι : G →* H) (ρ : H →* GL n R) (hρ : Function.Injective ⇑ρ) : IsEquationallyNoetherian ι

A group with an injective homomorphism into GL n R, for a commutative Noetherian ring R, is equationally Noetherian over any coefficients.

theorem TauCeti.GroupAlgGeom.isEquationallyNoetherian_specialLinearGroup {G : Type u_1} [Group G] {R : Type u_4} {n : Type u_5} [CommRing R] [IsNoetherianRing R] [Fintype n] [DecidableEq n] (ι : G →* Matrix.SpecialLinearGroup n R) : IsEquationallyNoetherian ι

Over a commutative Noetherian ring R, the special linear group SL n R is equationally Noetherian over any coefficients.

Free groups

theorem TauCeti.GroupAlgGeom.isEquationallyNoetherian_of_freeGroupBasis {G : Type u_1} {H : Type u_2} [Group G] [Group H] {κ : Type u_6} [Countable κ] (ι : G →* H) (b : FreeGroupBasis κ H) : IsEquationallyNoetherian ι

Free groups of countable rank are equationally Noetherian. A group with a countable free basis is equationally Noetherian over any coefficients; for free groups of finite rank this is Guba's theorem.

theorem TauCeti.GroupAlgGeom.isEquationallyNoetherian_freeGroup {G : Type u_1} [Group G] {α : Type u_6} [Countable α] (ι : G →* FreeGroup α) : IsEquationallyNoetherian ι

The free group on a countable type is equationally Noetherian over any coefficients. In particular, so is every free group FreeGroup (Fin n) of finite rank.