Zero divisors and domains over a group of coefficients

Let H be a group receiving coefficients from G through ι : G →* H. A nonidentity element x : H is a G-zero divisor when there is a nonidentity y : H such that x commutes with every conjugate ι g * y * (ι g)⁻¹ of y by a coefficient, and H is a G-domain when it has no G-zero divisors. Taking for ι the identity of H, these are the zero divisors and the domains of the group H itself.

In a G-domain, for any two nonidentity elements x and y some commutator ⁅x, ι g * y * (ι g)⁻¹⁆ is nontrivial. This is what makes the union of two algebraic sets over a G-domain algebraic, cut out by such commutators of their equations; domains thus appear as the hypothesis under which the closed sets of the Zariski topology are the algebraic sets, and in the irreducibility criterion for algebraic sets over groups.

Being a domain is not torsion-freeness but a strong form of noncommutativity: a nontrivial group with nontrivial centre, in particular a nontrivial abelian group, is never a domain, and neither is a direct product of two nontrivial groups. On the other hand a CSA group in which two coefficients do not commute is a G-domain (Baumslag–Myasnikov–Remeslennikov, Proposition 1). Hence a nonabelian free group F is a domain, and every CSA group containing F is an F-domain. The noncommuting coefficients cannot be dropped: Multiplicative ℤ is CSA, but it is not a domain over any coefficients.

In a domain any two nontrivial normal subgroups meet nontrivially, so finitely many nonidentity elements have a common nonidentity element in their normal closures. This is why, over a domain H, discrimination by H is separation by H plus being a domain (Baumslag–Myasnikov– Remeslennikov, Theorem C1): a homomorphism keeping that common element nontrivial keeps all the given elements nontrivial, and conversely discrimination transports zero divisors to H.

The coefficient map need not be injective, matching TauCeti.GroupAlgGeom.IsSeparatedBy.

Main definitions

• TauCeti.GroupAlgGeom.IsZeroDivisor ι x: x is a G-zero divisor of H.
• TauCeti.GroupAlgGeom.IsGDomain ι: H has no G-zero divisors.

Main results

• TauCeti.GroupAlgGeom.isGDomain_iff: H is a G-domain iff for any nonidentity x and y some coefficient conjugate of y does not commute with x.
• TauCeti.GroupAlgGeom.IsGDomain.mono: enlarging the image of the coefficients preserves being a domain; in particular a G-domain is a domain.
• TauCeti.GroupAlgGeom.IsGDomain.of_injective: a group embedding into a G-domain by a coefficient-preserving map is a G-domain.
• TauCeti.GroupAlgGeom.IsGDomain.of_isCSA: a CSA group with two noncommuting coefficients is a G-domain.
• TauCeti.GroupAlgGeom.IsGDomain.inf_ne_bot: in a G-domain two nontrivial normal subgroups intersect nontrivially.
• TauCeti.GroupAlgGeom.IsDiscriminatedBy.isGDomain: a group discriminated by a G-domain is a G-domain.
• TauCeti.GroupAlgGeom.IsSeparatedBy.isDiscriminatedBy: a G-domain separated by H is discriminated by H, provided some coefficient-preserving homomorphism to H exists.
• TauCeti.GroupAlgGeom.isDiscriminatedBy_iff_isSeparatedBy_and_isGDomain: over a G-domain, a nontrivial group is discriminated exactly when it is separated and a G-domain.
• IsFreeGroup.isGDomain_id, FreeGroup.isGDomain_id: nonabelian free groups are domains.
• TauCeti.GroupAlgGeom.not_isGDomain_of_center_ne_bot, TauCeti.GroupAlgGeom.not_isGDomain_prod: groups with nontrivial centre and products of two nontrivial groups are not domains over any coefficients.

References

• G. Baumslag, A. Myasnikov, V. Remeslennikov, Algebraic geometry over groups I. Algebraic sets and ideal theory, J. Algebra 219 (1999), Theorem C1 and §2.1, Definition 1, Proposition 1 and Corollary 1.

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

A nonidentity x : H is a zero divisor over G, for the coefficient map ι, when some nonidentity y : H has all its conjugates ι g * y * (ι g)⁻¹ by coefficients commuting with x.

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

H is a domain over G, for the coefficient map ι, when it has no zero divisors over G. For ι the identity of H, this says that H is a domain.

theorem TauCeti.GroupAlgGeom.isZeroDivisor_def {G : Type u_1} {H : Type u_3} [Group G] [Group H] (ι : G →* H) (x : H) : IsZeroDivisor ι x ↔ x ≠ 1 ∧ ∃ (y : H), y ≠ 1 ∧ ∀ (g : G), Commute x (ι g * y * (ι g)⁻¹)

The defining condition for a zero divisor over G.

theorem TauCeti.GroupAlgGeom.isGDomain_def {G : Type u_1} {H : Type u_3} [Group G] [Group H] (ι : G →* H) : IsGDomain ι ↔ ∀ (x : H), ¬IsZeroDivisor ι x

The defining condition for a domain over G.

theorem TauCeti.GroupAlgGeom.isGDomain_iff {G : Type u_1} {H : Type u_3} [Group G] [Group H] (ι : G →* H) : IsGDomain ι ↔ ∀ (x y : H), x ≠ 1 → y ≠ 1 → ∃ (g : G), ¬Commute x (ι g * y * (ι g)⁻¹)

H is a domain over G exactly when, for any two nonidentity elements x and y, some conjugate of y by a coefficient does not commute with x.

theorem TauCeti.GroupAlgGeom.isGDomain_of_subsingleton {G : Type u_1} {H : Type u_3} [Group G] [Group H] [Subsingleton H] (ι : G →* H) : IsGDomain ι

Every group with trivial underlying type is a domain over any coefficients.

theorem TauCeti.GroupAlgGeom.IsGDomain.mono {G : Type u_1} {G' : Type u_2} {H : Type u_3} [Group G] [Group G'] [Group H] {ι : G →* H} {ι' : G' →* H} (h : IsGDomain ι) (hle : ι.range ≤ ι'.range) : IsGDomain ι'

A domain over G is a domain over any coefficients with a larger image: commuting with more conjugates is harder. In particular a domain over G is a domain over itself.

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

The source of an injective coefficient-preserving map into a domain over G is a domain over G.

theorem TauCeti.GroupAlgGeom.IsGDomain.of_isCSA {G : Type u_1} {H : Type u_3} [Group G] [Group H] {ι : G →* H} (hH : Group.IsCSA H) {a b : G} (hab : ¬Commute (ι a) (ι b)) : IsGDomain ι

CSA groups are domains (Baumslag–Myasnikov–Remeslennikov, Proposition 1). A CSA group in which the images of two coefficients do not commute is a domain over these coefficients.

theorem TauCeti.GroupAlgGeom.IsGDomain.of_isCSA_of_injective {G : Type u_1} {H : Type u_3} [Group G] [Group H] {ι : G →* H} (hH : Group.IsCSA H) (hι : Function.Injective ⇑ι) (hG : ¬IsMulCommutative G) : IsGDomain ι

A CSA group receiving a nonabelian group of coefficients injectively is a domain over it.

theorem TauCeti.GroupAlgGeom.IsGDomain.inf_ne_bot {G : Type u_1} {H : Type u_3} [Group G] [Group H] {ι : G →* H} (h : IsGDomain ι) {N₁ N₂ : Subgroup H} [N₁.Normal] [N₂.Normal] (h₁ : N₁ ≠ ⊥) (h₂ : N₂ ≠ ⊥) : N₁ ⊓ N₂ ≠ ⊥

In a domain over G, two nontrivial normal subgroups intersect nontrivially: a nonidentity element of the first has a nonidentity commutator with some coefficient conjugate of a nonidentity element of the second, and that commutator lies in both.

Discrimination by a domain

theorem TauCeti.GroupAlgGeom.IsDiscriminatedBy.isGDomain {G : Type u_1} {H : Type u_3} {K : Type u_4} [Group G] [Group H] [Group K] {ιK : G →* K} {ιH : G →* H} (h : IsDiscriminatedBy ιK ιH) (hH : IsGDomain ιH) : IsGDomain ιK

A group discriminated by a domain over G is a domain over G: a homomorphism keeping a zero divisor and its witness nontrivial makes their images a zero divisor of the target.

theorem TauCeti.GroupAlgGeom.IsSeparatedBy.isDiscriminatedBy {G : Type u_1} {H : Type u_3} {K : Type u_4} [Group G] [Group H] [Group K] {ιK : G →* K} {ιH : G →* H} (h : IsSeparatedBy ιK ιH) (hK : IsGDomain ιK) (hne : Nonempty (GHom ιK ιH)) : IsDiscriminatedBy ιK ιH

A domain over G that is separated by H is discriminated by H, as soon as some coefficient-preserving homomorphism to H exists: one homomorphism keeping a common nonidentity element of the normal closures of the given elements nontrivial keeps all of them nontrivial. No hypothesis on H is needed. The existence of a homomorphism only matters when K is trivial; otherwise it follows from separation (IsSeparatedBy.nonempty_gHom).

theorem TauCeti.GroupAlgGeom.isDiscriminatedBy_iff_isSeparatedBy_and_isGDomain {G : Type u_1} {H : Type u_3} {K : Type u_4} [Group G] [Group H] [Group K] [Nontrivial K] {ιK : G →* K} {ιH : G →* H} (hH : IsGDomain ιH) : IsDiscriminatedBy ιK ιH ↔ IsSeparatedBy ιK ιH ∧ IsGDomain ιK

Discrimination is separation plus being a domain (Baumslag–Myasnikov–Remeslennikov, Theorem C1). Over a domain H over G, a nontrivial group is discriminated by H if and only if it is separated by H and is itself a domain over G. For a trivial group the separation condition is vacuous, while discrimination still asks for a coefficient-preserving homomorphism to H.

theorem TauCeti.GroupAlgGeom.not_isGDomain_of_center_ne_bot {G : Type u_1} {H : Type u_3} [Group G] [Group H] (ι : G →* H) (hH : Subgroup.center H ≠ ⊥) : ¬IsGDomain ι

A group with a nonidentity central element is not a domain over any coefficients: the central element commutes with every conjugate of itself.

theorem TauCeti.GroupAlgGeom.not_isGDomain_of_isMulCommutative {G : Type u_1} {H : Type u_3} [Group G] [Group H] [IsMulCommutative H] [Nontrivial H] (ι : G →* H) : ¬IsGDomain ι

A nontrivial abelian group is not a domain over any coefficients, although it may be torsion-free: being a domain is a noncommutativity condition.

theorem TauCeti.GroupAlgGeom.not_isGDomain_prod {G : Type u_1} [Group G] {H₁ : Type u_5} {H₂ : Type u_6} [Group H₁] [Group H₂] [Nontrivial H₁] [Nontrivial H₂] (ι : G →* H₁ × H₂) : ¬IsGDomain ι

A direct product of two nontrivial groups is not a domain over any coefficients: (x, 1) commutes with every conjugate of (1, y).

theorem IsFreeGroup.isGDomain_id {F : Type u_1} [Group F] [IsFreeGroup F] (hF : ¬IsMulCommutative F) : TauCeti.GroupAlgGeom.IsGDomain (MonoidHom.id F)

Nonabelian free groups are domains (Baumslag–Myasnikov–Remeslennikov, Corollary 1).

theorem FreeGroup.isGDomain_id {α : Type u_1} [Nontrivial α] : TauCeti.GroupAlgGeom.IsGDomain (MonoidHom.id (FreeGroup α))

The free group on at least two generators is a domain.