Skip to content

Conversation

Copy link
Contributor

Copilot AI commented Dec 16, 2025

Updated the solution to chapter I, exercise 2.5 to use the correct right-cancellation definition of epimorphism.

Changes Made

  • Definition: Changed from an incorrect "lifting property" style definition to the proper right-cancellation definition: A function f: A→B is an epimorphism iff for all sets Z and all functions β', β'': B→Z, if β'∘f = β''∘f, then β' = β''.

  • Proof (⟹): Rewrote the proof that surjection implies epimorphism to use the right-cancellation property, showing that if f is surjective, then for any b∈B we can find a∈A with f(a)=b and prove β'(b) = β''(b).

  • Proof (⟸): Rewrote the proof that epimorphism implies surjection by constructing two specific functions β', β'': B→{0,1} that distinguish elements in the image from those outside, using the cancellation property to show all elements of B must be in the image.

The solution now properly uses the right-cancellation definition, making it the categorical dual of the monomorphism (left-cancellation) definition as expected for this exercise.

Original prompt

This section details on the original issue you should resolve

<issue_title>exercise 2.5</issue_title>
<issue_description>Won't this exercise expect a right-cancellation definition?

​</issue_description>

<agent_instructions>please modify the solution to chapter I, exercise 2.5. you should use right-cancellation definition of the epimorphism.</agent_instructions>

Comments on the Issue (you are @copilot in this section)

@hooyuser Good catch! Thanks for pointing that out—I'll fix it shortly.

✨ Let Copilot coding agent set things up for you — coding agent works faster and does higher quality work when set up for your repo.

Copilot stopped work on behalf of hooyuser due to an error December 16, 2025 12:16
Copilot stopped work on behalf of hooyuser due to an error December 16, 2025 12:18
Copilot stopped work on behalf of hooyuser due to an error December 16, 2025 12:20
@hooyuser hooyuser requested a review from Copilot December 16, 2025 12:28
Copy link

Copilot AI left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Copilot wasn't able to review any files in this pull request.


💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

@hooyuser
Copy link
Owner

@copilot ?

Co-authored-by: hooyuser <10691820+hooyuser@users.noreply.github.com>
Copy link
Contributor Author

Copilot AI commented Dec 16, 2025

@copilot ?

I've updated exercise 2.5 to use the correct right-cancellation definition of epimorphism. The definition now states that f: A→B is an epimorphism iff for all sets Z and all functions β', β'': B→Z, if β'∘f = β''∘f, then β' = β''. I also rewrote both directions of the proof accordingly. See commit 86ebc1e.

Copilot AI changed the title [WIP] Update solution for chapter I exercise 2.5 using right-cancellation Update solution for chapter I exercise 2.5 using right-cancellation Dec 16, 2025
Copilot AI requested a review from hooyuser December 16, 2025 12:34
@hooyuser hooyuser marked this pull request as ready for review December 16, 2025 12:38
@hooyuser hooyuser merged commit fd0c116 into master Dec 16, 2025
2 checks passed
@hooyuser hooyuser deleted the copilot/modify-right-cancellation-definition branch December 16, 2025 12:45
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

Successfully merging this pull request may close these issues.

exercise 2.5

2 participants