Documentation

TauCeti.GroupTheory.GroupAlgGeom.EquationallyNoetherian

Equationally Noetherian groups #

A group H receiving the coefficients G through ι : G →* H is equationally Noetherian when every system of equations S ⊆ G[X] in finitely many variables is equivalent over H to a finite subsystem: some finite S₀ ⊆ S has the same solutions V_H(S₀) = V_H(S), and then the same radical. Baumslag, Myasnikov and Remeslennikov show that this is equivalent to the descending chain condition on the algebraic sets over H, which is what makes them finite unions of irreducible components. The definition asserts only the existence of S₀, not a way of finding it.

The property passes to subgroups (more precisely, to the source of an injective homomorphism compatible with the coefficients) and survives restriction of the coefficients along any homomorphism G' →* G. Finite groups are equationally Noetherian, and so are commutative groups such as ℤ, because a system over a commutative group is a system of linear equations whose exponent vectors span a finitely generated submodule of ℤⁿ. The property is not automatic: in a direct product of infinitely many copies of a nonabelian group, the system [x, aᵢ] = 1 asking x to commute with the copy aᵢ of a fixed element in every coordinate is equivalent to none of its finite subsystems.

Main definitions #

Main results #

References #

source
def TauCeti.GroupAlgGeom.IsEquationallyNoetherian {G : Type u_1} {H : Type u_3} [Group G] [Group H] (ι : G →* H) :
Prop

H is equationally Noetherian over the coefficients ι : G →* H when every system of equations S ⊆ G[X] in finitely many variables has a finite subsystem S₀ ⊆ S with the same solutions in H. The variables are taken to be Fin n; see IsEquationallyNoetherian.exists_finite for an arbitrary finite type of variables.

Instances For
    source
    theorem TauCeti.GroupAlgGeom.IsEquationallyNoetherian.exists_finite {G : Type u_1} {H : Type u_3} {X : Type u_5} [Group G] [Group H] {ι : G →* H} (h : IsEquationallyNoetherian ι) [Finite X] (S : Set (GX G X)) :
    ∃ S₀ ⊆ S, S₀.Finite ∧ V ι S₀ = V ι S

    Over an equationally Noetherian group, every system in a finite type of variables has a finite subsystem with the same solutions.

    source
    theorem TauCeti.GroupAlgGeom.IsEquationallyNoetherian.exists_finite_Rad_eq {G : Type u_1} {H : Type u_3} {X : Type u_5} [Group G] [Group H] {ι : G →* H} (h : IsEquationallyNoetherian ι) [Finite X] (S : Set (GX G X)) :
    ∃ S₀ ⊆ S, S₀.Finite ∧ Rad ι S₀ = Rad ι S

    Over an equationally Noetherian group, every system in a finite type of variables has a finite subsystem with the same radical.

    source
    theorem TauCeti.GroupAlgGeom.IsEquationallyNoetherian.of_injective {G : Type u_1} {H : Type u_3} {K : Type u_4} [Group G] [Group H] [Group K] {ι : G →* H} {ιK : G →* K} (h : IsEquationallyNoetherian ι) (f : GHom ιK ι) (hf : Function.Injective ⇑f) :
    IsEquationallyNoetherian ιK

    The source of an injective homomorphism compatible with the coefficients into an equationally Noetherian group is equationally Noetherian; in particular so is every subgroup containing the image of the coefficients.

    source
    theorem TauCeti.GroupAlgGeom.IsEquationallyNoetherian.comp {G : Type u_1} {G' : Type u_2} {H : Type u_3} [Group G] [Group G'] [Group H] {ι : G →* H} (h : IsEquationallyNoetherian ι) (f : G' →* G) :
    IsEquationallyNoetherian (ι.comp f)

    Restricting the coefficients along a homomorphism f : G' →* G preserves equational Noetherianity. In particular a group which is equationally Noetherian over itself is equationally Noetherian over each of its subgroups.

    source
    theorem TauCeti.GroupAlgGeom.isEquationallyNoetherian_iff {G : Type u_1} {H : Type u_3} [Group G] [Group H] {ι : G →* H} :
    IsEquationallyNoetherian ι ↔ ∀ (X : Type u_6) [Finite X] (S : Set (GX G X)), ∃ S₀ ⊆ S, S₀.Finite ∧ V ι S₀ = V ι S

    The equational Noetherianity of H does not depend on how the variables are indexed: it holds if and only if every system in any finite type of variables, in any universe, has a finite subsystem with the same solutions.

    Finite groups #

    source
    theorem TauCeti.GroupAlgGeom.isEquationallyNoetherian_of_finite {G : Type u_1} {H : Type u_3} [Group G] [Group H] [Finite H] (ι : G →* H) :
    IsEquationallyNoetherian ι

    Finite groups are equationally Noetherian, over any coefficients.

    Commutative groups #

    source
    theorem TauCeti.GroupAlgGeom.isEquationallyNoetherian_of_commGroup {G : Type u_1} [Group G] {H : Type u_6} [CommGroup H] (ι : G →* H) :
    IsEquationallyNoetherian ι

    Commutative groups are equationally Noetherian, over any coefficients. At a point v, an equation w evaluates to w(1) * ∏ₓ v x ^ nₓ(w), where nₓ(w) is the exponent sum of the variable x in w; so two points give the same value on w exactly when the exponent vector n(w), which lies in the Noetherian ℤ-module ℤⁿ, is in the kernel of an additive map.

    source
    theorem TauCeti.GroupAlgGeom.isEquationallyNoetherian_int :
    IsEquationallyNoetherian (MonoidHom.id (Multiplicative ℤ))

    The infinite cyclic group is equationally Noetherian over itself.

    A group which is not equationally Noetherian #

    source
    theorem TauCeti.GroupAlgGeom.not_isEquationallyNoetherian_pi {K : Type u_4} [Group K] {κ : Type u_6} [Infinite κ] {a b : K} (hab : ¬Commute a b) :
    ¬IsEquationallyNoetherian (MonoidHom.id (κ → K))

    A direct product κ → K of infinitely many copies of a nonabelian group is not equationally Noetherian over itself. If a and b do not commute, the one-variable system [x, aᵢ] = 1 (i : κ), where aᵢ is a in the coordinate i and 1 elsewhere, is equivalent to none of its finite subsystems: for j outside the finitely many coordinates involved, x = bⱼ solves the subsystem but not [x, aⱼ] = 1.