English
There is a star-algebra equivalence reindexₐ between CStarMatrix m m A and CStarMatrix n n A induced by an equivalence e: m ≃ n.
Русский
Существует эквивалентность звуковой алгебры reindexₐ между CStarMatrix m×m A и CStarMatrix n×n A, индукируемая по эквивалентности e: m ≃ n.
LaTeX
$$$\mathrm{reindex}_{\mathsf{\!a}}(R,A,e) : C^*\text{-Matrix}_{m,m}(A) \simeq_{\ast}^{R} C^*\text{-Matrix}_{n,n}(A).$$$
Lean4
/-- The natural map that reindexes a matrix's rows and columns with equivalent types is an
equivalence. -/
def reindexₐ (R) (A) [Fintype m] [Fintype n] [Semiring R] [AddCommMonoid A] [Mul A] [Module R A] [Star A] (e : m ≃ n) :
CStarMatrix m m A ≃⋆ₐ[R] CStarMatrix n n A :=
{
reindexₗ R A e
e with
map_mul' M
N := by
ext i j
simp only [mul_apply]
refine Fintype.sum_equiv e _ _ ?_
intro k
simp
map_star'
M := by
ext
unfold reindexₗ
dsimp only [Equiv.toFun_as_coe, Equiv.invFun_as_coe, Matrix.reindex_symm, AddHom.toFun_eq_coe, AddHom.coe_mk,
Matrix.reindex_apply, Matrix.submatrix_apply]
rw [Matrix.star_apply, Matrix.star_apply]
simp [Matrix.submatrix_apply] }