Description: 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. ( BaseW ) .
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)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | asclelbas.a | |- A = ( algSc ` W ) |
|
| asclelbas.f | |- F = ( Scalar ` W ) |
||
| asclelbas.b | |- B = ( Base ` F ) |
||
| asclelbas.w | |- ( ph -> W e. AssAlg ) |
||
| asclelbas.c | |- ( ph -> C e. B ) |
||
| asclcom.m | |- .* = ( .r ` F ) |
||
| asclcom.d | |- ( ph -> D e. B ) |
||
| Assertion | asclcom | |- ( ph -> ( A ` ( C .* D ) ) = ( A ` ( D .* C ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | asclelbas.a | |- A = ( algSc ` W ) |
|
| 2 | asclelbas.f | |- F = ( Scalar ` W ) |
|
| 3 | asclelbas.b | |- B = ( Base ` F ) |
|
| 4 | asclelbas.w | |- ( ph -> W e. AssAlg ) |
|
| 5 | asclelbas.c | |- ( ph -> C e. B ) |
|
| 6 | asclcom.m | |- .* = ( .r ` F ) |
|
| 7 | asclcom.d | |- ( ph -> D e. B ) |
|
| 8 | 1 2 3 4 7 | asclelbas | |- ( ph -> ( A ` D ) e. ( Base ` W ) ) |
| 9 | eqid | |- ( Base ` W ) = ( Base ` W ) |
|
| 10 | eqid | |- ( .r ` W ) = ( .r ` W ) |
|
| 11 | eqid | |- ( .s ` W ) = ( .s ` W ) |
|
| 12 | 1 2 3 9 10 11 | asclmul1 | |- ( ( W e. AssAlg /\ C e. B /\ ( A ` D ) e. ( Base ` W ) ) -> ( ( A ` C ) ( .r ` W ) ( A ` D ) ) = ( C ( .s ` W ) ( A ` D ) ) ) |
| 13 | 1 2 3 9 10 11 | asclmul2 | |- ( ( W e. AssAlg /\ C e. B /\ ( A ` D ) e. ( Base ` W ) ) -> ( ( A ` D ) ( .r ` W ) ( A ` C ) ) = ( C ( .s ` W ) ( A ` D ) ) ) |
| 14 | 12 13 | eqtr4d | |- ( ( W e. AssAlg /\ C e. B /\ ( A ` D ) e. ( Base ` W ) ) -> ( ( A ` C ) ( .r ` W ) ( A ` D ) ) = ( ( A ` D ) ( .r ` W ) ( A ` C ) ) ) |
| 15 | 4 5 8 14 | syl3anc | |- ( ph -> ( ( A ` C ) ( .r ` W ) ( A ` D ) ) = ( ( A ` D ) ( .r ` W ) ( A ` C ) ) ) |
| 16 | 1 2 3 10 6 | ascldimul | |- ( ( W e. AssAlg /\ C e. B /\ D e. B ) -> ( A ` ( C .* D ) ) = ( ( A ` C ) ( .r ` W ) ( A ` D ) ) ) |
| 17 | 4 5 7 16 | syl3anc | |- ( ph -> ( A ` ( C .* D ) ) = ( ( A ` C ) ( .r ` W ) ( A ` D ) ) ) |
| 18 | 1 2 3 10 6 | ascldimul | |- ( ( W e. AssAlg /\ D e. B /\ C e. B ) -> ( A ` ( D .* C ) ) = ( ( A ` D ) ( .r ` W ) ( A ` C ) ) ) |
| 19 | 4 7 5 18 | syl3anc | |- ( ph -> ( A ` ( D .* C ) ) = ( ( A ` D ) ( .r ` W ) ( A ` C ) ) ) |
| 20 | 15 17 19 | 3eqtr4d | |- ( ph -> ( A ` ( C .* D ) ) = ( A ` ( D .* C ) ) ) |