Documentation

Mathlib.Analysis.CStarAlgebra.CStarMatrix

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

Instances For

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

Instances For

@[simp]

theorem CStarMatrix.ofMatrix_apply {m : Type u_1} {n : Type u_2} {A : Type u_5} {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_5} {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_5} {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_5} {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_5} {B : Type u_6} (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

Instances For

@[simp]

theorem CStarMatrix.map_apply {m : Type u_1} {n : Type u_2} {A : Type u_5} {B : Type u_6} {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_5} (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_5} (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_5} {B : Type u_6} {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_5} {B : Type u_6} {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_5} (M : CStarMatrix m n A) :

CStarMatrix n m A

The transpose of a matrix.

Equations

Instances For

@[simp]

theorem CStarMatrix.transpose_apply {m : Type u_1} {n : Type u_2} {A : Type u_5} (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_5} [Star A] (M : CStarMatrix m n A) :

CStarMatrix n m A

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

Equations

Instances For

@[simp]

theorem CStarMatrix.conjTranspose_apply {m : Type u_1} {n : Type u_2} {A : Type u_5} [Star A] (M : CStarMatrix m n A) (i : n) (j : m) :

M.conjTranspose i j = star (M j i)

instance CStarMatrix.instStar {n : Type u_2} {A : Type u_5} [Star A] :

Star (CStarMatrix n n A)

Equations

theorem CStarMatrix.star_eq_conjTranspose {n : Type u_2} {A : Type u_5} [Star A] {M : CStarMatrix n n A} :

star M = M.conjTranspose

instance CStarMatrix.instInvolutiveStar {n : Type u_2} {A : Type u_5} [InvolutiveStar A] :

InvolutiveStar (CStarMatrix n n A)

Equations

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

Inhabited (CStarMatrix m n A)

Equations

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

DecidableEq (CStarMatrix m n A)

Equations

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

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_5} [Add A] :

Add (CStarMatrix m n A)

Equations

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

AddSemigroup (CStarMatrix m n A)

Equations

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

AddCommSemigroup (CStarMatrix m n A)

Equations

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

Zero (CStarMatrix m n A)

Equations

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

AddZeroClass (CStarMatrix m n A)

Equations

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

AddMonoid (CStarMatrix m n A)

Equations

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

AddCommMonoid (CStarMatrix m n A)

Equations

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

Neg (CStarMatrix m n A)

Equations

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

Sub (CStarMatrix m n A)

Equations

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

AddGroup (CStarMatrix m n A)

Equations

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

AddCommGroup (CStarMatrix m n A)

Equations

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

Unique (CStarMatrix m n A)

Equations

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

Subsingleton (CStarMatrix m n A)

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

Nontrivial (CStarMatrix m n A)

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

SMul R (CStarMatrix m n A)

Equations

instance CStarMatrix.instSMulCommClass {m : Type u_1} {n : Type u_2} {R : Type u_3} {S : Type u_4} {A : Type u_5} [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} {R : Type u_3} {S : Type u_4} {A : Type u_5} [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} {R : Type u_3} {A : 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} {R : Type u_3} {A : Type u_5} [Monoid R] [MulAction R A] :

MulAction R (CStarMatrix m n A)

Equations

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

DistribMulAction R (CStarMatrix m n A)

Equations

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

Module R (CStarMatrix m n A)

Equations

@[simp]

theorem CStarMatrix.zero_apply {m : Type u_1} {n : Type u_2} {A : Type u_5} [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_5} [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_5} {B : Type u_6} [SMul B A] (r : B) (M : CStarMatrix 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_5} [Sub A] (M N : CStarMatrix 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_5} [Neg A] (M : CStarMatrix m n A) (i : m) (j : n) :

(-M) i j = -M i j

@[simp]

theorem CStarMatrix.conjTranspose_zero {m : Type u_1} {n : Type u_2} {A : Type u_5} [AddMonoid A] [StarAddMonoid A] :

conjTranspose 0 = 0

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_5} [Zero A] :

@[simp]

theorem CStarMatrix.of_add_of {m : Type u_1} {n : Type u_2} {A : Type u_5} [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_5} [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_5} [Neg A] (f : Matrix m n A) :

-ofMatrix f = ofMatrix (-f)

@[simp]

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

r • ofMatrix f = ofMatrix (r • f)

theorem CStarMatrix.star_apply {n : Type u_2} {A : Type u_5} [Star A] {f : CStarMatrix n n A} {i j : n} :

star f i j = star (f j i)

theorem CStarMatrix.star_apply_of_isSelfAdjoint {n : Type u_2} {A : Type u_5} [Star A] {f : CStarMatrix n n A} (hf : IsSelfAdjoint f) {i j : n} :

star (f i j) = f j i

instance CStarMatrix.instStarAddMonoid {n : Type u_2} {A : Type u_5} [AddMonoid A] [StarAddMonoid A] :

StarAddMonoid (CStarMatrix n n A)

Equations

instance CStarMatrix.instStarModule {n : Type u_2} {R : Type u_3} {A : 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} {R : Type u_3} {A : 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

Instances For

def CStarMatrix.mapₗ {m : Type u_1} {n : Type u_2} {R : Type u_3} {S : Type u_4} {A : Type u_5} {B : Type u_6} [Semiring R] [Semiring S] {σ : R →+* S} [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module S B] (f : A →ₛₗ[σ] B) :

CStarMatrix m n A →ₛₗ[σ] CStarMatrix m n B

The semilinear map constructed by applying a semilinear map to all the entries of the matrix.

Equations

Instances For

@[simp]

theorem CStarMatrix.mapₗ_apply {m : Type u_1} {n : Type u_2} {R : Type u_3} {S : Type u_4} {A : Type u_5} {B : Type u_6} [Semiring R] [Semiring S] {σ : R →+* S} [AddCommMonoid A] [AddCommMonoid B] [Module R A] [Module S B] (f : A →ₛₗ[σ] B) (M : CStarMatrix m n A) :

(mapₗ f) M = M.map ⇑f

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

One (CStarMatrix n n A)

Equations

theorem CStarMatrix.one_apply {n : Type u_2} {A : Type u_5} [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_5} [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_5} [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_5} [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_5} [Zero A] [One A] [DecidableEq n] [AddMonoidWithOne A] :

AddMonoidWithOne (CStarMatrix n n A)

Equations

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

AddGroupWithOne (CStarMatrix n n A)

Equations

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

AddCommMonoidWithOne (CStarMatrix n n A)

Equations

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

AddCommGroupWithOne (CStarMatrix n n A)

Equations

@[defaultInstance 100]

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

HMul (CStarMatrix l m A) (CStarMatrix m n A) (CStarMatrix l n A)

Equations

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

Mul (CStarMatrix n n A)

Equations

theorem CStarMatrix.mul_apply {m : Type u_1} {n : Type u_2} {A : Type u_5} {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_5} {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} {R : Type u_3} {A : 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} {R : Type u_3} {A : Type u_5} {l : Type u_7} [Fintype n] [Monoid R] [AddCommMonoid A] [Mul A] [DistribMulAction R A] [SMulCommClass R A A] (M : CStarMatrix m n A) (a : R) (N : CStarMatrix n l A) :

M * a • N = a • (M * N)

@[simp]

theorem CStarMatrix.mul_zero {m : Type u_1} {n : Type u_2} {A : Type u_5} {o : Type u_7} [Fintype n] [NonUnitalNonAssocSemiring A] (M : CStarMatrix m n A) :

M * 0 = 0

@[simp]

theorem CStarMatrix.zero_mul {m : Type u_1} {n : Type u_2} {A : Type u_5} {l : Type u_7} [Fintype m] [NonUnitalNonAssocSemiring A] (M : CStarMatrix m n A) :

0 * M = 0

theorem CStarMatrix.mul_add {m : Type u_1} {n : Type u_2} {A : Type u_5} {o : Type u_7} [Fintype n] [NonUnitalNonAssocSemiring A] (L : CStarMatrix m n A) (M N : CStarMatrix n o A) :

L * (M + N) = L * M + L * N

theorem CStarMatrix.add_mul {m : Type u_1} {n : Type u_2} {A : Type u_5} {l : Type u_7} [Fintype m] [NonUnitalNonAssocSemiring A] (L M : CStarMatrix l m A) (N : CStarMatrix m n A) :

(L + M) * N = L * N + M * N

instance CStarMatrix.instNonUnitalNonAssocSemiring {n : Type u_2} {A : Type u_5} [Fintype n] [NonUnitalNonAssocSemiring A] :

NonUnitalNonAssocSemiring (CStarMatrix n n A)

Equations

instance CStarMatrix.instNonUnitalNonAssocRing {n : Type u_2} {A : Type u_5} [Fintype n] [NonUnitalNonAssocRing A] :

NonUnitalNonAssocRing (CStarMatrix n n A)

Equations

instance CStarMatrix.instNonUnitalSemiring {n : Type u_2} {A : Type u_5} [Fintype n] [NonUnitalSemiring A] :

NonUnitalSemiring (CStarMatrix n n A)

Equations

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

NonAssocSemiring (CStarMatrix n n A)

Equations

instance CStarMatrix.instNonUnitalRing {n : Type u_2} {A : Type u_5} [Fintype n] [NonUnitalRing A] :

NonUnitalRing (CStarMatrix n n A)

Equations

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

NonAssocRing (CStarMatrix n n A)

Equations

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

Semiring (CStarMatrix n n A)

Equations

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

Ring (CStarMatrix n n A)

Equations

def CStarMatrix.ofMatrixRingEquiv {n : Type u_2} {A : Type u_5} [Fintype n] [Semiring A] :

Matrix n n A ≃+* CStarMatrix n n A

ofMatrix bundled as a ring equivalence.

Equations

Instances For

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

StarRing (CStarMatrix n n A)

Equations

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

Algebra R (CStarMatrix n n A)

Equations

def CStarMatrix.ofMatrixStarAlgEquiv {n : Type u_2} {A : Type u_5} [Fintype n] [SMul ℂ A] [Semiring A] [StarRing A] :

Matrix n n A ≃⋆ₐ[ℂ ] CStarMatrix n n A

ofMatrix bundled as a star algebra equivalence.

Equations

Instances For

theorem CStarMatrix.ofMatrix_eq_ofMatrixStarAlgEquiv {n : Type u_2} {A : Type u_5} [Fintype n] [SMul ℂ A] [Semiring A] [StarRing A] :

⇑ofMatrix = ⇑ofMatrixStarAlgEquiv

def CStarMatrix.reindexₗ {m : Type u_1} {n : Type u_2} (R : Type u_3) (A : Type u_5) {l : Type u_7} {o : Type u_8} [Semiring R] [AddCommMonoid A] [Module R A] (eₘ : m ≃ l) (eₙ : n ≃ o) :

CStarMatrix m n A ≃ₗ[R] CStarMatrix l o A

The natural map that reindexes a matrix's rows and columns with equivalent types is an equivalence.

Equations

Instances For

@[simp]

theorem CStarMatrix.reindexₗ_apply {m : Type u_1} {n : Type u_2} {R : Type u_3} {A : Type u_5} {l : Type u_7} {o : Type u_8} [Semiring R] [AddCommMonoid A] [Module R A] {eₘ : m ≃ l} {eₙ : n ≃ o} {M : CStarMatrix m n A} {i : l} {j : o} :

(reindexₗ R A eₘ eₙ) M i j = (Matrix.reindex eₘ eₙ) M i j

def CStarMatrix.reindexₐ {m : Type u_1} {n : Type u_2} (R : Type u_7) (A : Type u_8) [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

The natural map that reindexes a matrix's rows and columns with equivalent types is an equivalence.

Equations

Instances For

@[simp]

theorem CStarMatrix.reindexₐ_apply {m : Type u_1} {n : Type u_2} {R : Type u_3} {A : Type u_5} [Fintype m] [Fintype n] [Semiring R] [AddCommMonoid A] [Mul A] [Star A] [Module R A] {e : m ≃ n} {M : CStarMatrix m m A} {i j : n} :

(reindexₐ R A e) M i j = (Matrix.reindex e e) M i j

theorem CStarMatrix.mapₗ_reindexₐ {m : Type u_1} {n : Type u_2} {R : Type u_3} {A : Type u_5} {B : Type u_6} [Fintype m] [Fintype n] [Semiring R] [AddCommMonoid A] [Mul A] [Module R A] [Star A] [AddCommMonoid B] [Mul B] [Module R B] [Star B] {e : m ≃ n} {M : CStarMatrix m m A} (φ : A →ₗ[R] B) :

(reindexₐ R B e) ((mapₗ φ) M) = (mapₗ φ) ((reindexₐ R A e) M)

@[simp]

theorem CStarMatrix.reindexₐ_symm {m : Type u_1} {n : Type u_2} {R : Type u_3} {A : Type u_5} [Fintype m] [Fintype n] [Semiring R] [AddCommMonoid A] [Mul A] [Module R A] [Star A] {e : m ≃ n} :

reindexₐ R A e.symm = (reindexₐ R A e).symm

def CStarMatrix.mapₙₐ {n : Type u_2} {R : Type u_3} {A : Type u_5} {B : Type u_6} [Fintype n] [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] (f : A →⋆ₙₐ[R] B) :

CStarMatrix n n A →⋆ₙₐ[R] CStarMatrix n n B

Applying a non-unital ⋆-algebra homomorphism to every entry of a matrix is itself a ⋆-algebra homomorphism on matrices.

Equations

Instances For

@[simp]

theorem CStarMatrix.mapₙₐ_apply {n : Type u_2} {R : Type u_3} {A : Type u_5} {B : Type u_6} [Fintype n] [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [Star A] [NonUnitalNonAssocSemiring B] [Module R B] [Star B] (f : A →⋆ₙₐ[R] B) (M : CStarMatrix n n A) :

(mapₙₐ f) M = (mapₗ ↑f) M

theorem CStarMatrix.algebraMap_apply {n : Type u_2} {R : Type u_3} {A : Type u_5} [Fintype n] [DecidableEq n] [CommSemiring R] [Semiring A] [Algebra R A] {r : R} {i j : n} :

(algebraMap R (CStarMatrix n n A)) r i j = if i = j then (algebraMap R A) r else 0

def CStarMatrix.toOneByOne (n : Type u_2) (R : Type u_3) (A : Type u_5) [Unique n] [Semiring R] [AddCommMonoid A] [Mul A] [Star A] [Module R A] :

A ≃⋆ₐ[R] CStarMatrix n n A

The ⋆-algebra equivalence between A and 1×1 matrices with its entry in A.

Equations

Instances For

noncomputable def CStarMatrix.toCLM {m : Type u_1} {n : Type u_2} {A : Type u_5} [Fintype m] [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] :

CStarMatrix m n A →ₗ[ℂ ] WithCStarModule A (m → A) →L[ℂ ] WithCStarModule A (n → A)

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

Equations

Instances For

theorem CStarMatrix.toCLM_apply {m : Type u_1} {n : Type u_2} {A : Type u_5} [Fintype m] [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {M : CStarMatrix m n A} {v : WithCStarModule A (m → A)} :

(toCLM M) v = (WithCStarModule.equiv A (n → A)).symm (Matrix.vecMul v M)

theorem CStarMatrix.toCLM_apply_eq_sum {m : Type u_1} {n : Type u_2} {A : Type u_5} [Fintype m] [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {M : CStarMatrix m n A} {v : WithCStarModule A (m → A)} :

(toCLM M) v = (WithCStarModule.equiv A (n → A)).symm fun (j : n) => ∑ i : m, v i * M i j

noncomputable def CStarMatrix.toCLMNonUnitalAlgHom {n : Type u_2} {A : Type u_5} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] [Fintype n] :

CStarMatrix n n A →ₙₐ[ℂ ] (WithCStarModule A (n → A) →L[ℂ ] WithCStarModule A (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

Instances For

theorem CStarMatrix.toCLMNonUnitalAlgHom_eq_toCLM {n : Type u_2} {A : Type u_5} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] [Fintype n] {M : CStarMatrix n n A} :

toCLMNonUnitalAlgHom M = MulOpposite.op (toCLM M)

@[simp]

theorem CStarMatrix.toCLM_apply_single {m : Type u_1} {n : Type u_2} {A : Type u_5} [Fintype m] [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] [DecidableEq m] {M : CStarMatrix m n A} {i : m} (a : A) :

(toCLM M) ((WithCStarModule.equiv A (m → A)).symm (Pi.single i a)) = (WithCStarModule.equiv A (n → A)).symm fun (j : n) => a * M i j

theorem CStarMatrix.toCLM_apply_single_apply {m : Type u_1} {n : Type u_2} {A : Type u_5} [Fintype m] [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] [DecidableEq m] {M : CStarMatrix m n A} {i : m} {j : n} (a : A) :

(toCLM M) ((WithCStarModule.equiv A (m → A)).symm (Pi.single i a)) j = a * M i j

theorem CStarMatrix.mul_entry_mul_eq_inner_toCLM {m : Type u_1} {n : Type u_2} {A : Type u_5} [Fintype m] [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] [Fintype n] [DecidableEq m] [DecidableEq n] {M : CStarMatrix m n A} {i : m} {j : n} (a b : A) :

a * M i j * star b = inner A ((WithCStarModule.equiv A (n → A)).symm (Pi.single j b)) ((toCLM M) ((WithCStarModule.equiv A (m → A)).symm (Pi.single i a)))

theorem CStarMatrix.toCLM_injective {m : Type u_1} {n : Type u_2} {A : Type u_5} [Fintype m] [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] :

Function.Injective ⇑toCLM

theorem CStarMatrix.inner_toCLM_conjTranspose_left {m : Type u_1} {n : Type u_2} {A : Type u_5} [Fintype m] [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] [Fintype n] {M : CStarMatrix m n A} {v : WithCStarModule A (n → A)} {w : WithCStarModule A (m → A)} :

inner A ((toCLM (Matrix.conjTranspose M)) v) w = inner A v ((toCLM M) w)

theorem CStarMatrix.inner_toCLM_conjTranspose_right {m : Type u_1} {n : Type u_2} {A : Type u_5} [Fintype m] [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] [Fintype n] {M : CStarMatrix m n A} {v : WithCStarModule A (m → A)} {w : WithCStarModule A (n → A)} :

inner A v ((toCLM (Matrix.conjTranspose M)) w) = inner A ((toCLM M) v) w

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

Norm (CStarMatrix m n A)

The operator norm on CStarMatrix m n A.

Equations

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

‖M‖ = ‖toCLM M‖

theorem CStarMatrix.norm_def' {n : Type u_2} {A : Type u_5} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] [Fintype n] {M : CStarMatrix n n A} :

‖M‖ = ‖toCLMNonUnitalAlgHom M‖

theorem CStarMatrix.normedSpaceCore {m : Type u_1} {n : Type u_2} {A : Type u_5} [Fintype m] [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] [Fintype n] :

NormedSpace.Core ℂ (CStarMatrix m n A)

theorem CStarMatrix.norm_entry_le_norm {m : Type u_1} {n : Type u_2} {A : Type u_5} [Fintype m] [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] [Fintype 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_5} [Fintype m] [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] [Fintype n] {M : CStarMatrix m n A} {C : NNReal} (h : ∀ (v : WithCStarModule A (m → A)) (w : WithCStarModule A (n → A)), ‖inner A 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

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

UniformSpace (CStarMatrix m n A)

Equations

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

Bornology (CStarMatrix m n A)

Equations

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.instIsTopologicalAddGroup {A : Type u_1} [NonUnitalCStarAlgebra A] {m : Type u_2} {n : Type u_3} :

IsTopologicalAddGroup (CStarMatrix m n A)

instance CStarMatrix.instIsUniformAddGroup {A : Type u_1} [NonUnitalCStarAlgebra A] {m : Type u_2} {n : Type u_3} :

IsUniformAddGroup (CStarMatrix m n A)

@[deprecated CStarMatrix.instIsUniformAddGroup (since := "2025-03-31")]

theorem CStarMatrix.instUniformAddGroup {A : Type u_1} [NonUnitalCStarAlgebra A] {m : Type u_2} {n : Type u_3} :

IsUniformAddGroup (CStarMatrix m n A)

Alias of CStarMatrix.instIsUniformAddGroup.

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

NormedAddCommGroup (CStarMatrix m n A)

Equations

noncomputable 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] :

NormedSpace ℂ (CStarMatrix m n A)

Equations

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

NonUnitalNormedRing (CStarMatrix n n A)

Equations

instance CStarMatrix.instCStarRing {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {n : Type u_3} [Fintype 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] :

NonUnitalCStarAlgebra (CStarMatrix n n A)

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

Equations

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

PartialOrder (CStarMatrix n n A)

Equations

instance CStarMatrix.instStarOrderedRing {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {n : Type u_3} [Fintype 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

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

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

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

Instances For

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

⇑ofMatrix = ⇑ofMatrixL