QuantumInfo.ForMathlib.HermitianMat.Reindex

Given a Hermitian matrix $A$ indexed by a type $d$ and an equivalence (bijection) $e: d \simeq d_2$, the reindexed matrix $A.\text{reindex}(e)$ is the Hermitian matrix indexed by $d_2$ whose underlying matrix is $A$ with both its rows and columns reindexed by $e$. Formally, the resulting matrix $A'$ has entries $A'_{i, j} = A_{e^{-1}(i), e^{-1}(j)}$ for $i, j \in d_2$.

Let $A$ be a Hermitian matrix indexed by $d$. Given an equivalence (permutation) $e: d \simeq d_2$, the underlying matrix of the reindexed Hermitian matrix $A.\text{reindex}(e)$ is equal to the matrix $A$ reindexed by $e$ on both rows and columns. That is, $(A.\text{reindex}(e)).\text{mat} = A.\text{mat}.\text{reindex}(e, e)$.

For any Hermitian matrix $A$ with indices in $d$ over a field $\mathbf{k}$, reindexing $A$ using the identity equivalence (the reflexive equivalence) results in the original matrix $A$. Here, $A.\text{reindex}(\text{refl})$ denotes the operation of permuting the rows and columns of $A$ by the identity map.

Let $A$ be a Hermitian matrix with indices in $d$. Given two bijections (equivalences) $e: d \simeq d_2$ and $f: d_2 \simeq d_3$, the result of first reindexing $A$ by $e$ and then reindexing the result by $f$ is equal to reindexing $A$ by the composition ($e$ trans $f$) of the two bijections. That is, $(A_{\text{reindexed by } e})_{\text{reindexed by } f} = A_{\text{reindexed by } (f \circ e)}$.

For any Hermitian matrix $0$ (the zero matrix) indexed by $d$ over a field $\mathbf{k}$, and for any equivalence (permutation) $e: d \simeq d_2$, the reindexed matrix $0_{\text{reindexed by } e}$ remains the zero matrix of the new indexing type $d_2$. In other words, reindexing the zero Hermitian matrix results in a zero Hermitian matrix.

Let $d$ and $d_2$ be types with decidable equality, and $e: d \simeq d_2$ be an equivalence between them. Then the reindexing of the identity Hermitian matrix $I_d$ (of type `HermitianMat d 𝕜`) by $e$ is equal to the identity Hermitian matrix $I_{d_2}$ (of type `HermitianMat d₂ 𝕜`). That is, $I_d.\text{reindex}(e) = I_{d_2}$.

Let $A$ and $B$ be Hermitian matrices indexed by $d$ over the field $\mathbb{k}$, and let $e: d \simeq d_2$ be an equivalence (reindexing) between types $d$ and $d_2$. Then the sum of the reindexed matrices $A$ and $B$ is equal to the reindex of their sum: $$(A. \text{reindex } e) + (B. \text{reindex } e) = (A + B). \text{reindex } e$$

Let $A$ and $B$ be Hermitian matrices indexed by $d$, and let $e: d \simeq d_2$ be an equivalence (permutation) between index types. The difference of the reindexed matrices is equal to the reindexing of their difference: $$(A.reindex(e)) - (B.reindex(e)) = (A - B).reindex(e)$$ where $A.reindex(e)$ denotes the Hermitian matrix obtained by permuting the rows and columns of $A$ according to $e$.

Let $A$ be a Hermitian matrix indexed by $d$, and let $e: d \simeq d_2$ be an equivalence between index types. Then the reindexing of the negation of $A$ is equal to the negation of the reindexed matrix, i.e., $(-A). \text{reindex}(e) = -(A. \text{reindex}(e))$.

Let $A$ be a Hermitian matrix indexed by $d$, and let $e: d \simeq d_2$ be an equivalence between index types. For any real scalar $c \in \mathbb{R}$, the reindexing of the scalar product $c \cdot A$ by $e$ is equal to the scalar product of $c$ and the reindexed matrix $A$, i.e., $(c \cdot A).reindex(e) = c \cdot (A.reindex(e))$.

Let $A$ be a Hermitian matrix indexed by $d$, and let $e: d \simeq d_2$ be an equivalence between index types $d$ and $d_2$. For any matrix $B$ indexed by $d_3 \times d_2$ over a field $\mathbf{k}$, where $d$ and $d_2$ are finite types, the conjugation of the reindexed Hermitian matrix $A$ by $B$ is equal to the conjugation of $A$ by the submatrix of $B$ obtained by reindexing its columns with $e$. That is, $$(A.\text{reindex } e).\text{conj } B = A.\text{conj } (B \circ (\text{id}, e))$$ where the submatrix $B.\text{submatrix id } e$ is defined by elements $(B.\text{submatrix id } e)_{i, j} = B_{i, e(j)}$.

Let $A$ be a Hermitian matrix, $B$ be a matrix of dimension $d_2 \times d_4$, $e: d_3 \simeq d_2$ be an equivalence of index types, and $f: d \to d_4$ be a mapping. Then the conjugation of $A$ by the submatrix of $B$ indexed by $e$ and $f$ is equal to the reindexing of the conjugation of $A$ by the submatrix of $B$ indexed by the identity and $f$, specifically: $$A.\text{conj}(B_{\text{submatrix}(e, f)}) = (A.\text{conj}(B_{\text{submatrix}(\text{id}, f)})).\text{reindex}(e^{-1})$$ where $e^{-1}$ denotes the inverse equivalence of $e$.

Let $A$ be a Hermitian matrix indexed by $d$. Given an equivalence (permutation) $e: d \simeq d_2$ between index types, the reindexed Hermitian matrix $A.\text{reindex}(e)$ can be expressed as a conjugation of $A$. Specifically, $A.\text{reindex}(e) = A.\text{conj}(M)$, where $M$ is the matrix formed by reindexing the identity matrix $1$ by the equivalence $e$ on the rows and the identity map on the columns.

Let $A$ be a Hermitian matrix indexed by $d$ over a field $\mathbb{k}$, and let $e: d \simeq d_2$ be an equivalence between indexing sets. Let $\text{ker}(A)$ denote the kernel of the linear operator associated with $A$ acting on the Euclidean space $\mathbb{E}^d$. Then the kernel of the reindexed Hermitian matrix $A.\text{reindex}(e)$ is equal to the preimage (comap) of the kernel of $A$ under the linear map induced by the coordinate relabeling $e$, denoted by $\text{ker}(A.\text{reindex}(e)) = \text{ker}(A).\text{comap}(L_e)$, where $L_e: \mathbb{E}^{d_2} \to \mathbb{E}^d$ is the linear equivalence $v \mapsto v \circ e$.

Let $A$ and $B$ be Hermitian matrices indexed by $d$, and let $e: d \simeq d_2$ be a bijection between indexing sets. The kernel of the reindexed matrix $A$ (under $e$) is a subspace of the kernel of the reindexed matrix $B$ if and only if the kernel of $A$ is a subspace of the kernel of $B$. That is, $(A.\text{reindex } e).\ker \le (B.\text{reindex } e).\ker \iff A.\ker \le B.\ker$.