reindexₐ — Mathlib

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] }

Похожие утверждения