-
Notifications
You must be signed in to change notification settings - Fork 88
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 MndToCat and other related theorems #4242
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Very nice!
Maybe it would be necessary to add a theorem stating explicitly that given any category C, every diagonal Hom-set in C equipped with the restriction of the binary operation of composition has a structure of monoid ? |
Something like this... Will do it in the next PR.
|
Yes, exactly. So that every category whose base set is a singleton will have a structure of Monoid |
Moreover, in the case that CAT 1 is true, so that the Hom-sets are distinct, for the structure <Hom(C), comp(C)> to be a monoid, the base B of the category C must be the singleton of a set. This is because : |
|
The whole section "Monoid of endomorphisms" in your mathbox should be moved to main, IMO. |
I had not seen bj-endmnd, and I am happy that we have it. |
Oof... I already proved the theorem. This could be a lemma for your proof to shorten it significantly. Maybe I should rename it to endmndlem.
|
Done in #4249.
I don't see |
Added
dtrucor3
as a learning process of how I understandax-5
.idmon
andidepi
showing identity morphisms are both monomorphisms and epimorphisms.