Commit 2024-11-25 15:32 dbcafd02

feat: vertical line test for functions, group homs, linear maps (#18822) Prove the vertical line test for monoid homomorphisms/isomorphisms. Let f : G → H × I be a homomorphism to a product of monoids. Assume that f is surjective on the first factor and that the image of f intersects every "vertical line" {(h, i) | i : I} at most once. Then the image of f is the graph of some monoid homomorphism f' : H → I. Furthermore, if f is also surjective on the second factor and its image intersects every "horizontal line" {(h, i) | h : H} at most once, then f' is actually an isomorphism f' : H ≃ I.