Move 'monoid of endomorphisms' subsection from my mathbox to Main.

[benjub]

Move 'monoid of endomorphisms' subsection from my mathbox to Main.

Shorten a few proofs.

[avekens]

Do we really need a definition df-end and a new symbol End for the monoid of endomorphisms on an object of a category? Are there any applications of this definition? Wouldn't be a theorem like ~catmnd as discussed in #4242 and provided in #4248 be sufficient?

According our convention "New definitions infrequent",

new definitions ... are introduced only when a clear advantage becomes apparent for reducing the number of symbols, shortening proofs, etc."

I don't see any of these advantages (yet). Therefore, this PR must be rejected (sorry).

I remember that I proposed to move some definitions from my Mathbox to main some time ago (see, for example, #1389) which was rejected for this reason...

[benjub]

Yes, https://us.metamath.org/mpeuni/df-bj-end.html is a worthy addition to set.mm. This is an important notion, which a quick internet or library search will suffice to confirm. I move it to Main with this PR as requested by @tirix @zwang123 and @langgerard in #4242 (comment) and #4242 (comment). Actually, had this already been in Main before #4242, @zwang123 would have probably spent less time reproving some results, and would have used that definition instead. I think the comparison of the statements

|- ( ph -> C e. Cat )
|- ( ph -> X e. ( Base ` C ) )
=>
|- ( ph -> ( ( End ` C ) ` X ) e. Mnd )

and

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

speaks for itself. In particular, the first statement is more readily understandable to readers, without having to know about the implementation details exposed in the second.

[avekens]

Yes, https://us.metamath.org/mpeuni/df-bj-end.html is a worthy addition to set.mm. This is an important notion, which a quick internet or library search will suffice to confirm. I move it to Main with this PR as requested by @tirix @zwang123 and @langgerard in #4242 (comment) and #4242 (comment). Actually, had this already been in Main before #4242, @zwang123 would have probably spent less time reproving some results, and would have used that definition instead.

With the same arguments, my definition of non-unitary rings (and maybe others) can also be moved to main, which was rejected some time ago. So can I move df-rng0 and related theorems also to main (so #1389 will be solved, being "on hold" for more than 4 years)?

I want to hear the opinion of @david-a-wheeler and @digama0 at least.

[langgerard]

1 : In my personal opinion, the position of BJ is basically correct, and he should be allowed to move his "monoid of endomorphisms subsection " to the main part of set.mm.
Let me remark that this subsection is the generalization to the case of all categories C of AV subsection "monoid of endofunctions" that is the case where C= SetCat(U), so that the endomorphism of an object x in C become the endofunctions of a set x in U.
2 : Also, in my personal opinion, the position of AV is basically correct, and he should be allowed to move his work on
non-unitary rings

[benjub]

With the same arguments, my definition of non-unitary rings (and maybe others) can also be moved to main

The same arguments? When that move to Main was proposed, had that move been requested by three other contributors too? Had another contributor started working independently on the same topic and accidentally duplicated the work, too?

More generally, this really shouldn't become a bargaining of the form: "you accept my definition, I accept yours".

As for df-rng0 specifically, the first reply to your issue #1389 was by me and it was an approval to move df-rng0 to Main as df-rng. I haven't changed on that point. So to be explicit: I do approve the moving of df-rng0 to Main (relabeled to df-rng). I reiterated my approval in #1389 (comment) and then I gave ideas of developments in #1389 (comment). That's the least I could do since I drew attention to them in https://groups.google.com/g/metamath/c/XKl7K0qx4uc/m/WOghVowaDgAJ and in #866 (comment).

In the case of endomorphisms, I also drew attention to them in #3782 (comment), in which I used them to answer a basic question that was asked by contributors. This is actually the reason why I felt I had to provide the associated definition in my mathbox. Recently, three contributors requested that I move it to Main, which I accepted, and here we are.

[savask]

Sorry for nosing in, but maybe someone (say, zwang123) could prove prove a few theorems using benjub's definitions, and that would trigger the formal criteria for moving material from his mathbox? I think we have been routinely moving stuff into main if it's required by other contributors. That way we can rely on a strict procedure instead of judging whether some results are better than others.

[digama0]

I find some of these reformattings a bit dubious. I'm very much not a fan of right alignment, and would prefer we used a consistent formatting style in the library.

[benjub]

I can revert that. I thought the rule of thumb was to break line at highest possible token (in the sense of "oldest in the syntax tree), and I would actually break these at $p if not for formatting problems arising from that choice.

Consistency is indeed paramount. Actually, I wouldn't mind having an automatic "dumb" line-wrap as for proofs and comments.

[digama0]

I have no substantive comments, but I agree with @savask that when in doubt we should apply our procedures. If there is consensus that it should be moved to main then I am not opposed, but if there is any doubt or debate then probably it would be better to wait until some other mechanism kicks in, like usage by multiple contributors.

[avekens]

Sorry for nosing in, but maybe someone (say, zwang123) could prove prove a few theorems using benjub's definitions, and that would trigger the formal criteria for moving material from his mathbox? I think we have been routinely moving stuff into main if it's required by other contributors. That way we can rely on a strict procedure instead of judging whether some results are better than others.

I think this is exactly the way which should be followed, because it is completely in accordance with our conventions.

[avekens]

Is here a kind of dead lock with #4248, that means this PR can only be accepted/merged after/together with #4248?

[zwang123]

I think #4248 is independent. catmnd (now renamed as endmndlem) can be moved to main later if this is merged, or go wherever it should be if this is not. Other parts of #4248 is totally unrelated.