CSA groups

A group is CSA if its maximal abelian subgroups are malnormal. The centralizer of a nonidentity element in such a group is its unique maximal abelian subgroup containing that element. In particular, commutation is transitive through a nonidentity element. In a torsion-free commutative-transitive group roots are unique and no nonidentity element is conjugate to its inverse. In a torsion-free CSA group, conjugates of nontrivial powers of u ≠ 1 by elements of different cosets of the centralizer of u do not commute. A group is CSA exactly when it is commutative transitive and every nonidentity element commuting with one of its conjugates g * x * g⁻¹ commutes with g. Consequently, given two noncommuting elements a and b, the disjunction x = 1 ∨ y = 1 is equivalent to x commuting with y, a * y * a⁻¹ and b * y * b⁻¹. A failure of either condition is witnessed by a nonidentity element together with a nontrivial commutator, so both conditions pass to any group in which every pair of nonidentity elements survives under one homomorphism to a CSA group. This is how fully residually free groups inherit the CSA property from free groups. These properties are useful for the centralizers and equations of free groups and limit groups.

The definition follows Baumslag, Myasnikov and Remeslennikov, Algebraic geometry over groups I, §§1–2.

def Group.IsCSA (G : Type u_1) [Group G] : Prop

A group is CSA if each maximal abelian subgroup is malnormal.

def Group.IsCommTransitive (G : Type u_1) [Group G] : Prop

Commutation in a group is transitive when the middle element is nonidentity.

theorem Group.isCSA_iff (G : Type u_1) [Group G] : IsCSA G ↔ ∀ (M : Subgroup G), Maximal (fun (K : Subgroup G) => IsMulCommutative ↥K) M → TauCeti.IsTISubgroup M

The defining malnormality condition for a CSA group.

theorem Group.isCommTransitive_iff (G : Type u_1) [Group G] : IsCommTransitive G ↔ ∀ (x y z : G), y ≠ 1 → Commute x y → Commute y z → Commute x z

The defining condition for commutation transitivity.

theorem Group.IsCSA.of_commGroup {G : Type u_1} [Group G] [IsMulCommutative G] : IsCSA G

Every abelian group is CSA.

theorem Group.IsCSA.eq_centralizer_of_mem {G : Type u_1} [Group G] (hG : IsCSA G) {M : Subgroup G} (hM : Maximal (fun (K : Subgroup G) => IsMulCommutative ↥K) M) {y : G} (hyM : y ∈ M) (hy : y ≠ 1) : M = Subgroup.centralizer {y}

A maximal abelian subgroup in a CSA group is the centralizer of each of its nonidentity elements. Hence it is the unique maximal abelian subgroup containing such an element.

theorem Group.IsCSA.centralizer_isMaximalAbelian {G : Type u_1} [Group G] (hG : IsCSA G) {y : G} (hy : y ≠ 1) : Maximal (fun (K : Subgroup G) => IsMulCommutative ↥K) (Subgroup.centralizer {y})

The centralizer of a nonidentity element in a CSA group is maximal abelian.

theorem Group.IsCSA.centralizer_isMulCommutative {G : Type u_1} [Group G] (hG : IsCSA G) {y : G} (hy : y ≠ 1) : IsMulCommutative ↥(Subgroup.centralizer {y})

The centralizer of a nonidentity element in a CSA group is abelian.

theorem Group.IsCSA.centralizer_isTISubgroup {G : Type u_1} [Group G] (hG : IsCSA G) (y : G) : TauCeti.IsTISubgroup (Subgroup.centralizer {y})

The centralizer of an element in a CSA group is malnormal.

theorem Group.isCommTransitive_iff_centralizer_isMulCommutative {G : Type u_1} [Group G] : IsCommTransitive G ↔ ∀ (y : G), y ≠ 1 → IsMulCommutative ↥(Subgroup.centralizer {y})

Commutation is transitive through a nonidentity element exactly when every nonidentity element has an abelian centralizer.

theorem Group.IsCSA.isCommTransitive {G : Type u_1} [Group G] (hG : IsCSA G) : IsCommTransitive G

CSA groups have transitive commutation through every nonidentity element.

theorem Group.isCSA_iff_isCommTransitive_and_commute_conj {G : Type u_1} [Group G] : IsCSA G ↔ IsCommTransitive G ∧ ∀ (x g : G), x ≠ 1 → Commute x (g * x * g⁻¹) → Commute x g

Elementwise characterization of CSA groups. A group is CSA exactly when commutation is transitive through nonidentity elements and every nonidentity element x commuting with a conjugate g * x * g⁻¹ commutes with g.

theorem Group.IsCSA.mem_centralizer_of_commute_conj {G : Type u_1} [Group G] (hG : IsCSA G) {u x y g : G} (hx : x ∈ Subgroup.centralizer {u}) (hx1 : x ≠ 1) (hy : y ∈ Subgroup.centralizer {u}) (hy1 : y ≠ 1) (h : Commute x (g * y * g⁻¹)) : g ∈ Subgroup.centralizer {u}

In a CSA group, if a nonidentity element x of the centralizer of u commutes with a conjugate g * y * g⁻¹ of another nonidentity element y of that centralizer, then g centralizes u.

theorem Group.IsCSA.not_commute_conj_zpow {G : Type u_1} [Group G] (hG : IsCSA G) [IsMulTorsionFree G] {u y y' : G} {e e' : ℤ} (he : e ≠ 0) (he' : e' ≠ 0) (hy : y⁻¹ * y' ∉ Subgroup.centralizer {u}) : ¬Commute (y * u ^ e * y⁻¹) (y' * u ^ e' * y'⁻¹)

In a torsion-free CSA group, conjugates of nonzero powers of u by y and y' do not commute unless y⁻¹ * y' centralizes u.

theorem Group.IsCSA.exists_inv_mul_notMem_centralizer {G : Type u_1} [Group G] (hG : IsCSA G) {u g : G} (hu : u ≠ 1) (hg : g ∉ Subgroup.centralizer {u}) (a b : G) : ∃ (W : G), a⁻¹ * W ∉ Subgroup.centralizer {u} ∧ b⁻¹ * W ∉ Subgroup.centralizer {u}

In a CSA group, if some element lies outside the centralizer C_G(u) of u ≠ 1, then G is not covered by two left cosets a * C_G(u) and b * C_G(u); this uses malnormality of C_G(u).

theorem Group.IsCSA.eq_one_or_eq_one_iff_commute_conj {G : Type u_1} [Group G] (hG : IsCSA G) {a b x y : G} (hab : ¬Commute a b) : x = 1 ∨ y = 1 ↔ Commute x y ∧ Commute x (a * y * a⁻¹) ∧ Commute x (b * y * b⁻¹)

In a CSA group with two noncommuting elements a and b, an element x is trivial or y is trivial exactly when x commutes with y, a * y * a⁻¹ and b * y * b⁻¹. This expresses the disjunction x = 1 ∨ y = 1 by three equations.

theorem Group.IsCommTransitive.not_isConj_inv {G : Type u_1} [Group G] [IsMulTorsionFree G] (hG : IsCommTransitive G) {x : G} (hx : x ≠ 1) : ¬IsConj x x⁻¹

In a torsion-free commutative-transitive group, a nonidentity element is not conjugate to its inverse.

theorem Group.IsCommTransitive.hasUniqueRoots {G : Type u_1} [Group G] [IsMulTorsionFree G] (hG : IsCommTransitive G) : HasUniqueRoots G

A torsion-free commutative-transitive group has unique roots: for all x and y, if x ^ n = y ^ n with n ≠ 0, then x = y.

theorem Group.IsCommTransitive.center_eq_bot {G : Type u_1} [Group G] (hG : IsCommTransitive G) (h : ¬IsMulCommutative G) : Subgroup.center G = ⊥

A nonabelian commutative-transitive group has trivial center.

theorem Group.IsCSA.center_eq_bot {G : Type u_1} [Group G] (hG : IsCSA G) (h : ¬IsMulCommutative G) : Subgroup.center G = ⊥

A nonabelian CSA group has trivial center.

theorem Group.IsCSA.of_injective {G : Type u_1} [Group G] {H : Type u_2} [Group H] (hG : IsCSA G) (f : H →* G) (hf : Function.Injective ⇑f) : IsCSA H

An injective homomorphism into a CSA group has CSA domain.

theorem Group.IsCommTransitive.of_forall_exists_monoidHom {G : Type u_1} [Group G] {H : Type u_2} [Group H] (hH : IsCommTransitive H) (h : ∀ (a b : G), a ≠ 1 → b ≠ 1 → ∃ (φ : G →* H), φ a ≠ 1 ∧ φ b ≠ 1) : IsCommTransitive G

Commutation transitivity passes from H to G when any two nonidentity elements of G survive together under some homomorphism G →* H.

theorem Group.IsCSA.of_forall_exists_monoidHom {G : Type u_1} [Group G] {H : Type u_2} [Group H] (hH : IsCSA H) (h : ∀ (a b : G), a ≠ 1 → b ≠ 1 → ∃ (φ : G →* H), φ a ≠ 1 ∧ φ b ≠ 1) : IsCSA G

Being CSA passes from H to G when any two nonidentity elements of G survive together under some homomorphism G →* H. In particular a group discriminated by a CSA group is CSA.

theorem Group.not_isCommTransitive_prod_of_nontrivial {G : Type u_1} [Group G] {C : Type u_2} [Group C] [Nontrivial C] (hG : ¬IsMulCommutative G) : ¬IsCommTransitive (G × C)

If G is nonabelian and C is nontrivial, then G × C is not commutative transitive.

theorem Group.not_isCSA_prod_of_nontrivial {G : Type u_1} [Group G] {C : Type u_2} [Group C] [Nontrivial C] (hG : ¬IsMulCommutative G) : ¬IsCSA (G × C)

If G is nonabelian and C is nontrivial, then G × C is not CSA.