Matrices with entries in a C⋆-algebra

This file creates a type copy of Matrix m n A called CStarMatrix m n A meant for matrices with entries in a C⋆-algebra A. Its action on C⋆ᵐᵒᵈ (n → A) (via Matrix.mulVec) gives it the operator norm, and this norm makes CStarMatrix n n A a C⋆-algebra.

Main declarations

• CStarMatrix m n A: the type copy
• CStarMatrix.instNonUnitalCStarAlgebra: square matrices with entries in a non-unital C⋆-algebra form a non-unital C⋆-algebra
• CStarMatrix.instCStarAlgebra: square matrices with entries in a unital C⋆-algebra form a unital C⋆-algebra

Implementation notes

The norm on this type induces the product uniformity and bornology, but these are not defeq to Pi.uniformSpace and Pi.instBornology. Hence, we prove the equality to the Pi instances and replace the uniformity and bornology by the Pi ones when registering the NormedAddCommGroup (CStarMatrix m n A) instance. See the docstring of the TopologyAux section below for more details.

def CStarMatrix (m : Type u_1) (n : Type u_2) (A : Type u_3) : Type (max u_1 u_2 u_3)

Type copy Matrix m n A meant for matrices with entries in a C⋆-algebra. This is a C⋆-algebra when m = n.

Equations

• CStarMatrix m n A = Matrix m n A

def CStarMatrix.ofMatrix {m : Type u_7} {n : Type u_8} {A : Type u_9} : Matrix m n A ≃ CStarMatrix m n A

The equivalence between Matrix m n A and CStarMatrix m n A.

Equations

• CStarMatrix.ofMatrix = Equiv.refl (Matrix m n A)

@[simp]

theorem CStarMatrix.ofMatrix_apply {m : Type u_1} {n : Type u_2} {A : Type u_3} {M : Matrix m n A} {i : m} : ofMatrix M i = M i

@[simp]

theorem CStarMatrix.ofMatrix_symm_apply {m : Type u_1} {n : Type u_2} {A : Type u_3} {M : CStarMatrix m n A} {i : m} : ofMatrix.symm M i = M i

theorem CStarMatrix.ext_iff {m : Type u_1} {n : Type u_2} {A : Type u_3} {M N : CStarMatrix m n A} : (∀ (i : m) (j : n), M i j = N i j) ↔ M = N

theorem CStarMatrix.ext {m : Type u_1} {n : Type u_2} {A : Type u_3} {M₁ M₂ : CStarMatrix m n A} (h : ∀ (i : m) (j : n), M₁ i j = M₂ i j) : M₁ = M₂

def CStarMatrix.map {m : Type u_1} {n : Type u_2} {A : Type u_3} {B : Type u_4} (M : CStarMatrix m n A) (f : A → B) : CStarMatrix m n B

M.map f is the matrix obtained by applying f to each entry of the matrix M.

Equations

• M.map f = CStarMatrix.ofMatrix fun (i : m) (j : n) => f (M i j)

@[simp]

theorem CStarMatrix.map_apply {m : Type u_1} {n : Type u_2} {A : Type u_3} {B : Type u_4} {M : CStarMatrix m n A} {f : A → B} {i : m} {j : n} : M.map f i j = f (M i j)

@[simp]

theorem CStarMatrix.map_id {m : Type u_1} {n : Type u_2} {A : Type u_3} (M : CStarMatrix m n A) : M.map id = M

@[simp]

theorem CStarMatrix.map_id' {m : Type u_1} {n : Type u_2} {A : Type u_3} (M : CStarMatrix m n A) : (M.map fun (x : A) => x) = M

theorem CStarMatrix.map_map {m : Type u_1} {n : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_7} {M : Matrix m n A} {f : A → B} {g : B → C} : (M.map f).map g = M.map (g ∘ f)

theorem CStarMatrix.map_injective {m : Type u_1} {n : Type u_2} {A : Type u_3} {B : Type u_4} {f : A → B} (hf : Function.Injective f) : Function.Injective fun (M : CStarMatrix m n A) => M.map f

def CStarMatrix.transpose {m : Type u_1} {n : Type u_2} {A : Type u_3} (M : CStarMatrix m n A) : CStarMatrix n m A

The transpose of a matrix.

Equations

• M.transpose = CStarMatrix.ofMatrix fun (x : n) (y : m) => M y x

@[simp]

theorem CStarMatrix.transpose_apply {m : Type u_1} {n : Type u_2} {A : Type u_3} (M : CStarMatrix m n A) (i : n) (j : m) : M.transpose i j = M j i

def CStarMatrix.conjTranspose {m : Type u_1} {n : Type u_2} {A : Type u_3} [Star A] (M : CStarMatrix m n A) : CStarMatrix n m A

The conjugate transpose of a matrix defined in term of star.

Equations

• M.conjTranspose = M.transpose.map star

instance CStarMatrix.instStar {n : Type u_2} {A : Type u_3} [Star A] : Star (CStarMatrix n n A)

Equations

• CStarMatrix.instStar = { star := fun (M : CStarMatrix n n A) => M.conjTranspose }

instance CStarMatrix.instInvolutiveStar {n : Type u_2} {A : Type u_3} [InvolutiveStar A] : InvolutiveStar (CStarMatrix n n A)

Equations

• CStarMatrix.instInvolutiveStar = InvolutiveStar.mk ⋯

instance CStarMatrix.instInhabited {m : Type u_1} {n : Type u_2} {A : Type u_3} [Inhabited A] : Inhabited (CStarMatrix m n A)

Equations

• CStarMatrix.instInhabited = inferInstanceAs (Inhabited (m → n → A))

instance CStarMatrix.instDecidableEq {m : Type u_1} {n : Type u_2} {A : Type u_3} [DecidableEq A] [Fintype m] [Fintype n] : DecidableEq (CStarMatrix m n A)

Equations

• CStarMatrix.instDecidableEq = Fintype.decidablePiFintype

instance CStarMatrix.instFintypeOfDecidableEq {n : Type u_7} {m : Type u_8} [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] (α : Type u_9) [Fintype α] : Fintype (CStarMatrix m n α)

Equations

• CStarMatrix.instFintypeOfDecidableEq α = inferInstanceAs (Fintype (m → n → α))

instance CStarMatrix.instFinite {n : Type u_7} {m : Type u_8} [Finite m] [Finite n] (α : Type u_9) [Finite α] : Finite (CStarMatrix m n α)

instance CStarMatrix.instAdd {m : Type u_1} {n : Type u_2} {A : Type u_3} [Add A] : Add (CStarMatrix m n A)

Equations

• CStarMatrix.instAdd = Pi.instAdd

instance CStarMatrix.instAddSemigroup {m : Type u_1} {n : Type u_2} {A : Type u_3} [AddSemigroup A] : AddSemigroup (CStarMatrix m n A)

Equations

• CStarMatrix.instAddSemigroup = Pi.addSemigroup

instance CStarMatrix.instAddCommSemigroup {m : Type u_1} {n : Type u_2} {A : Type u_3} [AddCommSemigroup A] : AddCommSemigroup (CStarMatrix m n A)

Equations

• CStarMatrix.instAddCommSemigroup = Pi.addCommSemigroup

instance CStarMatrix.instZero {m : Type u_1} {n : Type u_2} {A : Type u_3} [Zero A] : Zero (CStarMatrix m n A)

Equations

• CStarMatrix.instZero = Pi.instZero

instance CStarMatrix.instAddZeroClass {m : Type u_1} {n : Type u_2} {A : Type u_3} [AddZeroClass A] : AddZeroClass (CStarMatrix m n A)

Equations

• CStarMatrix.instAddZeroClass = Pi.addZeroClass

instance CStarMatrix.instAddMonoid {m : Type u_1} {n : Type u_2} {A : Type u_3} [AddMonoid A] : AddMonoid (CStarMatrix m n A)

Equations

• CStarMatrix.instAddMonoid = Pi.addMonoid

instance CStarMatrix.instAddCommMonoid {m : Type u_1} {n : Type u_2} {A : Type u_3} [AddCommMonoid A] : AddCommMonoid (CStarMatrix m n A)

Equations

• CStarMatrix.instAddCommMonoid = Pi.addCommMonoid

instance CStarMatrix.instNeg {m : Type u_1} {n : Type u_2} {A : Type u_3} [Neg A] : Neg (CStarMatrix m n A)

Equations

• CStarMatrix.instNeg = Pi.instNeg

instance CStarMatrix.instSub {m : Type u_1} {n : Type u_2} {A : Type u_3} [Sub A] : Sub (CStarMatrix m n A)

Equations

• CStarMatrix.instSub = Pi.instSub

instance CStarMatrix.instAddGroup {m : Type u_1} {n : Type u_2} {A : Type u_3} [AddGroup A] : AddGroup (CStarMatrix m n A)

Equations

• CStarMatrix.instAddGroup = Pi.addGroup

instance CStarMatrix.instAddCommGroup {m : Type u_1} {n : Type u_2} {A : Type u_3} [AddCommGroup A] : AddCommGroup (CStarMatrix m n A)

Equations

• CStarMatrix.instAddCommGroup = Pi.addCommGroup

instance CStarMatrix.instUnique {m : Type u_1} {n : Type u_2} {A : Type u_3} [Unique A] : Unique (CStarMatrix m n A)

Equations

• CStarMatrix.instUnique = Pi.unique

instance CStarMatrix.instSubsingleton {m : Type u_1} {n : Type u_2} {A : Type u_3} [Subsingleton A] : Subsingleton (CStarMatrix m n A)

instance CStarMatrix.instNontrivial {m : Type u_1} {n : Type u_2} {A : Type u_3} [Nonempty m] [Nonempty n] [Nontrivial A] : Nontrivial (CStarMatrix m n A)

instance CStarMatrix.instSMul {m : Type u_1} {n : Type u_2} {A : Type u_3} {R : Type u_5} [SMul R A] : SMul R (CStarMatrix m n A)

Equations

• CStarMatrix.instSMul = Pi.instSMul

instance CStarMatrix.instSMulCommClass {m : Type u_1} {n : Type u_2} {A : Type u_3} {R : Type u_5} {S : Type u_6} [SMul R A] [SMul S A] [SMulCommClass R S A] : SMulCommClass R S (CStarMatrix m n A)

instance CStarMatrix.instIsScalarTower {m : Type u_1} {n : Type u_2} {A : Type u_3} {R : Type u_5} {S : Type u_6} [SMul R S] [SMul R A] [SMul S A] [IsScalarTower R S A] : IsScalarTower R S (CStarMatrix m n A)

instance CStarMatrix.instIsCentralScalar {m : Type u_1} {n : Type u_2} {A : Type u_3} {R : Type u_5} [SMul R A] [SMul Rᵐᵒᵖ A] [IsCentralScalar R A] : IsCentralScalar R (CStarMatrix m n A)

instance CStarMatrix.instMulAction {m : Type u_1} {n : Type u_2} {A : Type u_3} {R : Type u_5} [Monoid R] [MulAction R A] : MulAction R (CStarMatrix m n A)

Equations

• CStarMatrix.instMulAction = Pi.mulAction R

instance CStarMatrix.instDistribMulAction {m : Type u_1} {n : Type u_2} {A : Type u_3} {R : Type u_5} [Monoid R] [AddMonoid A] [DistribMulAction R A] : DistribMulAction R (CStarMatrix m n A)

Equations

• CStarMatrix.instDistribMulAction = Pi.distribMulAction R

instance CStarMatrix.instModule {m : Type u_1} {n : Type u_2} {A : Type u_3} {R : Type u_5} [Semiring R] [AddCommMonoid A] [Module R A] : Module R (CStarMatrix m n A)

Equations

• CStarMatrix.instModule = Pi.module m (fun (a : m) => n → A) R

@[simp]

theorem CStarMatrix.zero_apply {m : Type u_1} {n : Type u_2} {A : Type u_3} [Zero A] (i : m) (j : n) : 0 i j = 0

@[simp]

theorem CStarMatrix.add_apply {m : Type u_1} {n : Type u_2} {A : Type u_3} [Add A] (M N : CStarMatrix m n A) (i : m) (j : n) : (M + N) i j = M i j + N i j

@[simp]

theorem CStarMatrix.smul_apply {m : Type u_1} {n : Type u_2} {A : Type u_3} {B : Type u_4} [SMul B A] (r : B) (M : Matrix m n A) (i : m) (j : n) : (r • M) i j = r • M i j

@[simp]

theorem CStarMatrix.sub_apply {m : Type u_1} {n : Type u_2} {A : Type u_3} [Sub A] (M N : Matrix m n A) (i : m) (j : n) : (M - N) i j = M i j - N i j

@[simp]

theorem CStarMatrix.neg_apply {m : Type u_1} {n : Type u_2} {A : Type u_3} [Neg A] (M : Matrix m n A) (i : m) (j : n) : (-M) i j = -M i j

simp-normal form pulls of to the outside, to match the Matrix API.

@[simp]

theorem CStarMatrix.of_zero {m : Type u_1} {n : Type u_2} {A : Type u_3} [Zero A] : ofMatrix 0 = 0

@[simp]

theorem CStarMatrix.of_add_of {m : Type u_1} {n : Type u_2} {A : Type u_3} [Add A] (f g : Matrix m n A) : ofMatrix f + ofMatrix g = ofMatrix (f + g)

@[simp]

theorem CStarMatrix.of_sub_of {m : Type u_1} {n : Type u_2} {A : Type u_3} [Sub A] (f g : Matrix m n A) : ofMatrix f - ofMatrix g = ofMatrix (f - g)

@[simp]

theorem CStarMatrix.neg_of {m : Type u_1} {n : Type u_2} {A : Type u_3} [Neg A] (f : Matrix m n A) : -ofMatrix f = ofMatrix (-f)

@[simp]

theorem CStarMatrix.smul_of {m : Type u_1} {n : Type u_2} {A : Type u_3} {R : Type u_5} [SMul R A] (r : R) (f : Matrix m n A) : r • ofMatrix f = ofMatrix (r • f)

instance CStarMatrix.instStarAddMonoid {n : Type u_2} {A : Type u_3} [AddMonoid A] [StarAddMonoid A] : StarAddMonoid (CStarMatrix n n A)

Equations

• CStarMatrix.instStarAddMonoid = StarAddMonoid.mk ⋯

instance CStarMatrix.instStarModule {n : Type u_2} {A : Type u_3} {R : Type u_5} [Star R] [Star A] [SMul R A] [StarModule R A] : StarModule R (CStarMatrix n n A)

def CStarMatrix.ofMatrixₗ {m : Type u_1} {n : Type u_2} {A : Type u_3} {R : Type u_5} [AddCommMonoid A] [Semiring R] [Module R A] : Matrix m n A ≃ₗ[R] CStarMatrix m n A

The equivalence to matrices, bundled as a linear equivalence.

Equations

• CStarMatrix.ofMatrixₗ = LinearEquiv.refl R (Matrix m n A)

instance CStarMatrix.instOne {n : Type u_2} {A : Type u_3} [Zero A] [One A] [DecidableEq n] : One (CStarMatrix n n A)

Equations

• CStarMatrix.instOne = inferInstanceAs (One (Matrix n n A))

theorem CStarMatrix.one_apply {n : Type u_2} {A : Type u_3} [Zero A] [One A] [DecidableEq n] {i j : n} : 1 i j = if i = j then 1 else 0

@[simp]

theorem CStarMatrix.one_apply_eq {n : Type u_2} {A : Type u_3} [Zero A] [One A] [DecidableEq n] (i : n) : 1 i i = 1

@[simp]

theorem CStarMatrix.one_apply_ne {n : Type u_2} {A : Type u_3} [Zero A] [One A] [DecidableEq n] {i j : n} : i ≠ j → 1 i j = 0

theorem CStarMatrix.one_apply_ne' {n : Type u_2} {A : Type u_3} [Zero A] [One A] [DecidableEq n] {i j : n} : j ≠ i → 1 i j = 0

instance CStarMatrix.instAddMonoidWithOne {n : Type u_2} {A : Type u_3} [Zero A] [One A] [DecidableEq n] [AddMonoidWithOne A] : AddMonoidWithOne (CStarMatrix n n A)

Equations

• CStarMatrix.instAddMonoidWithOne = AddMonoidWithOne.mk ⋯ ⋯

instance CStarMatrix.instAddGroupWithOne {n : Type u_2} {A : Type u_3} [Zero A] [One A] [DecidableEq n] [AddGroupWithOne A] : AddGroupWithOne (CStarMatrix n n A)

Equations

• CStarMatrix.instAddGroupWithOne = AddGroupWithOne.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance CStarMatrix.instAddCommMonoidWithOne {n : Type u_2} {A : Type u_3} [Zero A] [One A] [DecidableEq n] [AddCommMonoidWithOne A] : AddCommMonoidWithOne (CStarMatrix n n A)

Equations

• CStarMatrix.instAddCommMonoidWithOne = AddCommMonoidWithOne.mk ⋯

instance CStarMatrix.instAddCommGroupWithOne {n : Type u_2} {A : Type u_3} [Zero A] [One A] [DecidableEq n] [AddCommGroupWithOne A] : AddCommGroupWithOne (CStarMatrix n n A)

Equations

• CStarMatrix.instAddCommGroupWithOne = AddCommGroupWithOne.mk ⋯ ⋯ ⋯ ⋯

@[defaultInstance 100]

instance CStarMatrix.instHMulOfFintypeOfMulOfAddCommMonoid {m : Type u_1} {n : Type u_2} {A : Type u_3} {l : Type u_7} [Fintype m] [Mul A] [AddCommMonoid A] : HMul (CStarMatrix l m A) (CStarMatrix m n A) (CStarMatrix l n A)

Equations

• One or more equations did not get rendered due to their size.

instance CStarMatrix.instMulOfFintypeOfAddCommMonoid {n : Type u_2} {A : Type u_3} [Fintype n] [Mul A] [AddCommMonoid A] : Mul (CStarMatrix n n A)

Equations

• CStarMatrix.instMulOfFintypeOfAddCommMonoid = { mul := fun (M N : CStarMatrix n n A) => M * N }

theorem CStarMatrix.mul_apply {m : Type u_1} {n : Type u_2} {A : Type u_3} {l : Type u_7} [Fintype m] [Mul A] [AddCommMonoid A] {M : CStarMatrix l m A} {N : CStarMatrix m n A} {i : l} {k : n} : (M * N) i k = ∑ j : m, M i j * N j k

theorem CStarMatrix.mul_apply' {m : Type u_1} {n : Type u_2} {A : Type u_3} {l : Type u_7} [Fintype m] [Mul A] [AddCommMonoid A] {M : CStarMatrix l m A} {N : CStarMatrix m n A} {i : l} {k : n} : (M * N) i k = (fun (j : m) => M i j) ⬝ᵥ fun (j : m) => N j k

@[simp]

theorem CStarMatrix.smul_mul {m : Type u_1} {n : Type u_2} {A : Type u_3} {R : Type u_5} {l : Type u_7} [Fintype n] [Monoid R] [AddCommMonoid A] [Mul A] [DistribMulAction R A] [IsScalarTower R A A] (a : R) (M : CStarMatrix m n A) (N : CStarMatrix n l A) : a • M * N = a • (M * N)

theorem CStarMatrix.mul_smul {m : Type u_1} {n : Type u_2} {A : Type u_3} {R : Type u_5} {l : Type u_7} [Fintype n] [Monoid R] [AddCommMonoid A] [Mul A] [DistribMulAction R A] [SMulCommClass R A A] (M : Matrix m n A) (a : R) (N : Matrix n l A) : M * a • N = a • (M * N)

instance CStarMatrix.instNonUnitalNonAssocSemiring {n : Type u_2} {A : Type u_3} [Fintype n] [NonUnitalNonAssocSemiring A] : NonUnitalNonAssocSemiring (CStarMatrix n n A)

Equations

• CStarMatrix.instNonUnitalNonAssocSemiring = inferInstanceAs (NonUnitalNonAssocSemiring (Matrix n n A))

instance CStarMatrix.instNonUnitalNonAssocRing {n : Type u_2} {A : Type u_3} [Fintype n] [NonUnitalNonAssocRing A] : NonUnitalNonAssocRing (CStarMatrix n n A)

Equations

• CStarMatrix.instNonUnitalNonAssocRing = inferInstanceAs (NonUnitalNonAssocRing (Matrix n n A))

instance CStarMatrix.instNonUnitalSemiring {n : Type u_2} {A : Type u_3} [Fintype n] [NonUnitalSemiring A] : NonUnitalSemiring (CStarMatrix n n A)

Equations

• CStarMatrix.instNonUnitalSemiring = inferInstanceAs (NonUnitalSemiring (Matrix n n A))

instance CStarMatrix.instNonAssocSemiring {n : Type u_2} {A : Type u_3} [Fintype n] [DecidableEq n] [NonAssocSemiring A] : NonAssocSemiring (CStarMatrix n n A)

Equations

• CStarMatrix.instNonAssocSemiring = inferInstanceAs (NonAssocSemiring (Matrix n n A))

instance CStarMatrix.instNonUnitalRing {n : Type u_2} {A : Type u_3} [Fintype n] [NonUnitalRing A] : NonUnitalRing (CStarMatrix n n A)

Equations

• CStarMatrix.instNonUnitalRing = inferInstanceAs (NonUnitalRing (Matrix n n A))

instance CStarMatrix.instNonAssocRing {n : Type u_2} {A : Type u_3} [Fintype n] [DecidableEq n] [NonAssocRing A] : NonAssocRing (CStarMatrix n n A)

Equations

• CStarMatrix.instNonAssocRing = inferInstanceAs (NonAssocRing (Matrix n n A))

instance CStarMatrix.instSemiring {n : Type u_2} {A : Type u_3} [Fintype n] [DecidableEq n] [Semiring A] : Semiring (CStarMatrix n n A)

Equations

• CStarMatrix.instSemiring = inferInstanceAs (Semiring (Matrix n n A))

instance CStarMatrix.instRing {n : Type u_2} {A : Type u_3} [Fintype n] [DecidableEq n] [Ring A] : Ring (CStarMatrix n n A)

Equations

• CStarMatrix.instRing = inferInstanceAs (Ring (Matrix n n A))

def CStarMatrix.ofMatrixRingEquiv {n : Type u_2} {A : Type u_3} [Fintype n] [Semiring A] : Matrix n n A ≃+* CStarMatrix n n A

ofMatrix bundled as a ring equivalence.

Equations

• CStarMatrix.ofMatrixRingEquiv = { toEquiv := CStarMatrix.ofMatrix, map_mul' := ⋯, map_add' := ⋯ }

instance CStarMatrix.instStarRing {n : Type u_2} {A : Type u_3} [Fintype n] [NonUnitalSemiring A] [StarRing A] : StarRing (CStarMatrix n n A)

Equations

• CStarMatrix.instStarRing = inferInstanceAs (StarRing (Matrix n n A))

instance CStarMatrix.instAlgebra {n : Type u_2} {A : Type u_3} {R : Type u_5} [Fintype n] [DecidableEq n] [CommSemiring R] [Semiring A] [Algebra R A] : Algebra R (CStarMatrix n n A)

Equations

• CStarMatrix.instAlgebra = inferInstanceAs (Algebra R (Matrix n n A))

def CStarMatrix.ofMatrixStarAlgEquiv {n : Type u_2} {A : Type u_3} [Fintype n] [SMul ℂ A] [Semiring A] [StarRing A] : Matrix n n A ≃⋆ₐ[ℂ] CStarMatrix n n A

ofMatrix bundled as a star algebra equivalence.

Equations

• CStarMatrix.ofMatrixStarAlgEquiv = { toRingEquiv := CStarMatrix.ofMatrixRingEquiv, map_star' := ⋯, map_smul' := ⋯ }

theorem CStarMatrix.ofMatrix_eq_ofMatrixStarAlgEquiv {n : Type u_2} {A : Type u_3} [Fintype n] [SMul ℂ A] [Semiring A] [StarRing A] : ⇑ofMatrix = ⇑ofMatrixStarAlgEquiv

def CStarMatrix.toCLM {m : Type u_1} {n : Type u_2} {A : Type u_3} [Fintype m] [Fintype n] [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] : CStarMatrix m n A →ₗ[ℂ] WithCStarModule (n → A) →L[ℂ] WithCStarModule (m → A)

Interpret a CStarMatrix m n A as a continuous linear map acting on C⋆ᵐᵒᵈ (n → A).

Equations

• One or more equations did not get rendered due to their size.

theorem CStarMatrix.toCLM_apply {m : Type u_1} {n : Type u_2} {A : Type u_3} [Fintype m] [Fintype n] [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {M : CStarMatrix m n A} {v : WithCStarModule (n → A)} : (toCLM M) v = (WithCStarModule.equiv (m → A)).symm (Matrix.mulVec M v)

theorem CStarMatrix.toCLM_apply_eq_sum {m : Type u_1} {n : Type u_2} {A : Type u_3} [Fintype m] [Fintype n] [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {M : CStarMatrix m n A} {v : WithCStarModule (n → A)} : (toCLM M) v = (WithCStarModule.equiv (m → A)).symm fun (i : m) => ∑ j : n, M i j * v j

def CStarMatrix.toCLMNonUnitalAlgHom {n : Type u_2} {A : Type u_3} [Fintype n] [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] : CStarMatrix n n A →ₙₐ[ℂ] WithCStarModule (n → A) →L[ℂ] WithCStarModule (n → A)

Interpret a CStarMatrix m n A as a continuous linear map acting on C⋆ᵐᵒᵈ (n → A). This version is specialized to the case m = n and is bundled as a non-unital algebra homomorphism.

Equations

• CStarMatrix.toCLMNonUnitalAlgHom = { toFun := CStarMatrix.toCLM.toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ }

theorem CStarMatrix.toCLMNonUnitalAlgHom_eq_toCLM {n : Type u_2} {A : Type u_3} [Fintype n] [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {M : CStarMatrix n n A} : toCLMNonUnitalAlgHom M = toCLM M

@[simp]

theorem CStarMatrix.toCLM_apply_single {m : Type u_1} {n : Type u_2} {A : Type u_3} [Fintype m] [Fintype n] [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] [DecidableEq n] {M : CStarMatrix m n A} {j : n} (a : A) : (toCLM M) ((WithCStarModule.equiv (n → A)).symm (Pi.single j a)) = (WithCStarModule.equiv (m → A)).symm fun (i : m) => M i j * a

theorem CStarMatrix.toCLM_apply_single_apply {m : Type u_1} {n : Type u_2} {A : Type u_3} [Fintype m] [Fintype n] [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] [DecidableEq n] {M : CStarMatrix m n A} {i : m} {j : n} (a : A) : (toCLM M) ((WithCStarModule.equiv (n → A)).symm (Pi.single j a)) i = M i j * a

theorem CStarMatrix.mul_entry_mul_eq_inner_toCLM {m : Type u_1} {n : Type u_2} {A : Type u_3} [Fintype m] [Fintype n] [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] [DecidableEq m] [DecidableEq n] {M : CStarMatrix m n A} {i : m} {j : n} (a b : A) : star a * M i j * b = inner ((WithCStarModule.equiv (m → A)).symm (Pi.single i a)) ((toCLM M) ((WithCStarModule.equiv (n → A)).symm (Pi.single j b)))

theorem CStarMatrix.toCLM_injective {m : Type u_1} {n : Type u_2} {A : Type u_3} [Fintype m] [Fintype n] [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] [DecidableEq n] : Function.Injective ⇑toCLM

theorem CStarMatrix.inner_toCLM_conjTranspose_left {m : Type u_1} {n : Type u_2} {A : Type u_3} [Fintype m] [Fintype n] [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {M : CStarMatrix m n A} {v : WithCStarModule (m → A)} {w : WithCStarModule (n → A)} : inner ((toCLM (Matrix.conjTranspose M)) v) w = inner v ((toCLM M) w)

theorem CStarMatrix.inner_toCLM_conjTranspose_right {m : Type u_1} {n : Type u_2} {A : Type u_3} [Fintype m] [Fintype n] [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {M : CStarMatrix m n A} {v : WithCStarModule (n → A)} {w : WithCStarModule (m → A)} : inner v ((toCLM (Matrix.conjTranspose M)) w) = inner ((toCLM M) v) w

noncomputable instance CStarMatrix.instNorm {m : Type u_1} {n : Type u_2} {A : Type u_3} [Fintype m] [Fintype n] [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] : Norm (CStarMatrix m n A)

The operator norm on CStarMatrix m n A.

Equations

• CStarMatrix.instNorm = { norm := fun (M : CStarMatrix m n A) => ‖CStarMatrix.toCLM M‖ }

theorem CStarMatrix.norm_def {m : Type u_1} {n : Type u_2} {A : Type u_3} [Fintype m] [Fintype n] [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {M : CStarMatrix m n A} : ‖M‖ = ‖toCLM M‖

theorem CStarMatrix.norm_def' {n : Type u_2} {A : Type u_3} [Fintype n] [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {M : CStarMatrix n n A} : ‖M‖ = ‖toCLMNonUnitalAlgHom M‖

theorem CStarMatrix.normedSpaceCore {m : Type u_1} {n : Type u_2} {A : Type u_3} [Fintype m] [Fintype n] [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] [DecidableEq n] : NormedSpace.Core ℂ (CStarMatrix m n A)

theorem CStarMatrix.norm_entry_le_norm {m : Type u_1} {n : Type u_2} {A : Type u_3} [Fintype m] [Fintype n] [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] [DecidableEq n] {M : CStarMatrix m n A} {i : m} {j : n} : ‖M i j‖ ≤ ‖M‖

theorem CStarMatrix.norm_le_of_forall_inner_le {m : Type u_1} {n : Type u_2} {A : Type u_3} [Fintype m] [Fintype n] [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {M : CStarMatrix m n A} {C : NNReal} (h : ∀ (v : WithCStarModule (n → A)) (w : WithCStarModule (m → A)), ‖inner w ((toCLM M) v)‖ ≤ ↑C * ‖v‖ * ‖w‖) : ‖M‖ ≤ ↑C

instance CStarMatrix.instTopologicalSpace {A : Type u_1} [NonUnitalCStarAlgebra A] {m : Type u_2} {n : Type u_3} : TopologicalSpace (CStarMatrix m n A)

Equations

• CStarMatrix.instTopologicalSpace = Pi.topologicalSpace

instance CStarMatrix.instUniformSpace {A : Type u_1} [NonUnitalCStarAlgebra A] {m : Type u_2} {n : Type u_3} : UniformSpace (CStarMatrix m n A)

Equations

• CStarMatrix.instUniformSpace = Pi.uniformSpace fun (a : m) => n → A

instance CStarMatrix.instBornology {A : Type u_1} [NonUnitalCStarAlgebra A] {m : Type u_2} {n : Type u_3} : Bornology (CStarMatrix m n A)

Equations

• CStarMatrix.instBornology = Pi.instBornology

instance CStarMatrix.instCompleteSpace {A : Type u_1} [NonUnitalCStarAlgebra A] {m : Type u_2} {n : Type u_3} : CompleteSpace (CStarMatrix m n A)

instance CStarMatrix.instT2Space {A : Type u_1} [NonUnitalCStarAlgebra A] {m : Type u_2} {n : Type u_3} : T2Space (CStarMatrix m n A)

instance CStarMatrix.instT3Space {A : Type u_1} [NonUnitalCStarAlgebra A] {m : Type u_2} {n : Type u_3} : T3Space (CStarMatrix m n A)

instance CStarMatrix.instTopologicalAddGroup {A : Type u_1} [NonUnitalCStarAlgebra A] {m : Type u_2} {n : Type u_3} : TopologicalAddGroup (CStarMatrix m n A)

instance CStarMatrix.instUniformAddGroup {A : Type u_1} [NonUnitalCStarAlgebra A] {m : Type u_2} {n : Type u_3} : UniformAddGroup (CStarMatrix m n A)

instance CStarMatrix.instContinuousSMul {A : Type u_1} [NonUnitalCStarAlgebra A] {m : Type u_2} {n : Type u_3} {R : Type u_4} [SMul R A] [TopologicalSpace R] [ContinuousSMul R A] : ContinuousSMul R (CStarMatrix m n A)

noncomputable instance CStarMatrix.instNormedAddCommGroup {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {m : Type u_2} {n : Type u_3} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] : NormedAddCommGroup (CStarMatrix m n A)

Equations

• CStarMatrix.instNormedAddCommGroup = NormedAddCommGroup.ofCoreReplaceAll ⋯ ⋯ ⋯

instance CStarMatrix.instNormedSpace {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {m : Type u_2} {n : Type u_3} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] : NormedSpace ℂ (CStarMatrix m n A)

Equations

• CStarMatrix.instNormedSpace = NormedSpace.ofCore ⋯

noncomputable instance CStarMatrix.instNonUnitalNormedRing {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {n : Type u_3} [Fintype n] [DecidableEq n] : NonUnitalNormedRing (CStarMatrix n n A)

Equations

• CStarMatrix.instNonUnitalNormedRing = NonUnitalNormedRing.mk ⋯ ⋯

instance CStarMatrix.instCStarRing {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {n : Type u_3} [Fintype n] [DecidableEq n] : CStarRing (CStarMatrix n n A)

Matrices with entries in a C⋆-algebra form a C⋆-algebra.

noncomputable instance CStarMatrix.instNonUnitalCStarAlgebra {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {n : Type u_3} [Fintype n] [DecidableEq n] : NonUnitalCStarAlgebra (CStarMatrix n n A)

Matrices with entries in a non-unital C⋆-algebra form a non-unital C⋆-algebra.

Equations

• CStarMatrix.instNonUnitalCStarAlgebra = NonUnitalCStarAlgebra.mk

instance CStarMatrix.instPartialOrder {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {n : Type u_3} [Fintype n] [DecidableEq n] : PartialOrder (CStarMatrix n n A)

Equations

• CStarMatrix.instPartialOrder = CStarAlgebra.spectralOrder (CStarMatrix n n A)

instance CStarMatrix.instStarOrderedRing {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {n : Type u_3} [Fintype n] [DecidableEq n] : StarOrderedRing (CStarMatrix n n A)

noncomputable instance CStarMatrix.instNormedRing {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {n : Type u_2} [Fintype n] [DecidableEq n] : NormedRing (CStarMatrix n n A)

Equations

• CStarMatrix.instNormedRing = NormedRing.mk ⋯ ⋯

noncomputable instance CStarMatrix.instNormedAlgebra {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {n : Type u_2} [Fintype n] [DecidableEq n] : NormedAlgebra ℂ (CStarMatrix n n A)

Equations

• CStarMatrix.instNormedAlgebra = NormedAlgebra.mk ⋯

noncomputable instance CStarMatrix.instCStarAlgebra {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {n : Type u_2} [Fintype n] [DecidableEq n] : CStarAlgebra (CStarMatrix n n A)

Matrices with entries in a unital C⋆-algebra form a unital C⋆-algebra.

Equations

• CStarMatrix.instCStarAlgebra = CStarAlgebra.mk

theorem CStarMatrix.uniformEmbedding_ofMatrix {m : Type u_1} {n : Type u_2} {A : Type u_3} [NonUnitalCStarAlgebra A] : IsUniformEmbedding ⇑ofMatrix

def CStarMatrix.ofMatrixL {m : Type u_1} {n : Type u_2} {A : Type u_3} [NonUnitalCStarAlgebra A] : Matrix m n A ≃L[ℂ] CStarMatrix m n A

ofMatrix bundled as a continuous linear equivalence.

Equations

• CStarMatrix.ofMatrixL = { toLinearEquiv := CStarMatrix.ofMatrixₗ, continuous_toFun := ⋯, continuous_invFun := ⋯ }

theorem CStarMatrix.ofMatrix_eq_ofMatrixL {m : Type u_1} {n : Type u_2} {A : Type u_3} [NonUnitalCStarAlgebra A] : ⇑ofMatrix = ⇑ofMatrixL