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

Author: zwang123

changes-set.txt

@@ -92,6 +92,7 @@ make a github issue.)
 
 DONE:
 Date      Old       New         Notes
+11-Sep-25 cascl     [same]      revised - algSc may be non-injective
 24-Aug-25 elrab2w   [same]      Moved from SN's mathbox to main set.mm
 24-Aug-25 elab2gw   [same]      Moved from SN's mathbox to main set.mm
 24-Aug-25 elabgw    [same]      Moved from SN's mathbox to main set.mm

set.mm

@@ -283923,7 +283923,7 @@ the same dimension over the same (nonzero) ring.  (Contributed by AV,
   $( Algebraic span function. $)
   casp $a class AlgSpan $.
 
-  $( Class of algebra scalar injection function. $)
+  $( Class of algebra scalars function. $)
   cascl $a class algSc $.
 
   ${
@@ -284335,7 +284335,7 @@ the same dimension over the same (nonzero) ring.  (Contributed by AV,
     asclfval.k $e |- K = ( Base ` F ) $.
     asclfval.s $e |- .x. = ( .s ` W ) $.
     asclfval.o $e |- .1. = ( 1r ` W ) $.
-    $( Function value of the algebraic scalars function.  (Contributed by Mario
+    $( Function value of the algebra scalars function.  (Contributed by Mario
        Carneiro, 8-Mar-2015.) $)
     asclfval $p |- A = ( x e. K |-> ( x .x. .1. ) ) $=
       ( vw cascl cfv cmpt cbs csca eqtr4di c0 cv cvv wcel wceq cur cvsca fveq2d
@@ -284492,8 +284492,8 @@ the same dimension over the same (nonzero) ring.  (Contributed by AV,
     $d x y A $.  $d x y F $.  $d x y W $.
     asclrhm.a $e |- A = ( algSc ` W ) $.
     asclrhm.f $e |- F = ( Scalar ` W ) $.
-    $( The scalar injection is a ring homomorphism.  (Contributed by Mario
-       Carneiro, 8-Mar-2015.) $)
+    $( The algebra scalars function is a ring homomorphism.  (Contributed by
+       Mario Carneiro, 8-Mar-2015.) $)
     asclrhm $p |- ( W e. AssAlg -> A e. ( F RingHom W ) ) $=
       ( vx vy casa wcel cbs cfv cmulr cur assasca assaring assalmod ascl1 cv co
       eqid wceq ascldimul 3expb asclghm isrhm2d ) CHIZFGBJKZBCBLKZCLKZBMKZACMKZ
@@ -284506,7 +284506,7 @@ the same dimension over the same (nonzero) ring.  (Contributed by AV,
     rnascl.a $e |- A = ( algSc ` W ) $.
     rnascl.o $e |- .1. = ( 1r ` W ) $.
     rnascl.n $e |- N = ( LSpan ` W ) $.
-    $( The set of injected scalars is also interpretable as the span of the
+    $( The set of lifted scalars is also interpretable as the span of the
        identity.  (Contributed by Mario Carneiro, 9-Mar-2015.) $)
     rnascl $p |- ( W e. AssAlg -> ran A = ( N ` { .1. } ) ) $=
       ( vx vy casa wcel crn cv cvsca cfv co wceq csca cbs eqid cab csn asclfval
@@ -284579,7 +284579,7 @@ the same dimension over the same (nonzero) ring.  (Contributed by AV,
     $d S x $.  $d W x $.  $d X x $.
     ressascl.a $e |- A = ( algSc ` W ) $.
     ressascl.x $e |- X = ( W |`s S ) $.
-    $( The injection of scalars is invariant between subalgebras and
+    $( The lifting of scalars is invariant between subalgebras and
        superalgebras.  (Contributed by Mario Carneiro, 9-Mar-2015.) $)
     ressascl $p |- ( S e. ( SubRing ` W ) -> A = ( algSc ` X ) ) $=
       ( vx csubrg cfv wcel csca cbs cv cur cvsca co cmpt cascl eqid asclfval
@@ -835234,7 +835234,7 @@ have GLB (expanded version).  (Contributed by Zhi Wang,
 
          Equivalently, the algebra scalars function is not necessarily
          injective unless the algebra is faithful.  Therefore, all "scalar
-         injection" should be renamed.
+         injection" was renamed.
 
          Alternate proof involves ~ assa2ass , ~ assa2ass2 , and ~ asclval , by
          setting ` X ` and ` Y ` the multiplicative identity of the algebra.