Separation and discrimination of groups with coefficients

A group under G is separated by another when each nonidentity element survives under some homomorphism fixing G. Discrimination asks for one homomorphism to preserve every element of any given finite family simultaneously. The latter is the relative version of full residuality used to recognize irreducible coordinate groups and, with trivial coefficients, limit groups.

The coefficient maps need not be injective: the same definitions apply to the coefficient maps of quotients of free G-groups, even before the quotient is known to be a G-group.

Main results

• TauCeti.GroupAlgGeom.IsDiscriminatedBy.isSeparatedBy: discrimination implies separation.
• TauCeti.GroupAlgGeom.IsDiscriminatedBy.trans, TauCeti.GroupAlgGeom.IsSeparatedBy.trans: discrimination and separation are transitive.
• TauCeti.GroupAlgGeom.IsDiscriminatedBy.comp, TauCeti.GroupAlgGeom.IsSeparatedBy.comp: discrimination and separation survive restriction of the coefficients.
• TauCeti.GroupAlgGeom.IsSeparatedBy.nonempty_gHom: a nontrivial group separated by H admits a coefficient-preserving homomorphism to H.
• TauCeti.GroupAlgGeom.isSeparatedBy_iff_iInf_ker: separation by H means the kernels of all coefficient-preserving homomorphisms to H intersect trivially.

References

• G. Baumslag, A. Myasnikov, V. Remeslennikov, Algebraic geometry over groups I. Algebraic sets and ideal theory, J. Algebra 219 (1999), §1.
• O. Kharlampovich, A. Myasnikov, Implicit function theorem over free groups, J. Algebra 290 (2005), §2.5.

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

K is separated by H over G when every nonidentity element of K survives in some homomorphism to H fixing the coefficients.

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

K is discriminated by H over G when any finite family of nonidentity elements of K survives simultaneously under one homomorphism to H fixing the coefficients.

theorem TauCeti.GroupAlgGeom.isSeparatedBy_def {G : Type u_1} {K : Type u_2} {H : Type u_3} [Group G] [Group K] [Group H] (ιK : G →* K) (ιH : G →* H) : IsSeparatedBy ιK ιH ↔ ∀ (k : K), k ≠ 1 → ∃ (φ : GHom ιK ιH), φ k ≠ 1

Characterization of separation by coefficient-preserving homomorphisms.

theorem TauCeti.GroupAlgGeom.isDiscriminatedBy_def {G : Type u_1} {K : Type u_2} {H : Type u_3} [Group G] [Group K] [Group H] (ιK : G →* K) (ιH : G →* H) : IsDiscriminatedBy ιK ιH ↔ ∀ (s : Finset K), (∀ k ∈ s, k ≠ 1) → ∃ (φ : GHom ιK ιH), ∀ k ∈ s, φ k ≠ 1

Characterization of discrimination by coefficient-preserving homomorphisms.

theorem TauCeti.GroupAlgGeom.IsDiscriminatedBy.isSeparatedBy {G : Type u_1} {K : Type u_2} {H : Type u_3} [Group G] [Group K] [Group H] {ιK : G →* K} {ιH : G →* H} (h : IsDiscriminatedBy ιK ιH) : IsSeparatedBy ιK ιH

Discrimination implies separation by testing a singleton.

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

The source of an injective coefficient-preserving map into a discriminated group is discriminated by the same target.

theorem TauCeti.GroupAlgGeom.IsDiscriminatedBy.self {G : Type u_1} {K : Type u_2} [Group G] [Group K] (ιK : G →* K) : IsDiscriminatedBy ιK ιK

Every group with a coefficient map discriminates itself through the identity.

theorem TauCeti.GroupAlgGeom.IsDiscriminatedBy.trans {G : Type u_1} {K : Type u_2} {H : Type u_3} {L : Type u_4} [Group G] [Group K] [Group H] [Group L] {ιK : G →* K} {ιL : G →* L} {ιH : G →* H} (hKL : IsDiscriminatedBy ιK ιL) (hLH : IsDiscriminatedBy ιL ιH) : IsDiscriminatedBy ιK ιH

Discrimination is transitive: if K is discriminated by L and L by H, all over G, then K is discriminated by H.

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

Discrimination survives restriction of the coefficients along any homomorphism f : G' →* G.

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

The source of an injective coefficient-preserving map into a separated group is separated by the same target.

theorem TauCeti.GroupAlgGeom.IsSeparatedBy.trans {G : Type u_1} {K : Type u_2} {H : Type u_3} {L : Type u_4} [Group G] [Group K] [Group H] [Group L] {ιK : G →* K} {ιL : G →* L} {ιH : G →* H} (hKL : IsSeparatedBy ιK ιL) (hLH : IsSeparatedBy ιL ιH) : IsSeparatedBy ιK ιH

Separation is transitive: if K is separated by L and L by H, all over G, then K is separated by H.

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

Separation survives restriction of the coefficients along any homomorphism f : G' →* G.

theorem TauCeti.GroupAlgGeom.IsSeparatedBy.nonempty_gHom {G : Type u_1} {K : Type u_2} {H : Type u_3} [Group G] [Group K] [Group H] [Nontrivial K] {ιK : G →* K} {ιH : G →* H} (h : IsSeparatedBy ιK ιH) : Nonempty (GHom ιK ιH)

A nontrivial group separated by H admits a coefficient-preserving homomorphism to H.

theorem TauCeti.GroupAlgGeom.isSeparatedBy_iff_iInf_ker {G : Type u_1} {K : Type u_2} {H : Type u_3} [Group G] [Group K] [Group H] (ιK : G →* K) (ιH : G →* H) : IsSeparatedBy ιK ιH ↔ ⨅ (φ : GHom ιK ιH), (↑φ).ker = ⊥

Separation by H is equivalent to triviality of the intersection of kernels of all coefficient-preserving homomorphisms to H.