diff --git a/changes-set.txt b/changes-set.txt index 1dbbb68cc..113e879a5 100644 --- a/changes-set.txt +++ b/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 diff --git a/set.mm b/set.mm index 6cf708df0..fb38fbd7a 100644 --- a/set.mm +++ b/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