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_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

• 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_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

• 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_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

• M.conjTranspose = M.transpose.map star

@[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

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

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

• CStarMatrix.instInvolutiveStar = { toStar := CStarMatrix.instStar, star_involutive := ⋯ }

instance CStarMatrix.instInhabited {m : Type u_1} {n : Type u_2} {A : Type u_5} [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_5} [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_5} [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_5} [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_5} [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_5} [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_5} [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_5} [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_5} [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_5} [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_5} [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_5} [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_5} [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_5} [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_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

• CStarMatrix.instSMul = Pi.instSMul

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

• CStarMatrix.instMulAction = Pi.mulAction R

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

• CStarMatrix.instDistribMulAction = Pi.distribMulAction R

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

• 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_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] : ofMatrix 0 = 0

@[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

• CStarMatrix.instStarAddMonoid = { toInvolutiveStar := CStarMatrix.instInvolutiveStar, star_add := ⋯ }

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

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

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

• CStarMatrix.mapₗ f = { toFun := fun (M : CStarMatrix m n A) => M.map ⇑f, map_add' := ⋯, map_smul' := ⋯ }

@[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

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

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

• CStarMatrix.instAddMonoidWithOne = { natCast := Nat.unaryCast, toAddMonoid := CStarMatrix.instAddMonoid, toOne := CStarMatrix.instOne, natCast_zero := ⋯, natCast_succ := ⋯ }

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

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

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

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

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

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

@[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

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

instance CStarMatrix.instMulOfFintypeOfAddCommMonoid {n : Type u_2} {A : Type u_5} [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_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

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

instance CStarMatrix.instNonUnitalNonAssocRing {n : Type u_2} {A : Type u_5} [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_5} [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_5} [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_5} [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_5} [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_5} [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_5} [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_5} [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_5} [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} {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

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

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

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

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

• CStarMatrix.reindexₗ R A eₘ eₙ = { toFun := (Matrix.reindex eₘ eₙ).toFun, map_add' := ⋯, map_smul' := ⋯, invFun := (Matrix.reindex eₘ eₙ).invFun, left_inv := ⋯, right_inv := ⋯ }

@[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

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

@[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

• CStarMatrix.mapₙₐ f = { toFun := fun (M : CStarMatrix n n A) => (CStarMatrix.mapₗ ↑f) M, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }

@[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

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

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

• 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_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

• CStarMatrix.toCLMNonUnitalAlgHom = { toFun := (↑(MulOpposite.opLinearEquiv ℂ) ∘ₗ CStarMatrix.toCLM).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ }

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

• 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_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

• 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.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

• CStarMatrix.instNormedAddCommGroup = NormedAddCommGroup.ofCoreReplaceAll ⋯ ⋯ ⋯

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

• CStarMatrix.instNormedSpace = NormedSpace.ofCore ⋯

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

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

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

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

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

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

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

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 = { toAlgebra := CStarMatrix.instAlgebra, norm_smul_le := ⋯ }

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

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

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