Documentation

TauCeti.GroupTheory.FreeGroup.CSA

Free groups are CSA #

Let u be a nontrivial element of a free group which is not a proper power. Then the cyclic subgroup zpowers u is a maximal abelian subgroup, and it is malnormal: an element conjugating a nonidentity power of u back into zpowers u already lies in zpowers u. Since every maximal abelian subgroup of a nontrivial free group is of this form, every free group is a CSA group, and commutation is transitive on its nontrivial elements.

The hypothesis that u is not a proper power is needed: for u = a ^ 2 the element a lies outside zpowers u but commutes with u. Both malnormality and maximality characterize the non-proper-powers among the nontrivial elements.

The argument avoids reduced words. If g * u ^ m * g⁻¹ = u ^ n with u ^ m ≠ 1, commutation transitivity through u ^ n shows that g * u * g⁻¹ commutes with u, so it lies in zpowers u, the centralizer of u. Since g * u * g⁻¹ is not a proper power, it is u or u⁻¹. A nontrivial element of a free group is not conjugate to its inverse (Group.IsCommTransitive.not_isConj_inv), so g commutes with u and lies in zpowers u.

The file also records two groups built from free groups that are not CSA. First, FreeGroup (Fin 2) × Multiplicative ℤ: the free group on two generators is nonabelian, but its product with a nontrivial abelian group has a nonidentity central element. Second, the HNN extension ⟨F, t | [a ^ 2, t] = 1⟩ of a free group F along the identity of zpowers (a ^ 2) for a basis element a: there t commutes with a ^ 2 but not with a, although a commutes with a ^ 2. This is why an extension of the centralizer of u must use the full centralizer of u, here zpowers a, rather than zpowers u.

Main results #

References #

source
theorem IsFreeGroup.isCommTransitive {G : Type u_1} [Group G] [IsFreeGroup G] :
Group.IsCommTransitive G

Commutation is transitive on the nontrivial elements of a free group.

source
theorem IsFreeGroup.isTISubgroup_zpowers {G : Type u_1} [Group G] [IsFreeGroup G] {u : G} (hu : ¬Group.IsProperPower u) :
TauCeti.IsTISubgroup (Subgroup.zpowers u)

Maximal cyclic subgroups of a free group are malnormal. If u is not a proper power, then an element outside zpowers u conjugates no nonidentity element of zpowers u back into zpowers u.

source
theorem IsFreeGroup.maximal_isMulCommutative_zpowers {G : Type u_1} [Group G] [IsFreeGroup G] {u : G} (hu : ¬Group.IsProperPower u) :
Maximal (fun (K : Subgroup G) => IsMulCommutative ↥K) (Subgroup.zpowers u)

In a free group, the cyclic subgroup generated by a non-proper-power is a maximal abelian subgroup.

source
theorem IsFreeGroup.isTISubgroup_zpowers_iff {G : Type u_1} [Group G] [IsFreeGroup G] {u : G} (hu : u ≠ 1) :
TauCeti.IsTISubgroup (Subgroup.zpowers u) ↔ ¬Group.IsProperPower u

A nontrivial element u of a free group generates a malnormal subgroup exactly when u is not a proper power.

source
theorem IsFreeGroup.maximal_isMulCommutative_zpowers_iff {G : Type u_1} [Group G] [IsFreeGroup G] {u : G} (hu : u ≠ 1) :
Maximal (fun (K : Subgroup G) => IsMulCommutative ↥K) (Subgroup.zpowers u) ↔ ¬Group.IsProperPower u

A nontrivial element u of a free group generates a maximal abelian subgroup exactly when u is not a proper power.

source
theorem IsFreeGroup.maximal_isMulCommutative_iff {G : Type u_1} [Group G] [IsFreeGroup G] [Nontrivial G] {M : Subgroup G} :
Maximal (fun (K : Subgroup G) => IsMulCommutative ↥K) M ↔ ∃ (u : G), ¬Group.IsProperPower u ∧ M = Subgroup.zpowers u

The maximal abelian subgroups of a nontrivial free group are exactly the cyclic subgroups generated by elements that are not proper powers.

source
theorem IsFreeGroup.isCSA {G : Type u_1} [Group G] [IsFreeGroup G] :
Group.IsCSA G

Free groups are CSA: every maximal abelian subgroup of a free group is malnormal.

source
theorem Group.not_isCSA_prod_int :
¬IsCSA (FreeGroup (Fin 2) × Multiplicative ℤ)

The product of the free group on two generators with ℤ is not CSA.

source
theorem Group.not_commute_hnnExtension_of_t_zpowers_sq {α : Type u_1} (a : α) :
¬Commute (HNNExtension.of (FreeGroup.of a)) HNNExtension.t

In the HNN extension of a free group along the identity of zpowers (a ^ 2), the image of the basis element a does not commute with the stable letter, although a ^ 2 does.

source
theorem Group.not_isCommTransitive_hnnExtension_zpowers_sq {α : Type u_1} (a : α) :
¬IsCommTransitive (HNNExtension (FreeGroup α) (Subgroup.zpowers (FreeGroup.of a ^ 2)) (Subgroup.zpowers (FreeGroup.of a ^ 2)) (MulEquiv.refl ↥(Subgroup.zpowers (FreeGroup.of a ^ 2))))

The HNN extension of a free group along the identity of zpowers (a ^ 2) is not commutative transitive: a commutes with a ^ 2, which commutes with the stable letter, but a does not.

source
theorem Group.not_isCSA_hnnExtension_zpowers_sq {α : Type u_1} (a : α) :
¬IsCSA (HNNExtension (FreeGroup α) (Subgroup.zpowers (FreeGroup.of a ^ 2)) (Subgroup.zpowers (FreeGroup.of a ^ 2)) (MulEquiv.refl ↥(Subgroup.zpowers (FreeGroup.of a ^ 2))))

The HNN extension of a free group along the identity of zpowers (a ^ 2) is not CSA. This is the extension of the centralizer of a ^ 2 taken with zpowers (a ^ 2) in place of the full centralizer zpowers a.