Physlib.Mathematics.KroneckerDelta.Basic

Let $f: \text{Fin } 1 \oplus \text{Fin } 3 \simeq \text{Fin } 4$ be the equivalence (denoted as `finSumFinEquiv`) that maps the direct sum of finite types to a single finite type. For any elements $a, b \in \text{Fin } 1 \oplus \text{Fin } 3$, the Kronecker delta $\delta_{ij}$ satisfies the identity $\delta_{f(a), f(b)} = \delta_{a, b}$.

For a type $\alpha$ with decidable equality and a finite index set $\iota$, given two sequences of indices $\mu, \nu : \iota \to \alpha$, the generalized Kronecker delta is defined as the determinant of the matrix whose $(i, j)$-th entry is the Kronecker delta $\delta_{\mu_i, \nu_j}$. Mathematically, this is expressed as: $$\delta^{\mu_1 \dots \mu_n}_{\nu_1 \dots \nu_n} = \det \begin{pmatrix} \delta_{\mu_1 \nu_1} & \dots & \delta_{\mu_1 \nu_n} \\ \vdots & \ddots & \vdots \\ \delta_{\mu_n \nu_1} & \dots & \delta_{\mu_n \nu_n} \end{pmatrix}$$ where $n$ is the cardinality of the index set $\iota$.

Let $\alpha$ be a type with decidable equality and $\iota$ be a finite index set. Given two sequences of indices $\mu, \nu : \iota \to \alpha$, the generalized Kronecker delta $\delta^{\mu}_{\nu}$ is defined as the determinant of the matrix whose $(i, j)$-th entry is the Kronecker delta $\delta_{\mu_i, \nu_j}$. For any two distinct indices $i, j \in \iota$, swapping the values in the upper index sequence $\mu$ at positions $i$ and $j$ negates the value of the generalized Kronecker delta: $$\delta^{\mu \circ \tau_{i,j}}_{\nu} = -\delta^{\mu}_{\nu}$$ where $\tau_{i,j}$ denotes the transposition (swap) of $i$ and $j$. This property follows from the fact that swapping two indices in $\mu$ corresponds to a row transposition in the underlying determinant.