{"id":"palomar/PALOMAR-2026-09-01-000009","url":"https://github.com/Arthur742Ramos/HowsonIntersectionTheorem/tree/19aa5cdfb1e4c4711ab28304cd7f602b6500a3e9","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-01-000009-v1.json","repo":"https://github.com/Arthur742Ramos/HowsonIntersectionTheorem","tags":["math.GR","msc:20E07","msc:20F65","msc:05C25","group-theory","free-groups","lean","howson-theorem"],"score":0,"title":"Howson's theorem through finite cores and Kurosh decomposition","trust":"high","domain":"math.GR","source":"palomar","authors":["Arthur Freitas Ramos","David Barros Hulak","Ruy J. G. B. de Queiroz"],"reviews":0,"subject":"math.GR","summary":"Formalizes Howson's theorem for finite-rank free groups: the intersection of two finitely generated subgroups is finitely generated. The proof uses the repository's inclusion-compatible Marshall Hall construction to place one subgroup as a free factor of a finite-index overgroup, applies Schreier's finite-index theorem to the other subgroup, and then uses the actual Kurosh decomposition of the resulting subgroup of a binary free product. The final map from the relevant conjugate-intersection factor is defined from the factor inclusions and proved surjective onto the internal subgroup…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-01","reactions":{},"formalized":true,"formalizes":[{"title":"On the Intersection of Finitely Generated Free Groups","identifier":"10.1112/jlms/s1-29.4.428","relationship":"formalizes"}]}