Add MndToCat and other related theorems

[zwang123]

Added

• dtrucor3 as a learning process of how I understand ax-5.
• idmon and idepi showing identity morphisms are both monomorphisms and epimorphisms.
• Relevant theorems regarding monoids as categories
• The existence of non-thin categories where all morphisms are simultaneously monomorphisms and epimorphisms.

[tirix]

Very nice!

[langgerard]

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 ?

[zwang123]

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.

|- ( ph -> C e. Cat )
|- B = ( Base ` C )
|- ( ph -> X e. B )
|- H = ( Hom ` C )
|- ( X H X ) = ( Base ` M )
|- .x. = ( comp ` C )
|- ( <. X , X >. .x. X ) = ( +g ` M )

|- ( ph -> M e. Mnd )

[langgerard]

Yes, exactly. So that every category whose base set is a singleton will have a structure of Monoid

[langgerard]

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 :
-if B is empty, then H is empty and cannot be the base set of a monoid ;
-if two distinct objects a and b are in b, then the diagonal hom-sets H(a,a) and H(b,b) are non-empty and distinct, but if f is in H(a,a) and g is in H(b,b), with a and b distinct, there is no way to have a composite morphism for f and g in H(b,a) or g and f in H(a,b), so that comp(C) cannot be a binary internal operation on H because the composition of f and g does not exist.

[benjub]

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.

|- ( ph -> C e. Cat )
|- B = ( Base ` C )
|- ( ph -> X e. B )
|- H = ( Hom ` C )
|- ( X H X ) = ( Base ` M )
|- .x. = ( comp ` C )
|- ( <. X , X >. .x. X ) = ( +g ` M )

|- ( ph -> M e. Mnd )

This is https://us.metamath.org/mpeuni/bj-endmnd.html

[tirix]

This is https://us.metamath.org/mpeuni/bj-endmnd.html

The whole section "Monoid of endomorphisms" in your mathbox should be moved to main, IMO.

[langgerard]

I had not seen bj-endmnd, and I am happy that we have it.
And I agree with Tirix that the whole section "Monoid of endomorphism" should be moved to main.

[zwang123]

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.

|- ( ph -> C e. Cat )
|- B = ( Base ` C )
|- ( ph -> X e. B )
|- H = ( Hom ` C )
|- ( X H X ) = ( Base ` M )
|- .x. = ( comp ` C )
|- ( <. X , X >. .x. X ) = ( +g ` M )

|- ( ph -> M e. Mnd )

This is https://us.metamath.org/mpeuni/bj-endmnd.html

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.

    catmnd.b $e |- B = ( Base ` C ) $.
    catmnd.h $e |- H = ( Hom ` C ) $.
    catmnd.o $e |- .x. = ( comp ` C ) $.
    catmnd.c $e |- ( ph -> C e. Cat ) $.
    catmnd.x $e |- ( ph -> X e. B ) $.
    catmnd.m $e |- ( ph -> ( X H X ) = ( Base ` M ) ) $.
    catmnd.p $e |- ( ph -> ( <. X , X >. .x. X ) = ( +g ` M ) ) $.

    catmnd $p |- ( ph -> M e. Mnd ) $=

[benjub]

This is https://us.metamath.org/mpeuni/bj-endmnd.html

The whole section "Monoid of endomorphisms" in your mathbox should be moved to main, IMO.

Done in #4249.

This [catmnd] could be a lemma for your proof to shorten it significantly. Maybe I should rename it to endmndlem.

I don't see catmnd, but if you can shorten a proof, then you are encouraged to do it of course !