Diagonal and scalar matrices

[Alexander van der Vekens]

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 little difference between these alternatives, I have to select one of them...

[Alexander van der Vekens]

Thierry posted the follwing in GitHub:

I think my vote may go to your current ‘ DMatALT ‘, since its definition is simpler, the operations are identical, and I would assume that later developments would use more often statements like “M is a diagonal matrix” rather than “the set of diagonal matrices forms a ring”.

 

I think these are good arguments for defining substructures as sets (and not structures). Meanwhile, I would also prefer these definitions (DMatALT, ScMatALT), because they better fit to the way substructures are currently used in set.mm. Furthermore, it will be easier to revise the existing theorems about diagonal/scalar matrices, because they are based on the set-like definitions already.

If nobody has arguments for a structure-like definition, I will switch the names of the definitions (ALT vs. non-ALT) and start to revise the theorems about diagonal/scalar matrices using the set-like definitions.

Alexander

[Norman Megill]

I looked this over but haven't formed a strong opinion one way or the other.  So if you prefer to use a set instead of a structure for this application, it is acceptable to me.

Norm

[Mario Carneiro]

The most similar case I know to this is the definition of polynomials (df-mpl) as a subset of power series (df-psr). In that case, I anticipated that we would not care so much about power series, so df-mpl itself defines a substructure, but the subset is also accessible using "the base set of polynomials" which is a subset of the set of power series, and theorem mplval2 supports this way of writing it.

My guess for this case is that it is more useful to have diagonal matrices be a subring (i.e. a subset about which you prove closure properties) rather than a freestanding structure. You still get most of the algebraic benefits with it being a subring, but this retains the connection between the two structures. Similar remarks apply to the orthogonal and special linear groups, although in these cases you will also want easy access to the group itself.

Mario

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/2ca0041c-fdf7-4bab-ad67-9fc7557a6e04%40googlegroups.com.