Virtually cyclic groups

A group is virtually cyclic if it has a cyclic subgroup of finite index. Virtually cyclic groups are fundamental in geometric group theory: they are exactly the elementary subgroups of hyperbolic groups, the groups with at most two ends, and the conclusion of the curvature-free Margulis lemma of Besson–Courtois–Gallot–Sambusetti.

Main definitions and results

• Group.IsVirtuallyCyclic : a group with a cyclic subgroup of finite index.
• Group.IsVirtuallyCyclic.isVirtuallyNilpotent : virtually cyclic groups are virtually nilpotent.
• Group.IsVirtuallyCyclic.of_surjective, Group.IsVirtuallyCyclic.of_injective : preservation under surjective and injective homomorphisms.

TODO

• A finitely generated group is virtually cyclic iff it has ≤ 2 ends (requires ends of groups, not yet in Mathlib).

class AddGroup.IsVirtuallyAddCyclic (G : Type u_3) [AddGroup G] : Prop

An additive group is virtually cyclic if it has a cyclic additive subgroup of finite index.

• exists_isAddCyclic_and_finiteIndex : ∃ (H : AddSubgroup G), IsAddCyclic ↥H ∧ H.FiniteIndex

theorem AddGroup.isVirtuallyAddCyclic_iff (G : Type u_3) [AddGroup G] : IsVirtuallyAddCyclic G ↔ ∃ (H : AddSubgroup G), IsAddCyclic ↥H ∧ H.FiniteIndex

class Group.IsVirtuallyCyclic (G : Type u_3) [Group G] : Prop

A group is virtually cyclic if it has a cyclic subgroup of finite index.

• exists_isCyclic_and_finiteIndex : ∃ (H : Subgroup G), IsCyclic ↥H ∧ H.FiniteIndex

theorem Group.isVirtuallyCyclic_iff (G : Type u_3) [Group G] : IsVirtuallyCyclic G ↔ ∃ (H : Subgroup G), IsCyclic ↥H ∧ H.FiniteIndex

@[instance 100]

instance Group.instIsVirtuallyCyclicOfIsCyclic {G : Type u_1} [Group G] [IsCyclic G] : IsVirtuallyCyclic G

A cyclic group is virtually cyclic.

@[instance 100]

instance AddGroup.instIsVirtuallyAddCyclicOfIsAddCyclic {G : Type u_1} [AddGroup G] [IsAddCyclic G] : IsVirtuallyAddCyclic G

@[instance 100]

instance Group.instIsVirtuallyCyclicOfFinite {G : Type u_1} [Group G] [Finite G] : IsVirtuallyCyclic G

A finite group is virtually cyclic.

@[instance 100]

instance AddGroup.instIsVirtuallyAddCyclicOfFinite {G : Type u_1} [AddGroup G] [Finite G] : IsVirtuallyAddCyclic G

theorem Group.IsVirtuallyCyclic.exists_isCyclic_and_finiteIndex_and_normal (G : Type u_1) [Group G] [IsVirtuallyCyclic G] : ∃ (H : Subgroup G), IsCyclic ↥H ∧ H.FiniteIndex ∧ H.Normal

A virtually cyclic group has a normal cyclic subgroup of finite index.

theorem AddGroup.IsVirtuallyAddCyclic.exists_isAddCyclic_and_finiteIndex_and_normal (G : Type u_1) [AddGroup G] [IsVirtuallyAddCyclic G] : ∃ (H : AddSubgroup G), IsAddCyclic ↥H ∧ H.FiniteIndex ∧ H.Normal

theorem Group.IsVirtuallyCyclic.isVirtuallyNilpotent {G : Type u_1} [Group G] [IsVirtuallyCyclic G] : IsVirtuallyNilpotent G

A virtually cyclic group is virtually nilpotent.

theorem AddGroup.IsVirtuallyAddCyclic.isVirtuallyNilpotent {G : Type u_1} [AddGroup G] [IsVirtuallyAddCyclic G] : IsVirtuallyNilpotent G

theorem Group.IsVirtuallyCyclic.of_surjective {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] (f : G →* G') (hf : Function.Surjective ⇑f) [IsVirtuallyCyclic G] : IsVirtuallyCyclic G'

The image of a virtually cyclic group under a surjective homomorphism is virtually cyclic.

theorem AddGroup.IsVirtuallyAddCyclic.of_surjective {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') (hf : Function.Surjective ⇑f) [IsVirtuallyAddCyclic G] : IsVirtuallyAddCyclic G'

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

A group embedding into a virtually cyclic group is virtually cyclic.

theorem AddGroup.IsVirtuallyAddCyclic.of_injective {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] (f : G →+ G') (hf : Function.Injective ⇑f) [IsVirtuallyAddCyclic G'] : IsVirtuallyAddCyclic G

instance Group.instIsVirtuallyCyclicSubtypeMemSubgroup {G : Type u_1} [Group G] [IsVirtuallyCyclic G] (K : Subgroup G) : IsVirtuallyCyclic ↥K

Every subgroup of a virtually cyclic group is virtually cyclic.

instance AddGroup.instIsVirtuallyAddCyclicSubtypeMemAddSubgroup {G : Type u_1} [AddGroup G] [IsVirtuallyAddCyclic G] (K : AddSubgroup G) : IsVirtuallyAddCyclic ↥K

instance Group.instIsVirtuallyCyclicQuotientSubgroup {G : Type u_1} [Group G] [IsVirtuallyCyclic G] (N : Subgroup G) [N.Normal] : IsVirtuallyCyclic (G ⧸ N)

Quotients of virtually cyclic groups are virtually cyclic.

instance AddGroup.instIsVirtuallyAddCyclicQuotientAddSubgroup {G : Type u_1} [AddGroup G] [IsVirtuallyAddCyclic G] (N : AddSubgroup G) [N.Normal] : IsVirtuallyAddCyclic (G ⧸ N)