Normalizers and commutators tested on generating sets

Subgroups presented by generators are controlled by inspecting generators only. Conjugation and commutation are not preserved by products, so the first two results below carry an auxiliary normalizing hypothesis. The last result uses a commutator relation to propagate membership along an ordered finite index set.

Mathlib has Subgroup.le_normalizer_closure_iff, which tests the conjugated subgroup on generators but still quantifies over the whole conjugating subgroup, and Subgroup.commutator_le, which quantifies over both subgroups. Neither reduces a comparison to generators on both sides.

Main results

• TauCeti.closure_le_normalizer_closure: a subgroup generated by X normalizes a subgroup generated by Y as soon as the generators of X conjugate those of Y into it, in both directions.
• TauCeti.commutator_closure_closure_le: the commutator of two subgroups presented by generators lies in a subgroup normalized by both, as soon as the commutators of the generators do.
• TauCeti.commutator_closure_le_iff: for a normal target, the commutator of a subgroup with a subgroup presented by generators is tested on those generators.
• TauCeti.commutator_le_iff_map_mk'_eq_bot: ⁅A, B⁆ ≤ N for a normal N says that the images of A and B in G ⧸ N commute.
• QuotientGroup.commute_mk_iff: two classes in G ⧸ N commute exactly when the commutator of representatives lies in N.
• MonoidHom.commutatorElement_mem_ker_iff: the images of two elements under a homomorphism into a monoid commute exactly when their commutator lies in the kernel.
• TauCeti.commutatorElement_pow_right_mem_iff: when ⁅a, y⁆ commutes with y modulo a normal N, the commutator ⁅a, y ^ n⁆ lies in N exactly when ⁅a, y⁆ ^ n does.
• TauCeti.commutatorElement_mul_mul_eq_mul_of_commute: the commutator of two paired products splits into the product of their same-position commutators when the required cross terms commute.
• Commute.mul_pow_eq_pow_mul_pow_mul_commutatorElement_pow_choose_two: the binomial formula (a * b) ^ n = a ^ n * b ^ n * ⁅b, a⁆ ^ (n choose 2) when ⁅b, a⁆ commutes with a and b.
• Commute.inv_pow_mul_pow_mul_pow_eq_commutatorElement_pow_mul_pow: conjugating b ^ n by a ^ k multiplies it by ⁅b, a⁆ ^ (k * n) when ⁅b, a⁆ commutes with a and b.
• Commute.mul_pow_two_mul_add_one_eq_pow_mul_inv_pow_mul_pow_mul_pow: under the same hypotheses, (a * b) ^ (2 * k + 1) is a ^ (2 * k + 1) times the conjugate of b ^ (2 * k + 1) by a ^ k.
• TauCeti.commutatorElement_pow_left_of_commute, TauCeti.commutatorElement_pow_right_of_commute: the collection formulas ⁅a ^ n, b⁆ = ⁅a, b⁆ ^ n * ⁅a, ⁅a, b⁆⁆ ^ (n choose 2) and ⁅a, b ^ n⁆ = ⁅a, b⁆ ^ n * ⁅b, ⁅a, b⁆⁆ ^ (n choose 2) when the iterated commutator commutes with ⁅a, b⁆ and with the powered input, for instance when it is central.
• TauCeti.commute_commutatorElement_of_inv_mul_mul_mem_zpowers: two elements conjugating g into ⟨g⟩ have a commutator that centralizes g.
• Subgroup.mem_of_adjacent_of_commutator: a structure-constant-one family indexed by ordered pairs of Fin m is generated by its adjacent members.
• TauCeti.isMulCommutative_of_forall_exists_monoidHom_apply_ne_one: homomorphisms into a commutative monoid separate the elements of G only when G is commutative, since each of them kills every commutator.

References

• R. W. Carter, Simple Groups of Lie Type, §5.3.

theorem TauCeti.commutatorElement_mul_mul_eq_mul_of_commute {G : Type u_1} [Group G] {a b c d : G} (hbc : Commute b c) (had : Commute a d) (hcbd : Commute c ⁅b, d⁆) (habd : Commute a ⁅b, d⁆) (hcomm : Commute ⁅a, c⁆ ⁅b, d⁆) : ⁅a * b, c * d⁆ = ⁅a, c⁆ * ⁅b, d⁆

The commutator of two paired products splits into the product of the same-position commutators when the cross terms and the resulting commutators commute as required.

theorem Commute.mul_pow_eq_pow_mul_pow_mul_commutatorElement_pow_choose_two {G : Type u_1} [Group G] {a b : G} (ha : Commute a ⁅b, a⁆) (hb : Commute b ⁅b, a⁆) (n : ℕ) : (a * b) ^ n = a ^ n * b ^ n * ⁅b, a⁆ ^ n.choose 2

The binomial formula of nilpotency class two: when the commutator ⁅b, a⁆ commutes with a and with b, for instance when it is central, (a * b) ^ n = a ^ n * b ^ n * ⁅b, a⁆ ^ (n choose 2).

theorem Commute.inv_pow_mul_pow_mul_pow_eq_commutatorElement_pow_mul_pow {G : Type u_1} [Group G] {a b : G} (ha : Commute a ⁅b, a⁆) (hb : Commute b ⁅b, a⁆) (k n : ℕ) : (a ^ k)⁻¹ * b ^ n * a ^ k = ⁅b, a⁆ ^ (k * n) * b ^ n

Conjugating a power in nilpotency class two: when the commutator ⁅b, a⁆ commutes with a and with b, for instance when it is central, conjugating b ^ n by a ^ k multiplies it by ⁅b, a⁆ ^ (k * n).

theorem Commute.mul_pow_two_mul_add_one_eq_pow_mul_inv_pow_mul_pow_mul_pow {G : Type u_1} [Group G] {a b : G} (ha : Commute a ⁅b, a⁆) (hb : Commute b ⁅b, a⁆) (k : ℕ) : (a * b) ^ (2 * k + 1) = a ^ (2 * k + 1) * ((a ^ k)⁻¹ * b ^ (2 * k + 1) * a ^ k)

Odd powers of a product in nilpotency class two: when the commutator ⁅b, a⁆ commutes with a and with b, for instance when it is central, (a * b) ^ (2 * k + 1) is a ^ (2 * k + 1) times the conjugate of b ^ (2 * k + 1) by a ^ k. The commutator correction ⁅b, a⁆ ^ ((2 * k + 1) choose 2) of the binomial formula is exactly the one produced by this conjugation.

theorem TauCeti.commutatorElement_pow_left_of_commute {G : Type u_1} [Group G] {a b : G} (ha : Commute a ⁅a, ⁅a, b⁆⁆) (hc : Commute ⁅a, b⁆ ⁅a, ⁅a, b⁆⁆) (n : ℕ) : ⁅a ^ n, b⁆ = ⁅a, b⁆ ^ n * ⁅a, ⁅a, b⁆⁆ ^ n.choose 2

Collection of a power in the left input: when the iterated commutator ⁅a, ⁅a, b⁆⁆ commutes with a and with ⁅a, b⁆, for instance when it is central, ⁅a ^ n, b⁆ = ⁅a, b⁆ ^ n * ⁅a, ⁅a, b⁆⁆ ^ (n choose 2).

theorem TauCeti.commutatorElement_pow_right_of_commute {G : Type u_1} [Group G] {a b : G} (hb : Commute b ⁅b, ⁅a, b⁆⁆) (hc : Commute ⁅a, b⁆ ⁅b, ⁅a, b⁆⁆) (n : ℕ) : ⁅a, b ^ n⁆ = ⁅a, b⁆ ^ n * ⁅b, ⁅a, b⁆⁆ ^ n.choose 2

Collection of a power in the right input: when the iterated commutator ⁅b, ⁅a, b⁆⁆ commutes with b and with ⁅a, b⁆, for instance when it is central, ⁅a, b ^ n⁆ = ⁅a, b⁆ ^ n * ⁅b, ⁅a, b⁆⁆ ^ (n choose 2).

theorem TauCeti.commute_commutatorElement_of_inv_mul_mul_mem_zpowers {G : Type u_1} [Group G] {g x y : G} (hx : x⁻¹ * g * x ∈ Subgroup.zpowers g) (hy : y⁻¹ * g * y ∈ Subgroup.zpowers g) : Commute ⁅x, y⁆ g

If x and y both conjugate g into the cyclic subgroup it generates, then their commutator ⁅x, y⁆ centralizes g. Such elements act on ⟨g⟩ through power maps, and power maps commute with each other.

theorem TauCeti.closure_le_normalizer_closure {G : Type u_1} [Group G] {X Y : Set G} (h : ∀ x ∈ X, ∀ y ∈ Y, x * y * x⁻¹ ∈ Subgroup.closure Y) (hinv : ∀ x ∈ X, ∀ y ∈ Y, x⁻¹ * y * x ∈ Subgroup.closure Y) : Subgroup.closure X ≤ Subgroup.normalizer ↑(Subgroup.closure Y)

A subgroup generated by X normalizes a subgroup generated by Y as soon as every generator of X conjugates every generator of Y into the latter, in both directions.

Both directions are genuinely needed: for an infinitely generated subgroup, a single inclusion g (closure Y) g⁻¹ ≤ closure Y does not place g in the normalizer. When X is closed under inverses the second hypothesis is the first one read at x⁻¹.

theorem TauCeti.commutator_closure_closure_le {G : Type u_1} [Group G] {X Y : Set G} {N : Subgroup G} (hX : Subgroup.closure X ≤ Subgroup.normalizer ↑N) (hY : Subgroup.closure Y ≤ Subgroup.normalizer ↑N) (h : ∀ x ∈ X, ∀ y ∈ Y, ⁅x, y⁆ ∈ N) : ⁅Subgroup.closure X, Subgroup.closure Y⁆ ≤ N

Commutators of generators control the commutator subgroup, provided the target subgroup is normalized by both factors.

The normalizing hypotheses are what makes the induction go through: expanding ⁅x, y₁ y₂⁆ and ⁅x₁ x₂, y⁆ produces conjugates of commutators by elements of closure Y and of closure X respectively.

theorem TauCeti.commutator_closure_le_iff {G : Type u_1} [Group G] {Y : Set G} {N : Subgroup G} [N.Normal] {A : Subgroup G} : ⁅A, Subgroup.closure Y⁆ ≤ N ↔ ∀ a ∈ A, ∀ y ∈ Y, ⁅a, y⁆ ∈ N

For a normal target, the commutator of a subgroup A with the subgroup generated by Y is tested on the generators: ⁅A, closure Y⁆ ≤ N exactly when ⁅a, y⁆ ∈ N for all a ∈ A and y ∈ Y.

theorem TauCeti.commutator_le_iff_map_mk'_eq_bot {G : Type u_1} [Group G] {N A B : Subgroup G} [N.Normal] : ⁅A, B⁆ ≤ N ↔ ⁅Subgroup.map (QuotientGroup.mk' N) A, Subgroup.map (QuotientGroup.mk' N) B⁆ = ⊥

For a normal subgroup N, the commutator ⁅A, B⁆ lies in N exactly when the images of A and B in the quotient G ⧸ N commute.

theorem QuotientGroup.commute_mk_iff {G : Type u_1} [Group G] {N : Subgroup G} [N.Normal] {a b : G} : Commute ↑a ↑b ↔ ⁅a, b⁆ ∈ N

Two classes in G ⧸ N commute exactly when the commutator of representatives lies in N.

theorem MonoidHom.commutatorElement_mem_ker_iff {G : Type u_1} [Group G] {M : Type u_2} [Monoid M] (f : G →* M) {a b : G} : ⁅a, b⁆ ∈ f.ker ↔ Commute (f a) (f b)

The images of a and b under a homomorphism f into a monoid commute exactly when the commutator ⁅a, b⁆ lies in the kernel of f. For f the quotient map this is QuotientGroup.commute_mk_iff; the target need not be a group, since f lands in its units.

theorem TauCeti.isMulCommutative_of_forall_exists_monoidHom_apply_ne_one {G : Type u_1} [Group G] {A : Type u_2} [CommMonoid A] (h : ∀ (g : G), g ≠ 1 → ∃ (φ : G →* A), φ g ≠ 1) : IsMulCommutative G

Homomorphisms into a commutative monoid separate elements only in a commutative group. If for every g ≠ 1 some homomorphism φ : G →* A into a commutative monoid has φ g ≠ 1, then G is commutative: such a φ sends every commutator ⁅a, b⁆ to φ a * φ b * φ a⁻¹ * φ b⁻¹ = (φ a * φ a⁻¹) * (φ b * φ b⁻¹) = 1, so no commutator can differ from 1. This is the converse of Mathlib's exists_apply_ne_one_of_hasEnoughRootsOfUnity, and it needs neither finiteness, nor roots of unity, nor inverses in A.

theorem TauCeti.commutatorElement_pow_right_mem_iff {G : Type u_1} [Group G] {N : Subgroup G} [N.Normal] {a y : G} (h : ⁅⁅a, y⁆, y⁆ ∈ N) (n : ℕ) : ⁅a, y ^ n⁆ ∈ N ↔ ⁅a, y⁆ ^ n ∈ N

If the commutator ⁅a, y⁆ commutes with y modulo a normal subgroup N, then modulo N the commutator ⁅a, y ^ n⁆ is the power ⁅a, y⁆ ^ n: one lies in N exactly when the other does.

Pair-indexed families generated by adjacent members

theorem Subgroup.mem_of_adjacent_of_commutator {G : Type u_1} [Group G] {P : Type u_2} [One P] {m : ℕ} (H : Subgroup G) (x : {i j : Fin m} → i ≠ j → P → G) (hcomm : ∀ {i j k : Fin m} (hij : i ≠ j) (hjk : j ≠ k) (hik : i ≠ k) (a : P), ⁅x hij a, x hjk 1⁆ = x hik a) (hadjacent : ∀ {i j : Fin m} (hij : i ≠ j) (a : P), ↑i + 1 = ↑j ∨ ↑j + 1 = ↑i → x hij a ∈ H) {i j : Fin m} (hij : i ≠ j) (a : P) : x hij a ∈ H

Suppose elements xᵢⱼ(a) indexed by distinct pairs in Fin m satisfy the relation

⁅xᵢⱼ(a), xⱼₖ(1)⁆ = xᵢₖ(a).

If a subgroup contains xᵢⱼ(a) whenever i and j are adjacent, in both orientations, then it contains every xᵢⱼ(a).