{"id":"palomar/PALOMAR-2026-10-04-000011","url":"https://github.com/Arthur742Ramos/cell-attachment-lean/tree/1c671038e320cecc58ca1d81dca11bbe2e2a507c","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-04-000011-v1.json","repo":"https://github.com/Arthur742Ramos/cell-attachment-lean","tags":["math.AT","math.CT","msc:55Q05","msc:18B40","algebraic-topology","fundamental-group","homotopy-theory","lean-formalization"],"score":0,"title":"Fundamental Groups of Arbitrary Two-Cell Attachments","trust":"high","domain":"math.AT","source":"palomar","authors":["Arthur Freitas Ramos","David Barros Hulak","Ruy Jose Guerra Barretto de Queiroz"],"reviews":0,"subject":"math.AT","summary":"The full arbitrary-family two-cell attachment theorem for ordinary topological fundamental groups. For any path-connected topological space X, any basepoint, and any indexed family of continuous circle attaching maps, a genuine adjunction quotient is constructed from X and the coproduct of closed complex unit disks. The actual inclusion-induced fundamental-group homomorphism is surjective and its kernel is precisely the normal closure of the once-around attaching loops, transported along the specified basepoint paths. A quotient group isomorphism is proved compatible with the actual…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-04","reactions":{},"formalized":true,"formalizes":[{"title":"Algebraic Topology","identifier":"https://pi.math.cornell.edu/~hatcher/AT/AT..pdf","relationship":"formalizes"}]}