I want to propose to provide definitions for diagonal and scalar matrices
in set.mm, because I think these are common and popular mathematical
concepts, and the definitions could simplify many proofs, at least for some
theorems in the context of the Cayley-Hamilton theorem. I wonder, however,
if it is better to provide a definition for the ring of diagonal matrices
(as extensible structure) or to provide a definition for the set of
diagonal matrices (as subset of the base set of the ring of sqare
matrices). The same holds for scalar matrices.
My latest contribution includes two alternative definitions reflecting
these two approaches (with A = ( N Mat R ) , B = ( Base ` A ) ):
- ` DMat ` defines the algebra of N x N diagonal matrices over a ring R:
( N DMat R ) = ( A |`s { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j
) = .0. ) } ) ) (see ~ dmatval )
- ` DMatALT ` defines the diagonal matrices as subset of the set of N x
N matrices over a ring R: ( N DMatALT R ) = { m e. B | A. i e. N A. j e. N
( i =/= j -> ( i m j ) = .0. ) } ) (see ~ dmatALTval)
The advantage of the first alternative is that we can regard the diagonal
matrices as independent concept, for example by proving:
- ( N DMat R ) e. Ring (analogous to ~ matrng )
- ( N DMat R ) e. AssAlg (analogous to ~ matassa )
Obviously, ( Base ` ( N DMat R ) ) C_ ( Base ` ( N Mat R ) ) holds. To
express, however, that "diagonal matrices are a subring of the square
matrices" (sloppy speaking), we have to write
( Base ` ( N DMat R ) ) e. ( SubRing ` ( N Mat R ) ),
because "substructures"are generally not defined as extensible structure,
but as subset of the base set of an extensible structure, and the
substructure must be expressed as extensible structure by itself by using
structure restriction, see, for example ~ subrgrng: S = ( R |`s A ) => ( A
e. ( SubRing ` R ) -> S e. Ring ).
So the advantage of the second alternative is that we can prove:
( N DMatALT R ) e. ( SubRing ` ( N Mat R ) )
(analogous to, for example, ~ zsubrg : ZZ e. ( SubRing ` CCfld ) ).
Obviously, ( N DMatALT R ) C_ ( Base ` ( N Mat R ) ) holds. On the other
hand, we have two write
( ( N Mat R ) |`s ( N DMatALT R ) ) e. Ring
if we want to regard the diagonal matrices as ring by themselves.
I do not know if there is an unspoken convention or intention which of
these alternatives should be used. In my opinion, I would prefer the
definition ` DMat `. What do others think about it?
Which alternative is preferable or appropriate? Although there is only a
ittle difference between these alternatives, I have to select one of them...
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/43d1ebf7-d97f-49d6-bcae-f57493d9f4ec%40googlegroups.com.
