PhyslibAlpha.Mathematics.LadderSystem.SymmetricPower

The excitation sector is the symmetric power

i. Overview

`vacuumSpan L Ω n` is linearly isomorphic to the `n`-th symmetric power of `K^d` -- concretely, to the free `K`-vector space on `Sym (Fin d) n` (Mathlib's own type of size-`n` multisets on `Fin d`, the standard combinatorial model of `Sym^n(K^d)`'s natural basis once a basis `e_1,…,e_d` of `K^d` is fixed: a multiset `{i_1,…,i_n}` names the basis vector `e_{i_1} ⊙ ⋯ ⊙ e_{i_n}`). The isomorphism sends this basis to the occupation-number states, i.e. it is exactly `OccupationBasis.lean`'s `vacuumBasis` reindexed along `countFunEquivSym`.

ii. Key results

`LadderSystem.vacuumSpanSymEquiv` : `vacuumSpan L Ω n ≃ₗ[K] (Sym (Fin d) n →₀ K)`.

iii. References

2 declarations

definition

Linear isomorphism $\text{Sym}^n(K^d) \cong \text{vacuumSpan}(L, \Omega, n)$

#vacuumSpanSymEquiv

For a $d$ -mode ladder system $L$ over a field $K$ and a vector space $V$ with vacuum state $\Omega$ , there exists a $K$ -linear isomorphism between the free $K$ -vector space generated by multisets of size $n$ on $\{0, 1, \dots, d-1\}$ (denoted as $\text{Sym}^n(\text{Fin } d) \to_0 K$ ) and the $n$ -th excitation-number sector $\text{vacuumSpan}(L, \Omega, n)$ . This isomorphism maps each multiset $\{i_1, i_2, \dots, i_n\}$ , representing a basis element of the symmetric power, to the corresponding occupation-number basis vector $a^\dagger_{i_1} a^\dagger_{i_2} \dots a^\dagger_{i_n} \Omega$ in the excitation sector.

theorem

The isomorphism `vacuumSpanSymEquiv` maps the basis multiset $s$ to its occupation-number state word $a^\dagger_{i_1} \dots a^\dagger_{i_n} \Omega$

#vacuumSpanSymEquiv_single

For a $d$ -mode ladder system $L$ with vacuum state $\Omega$ , let $\Phi_n: (\text{Sym}^n(\text{Fin } d) \to_0 K) \cong \text{vacuumSpan}(L, \Omega, n)$ be the $K$ -linear isomorphism between the free vector space on multisets of size $n$ and the $n$ -th excitation-number sector. For any multiset $s \in \text{Sym}^n(\text{Fin } d)$ , let $\delta_s$ be the basis vector corresponding to $s$ in the free $K$ -vector space. Then the isomorphism $\Phi_n$ maps $\delta_s$ to the occupation-number state obtained by applying the word of creation operators corresponding to the count function of $s$ to the vacuum $\Omega$ : $\Phi_n(\delta_s) = a^\dagger_{i_1} a^\dagger_{i_2} \dots a^\dagger_{i_n} \Omega$ where the list of indices $[i_1, i_2, \dots, i_n]$ is the canonical word (ordered by index) representing the multiset $s$ .