QuantumInfo.ForMathlib.LinearEquiv

Given an equivalence (bijection) $e: d \simeq d_2$ between two index sets, this definition provides a linear equivalence between the function spaces $R^{d_2}$ and $R^d$ over a ring $R$. The map sends a function $f \in R^{d_2}$ to the function $f \circ e \in R^d$, effectively relabeling the coordinates of the vector space.

Given an equivalence (or bijection) $e \colon \delta \simeq \delta_2$ between two indexing sets, there exists a linear equivalence between the Euclidean spaces $\mathbb{E}^{\delta_2}$ and $\mathbb{E}^{\delta}$ over a scalar field $\mathbb{k}$. This map is constructed by relabeling the coordinates of a vector in the function space $(\delta_2 \to \mathbb{k})$ according to $e$ and is compatible with the $L^2$ norm structure of the Euclidean spaces.

For a ring $R$ and an index set $d$, the linear equivalence $(d \to R) \simeq_R (d \to R)$ induced by the identity equivalence $\text{id} \colon d \simeq d$ (the relabeling of coordinates by the identity map) is equal to the identity linear equivalence $\text{id}_R$ on the function space $R^d$.

The linear equivalence between Euclidean spaces $\mathbb{E}^d$ and $\mathbb{E}^d$ induced by the identity (reflexive) relabeling $e = \text{refl}_d$ of the indexing set $d$ is equal to the identity linear equivalence on $\text{EuclideanSpace } \mathbb{k}^d$.

Let $R$ be a ring and $d_1, d_2, d_3, d$ be index sets. Given two bijections $e: d_1 \simeq d_3$ and $f: d_2 \simeq d$, and a matrix $M \in \text{Matrix}(d_1, d_2, R)$, let $M.\text{reindex}(e, f)$ be the matrix reindexed by $e$ on rows and $f$ on columns. Then the linear map associated with the reindexed matrix is given by the composition $(M.\text{reindex}(e, f)).\text{toLin'} = \phi_{e^{-1}} \circ M.\text{toLin'} \circ \phi_f$, where $\phi_\sigma$ denotes the linear equivalence $\text{LinearEquiv.of\_relabel}$ induced by an index bijection $\sigma$.

(e : d₁ ≃ d₃) (f : d₂ ≃ d) (M : Matrix d₁ d₂ 𝕜) : (M.reindex e f).toEuclideanLin = (LinearEquiv.euclidean_of_relabel 𝕜 e.symm) ∘ₗ M.toEuclideanLin ∘ₗ (LinearEquiv.euclidean_of_relabel 𝕜 f)

Let $R$ be a ring and $d, d_2, d_3$ be types. Given an equivalence (bijection) $e : d \simeq d_2$ and a matrix $M$ with row indices $d_3$ and column indices $d$, let $M.reindex(\text{id}, e)$ be the matrix where the columns are reindexed according to $e$. Then, the linear map associated with this reindexed matrix, $(M.\text{reindex}(\text{id}, e)).\text{toLin'}$, is equal to the composition of the linear map associated with $M$, $M.\text{toLin'}$, and the linear equivalence induced by relabeling indices, $\text{LinearEquiv.of\_relabel}(R, e)$.

Let $\mathbb{k}$ be a field and $M$ be a matrix with row index set $d_3$ and column index set $d$ with entries in $\mathbb{k}$. Given an equivalence (relabeling) of indices $e : d \simeq d_2$, the linear map between Euclidean spaces associated with the matrix $M$ reindexed on the right by $e$ is equal to the composition of the linear map associated with $M$ and the linear equivalence induced by $e$. That is, $(M.\text{reindex}(\text{refl}, e)).\text{toEuclideanLin} = M.\text{toEuclideanLin} \circ L_e$, where $L_e$ is the canonical linear equivalence between $\text{EuclideanSpace } \mathbb{k} \text{ } d_2$ and $\text{EuclideanSpace } \mathbb{k} \text{ } d$.

Let $R$ be a ring, and let $d_1, d_2, d_3$ be types used as indices. For any equivalence (bijection) $e : d_1 \simeq d_3$ and any matrix $M$ with row indices in $d_1$ and column indices in $d_2$ with entries in $R$, the linear map associated with the matrix $M$ reindexed on the left by $e$ is equal to the composition of the linear map associated with $M$ and the linear equivalence induced by the inverse of $e$. Specifically, $\text{toLin}'(M.\text{reindex}(e, \text{id})) = \text{of\_relabel}(e^{-1}) \circ \text{toLin}'(M)$, where $\text{toLin}'$ denotes the matrix-to-linear-map transformation and $\text{of\_relabel}$ is the linear equivalence $R^{d_3} \simeq_R R^{d_1}$ mapping $f$ to $f \circ e$.

Let $\mathbb{k}$ be a field and $M$ be a matrix with row indices in $d_1$ and column indices in $d_2$ with entries in $\mathbb{k}$. Given an equivalence (relabeling) of indices $e : d_1 \simeq d_3$, the linear map between Euclidean spaces associated with the matrix $M$ reindexed on the left by $e$ is equal to the composition of the linear equivalence induced by the inverse of $e$ and the linear map associated with $M$. Mathematically, $(M.\text{reindex}(e, \text{id})).\text{toEuclideanLin} = L_{e^{-1}} \circ M.\text{toEuclideanLin}$, where $L_{e^{-1}}$ is the canonical linear equivalence between $\text{EuclideanSpace } \mathbb{k} \text{ } d_3$ and $\text{EuclideanSpace } \mathbb{k} \text{ } d_1$ induced by the inverse relabeling $e^{-1}$.