Derived words and solvable groups

The nth derived word evaluates a perfect binary argument tree of depth n by balanced commutators: the zeroth word is one group element, and the successor word is the commutator of two copies of the preceding word. This file proves that its values generate the nth derived subgroup. Consequently, a group is solvable exactly when one derived word is identically one. It also records the characterization of solvability for direct products via the two surjective projections and the converse product instance.

The identity formulation is useful when a group is represented by an affine scheme: an identity between derived words can be checked on a schematically dense family of points, while the subgroup-valued definition of the derived series cannot be compared pointwise in that way.

Main declarations

• TauCeti.isSolvable_prod_iff: G × H is solvable if and only if both G and H are.
• TauCeti.DerivedWordArgs: the recursively paired arguments of a derived word.
• TauCeti.derivedWord: the balanced iterated commutator word.
• TauCeti.map_derivedWord: derived words commute with group homomorphisms.
• TauCeti.derivedSeries_eq_closure_range_derivedWord: the values of the nth derived word generate the nth derived subgroup.
• TauCeti.derivedWord_mem_derivedSeries: derived-word values lie in the corresponding derived subgroup.
• TauCeti.derivedSeries_eq_bot_iff_derivedWord_eq_one: a fixed derived subgroup vanishes exactly when its derived word is identically one.
• TauCeti.isSolvable_iff_exists_derivedWord_eq_one: solvability is equivalent to a derived-word identity.

This is a prerequisite for descending geometric solvability along schematically dense morphisms from smooth affine groups. That descent supplies the multiplication-image step in the construction of the solvable radical in Layer 6 of the ReductiveGroups roadmap.

@[simp]

theorem TauCeti.isSolvable_prod_iff {G : Type u_1} {H : Type u_2} [Group G] [Group H] : Group.IsSolvable (G × H) ↔ Group.IsSolvable G ∧ Group.IsSolvable H

A direct product of groups is solvable exactly when both of its factors are.

inductive TauCeti.DerivedWordArgs (G : Type u) : ℕ → Type u

The argument trees for derived words. A tree at depth zero is one group element, and a tree at successor depth consists of two argument trees of the preceding depth.

• leaf {G : Type u} : G → DerivedWordArgs G 0
• node {G : Type u} {n : ℕ} : DerivedWordArgs G n → DerivedWordArgs G n → DerivedWordArgs G (n + 1)

def TauCeti.DerivedWordArgs.map {G : Type u} {H : Type v} (f : G → H) (n : ℕ) : DerivedWordArgs G n → DerivedWordArgs H n

Apply a function to every entry in the arguments of a derived word.

Equations

• TauCeti.DerivedWordArgs.map f 0 (TauCeti.DerivedWordArgs.leaf x_2) = TauCeti.DerivedWordArgs.leaf (f x_2)
• TauCeti.DerivedWordArgs.map f n.succ (x_2.node y) = (TauCeti.DerivedWordArgs.map f n x_2).node (TauCeti.DerivedWordArgs.map f n y)

@[simp]

theorem TauCeti.DerivedWordArgs.map_leaf {G : Type u} {H : Type v} (f : G → H) (x : G) : map f 0 (leaf x) = leaf (f x)

@[simp]

theorem TauCeti.DerivedWordArgs.map_node {G : Type u} {H : Type v} (f : G → H) (n : ℕ) (x y : DerivedWordArgs G n) : map f (n + 1) (x.node y) = (map f n x).node (map f n y)

@[simp]

theorem TauCeti.DerivedWordArgs.map_id {G : Type u} (n : ℕ) (x : DerivedWordArgs G n) : map id n x = x

Mapping the identity function leaves derived-word arguments unchanged.

theorem TauCeti.DerivedWordArgs.map_comp {G : Type u} {H : Type v} {K : Type u_1} (g : H → K) (f : G → H) (n : ℕ) (x : DerivedWordArgs G n) : map (g ∘ f) n x = map g n (map f n x)

Successive maps of derived-word arguments compose pointwise.

def TauCeti.derivedWord (G : Type u) [Group G] (n : ℕ) : DerivedWordArgs G n → G

Evaluate a depth-n argument tree by balanced commutators: a leaf evaluates to its element, and a node to the commutator of the values of its two subtrees. Its values generate derivedSeries G n (derivedSeries_eq_closure_range_derivedWord).

Equations

• TauCeti.derivedWord G 0 (TauCeti.DerivedWordArgs.leaf x_2) = x_2
• TauCeti.derivedWord G n.succ (x_2.node y) = ⁅TauCeti.derivedWord G n x_2, TauCeti.derivedWord G n y⁆

@[simp]

theorem TauCeti.derivedWord_leaf (G : Type u) [Group G] (x : G) : derivedWord G 0 (DerivedWordArgs.leaf x) = x

@[simp]

theorem TauCeti.derivedWord_node (G : Type u) [Group G] (n : ℕ) (x y : DerivedWordArgs G n) : derivedWord G (n + 1) (x.node y) = ⁅derivedWord G n x, derivedWord G n y⁆

@[simp]

theorem TauCeti.map_derivedWord {G : Type u} {H : Type v} {F : Type u_1} [Group G] [Group H] [FunLike F G H] [MonoidHomClass F G H] (f : F) (n : ℕ) (x : DerivedWordArgs G n) : f (derivedWord G n x) = derivedWord H n (DerivedWordArgs.map (⇑f) n x)

Derived words commute with group homomorphisms.

theorem TauCeti.derivedSeries_eq_closure_range_derivedWord (G : Type u) [Group G] (n : ℕ) : derivedSeries G n = Subgroup.closure (Set.range (derivedWord G n))

The values of the nth derived word generate the nth derived subgroup.

theorem TauCeti.derivedWord_mem_derivedSeries (G : Type u) [Group G] (n : ℕ) (x : DerivedWordArgs G n) : derivedWord G n x ∈ derivedSeries G n

Every value of the nth derived word belongs to the nth derived subgroup.

theorem TauCeti.derivedSeries_eq_bot_iff_derivedWord_eq_one (G : Type u) [Group G] (n : ℕ) : derivedSeries G n = ⊥ ↔ ∀ (x : DerivedWordArgs G n), derivedWord G n x = 1

The nth derived subgroup is trivial exactly when the nth derived word is identically one.

theorem TauCeti.isSolvable_iff_exists_derivedWord_eq_one (G : Type u) [Group G] : Group.IsSolvable G ↔ ∃ (n : ℕ), ∀ (x : DerivedWordArgs G n), derivedWord G n x = 1

A group is solvable exactly when some derived word is identically one.