The Zariski topology of equations over groups

The Zariski topology on tuples in a group receiving coefficients from G is generated by complements of solution sets of systems of equations over G. Thus every algebraic set is closed, whether or not the coefficient group or the target group is a domain. A tuple whose coordinates are coefficients is a closed point. Word maps are continuous because substitution pulls an equation back to an equation.

The topology is attached to the coefficient homomorphism: different choices of coefficients can give different closed sets on the same underlying group of points.

When the target is a domain over the coefficients and the coefficient image is nontrivial, commutator equations make finite unions algebraic. In that case all closed sets are algebraic and the closure of a set is the solution set of its ideal of vanishing equations. The nontrivial-image condition makes the empty set algebraic; it can fail even for injective coefficient maps when the coefficient group is trivial.

Without any domain hypothesis, the closure of an irreducible set Y is still the algebraic set V_H(I_H(Y)), so every irreducible closed set is algebraic.

References

• G. Baumslag, A. Myasnikov, V. Remeslennikov, Algebraic geometry over groups I. Algebraic sets and ideal theory, J. Algebra 219 (1999), §3.2, Theorem 3 and Lemma 11; §3.6, Proposition 10.

@[instance_reducible]

def TauCeti.GroupAlgGeom.zariskiTopology {G : Type u_1} {H : Type u_2} [Group G] [Group H] (ι : G →* H) (X : Type u_3) : TopologicalSpace (X → H)

The Zariski topology generated by the complements of algebraic sets over G.

theorem TauCeti.GroupAlgGeom.zariskiTopology_eq_generateFrom {G : Type u_1} {H : Type u_2} [Group G] [Group H] (ι : G →* H) (X : Type u_3) : zariskiTopology ι X = TopologicalSpace.generateFrom {U : Set (X → H) | ∃ (S : Set (GX G X)), U = (V ι S)ᶜ}

The Zariski topology is generated by the complements of solution sets, without any assumptions on the coefficient image or target group.

def TauCeti.GroupAlgGeom.unionEquations {G : Type u_1} [Group G] {X : Type u_3} (S T : Set (GX G X)) : Set (GX G X)

The commutator equations defining the union of two algebraic sets over a domain.

@[simp]

theorem TauCeti.GroupAlgGeom.mem_unionEquations {G : Type u_1} [Group G] {X : Type u_3} {S T : Set (GX G X)} {u : GX G X} : u ∈ unionEquations S T ↔ ∃ s ∈ S, ∃ t ∈ T, ∃ (g : G), u = ⁅s, Monoid.Coprod.inl g * t * (Monoid.Coprod.inl g)⁻¹⁆

The equations in unionEquations S T are the commutators of one equation from each system, conjugated by coefficients.

theorem TauCeti.GroupAlgGeom.union_subset_V_unionEquations {G : Type u_1} {H : Type u_2} [Group G] [Group H] {X : Type u_3} {ι : G →* H} (S T : Set (GX G X)) : V ι S ∪ V ι T ⊆ V ι (unionEquations S T)

Every solution of either system solves their commutator equations, in any group.

theorem TauCeti.GroupAlgGeom.V_unionEquations {G : Type u_1} {H : Type u_2} [Group G] [Group H] {X : Type u_3} {ι : G →* H} (hdom : IsGDomain ι) (S T : Set (GX G X)) : V ι (unionEquations S T) = V ι S ∪ V ι T

Over a group with no zero divisors relative to its coefficients, finite unions of algebraic sets are algebraic.

theorem TauCeti.GroupAlgGeom.isClosed_V {G : Type u_1} {H : Type u_2} [Group G] [Group H] {X : Type u_3} {ι : G →* H} (S : Set (GX G X)) : IsClosed (V ι S)

The solution set of any system of equations is Zariski closed.

theorem TauCeti.GroupAlgGeom.continuous_into_zariskiTopology_iff {G : Type u_1} {H : Type u_2} [Group G] [Group H] {X : Type u_3} {ι : G →* H} {A : Type u_4} [TopologicalSpace A] {f : A → X → H} : Continuous f ↔ ∀ (S : Set (GX G X)), IsClosed (f ⁻¹' V ι S)

A map into a Zariski space is continuous exactly when every algebraic set has closed preimage. This characterization does not require a domain or nontrivial coefficients.

theorem TauCeti.GroupAlgGeom.isClosed_singleton_comp {G : Type u_1} {H : Type u_2} [Group G] [Group H] {X : Type u_3} {ι : G →* H} (g : X → G) : IsClosed {⇑ι ∘ g}

A tuple of elements in the coefficient image is a closed point.

theorem TauCeti.GroupAlgGeom.t1Space_zariskiTopology {G : Type u_1} {H : Type u_2} [Group G] [Group H] {ι : G →* H} (hι : Function.Surjective ⇑ι) (X : Type u_4) : T1Space (X → H)

Surjective coefficients make every point closed, hence the Zariski topology is T1.

theorem TauCeti.GroupAlgGeom.continuous_wordMap {G : Type u_1} {H : Type u_2} [Group G] [Group H] {X : Type u_3} {ι : G →* H} {Y : Type u_4} (w : Y → GX G X) : Continuous (wordMap ι w)

A tuple of words defines a continuous map in the Zariski topologies on tuples.

theorem TauCeti.GroupAlgGeom.isClosed_iff_V {G : Type u_1} {H : Type u_2} [Group G] [Group H] {X : Type u_3} {ι : G →* H} (hdom : IsGDomain ι) (hcoeff : ∃ (g : G), ι g ≠ 1) (Y : Set (X → H)) : IsClosed Y ↔ ∃ (S : Set (GX G X)), Y = V ι S

Over a domain with a nontrivial coefficient image, the generated closed sets are exactly the algebraic sets. The nontrivial-image condition is needed for the empty closed set.

theorem TauCeti.GroupAlgGeom.closure_eq_V_I {G : Type u_1} {H : Type u_2} [Group G] [Group H] {X : Type u_3} {ι : G →* H} (hdom : IsGDomain ι) (hcoeff : ∃ (g : G), ι g ≠ 1) (Y : Set (X → H)) : closure Y = V ι ↑(I ι Y)

Over a domain with a nontrivial coefficient image, the Zariski closure is obtained by imposing all equations that vanish on the set.

theorem TauCeti.GroupAlgGeom.closure_eq_V_I_of_isIrreducible {G : Type u_1} {H : Type u_2} [Group G] [Group H] {X : Type u_3} {ι : G →* H} {Y : Set (X → H)} (hY : IsIrreducible Y) : closure Y = V ι ↑(I ι Y)

The Zariski closure of an irreducible set is the algebraic set cut out by its ideal. No domain hypothesis is needed.

theorem TauCeti.GroupAlgGeom.V_I_eq_of_isIrreducible_of_isClosed {G : Type u_1} {H : Type u_2} [Group G] [Group H] {X : Type u_3} {ι : G →* H} {Y : Set (X → H)} (hY : IsIrreducible Y) (hc : IsClosed Y) : V ι ↑(I ι Y) = Y

Every irreducible Zariski closed set is algebraic: it is cut out by its ideal.