Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add surjective homomorphisms #2037

Open
Taneb opened this issue Jul 31, 2023 · 1 comment
Open

Add surjective homomorphisms #2037

Taneb opened this issue Jul 31, 2023 · 1 comment

Comments

@Taneb
Copy link
Member

Taneb commented Jul 31, 2023

In Algebra.Morphism.Structures and the similar modules for lattices and modules, we define IsXHomomorphism, IsXMonomorphism, and IsXIsomorphism. We do not currently define IsXEpimorphism, for morphisms that are surjective but not necessarily injective. This feels an obvious omission, and would be useful for defining, for example, projective objects (cf. wp:Projective module)

@jamesmckinna
Copy link
Contributor

jamesmckinna commented Feb 16, 2024

... And for using the proof that the unique morphism from any Algebra to its corresponding terminal object is StrictlySurjective #2296

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants