Theorems for universal property (#5020)

* [add] assa2ass2; [shorten] assa2ass

* [add] asclcom

* [add] elmgpcntrd

* [prove] asclcntr; [add] asclelbas

* [minimize] asclcom

* [delete] assascacom and assascacrng

* [improve] explanation of asclcom

* [rename] structure map of associative algebra might be non-injective; [fix] algebraic scalars map -> algebra scalars map

* [add] upcic (empty proof), upciclem1

* [change] upciclem1: var change

* [add] isisod; [prove] upcic; [propose] upciclem2; [move] reueqdv to main

* [add] funcrcl2, funcrcl3; [update] upcic, upciclem2

* [shorten] upcic with funcrcl2

* [fix] functor

* [add] funcel1; [propose] funcel2

* Revert "[add] funcel1; [propose] funcel2"

This reverts commit 5fb5705.

* [prove] upciclem2

* [remove] upciclem2.n; [reformat] hypotheses; [trivial] formatting

* [trivial] formatting

* [add] a section for Universal property

* [add] upeu

* [fix] upeu description

* [add] upeu2lem, reuxfr1dd, upciclem2; [shorten] upciclem3; [propose] upeu2

* [prove] upeu2

* [move] reuxfr1dd; [fix] upciclem1 description

* [move and fix] upeu2lem and description and line length

* [shorten] asclelbas

* [rename] algebra scalars function -> algebra scalar lifting function

---------

Co-authored-by: avekens <[email protected]>

Author: zwang123

changes-set.txt

@@ -105,6 +105,7 @@ Date      Old       New         Notes
 16-Sep-25 ismhp     [same]      Removed unneeded hypotheses
 16-Sep-25 selvval   [same]      Removed unneeded hypotheses
 16-Sep-25 mplelsfi  [same]      Removed unused hypothesis
+16-Sep-25 reueqdv   [same]      Moved from GG's mathbox to main set.mm
 11-Sep-25 cascl     [same]      revised - algSc may be non-injective
 10-Sep-25 soeq12d   [same]      Moved from SO's mathbox to main set.mm
 10-Sep-25 freq12d   [same]      Moved from SO's mathbox to main set.mm

discouraged

@@ -14669,6 +14669,7 @@ New usage of "anmp" is discouraged (11 uses).
 New usage of "aprilfools2025" is discouraged (0 uses).
 New usage of "archnq" is discouraged (1 uses).
 New usage of "arglem1N" is discouraged (0 uses).
+New usage of "asclelbasALT" is discouraged (0 uses).
 New usage of "atabs2i" is discouraged (1 uses).
 New usage of "atabsi" is discouraged (1 uses).
 New usage of "atbtwnexOLDN" is discouraged (0 uses).
@@ -19982,6 +19983,7 @@ Proof modification of "anabss7p1" is discouraged (5 steps).
 Proof modification of "ancomstVD" is discouraged (22 steps).
 Proof modification of "anmp" is discouraged (8 steps).
 Proof modification of "aprilfools2025" is discouraged (116 steps).
+Proof modification of "asclelbasALT" is discouraged (84 steps).
 Proof modification of "avril1" is discouraged (194 steps).
 Proof modification of "ax1" is discouraged (3 steps).
 Proof modification of "ax10fromc7" is discouraged (50 steps).