Confusion with CommAlgCat R vs Under R

Stream: mathlib4

[Kenny Lau]

We have both CommAlgCat and Under R, and they are equivalent categories under commAlgCatEquivUnder. There are essentially two difference that I can think of:

1. CommAlgCat is universe polymorphic, i.e. the algebra can belong to a different universe than the base ring.
2. CommAlgCat stores the Algebra instance whereas Under R just stores the ring hom, which would lead to a round trip being not defeq (because the SMul instance in the Algebra can be not defeq to algebraMap _ _ r * x!)

Are these two the main reasons why we have two idioms?

[Christian Merten]

Yes, but your second point is the main reason.

[Bhavik Mehta]

Either the module or definition docstring should definitely explain this

[Bhavik Mehta]

It even looks like I asked for it to be explained in the implementation notes of the file during review, but that never happened