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 copyCStarMatrix.instNonUnitalCStarAlgebra: square matrices with entries in a non-unital C⋆-algebra form a non-unital C⋆-algebraCStarMatrix.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.
Type copy Matrix m n A meant for matrices with entries in a C⋆-algebra. This is
a C⋆-algebra when m = n.
Instances For
The equivalence between Matrix m n A and CStarMatrix m n A.
Instances For
@[simp]
@[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}
:
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.
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_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.
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.
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)
@[implicit_reducible]
theorem
CStarMatrix.star_eq_conjTranspose
{n : Type u_2}
{A : Type u_5}
[Star A]
{M : CStarMatrix n n A}
:
star M = M.conjTranspose
@[implicit_reducible]
instance
CStarMatrix.instInvolutiveStar
{n : Type u_2}
{A : Type u_5}
[InvolutiveStar A]
:
InvolutiveStar (CStarMatrix n n A)
@[implicit_reducible]
instance
CStarMatrix.instInhabited
{m : Type u_1}
{n : Type u_2}
{A : Type u_5}
[Inhabited A]
:
Inhabited (CStarMatrix m n A)
@[implicit_reducible]
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)
@[implicit_reducible]
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 α)
instance
CStarMatrix.instFinite
{n : Type u_7}
{m : Type u_8}
[Finite m]
[Finite n]
(α : Type u_9)
[Finite α]
:
Finite (CStarMatrix m n α)
@[implicit_reducible]
instance
CStarMatrix.instAdd
{m : Type u_1}
{n : Type u_2}
{A : Type u_5}
[Add A]
:
Add (CStarMatrix m n A)
@[implicit_reducible]
instance
CStarMatrix.instAddSemigroup
{m : Type u_1}
{n : Type u_2}
{A : Type u_5}
[AddSemigroup A]
:
AddSemigroup (CStarMatrix m n A)
@[implicit_reducible]
instance
CStarMatrix.instAddCommSemigroup
{m : Type u_1}
{n : Type u_2}
{A : Type u_5}
[AddCommSemigroup A]
:
AddCommSemigroup (CStarMatrix m n A)
@[implicit_reducible]
instance
CStarMatrix.instZero
{m : Type u_1}
{n : Type u_2}
{A : Type u_5}
[Zero A]
:
Zero (CStarMatrix m n A)
@[implicit_reducible]
instance
CStarMatrix.instAddZeroClass
{m : Type u_1}
{n : Type u_2}
{A : Type u_5}
[AddZeroClass A]
:
AddZeroClass (CStarMatrix m n A)
@[implicit_reducible]
instance
CStarMatrix.instAddMonoid
{m : Type u_1}
{n : Type u_2}
{A : Type u_5}
[AddMonoid A]
:
AddMonoid (CStarMatrix m n A)
@[implicit_reducible]
instance
CStarMatrix.instAddCommMonoid
{m : Type u_1}
{n : Type u_2}
{A : Type u_5}
[AddCommMonoid A]
:
AddCommMonoid (CStarMatrix m n A)
@[implicit_reducible]
instance
CStarMatrix.instNeg
{m : Type u_1}
{n : Type u_2}
{A : Type u_5}
[Neg A]
:
Neg (CStarMatrix m n A)
@[implicit_reducible]
instance
CStarMatrix.instSub
{m : Type u_1}
{n : Type u_2}
{A : Type u_5}
[Sub A]
:
Sub (CStarMatrix m n A)
@[implicit_reducible]
instance
CStarMatrix.instAddGroup
{m : Type u_1}
{n : Type u_2}
{A : Type u_5}
[AddGroup A]
:
AddGroup (CStarMatrix m n A)
@[implicit_reducible]
instance
CStarMatrix.instAddCommGroup
{m : Type u_1}
{n : Type u_2}
{A : Type u_5}
[AddCommGroup A]
:
AddCommGroup (CStarMatrix m n A)
@[implicit_reducible]
instance
CStarMatrix.instUnique
{m : Type u_1}
{n : Type u_2}
{A : Type u_5}
[Unique A]
:
Unique (CStarMatrix m n A)
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)
@[implicit_reducible]
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)
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)
@[implicit_reducible]
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)
@[implicit_reducible]
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)
@[implicit_reducible]
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)
@[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)
:
@[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]
@[simp]
@[simp]
@[simp]
theorem
CStarMatrix.star_apply
{n : Type u_2}
{A : Type u_5}
[Star A]
{f : CStarMatrix n n A}
{i j : n}
:
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
@[implicit_reducible]
instance
CStarMatrix.instStarAddMonoid
{n : Type u_2}
{A : Type u_5}
[AddMonoid A]
[StarAddMonoid A]
:
StarAddMonoid (CStarMatrix n n A)
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]
:
The equivalence to matrices, bundled as a linear equivalence.
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)
:
The semilinear map constructed by applying a semilinear map to all the entries of the matrix.
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)
:
@[implicit_reducible]
instance
CStarMatrix.instOne
{n : Type u_2}
{A : Type u_5}
[DecidableEq n]
[Zero A]
[One A]
:
One (CStarMatrix n n A)
theorem
CStarMatrix.one_apply
{n : Type u_2}
{A : Type u_5}
[DecidableEq n]
[Zero A]
[One A]
{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}
[DecidableEq n]
[Zero A]
[One A]
(i : n)
:
1 i i = 1
@[simp]
theorem
CStarMatrix.one_apply_ne
{n : Type u_2}
{A : Type u_5}
[DecidableEq n]
[Zero A]
[One A]
{i j : n}
:
i ≠ j → 1 i j = 0
theorem
CStarMatrix.one_apply_ne'
{n : Type u_2}
{A : Type u_5}
[DecidableEq n]
[Zero A]
[One A]
{i j : n}
:
j ≠ i → 1 i j = 0
@[implicit_reducible]
instance
CStarMatrix.instAddMonoidWithOne
{n : Type u_2}
{A : Type u_5}
[DecidableEq n]
[AddMonoidWithOne A]
:
AddMonoidWithOne (CStarMatrix n n A)
@[implicit_reducible]
instance
CStarMatrix.instAddGroupWithOne
{n : Type u_2}
{A : Type u_5}
[DecidableEq n]
[AddGroupWithOne A]
:
AddGroupWithOne (CStarMatrix n n A)
@[implicit_reducible]
instance
CStarMatrix.instAddCommMonoidWithOne
{n : Type u_2}
{A : Type u_5}
[DecidableEq n]
[AddCommMonoidWithOne A]
:
AddCommMonoidWithOne (CStarMatrix n n A)
@[implicit_reducible]
instance
CStarMatrix.instAddCommGroupWithOne
{n : Type u_2}
{A : Type u_5}
[DecidableEq n]
[AddCommGroupWithOne A]
:
AddCommGroupWithOne (CStarMatrix n n A)
@[implicit_reducible, 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)
@[implicit_reducible]
instance
CStarMatrix.instMulOfFintypeOfAddCommMonoid
{n : Type u_2}
{A : Type u_5}
[Fintype n]
[Mul A]
[AddCommMonoid A]
:
Mul (CStarMatrix n n A)
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
@[implicit_reducible]
instance
CStarMatrix.instNonUnitalNonAssocSemiring
{n : Type u_2}
{A : Type u_5}
[Fintype n]
[NonUnitalNonAssocSemiring A]
:
NonUnitalNonAssocSemiring (CStarMatrix n n A)
@[implicit_reducible]
instance
CStarMatrix.instNonUnitalNonAssocRing
{n : Type u_2}
{A : Type u_5}
[Fintype n]
[NonUnitalNonAssocRing A]
:
NonUnitalNonAssocRing (CStarMatrix n n A)
@[implicit_reducible]
instance
CStarMatrix.instNonUnitalSemiring
{n : Type u_2}
{A : Type u_5}
[Fintype n]
[NonUnitalSemiring A]
:
NonUnitalSemiring (CStarMatrix n n A)
@[implicit_reducible]
instance
CStarMatrix.instNonAssocSemiring
{n : Type u_2}
{A : Type u_5}
[Fintype n]
[DecidableEq n]
[NonAssocSemiring A]
:
NonAssocSemiring (CStarMatrix n n A)
@[implicit_reducible]
instance
CStarMatrix.instNonUnitalRing
{n : Type u_2}
{A : Type u_5}
[Fintype n]
[NonUnitalRing A]
:
NonUnitalRing (CStarMatrix n n A)
@[implicit_reducible]
instance
CStarMatrix.instNonAssocRing
{n : Type u_2}
{A : Type u_5}
[Fintype n]
[DecidableEq n]
[NonAssocRing A]
:
NonAssocRing (CStarMatrix n n A)
@[implicit_reducible]
instance
CStarMatrix.instSemiring
{n : Type u_2}
{A : Type u_5}
[Fintype n]
[DecidableEq n]
[Semiring A]
:
Semiring (CStarMatrix n n A)
@[implicit_reducible]
instance
CStarMatrix.instRing
{n : Type u_2}
{A : Type u_5}
[Fintype n]
[DecidableEq n]
[Ring A]
:
Ring (CStarMatrix n n A)
@[implicit_reducible]
instance
CStarMatrix.instStarRing
{n : Type u_2}
{A : Type u_5}
[Fintype n]
[NonUnitalSemiring A]
[StarRing A]
:
StarRing (CStarMatrix n n A)
@[implicit_reducible]
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)
@[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
@[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)
:
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)
:
Applying a non-unital ⋆-algebra homomorphism to every entry of a matrix is itself a ⋆-algebra homomorphism on matrices.
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)
:
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]
:
The ⋆-algebra equivalence between A and 1×1 matrices with its entry in A.
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]
:
Interpret a CStarMatrix m n A as a continuous linear map acting on C⋆ᵐᵒᵈ (n → A).
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]
:
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.
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
@[implicit_reducible]
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.
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}
:
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}
:
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‖)
:
@[implicit_reducible]
instance
CStarMatrix.instTopologicalSpace
{A : Type u_1}
[NonUnitalCStarAlgebra A]
{m : Type u_2}
{n : Type u_3}
:
TopologicalSpace (CStarMatrix m n A)
@[implicit_reducible]
instance
CStarMatrix.instUniformSpace
{A : Type u_1}
[NonUnitalCStarAlgebra A]
{m : Type u_2}
{n : Type u_3}
:
UniformSpace (CStarMatrix m n A)
@[implicit_reducible]
instance
CStarMatrix.instBornology
{A : Type u_1}
[NonUnitalCStarAlgebra A]
{m : Type u_2}
{n : Type u_3}
:
Bornology (CStarMatrix m n A)
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)
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)
@[implicit_reducible]
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)
@[implicit_reducible]
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)
@[implicit_reducible]
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)
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.
@[implicit_reducible]
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.
@[implicit_reducible]
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)
instance
CStarMatrix.instStarOrderedRing
{A : Type u_1}
[NonUnitalCStarAlgebra A]
[PartialOrder A]
[StarOrderedRing A]
{n : Type u_3}
[Fintype n]
:
StarOrderedRing (CStarMatrix n n A)
@[implicit_reducible]
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)
@[implicit_reducible]
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)
@[implicit_reducible]
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.
theorem
CStarMatrix.uniformEmbedding_ofMatrix
{m : Type u_1}
{n : Type u_2}
{A : Type u_3}
[NonUnitalCStarAlgebra A]
:
ofMatrix bundled as a continuous linear equivalence.
Instances For
theorem
CStarMatrix.ofMatrix_eq_ofMatrixL
{m : Type u_1}
{n : Type u_2}
{A : Type u_3}
[NonUnitalCStarAlgebra A]
: