G-groups and the free G-group G[X]

Algebraic geometry over a group G studies equations with coefficients in G. An equation in the variables X is an element of the free product G[X] = G ∗ F(X) of G with the free group on X, and a solution in a group H receiving the coefficients through ι : G →* H is a point v : X → H at which the evaluation G[X] →* H sends the equation to 1.

A G-group is a group H with an injective homomorphism G →* H, and a G-homomorphism is a homomorphism commuting with the coefficient maps. Quotients of G[X] (coordinate groups of systems of equations) carry a coefficient map which need not be injective, so G-homomorphisms and evaluation are set up here for arbitrary coefficient homomorphisms; the bundled GGroup adds injectivity.

Main definitions

• TauCeti.GroupAlgGeom.GGroup: a group with an embedding of G.
• TauCeti.GroupAlgGeom.GHom ιH ιK: homomorphisms H →* K with φ ∘ ιH = ιK.
• TauCeti.GroupAlgGeom.GX G X: the free G-group G[X] = Monoid.Coprod G (FreeGroup X).
• TauCeti.GroupAlgGeom.eval ι v: evaluation G[X] →* H at a point v : X → H.
• TauCeti.GroupAlgGeom.wordMap ι w: the map on tuples defined by substituting words w.
• TauCeti.GroupAlgGeom.homEquiv ι: G[X] is free on X among groups under G: G-homomorphisms G[X] → H correspond to points X → H.

Main results

• MonoidHom.comp_eval, TauCeti.GroupAlgGeom.map_eval: homomorphisms and G-homomorphisms commute with evaluation.
• TauCeti.GroupAlgGeom.eval_comp_eval: evaluating after word substitution is evaluation at the substituted tuple.
• TauCeti.GroupAlgGeom.wordMap_wordMap: composition of word maps is word substitution.
• TauCeti.GroupAlgGeom.GX.equivOfIsEmpty, TauCeti.GroupAlgGeom.GX.equivFreeGroup: G[∅] ≅ G and, for trivial G, G[X] ≅ F(X), under which evaluation is FreeGroup.lift.
• TauCeti.GroupAlgGeom.GX.not_commute_inl_inr_of: a nontrivial coefficient does not commute with a variable, so the inclusions of G and F(X) do not commute in G[X].

References

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

G-homomorphisms

structure TauCeti.GroupAlgGeom.GHom {G : Type u_1} {H : Type u_2} {K : Type u_3} [Group G] [Group H] [Group K] (ιH : G →* H) (ιK : G →* K) extends H →* K : Type (max u_2 u_3)

A G-homomorphism between groups receiving G through ιH and ιK: a homomorphism φ : H →* K with φ ∘ ιH = ιK.

• toFun : H → K
• map_one' : (↑self.toMonoidHom).toFun 1 = 1
• map_mul' (x y : H) : (↑self.toMonoidHom).toFun (x * y) = (↑self.toMonoidHom).toFun x * (↑self.toMonoidHom).toFun y
• map_coeff' (g : G) : (↑self.toMonoidHom).toFun (ιH g) = ιK g

  A G-homomorphism fixes the coefficients.

@[instance_reducible]

instance TauCeti.GroupAlgGeom.GHom.instFunLike {G : Type u_1} {H : Type u_2} {K : Type u_3} [Group G] [Group H] [Group K] {ιH : G →* H} {ιK : G →* K} : FunLike (GHom ιH ιK) H K

instance TauCeti.GroupAlgGeom.GHom.instMonoidHomClass {G : Type u_1} {H : Type u_2} {K : Type u_3} [Group G] [Group H] [Group K] {ιH : G →* H} {ιK : G →* K} : MonoidHomClass (GHom ιH ιK) H K

@[simp]

theorem TauCeti.GroupAlgGeom.GHom.toMonoidHom_eq_coe {G : Type u_1} {H : Type u_2} {K : Type u_3} [Group G] [Group H] [Group K] {ιH : G →* H} {ιK : G →* K} (φ : GHom ιH ιK) : φ.toMonoidHom = ↑φ

@[simp]

theorem TauCeti.GroupAlgGeom.GHom.coe_mk {G : Type u_1} {H : Type u_2} {K : Type u_3} [Group G] [Group H] [Group K] {ιH : G →* H} {ιK : G →* K} (φ : H →* K) (h : ∀ (g : G), (↑φ).toFun (ιH g) = ιK g) : ⇑{ toMonoidHom := φ, map_coeff' := h } = ⇑φ

theorem TauCeti.GroupAlgGeom.GHom.ext {G : Type u_1} {H : Type u_2} {K : Type u_3} [Group G] [Group H] [Group K] {ιH : G →* H} {ιK : G →* K} {φ ψ : GHom ιH ιK} (h : ∀ (x : H), φ x = ψ x) : φ = ψ

theorem TauCeti.GroupAlgGeom.GHom.ext_iff {G : Type u_1} {H : Type u_2} {K : Type u_3} [Group G] [Group H] [Group K] {ιH : G →* H} {ιK : G →* K} {φ ψ : GHom ιH ιK} : φ = ψ ↔ ∀ (x : H), φ x = ψ x

@[simp]

theorem TauCeti.GroupAlgGeom.GHom.map_coeff {G : Type u_1} {H : Type u_2} {K : Type u_3} [Group G] [Group H] [Group K] {ιH : G →* H} {ιK : G →* K} (φ : GHom ιH ιK) (g : G) : φ (ιH g) = ιK g

@[simp]

theorem TauCeti.GroupAlgGeom.GHom.comp_coeff {G : Type u_1} {H : Type u_2} {K : Type u_3} [Group G] [Group H] [Group K] {ιH : G →* H} {ιK : G →* K} (φ : GHom ιH ιK) : (↑φ).comp ιH = ιK

def TauCeti.GroupAlgGeom.GHom.id {G : Type u_1} {H : Type u_2} [Group G] [Group H] (ιH : G →* H) : GHom ιH ιH

The identity G-homomorphism.

@[simp]

theorem TauCeti.GroupAlgGeom.GHom.coe_id {G : Type u_1} {H : Type u_2} [Group G] [Group H] {ιH : G →* H} : ⇑(GHom.id ιH) = id

def TauCeti.GroupAlgGeom.GHom.comp {G : Type u_1} {H : Type u_2} {K : Type u_3} {L : Type u_4} [Group G] [Group H] [Group K] [Group L] {ιH : G →* H} {ιK : G →* K} {ιL : G →* L} (ψ : GHom ιK ιL) (φ : GHom ιH ιK) : GHom ιH ιL

The composite of two G-homomorphisms.

@[simp]

theorem TauCeti.GroupAlgGeom.GHom.coe_comp {G : Type u_1} {H : Type u_2} {K : Type u_3} {L : Type u_4} [Group G] [Group H] [Group K] [Group L] {ιH : G →* H} {ιK : G →* K} {ιL : G →* L} (ψ : GHom ιK ιL) (φ : GHom ιH ιK) : ⇑(ψ.comp φ) = ⇑ψ ∘ ⇑φ

@[simp]

theorem TauCeti.GroupAlgGeom.GHom.id_comp {G : Type u_1} {H : Type u_2} {K : Type u_3} [Group G] [Group H] [Group K] {ιH : G →* H} {ιK : G →* K} (φ : GHom ιH ιK) : (GHom.id ιK).comp φ = φ

@[simp]

theorem TauCeti.GroupAlgGeom.GHom.comp_id {G : Type u_1} {H : Type u_2} {K : Type u_3} [Group G] [Group H] [Group K] {ιH : G →* H} {ιK : G →* K} (φ : GHom ιH ιK) : φ.comp (GHom.id ιH) = φ

theorem TauCeti.GroupAlgGeom.GHom.comp_assoc {G : Type u_1} {H : Type u_2} {K : Type u_3} {L : Type u_4} [Group G] [Group H] [Group K] [Group L] {ιH : G →* H} {ιK : G →* K} {ιL : G →* L} {M : Type u_5} [Group M] {ιM : G →* M} (χ : GHom ιL ιM) (ψ : GHom ιK ιL) (φ : GHom ιH ιK) : (χ.comp ψ).comp φ = χ.comp (ψ.comp φ)

noncomputable def TauCeti.GroupAlgGeom.GHom.symmOfBijective {G : Type u_1} {H : Type u_2} {K : Type u_3} [Group G] [Group H] [Group K] {ιH : G →* H} {ιK : G →* K} (φ : GHom ιH ιK) (hφ : Function.Bijective ⇑φ) : GHom ιK ιH

The inverse of a bijective coefficient-preserving homomorphism preserves coefficients.

@[simp]

theorem TauCeti.GroupAlgGeom.GHom.apply_symmOfBijective_apply {G : Type u_1} {H : Type u_2} {K : Type u_3} [Group G] [Group H] [Group K] {ιH : G →* H} {ιK : G →* K} (φ : GHom ιH ιK) (hφ : Function.Bijective ⇑φ) (x : K) : φ ((φ.symmOfBijective hφ) x) = x

@[simp]

theorem TauCeti.GroupAlgGeom.GHom.symmOfBijective_apply_apply {G : Type u_1} {H : Type u_2} {K : Type u_3} [Group G] [Group H] [Group K] {ιH : G →* H} {ιK : G →* K} (φ : GHom ιH ιK) (hφ : Function.Bijective ⇑φ) (x : H) : (φ.symmOfBijective hφ) (φ x) = x

theorem TauCeti.GroupAlgGeom.GHom.symmOfBijective_injective {G : Type u_1} {H : Type u_2} {K : Type u_3} [Group G] [Group H] [Group K] {ιH : G →* H} {ιK : G →* K} (φ : GHom ιH ιK) (hφ : Function.Bijective ⇑φ) : Function.Injective ⇑(φ.symmOfBijective hφ)

@[simp]

theorem TauCeti.GroupAlgGeom.GHom.comp_symmOfBijective {G : Type u_1} {H : Type u_2} {K : Type u_3} [Group G] [Group H] [Group K] {ιH : G →* H} {ιK : G →* K} (φ : GHom ιH ιK) (hφ : Function.Bijective ⇑φ) : φ.comp (φ.symmOfBijective hφ) = GHom.id ιK

@[simp]

theorem TauCeti.GroupAlgGeom.GHom.symmOfBijective_comp {G : Type u_1} {H : Type u_2} {K : Type u_3} [Group G] [Group H] [Group K] {ιH : G →* H} {ιK : G →* K} (φ : GHom ιH ιK) (hφ : Function.Bijective ⇑φ) : (φ.symmOfBijective hφ).comp φ = GHom.id ιH

G-groups

structure TauCeti.GroupAlgGeom.GGroup (G : Type u) [Group G] : Type (max u (v + 1))

A G-group: a group together with an injective homomorphism from G, its coefficients. Homomorphisms between G-groups H and K are GHom H.coeff K.coeff.

• carrier : Type v

  The underlying type.

• instGroup : Group self.carrier
• coeff : G →* self.carrier

  The coefficient embedding.

• coeff_injective : Function.Injective ⇑self.coeff

@[instance_reducible]

instance TauCeti.GroupAlgGeom.GGroup.instCoeSortType {G : Type u} [Group G] : CoeSort (GGroup G) (Type v)

def TauCeti.GroupAlgGeom.GGroup.self (G : Type u) [Group G] : GGroup G

G is a G-group through the identity.

@[simp]

theorem TauCeti.GroupAlgGeom.GGroup.coeff_self {G : Type u} [Group G] : (self G).coeff = MonoidHom.id G

The free G-group G[X] and evaluation

@[reducible, inline]

abbrev TauCeti.GroupAlgGeom.GX (G : Type u_1) [Group G] (X : Type u_5) : Type (max u_5 u_1)

The free G-group G[X] = G ∗ F(X) on a type of variables X; its coefficients are the left inclusion Monoid.Coprod.inl, and the variable x is inr (FreeGroup.of x). Its elements are the equations over G in the variables X.

def TauCeti.GroupAlgGeom.GGroup.free (G : Type u_1) [Group G] (X : Type u_5) : GGroup G

G[X] as a G-group.

@[simp]

theorem TauCeti.GroupAlgGeom.GGroup.coeff_free {G : Type u_1} [Group G] {X : Type u_5} : (free G X).coeff = Monoid.Coprod.inl

def TauCeti.GroupAlgGeom.eval {G : Type u_1} {H : Type u_2} [Group G] [Group H] {X : Type u_5} (ι : G →* H) (v : X → H) : GX G X →* H

Evaluation w ↦ w(v) of G[X] at a point v : X → H, for a group H receiving the coefficients through ι: coefficients go to their images under ι and the variable x goes to v x.

@[simp]

theorem TauCeti.GroupAlgGeom.eval_inl {G : Type u_1} {H : Type u_2} [Group G] [Group H] {X : Type u_5} (ι : G →* H) (v : X → H) (g : G) : (eval ι v) (Monoid.Coprod.inl g) = ι g

@[simp]

theorem TauCeti.GroupAlgGeom.eval_inr {G : Type u_1} {H : Type u_2} [Group G] [Group H] {X : Type u_5} (ι : G →* H) (v : X → H) (w : FreeGroup X) : (eval ι v) (Monoid.Coprod.inr w) = (FreeGroup.lift v) w

theorem TauCeti.GroupAlgGeom.eval_inr_of {G : Type u_1} {H : Type u_2} [Group G] [Group H] {X : Type u_5} (ι : G →* H) (v : X → H) (x : X) : (eval ι v) (Monoid.Coprod.inr (FreeGroup.of x)) = v x

@[simp]

theorem TauCeti.GroupAlgGeom.eval_comp_inl {G : Type u_1} {H : Type u_2} [Group G] [Group H] {X : Type u_5} (ι : G →* H) (v : X → H) : (eval ι v).comp Monoid.Coprod.inl = ι

@[simp]

theorem TauCeti.GroupAlgGeom.eval_comp_inr {G : Type u_1} {H : Type u_2} [Group G] [Group H] {X : Type u_5} (ι : G →* H) (v : X → H) : (eval ι v).comp Monoid.Coprod.inr = FreeGroup.lift v

@[simp]

theorem TauCeti.GroupAlgGeom.eval_inl_inr_of {G : Type u_1} [Group G] {X : Type u_5} : (eval Monoid.Coprod.inl fun (x : X) => Monoid.Coprod.inr (FreeGroup.of x)) = MonoidHom.id (GX G X)

Evaluating at the generic point, the tuple of variables of G[X], is the identity.

theorem TauCeti.GroupAlgGeom.eq_eval {G : Type u_1} {H : Type u_2} [Group G] [Group H] {X : Type u_5} (f : GX G X →* H) : f = eval (f.comp Monoid.Coprod.inl) fun (x : X) => f (Monoid.Coprod.inr (FreeGroup.of x))

A homomorphism out of G[X] is determined by its restriction to the coefficients and its values on the variables: it is evaluation at those values.

def TauCeti.GroupAlgGeom.evalGHom {G : Type u_1} {H : Type u_2} [Group G] [Group H] {X : Type u_5} (ι : G →* H) (v : X → H) : GHom Monoid.Coprod.inl ι

Evaluation as a G-homomorphism from the free G-group G[X].

@[simp]

theorem TauCeti.GroupAlgGeom.coe_evalGHom {G : Type u_1} {H : Type u_2} [Group G] [Group H] {X : Type u_5} (ι : G →* H) (v : X → H) : ⇑(evalGHom ι v) = ⇑(eval ι v)

def TauCeti.GroupAlgGeom.homEquiv {G : Type u_1} {H : Type u_2} [Group G] [Group H] {X : Type u_5} (ι : G →* H) : GHom Monoid.Coprod.inl ι ≃ (X → H)

G[X] is the free G-group on X: G-homomorphisms G[X] → H correspond to points X → H, by restriction to the variables and by evaluation.

@[simp]

theorem TauCeti.GroupAlgGeom.homEquiv_apply {G : Type u_1} {H : Type u_2} [Group G] [Group H] {X : Type u_5} (ι : G →* H) (φ : GHom Monoid.Coprod.inl ι) (x : X) : (homEquiv ι) φ x = φ (Monoid.Coprod.inr (FreeGroup.of x))

@[simp]

theorem TauCeti.GroupAlgGeom.homEquiv_symm_apply {G : Type u_1} {H : Type u_2} [Group G] [Group H] {X : Type u_5} (ι : G →* H) (v : X → H) : (homEquiv ι).symm v = evalGHom ι v

theorem TauCeti.GroupAlgGeom.GX.gHom_ext {G : Type u_1} {H : Type u_2} [Group G] [Group H] {X : Type u_5} (ι : G →* H) {φ ψ : GHom Monoid.Coprod.inl ι} (h : ∀ (x : X), φ (Monoid.Coprod.inr (FreeGroup.of x)) = ψ (Monoid.Coprod.inr (FreeGroup.of x))) : φ = ψ

A G-homomorphism out of G[X] is determined by its values on the variables.

theorem TauCeti.GroupAlgGeom.GX.gHom_ext_iff {G : Type u_1} {H : Type u_2} [Group G] [Group H] {X : Type u_5} {ι : G →* H} {φ ψ : GHom Monoid.Coprod.inl ι} : φ = ψ ↔ ∀ (x : X), φ (Monoid.Coprod.inr (FreeGroup.of x)) = ψ (Monoid.Coprod.inr (FreeGroup.of x))

theorem TauCeti.GroupAlgGeom.eval_eq_of_comp_inl {G : Type u_1} {H : Type u_2} [Group G] [Group H] {X : Type u_5} {ι : G →* H} {f : GX G X →* H} (hf : f.comp Monoid.Coprod.inl = ι) : (eval ι fun (x : X) => f (Monoid.Coprod.inr (FreeGroup.of x))) = f

A homomorphism out of G[X] that restricts to ι on the coefficients is evaluation at its values on the variables.

theorem MonoidHom.comp_eval {G : Type u_1} {H : Type u_2} {K : Type u_3} [Group G] [Group H] [Group K] {X : Type u_5} (f : H →* K) {ι : G →* H} {v : X → H} : f.comp (TauCeti.GroupAlgGeom.eval ι v) = TauCeti.GroupAlgGeom.eval (f.comp ι) (⇑f ∘ v)

Homomorphisms commute with evaluation: f ∘ eval ι v = eval (f ∘ ι) (f ∘ v).

theorem TauCeti.GroupAlgGeom.hom_eval {G : Type u_1} {H : Type u_2} {K : Type u_3} [Group G] [Group H] [Group K] {X : Type u_5} {ι : G →* H} {v : X → H} {F : Type u_6} [FunLike F H K] [MonoidHomClass F H K] (f : F) (w : GX G X) : f ((eval ι v) w) = (eval ((↑f).comp ι) (⇑f ∘ v)) w

Homomorphisms commute with evaluation: f (w(v)) = w(f ∘ v), the coefficients being moved along f.

theorem TauCeti.GroupAlgGeom.comp_eval {G : Type u_1} {H : Type u_2} {K : Type u_3} [Group G] [Group H] [Group K] {X : Type u_5} {ι : G →* H} {v : X → H} {ιK : G →* K} (φ : GHom ι ιK) : (↑φ).comp (eval ι v) = eval ιK (⇑φ ∘ v)

G-homomorphisms commute with evaluation, as homomorphisms out of G[X].

def TauCeti.GroupAlgGeom.wordMap {G : Type u_1} {H : Type u_2} [Group G] [Group H] {X : Type u_5} {Y : Type u_6} (ι : G →* H) (w : Y → GX G X) (v : X → H) : Y → H

The word map determined by a tuple of words.

@[simp]

theorem TauCeti.GroupAlgGeom.wordMap_apply {G : Type u_1} {H : Type u_2} [Group G] [Group H] {X : Type u_5} {ι : G →* H} {Y : Type u_6} (w : Y → GX G X) (v : X → H) (y : Y) : wordMap ι w v y = (eval ι v) (w y)

Evaluating the word map at a coordinate evaluates its defining word.

theorem TauCeti.GroupAlgGeom.eval_comp_eval {G : Type u_1} {H : Type u_2} [Group G] [Group H] {X : Type u_5} {ι : G →* H} {Y : Type u_6} (w : Y → GX G X) (v : X → H) : (eval ι v).comp (eval Monoid.Coprod.inl w) = eval ι (wordMap ι w v)

Substituting words for variables and then evaluating agrees with evaluation of the substituted tuple.

theorem TauCeti.GroupAlgGeom.wordMap_wordMap {G : Type u_1} {H : Type u_2} [Group G] [Group H] {X : Type u_5} {ι : G →* H} {Y : Type u_6} {Z : Type u_7} (w : Y → GX G X) (u : Z → GX G Y) (v : X → H) : wordMap ι u (wordMap ι w v) = wordMap ι (fun (z : Z) => (eval Monoid.Coprod.inl w) (u z)) v

Composition of word maps is substitution of the defining words.

theorem TauCeti.GroupAlgGeom.eval_wordMap {G : Type u_1} {H : Type u_2} [Group G] [Group H] {X : Type u_5} {ι : G →* H} {Y : Type u_6} (σ : GHom Monoid.Coprod.inl Monoid.Coprod.inl) (v : X → H) : eval ι (wordMap ι (fun (y : Y) => σ (Monoid.Coprod.inr (FreeGroup.of y))) v) = (eval ι v).comp σ.toMonoidHom

Evaluation after a word map is composition with the word homomorphism.

@[simp]

theorem TauCeti.GroupAlgGeom.wordMap_id {G : Type u_1} {H : Type u_2} [Group G] [Group H] {X : Type u_5} {ι : G →* H} (v : X → H) : wordMap ι (fun (x : X) => Monoid.Coprod.inr (FreeGroup.of x)) v = v

The identity word homomorphism leaves tuples unchanged.

theorem TauCeti.GroupAlgGeom.wordMap_comp {G : Type u_1} {H : Type u_2} [Group G] [Group H] {X : Type u_5} {ι : G →* H} {Z : Type u_6} {Y : Type u_7} (σ : GHom Monoid.Coprod.inl Monoid.Coprod.inl) (τ : GHom Monoid.Coprod.inl Monoid.Coprod.inl) (v : X → H) : wordMap ι (fun (z : Z) => (τ.comp σ) (Monoid.Coprod.inr (FreeGroup.of z))) v = wordMap ι (fun (y : Z) => σ (Monoid.Coprod.inr (FreeGroup.of y))) (wordMap ι (fun (x : Y) => τ (Monoid.Coprod.inr (FreeGroup.of x))) v)

Word maps compose in the opposite order to word homomorphisms.

@[simp]

theorem TauCeti.GroupAlgGeom.map_eval {G : Type u_1} {H : Type u_2} {K : Type u_3} [Group G] [Group H] [Group K] {X : Type u_5} {ι : G →* H} {v : X → H} {ιK : G →* K} (φ : GHom ι ιK) (w : GX G X) : φ ((eval ι v) w) = (eval ιK (⇑φ ∘ v)) w

G-homomorphisms commute with evaluation: φ (w(v)) = w(φ ∘ v).

theorem TauCeti.GroupAlgGeom.eval_comp_map {G : Type u_1} {H : Type u_2} {K : Type u_3} [Group G] [Group H] [Group K] {X : Type u_5} {ι : G →* H} {v : X → H} {Y : Type u_6} (f : K →* G) (e : Y → X) : (eval ι v).comp (Monoid.Coprod.map f (FreeGroup.map e)) = eval (ι.comp f) (v ∘ e)

Changing the coefficients along f : K →* G and renaming the variables along e : Y → X before evaluating at v is evaluation at v ∘ e with coefficients ι ∘ f.

@[simp]

theorem TauCeti.GroupAlgGeom.eval_map {G : Type u_1} {H : Type u_2} {K : Type u_3} [Group G] [Group H] [Group K] {X : Type u_5} {ι : G →* H} {v : X → H} {Y : Type u_6} (f : K →* G) (e : Y → X) (w : GX K Y) : (eval ι v) ((Monoid.Coprod.map f (FreeGroup.map e)) w) = (eval (ι.comp f) (v ∘ e)) w

Degenerate cases and noncommutativity of G[X]

def TauCeti.GroupAlgGeom.GX.equivOfIsEmpty {G : Type u_1} [Group G] {X : Type u_5} [IsEmpty X] : GX G X ≃* G

With no variables, G[X] is G.

@[simp]

theorem TauCeti.GroupAlgGeom.GX.equivOfIsEmpty_apply {G : Type u_1} [Group G] {X : Type u_5} [IsEmpty X] (w : GX G X) : equivOfIsEmpty w = Monoid.Coprod.fst w

@[simp]

theorem TauCeti.GroupAlgGeom.GX.equivOfIsEmpty_symm_apply {G : Type u_1} [Group G] {X : Type u_5} [IsEmpty X] (g : G) : equivOfIsEmpty.symm g = Monoid.Coprod.inl g

def TauCeti.GroupAlgGeom.GX.equivFreeGroup (G : Type u_1) [Group G] (X : Type u_5) [Subsingleton G] : GX G X ≃* FreeGroup X

Over trivial coefficients, G[X] is the free group F(X).

@[simp]

theorem TauCeti.GroupAlgGeom.GX.equivFreeGroup_apply {G : Type u_1} [Group G] {X : Type u_5} [Subsingleton G] (w : GX G X) : (equivFreeGroup G X) w = Monoid.Coprod.snd w

@[simp]

theorem TauCeti.GroupAlgGeom.GX.equivFreeGroup_symm_apply {G : Type u_1} [Group G] {X : Type u_5} [Subsingleton G] (w : FreeGroup X) : (equivFreeGroup G X).symm w = Monoid.Coprod.inr w

theorem TauCeti.GroupAlgGeom.GX.eval_eq_lift_equivFreeGroup {G : Type u_1} {H : Type u_2} [Group G] [Group H] {X : Type u_5} [Subsingleton G] (ι : G →* H) (v : X → H) (w : GX G X) : (eval ι v) w = (FreeGroup.lift v) ((equivFreeGroup G X) w)

Over trivial coefficients, evaluation is FreeGroup.lift through G[X] ≅ F(X).

theorem TauCeti.GroupAlgGeom.GX.not_commute_inl_inr_of {G : Type u_1} [Group G] {X : Type u_5} {a : G} (ha : a ≠ 1) (x : X) : ¬Commute (Monoid.Coprod.inl a) (Monoid.Coprod.inr (FreeGroup.of x))

A nontrivial coefficient does not commute with a variable in G[X]; in particular the inclusions of G and F(X) do not commute, unlike in the direct product G × F(X).

Examples

theorem TauCeti.GroupAlgGeom.eval_commutator : have a := FreeGroup.of 0; have w := Monoid.Coprod.inr (FreeGroup.of ()) * Monoid.Coprod.inl a * (Monoid.Coprod.inr (FreeGroup.of ()))⁻¹ * (Monoid.Coprod.inl a)⁻¹; (eval (MonoidHom.id (FreeGroup (Fin 2))) fun (x : Unit) => a ^ 2) w = 1 ∧ (eval (MonoidHom.id (FreeGroup (Fin 2))) fun (x : Unit) => FreeGroup.of 1) w ≠ 1

Over G = F(a, b) with one variable x, the commutator x a x⁻¹ a⁻¹ vanishes at x = a² but not at x = b.