The Howson property of free groups #
The intersection of two finitely generated subgroups of a free group is finitely generated. Each finitely generated subgroup is accepted at the base vertex of its Stallings graph, a finite folded labelled graph. The product of two folded graphs accepts the intersection of their subgroups at the pair of base vertices, and the product of finite graphs has finitely many darts. A graph with finitely many darts accepts a finitely generated subgroup.
Main results #
Subgroup.FG.inf_of_isFreeGroup: Howson's theorem.
References #
- A. G. Howson, On the intersection of finitely generated free groups, J. London Math. Soc. 29 (1954), 428–434.
- I. Kapovich and A. Myasnikov, Stallings foldings and subgroups of free groups, Section 9, Proposition 9.4 and Corollary 9.5.
theorem
Subgroup.FG.inf_of_isFreeGroup
{G : Type u_1}
[Group G]
[IsFreeGroup G]
{H K : Subgroup G}
(hH : H.FG)
(hK : K.FG)
:
(H ⊓ K).FG
Howson's theorem: in a free group, the intersection of two finitely generated subgroups is finitely generated.