@@ -283964,7 +283964,7 @@ the same dimension over the same (nonzero) ring. (Contributed by AV,
283964
283964
$( Algebraic span function. $)
283965
283965
casp $a class AlgSpan $.
283966
283966
283967
- $( Class of algebra scalar injection function. $)
283967
+ $( Class of algebra scalars function. $)
283968
283968
cascl $a class algSc $.
283969
283969
283970
283970
${
@@ -284376,7 +284376,7 @@ the same dimension over the same (nonzero) ring. (Contributed by AV,
284376
284376
asclfval.k $e |- K = ( Base ` F ) $.
284377
284377
asclfval.s $e |- .x. = ( .s ` W ) $.
284378
284378
asclfval.o $e |- .1. = ( 1r ` W ) $.
284379
- $( Function value of the algebraic scalars function. (Contributed by Mario
284379
+ $( Function value of the algebra scalars function. (Contributed by Mario
284380
284380
Carneiro, 8-Mar-2015.) $)
284381
284381
asclfval $p |- A = ( x e. K |-> ( x .x. .1. ) ) $=
284382
284382
( 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,
284533
284533
$d x y A $. $d x y F $. $d x y W $.
284534
284534
asclrhm.a $e |- A = ( algSc ` W ) $.
284535
284535
asclrhm.f $e |- F = ( Scalar ` W ) $.
284536
- $( The scalar injection is a ring homomorphism. (Contributed by Mario
284537
- Carneiro, 8-Mar-2015.) $)
284536
+ $( The algebra scalars function is a ring homomorphism. (Contributed by
284537
+ Mario Carneiro, 8-Mar-2015.) $)
284538
284538
asclrhm $p |- ( W e. AssAlg -> A e. ( F RingHom W ) ) $=
284539
284539
( vx vy casa wcel cbs cfv cmulr cur assasca assaring assalmod ascl1 cv co
284540
284540
eqid wceq ascldimul 3expb asclghm isrhm2d ) CHIZFGBJKZBCBLKZCLKZBMKZACMKZ
@@ -284547,7 +284547,7 @@ the same dimension over the same (nonzero) ring. (Contributed by AV,
284547
284547
rnascl.a $e |- A = ( algSc ` W ) $.
284548
284548
rnascl.o $e |- .1. = ( 1r ` W ) $.
284549
284549
rnascl.n $e |- N = ( LSpan ` W ) $.
284550
- $( The set of injected scalars is also interpretable as the span of the
284550
+ $( The set of lifted scalars is also interpretable as the span of the
284551
284551
identity. (Contributed by Mario Carneiro, 9-Mar-2015.) $)
284552
284552
rnascl $p |- ( W e. AssAlg -> ran A = ( N ` { .1. } ) ) $=
284553
284553
( 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,
284620
284620
$d S x $. $d W x $. $d X x $.
284621
284621
ressascl.a $e |- A = ( algSc ` W ) $.
284622
284622
ressascl.x $e |- X = ( W |`s S ) $.
284623
- $( The injection of scalars is invariant between subalgebras and
284623
+ $( The lifting of scalars is invariant between subalgebras and
284624
284624
superalgebras. (Contributed by Mario Carneiro, 9-Mar-2015.) $)
284625
284625
ressascl $p |- ( S e. ( SubRing ` W ) -> A = ( algSc ` X ) ) $=
284626
284626
( 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,
835145
835145
$}
835146
835146
835147
835147
835148
+ $(
835149
+ =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
835150
+ Rings
835151
+ =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
835152
+ $)
835153
+
835154
+
835155
+ $(
835156
+ -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
835157
+ Multiplicative Group
835158
+ -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
835159
+ $)
835160
+
835161
+ ${
835162
+ $d B y $. $d M y $. $d R y $. $d X y $. $d ph y $.
835163
+ elmgpcntrd.b $e |- B = ( Base ` R ) $.
835164
+ elmgpcntrd.m $e |- M = ( mulGrp ` R ) $.
835165
+ elmgpcntrd.z $e |- Z = ( Cntr ` M ) $.
835166
+ elmgpcntrd.x $e |- ( ph -> X e. B ) $.
835167
+ elmgpcntrd.y $e |- ( ( ph /\ y e. B ) ->
835168
+ ( X ( .r ` R ) y ) = ( y ( .r ` R ) X ) ) $.
835169
+ $( The center of a ring. (Contributed by Zhi Wang, 11-Sep-2025.) $)
835170
+ elmgpcntrd $p |- ( ph -> X e. Z ) $=
835171
+ ( wcel cv cmulr cfv co wceq wral ralrimiva mgpbas eqid mgpplusg sylanbrc
835172
+ elcntr ) AFCMFBNZDOPZQUFFUGQRZBCSFGMKAUHBCLTBFCUGEGCDEIHUADUGEIUGUBUCJUEU
835173
+ D $.
835174
+ $}
835175
+
835176
+
835177
+ $(
835178
+ =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
835179
+ Associative algebras
835180
+ =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
835181
+ $)
835182
+
835183
+
835184
+ $(
835185
+ -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
835186
+ Definition and basic properties
835187
+ -.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-
835188
+ $)
835189
+
835190
+ ${
835191
+ asclelbas.a $e |- A = ( algSc ` W ) $.
835192
+ asclelbas.f $e |- F = ( Scalar ` W ) $.
835193
+ asclelbas.b $e |- B = ( Base ` F ) $.
835194
+ asclelbas.w $e |- ( ph -> W e. AssAlg ) $.
835195
+ asclelbas.c $e |- ( ph -> C e. B ) $.
835196
+ $( Lifted scalars are in the base set of the algebra. (Contributed by Zhi
835197
+ Wang, 11-Sep-2025.) $)
835198
+ asclelbas $p |- ( ph -> ( A ` C ) e. ( Base ` W ) ) $=
835199
+ ( cfv cur cvsca co cbs wcel wceq eqid syl asclval casa clmod assalmod crg
835200
+ assaring ringidcl 3syl lmodvscld eqeltrd ) ADBLZDFMLZFNLZOZFPLZADCQUKUNRK
835201
+ BUMULECFDGHIUMSZULSZUATADUMECUOFULUOSZHUPIAFUBQZFUCQJFUDTKAUSFUEQULUOQJFU
835202
+ FUOFULURUQUGUHUIUJ $.
835203
+
835204
+ ${
835205
+ $d A x $. $d C x $. $d M x $. $d W x $. $d ph x $.
835206
+ asclcntr.m $e |- M = ( mulGrp ` W ) $.
835207
+ $( The algebra scalars function maps into the center of the algebra.
835208
+ Equivalently, a lifted scalar is a center of the algebra.
835209
+ (Contributed by Zhi Wang, 11-Sep-2025.) $)
835210
+ asclcntr $p |- ( ph -> ( A ` C ) e. ( Cntr ` M ) ) $=
835211
+ ( vx cbs cfv eqid wcel co adantr ccntr asclelbas cv wa casa cmulr simpr
835212
+ wceq w3a cvsca asclmul1 asclmul2 eqtr4d syl3anc elmgpcntrd ) ANGOPZGFDB
835213
+ PZFUAPZUPQZMURQABCDEGHIJKLUBANUCZUPRZUDGUERZDCRZVAUQUTGUFPZSZUTUQVDSZUH
835214
+ AVBVAKTAVCVALTAVAUGVBVCVAUIVEDUTGUJPZSVFBDVGVDECUPGUTHIJUSVDQZVGQZUKBDV
835215
+ GVDECUPGUTHIJUSVHVIULUMUNUO $.
835216
+ $}
835217
+
835218
+ ${
835219
+ asclcom.m $e |- .* = ( .r ` F ) $.
835220
+ asclcom.d $e |- ( ph -> D e. B ) $.
835221
+ $( Scalars are commutative after being lifted.
835222
+
835223
+ However, the scalars themselves are not necessarily commutative if the
835224
+ algebra is not a faithful module. For example, Let ` F ` be the 2 by
835225
+ 2 upper triangular matrix algebra over a commutative ring ` W ` . It
835226
+ is provable that ` F ` is in general non-commutative. Define scalar
835227
+ multiplication ` C .x. X ` as multipying the top-left entry, which is
835228
+ a "vector" element of ` W ` , of the "scalar" ` C ` , which is now an
835229
+ upper triangular matrix, with the "vector" ` X e. ( Base `` W ) ` .
835230
+
835231
+ Equivalently, the algebra scalars function is not necessarily
835232
+ injective unless the algebra is faithful. Therefore, all "scalar
835233
+ injection" was renamed.
835234
+
835235
+ Alternate proof involves ~ assa2ass , ~ assa2ass2 , and ~ asclval , by
835236
+ setting ` X ` and ` Y ` the multiplicative identity of the algebra.
835237
+
835238
+ (Contributed by Zhi Wang, 11-Sep-2025.) $)
835239
+ asclcom $p |- ( ph -> ( A ` ( C .* D ) ) = ( A ` ( D .* C ) ) ) $=
835240
+ ( cfv co wcel wceq eqid cmulr cbs asclelbas w3a cvsca asclmul1 asclmul2
835241
+ casa eqtr4d syl3anc ascldimul 3eqtr4d ) ADBPZEBPZHUAPZQZUNUMUOQZDEGQBPZ
835242
+ EDGQBPZAHUHRZDCRZUNHUBPZRZUPUQSLMABCEFHIJKLOUCUTVAVCUDUPDUNHUEPZQUQBDVD
835243
+ UOFCVBHUNIJKVBTZUOTZVDTZUFBDVDUOFCVBHUNIJKVEVFVGUGUIUJAUTVAECRZURUPSLMO
835244
+ BDEGUOFCHIJKVFNUKUJAUTVHVAUSUQSLOMBEDGUOFCHIJKVFNUKUJUL $.
835245
+ $}
835246
+ $}
835247
+
835248
+
835148
835249
$(
835149
835250
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
835150
835251
Categories
0 commit comments