Scalars are commutative after being lifted into an associative algebra

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
 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
 10-Sep-25 weeq12d   [same]      Moved from SO's mathbox to main set.mm

set.mm

@@ -283964,7 +283964,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 $.
 
   ${
@@ -284376,7 +284376,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
@@ -284533,8 +284533,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
@@ -284547,7 +284547,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
@@ -284620,7 +284620,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
@@ -835145,6 +835145,107 @@ have GLB (expanded version).  (Contributed by Zhi Wang,
   $}
 
 
+$(
+=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
+  Rings
+=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
+$)
+
+
+$(
+-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
+  Multiplicative Group
+-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
+$)
+
+  ${
+    $d B y $.  $d M y $.  $d R y $.  $d X y $.  $d ph y $.
+    elmgpcntrd.b $e |- B = ( Base ` R ) $.
+    elmgpcntrd.m $e |- M = ( mulGrp ` R ) $.
+    elmgpcntrd.z $e |- Z = ( Cntr ` M ) $.
+    elmgpcntrd.x $e |- ( ph -> X e. B ) $.
+    elmgpcntrd.y $e |- ( ( ph /\ y e. B ) ->
+                         ( X ( .r ` R ) y ) = ( y ( .r ` R ) X ) ) $.
+    $( The center of a ring.  (Contributed by Zhi Wang, 11-Sep-2025.) $)
+    elmgpcntrd $p |- ( ph -> X e. Z ) $=
+      ( wcel cv cmulr cfv co wceq wral ralrimiva mgpbas eqid mgpplusg sylanbrc
+      elcntr ) AFCMFBNZDOPZQUFFUGQRZBCSFGMKAUHBCLTBFCUGEGCDEIHUADUGEIUGUBUCJUEU
+      D $.
+  $}
+
+
+$(
+=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
+  Associative algebras
+=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
+$)
+
+
+$(
+-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
+  Definition and basic properties
+-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
+$)
+
+  ${
+    asclelbas.a $e |- A = ( algSc ` W ) $.
+    asclelbas.f $e |- F = ( Scalar ` W ) $.
+    asclelbas.b $e |- B = ( Base ` F ) $.
+    asclelbas.w $e |- ( ph -> W e. AssAlg ) $.
+    asclelbas.c $e |- ( ph -> C e. B ) $.
+    $( Lifted scalars are in the base set of the algebra.  (Contributed by Zhi
+       Wang, 11-Sep-2025.) $)
+    asclelbas $p |- ( ph -> ( A ` C ) e. ( Base ` W ) ) $=
+      ( cfv cur cvsca co cbs wcel wceq eqid syl asclval casa clmod assalmod crg
+      assaring ringidcl 3syl lmodvscld eqeltrd ) ADBLZDFMLZFNLZOZFPLZADCQUKUNRK
+      BUMULECFDGHIUMSZULSZUATADUMECUOFULUOSZHUPIAFUBQZFUCQJFUDTKAUSFUEQULUOQJFU
+      FUOFULURUQUGUHUIUJ $.
+
+    ${
+      $d A x $.  $d C x $.  $d M x $.  $d W x $.  $d ph x $.
+      asclcntr.m $e |- M = ( mulGrp ` W ) $.
+      $( The algebra scalars function maps into the center of the algebra.
+         Equivalently, a lifted scalar is a center of the algebra.
+         (Contributed by Zhi Wang, 11-Sep-2025.) $)
+      asclcntr $p |- ( ph -> ( A ` C ) e. ( Cntr ` M ) ) $=
+        ( vx cbs cfv eqid wcel co adantr ccntr asclelbas cv wa casa cmulr simpr
+        wceq w3a cvsca asclmul1 asclmul2 eqtr4d syl3anc elmgpcntrd ) ANGOPZGFDB
+        PZFUAPZUPQZMURQABCDEGHIJKLUBANUCZUPRZUDGUERZDCRZVAUQUTGUFPZSZUTUQVDSZUH
+        AVBVAKTAVCVALTAVAUGVBVCVAUIVEDUTGUJPZSVFBDVGVDECUPGUTHIJUSVDQZVGQZUKBDV
+        GVDECUPGUTHIJUSVHVIULUMUNUO $.
+    $}
+
+    ${
+      asclcom.m $e |- .* = ( .r ` F ) $.
+      asclcom.d $e |- ( ph -> D e. B ) $.
+      $( Scalars are commutative after being lifted.
+
+         However, the scalars themselves are not necessarily commutative if the
+         algebra is not a faithful module.  For example, Let ` F ` be the 2 by
+         2 upper triangular matrix algebra over a commutative ring ` W ` .  It
+         is provable that ` F ` is in general non-commutative.  Define scalar
+         multiplication ` C .x. X ` as multipying the top-left entry, which is
+         a "vector" element of ` W ` , of the "scalar" ` C ` , which is now an
+         upper triangular matrix, with the "vector" ` X e. ( Base `` W ) ` .
+
+         Equivalently, the algebra scalars function is not necessarily
+         injective unless the algebra is faithful.  Therefore, all "scalar
+         injection" was renamed.
+
+         Alternate proof involves ~ assa2ass , ~ assa2ass2 , and ~ asclval , by
+         setting ` X ` and ` Y ` the multiplicative identity of the algebra.
+
+         (Contributed by Zhi Wang, 11-Sep-2025.) $)
+      asclcom $p |- ( ph -> ( A ` ( C .* D ) ) = ( A ` ( D .* C ) ) ) $=
+        ( cfv co wcel wceq eqid cmulr cbs asclelbas w3a cvsca asclmul1 asclmul2
+        casa eqtr4d syl3anc ascldimul 3eqtr4d ) ADBPZEBPZHUAPZQZUNUMUOQZDEGQBPZ
+        EDGQBPZAHUHRZDCRZUNHUBPZRZUPUQSLMABCEFHIJKLOUCUTVAVCUDUPDUNHUEPZQUQBDVD
+        UOFCVBHUNIJKVBTZUOTZVDTZUFBDVDUOFCVBHUNIJKVEVFVGUGUIUJAUTVAECRZURUPSLMO
+        BDEGUOFCHIJKVFNUKUJAUTVHVAUSUQSLOMBEDGUOFCHIJKVFNUKUJUL $.
+    $}
+  $}
+
+
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
   Categories