QuantumInfo.ForMathlib.HermitianMat.Jordan
19 declarations
Symmetric product of Hermitian matrices
#symmMulGiven two Hermitian matrices and in the space , the symmetric product is defined as the Jordan product: where and denote standard matrix multiplication. The resulting matrix is also Hermitian.
Commutativity of the Symmetric Product of Hermitian Matrices
#symmMul_commLet and be Hermitian matrices of dimension over the field . The symmetric product (or Jordan product) , defined by , is commutative, such that .
for the Jordan product of Hermitian matrices
#symmMul_zeroLet be a Hermitian matrix. The symmetric product of and the zero matrix, defined as , is equal to the zero matrix.
for Hermitian matrices
#zero_symmMulLet be a Hermitian matrix. The symmetric product (Jordan product) of the zero matrix and , defined as , results in the zero matrix.
Matrix Representation of the Symmetric Product of Hermitian Matrices
#symmMul_toMatLet and be Hermitian matrices of dimension over a field . The matrix representation of their symmetric product (also known as the Jordan product) is given by: where and are the underlying matrices of and respectively.
if and commute
#symmMul_of_commuteLet and be Hermitian matrices of dimension over a field . If the underlying matrices of and commute (i.e., ), then their symmetric product (defined as ) has an underlying matrix equal to the standard matrix product .
The symmetric product of a Hermitian matrix with itself equals
#symmMul_selfLet be a Hermitian matrix of dimension over a field . Let denote the symmetric product defined for Hermitian matrices. Then, the matrix representation of is equal to the square of the matrix representation of , i.e., .
for Hermitian matrices
#symmMul_oneLet be a Hermitian matrix of dimension over a field . Let the symmetric product of two Hermitian matrices and be defined as , where denotes standard matrix multiplication. Then, the symmetric product of with the identity matrix is equal to , i.e., .
for Hermitian matrices
#one_symmMulLet be a Hermitian matrix. The symmetric multiplication (Jordan product) of the identity matrix and , defined by , is equal to .
for Hermitian matrices
#symmMul_neg_oneFor any Hermitian matrix , let denote the symmetric product of Hermitian matrices. Then, the symmetric product of and the negative identity matrix satisfies .
For any Hermitian matrix , let the symmetric product (Jordan product) be defined as . Then the symmetric product of the negative identity matrix and the matrix satisfies .
Commutative magma structure on under symmetric multiplication
#instCommMagmaHermitianMatFor the space of Hermitian matrices of dimension over a field , denoted as , there exists a commutative magma structure where the binary operation is defined by the symmetric product . This structure ensures that the multiplication is commutative, satisfying for all Hermitian matrices and .
`*` coincides with `symmMul` for Hermitian matrices
#mul_eq_symmMulIn the context of the `HermMul` scope, the multiplication operation between two Hermitian matrices is equal to the symmetric product , defined as .
Hermitian matrices form a Commutative Jordan Algebra under the symmetric product
#instIsCommJordanHermitianMatLet be the space of Hermitian matrices over a field . When equipped with the symmetric product (also known as the Jordan product) defined by , the space forms a commutative Jordan algebra. This means the multiplication is commutative, , and satisfies the Jordan identity .
`MulZeroClass` instance for Hermitian matrices under the symmetric product \( A * B = \frac{1}{2}(AB + BA) \)
#instMulZeroClassHermitianMatFor the space of Hermitian matrices \( \text{HermitianMat}_d(\mathbb{k}) \) equipped with the symmetric product \( A * B = \frac{1}{2}(AB + BA) \), the zero matrix \( \mathbf{0} \) satisfies the property that \( \mathbf{0} * A = \mathbf{0} \) and \( A * \mathbf{0} = \mathbf{0} \) for any Hermitian matrix \( A \). This endows the Hermitian matrices with the structure of a `MulZeroClass`.
Jordan product on Hermitian matrices forms a `MulZeroOneClass`
#instMulZeroOneClassHermitianMatFor the set of Hermitian matrices of dimension over a field , the Jordan product defined by satisfies the properties of a `MulZeroOneClass`. This means the operation has a multiplicative identity element such that , and a zero element such that for any Hermitian matrix .
Non-unital non-associative ring structure of Hermitian matrices under symmetric multiplication
#instNonUnitalNonAssocRingHermitianMatThe set of Hermitian matrices of dimension over a field , denoted as , forms a non-unital non-associative ring. The multiplication operation in this structure is defined by the symmetric product , where and are standard matrix multiplications. This structure satisfies the left and right distributive laws: and .
Non-associative ring structure on via symmetric multiplication
#instNonAssocRingHermitianMatFor a given dimension and a field (typically or ), the set of Hermitian matrices equipped with the symmetric product forms a non-associative ring. This structure satisfies the axioms of an additive abelian group and possesses a distributive, non-associative multiplication with a multiplicative identity (the identity matrix ).
is a Scalar Tower for Hermitian Matrices under the Jordan Product
#instIsScalarTowerRealHermitianMatLet be the space of Hermitian matrices over a field endowed with the symmetric Jordan product . There exists an instance of a scalar tower for , , and . Specifically, for any and , the scalar multiplication satisfies .
