Basic finite-dimensional matrix operators

This module contains the elementary trace and matrix-algebra facts used by the finite-dimensional quantum layer. It introduces the local operator abbreviation Op d = Matrix d d ℂ and keeps the basic trace bookkeeping independent of the positive-semidefinite order and normalized-trace material.

References

The declarations in this file are matrix facts for the LDT formalization of references/ldt-paper/.

Trace bookkeeping

theorem Matrix.trace_reindex {α : Type u_1} {β : Type u_2} {R : Type u_3} [Fintype α] [Fintype β] [AddCommMonoid R] (e : α ≃ β) (M : Matrix α α R) : ((reindex e e) M).trace = M.trace

Reindexing rows and columns by the same equivalence preserves matrix trace.

This generic matrix lemma is used when moving between equivalent finite index presentations of the same operator.

Linear matrix maps

def Matrix.submatrixLinearMap (R : Type u_1) {m : Type u_2} {n : Type u_3} {m' : Type u_4} {n' : Type u_5} {α : Type u_6} [Semiring R] [AddCommMonoid α] [Module R α] (row : m' → m) (col : n' → n) : Matrix m n α →ₗ[R] Matrix m' n' α

Taking a submatrix is linear in the ambient matrix.

This packages the entrywise linearity of Matrix.submatrix in the same style as Mathlib's block-diagonal additive and linear maps.

Equations

• Matrix.submatrixLinearMap R row col = { toFun := fun (A : Matrix m n α) => A.submatrix row col, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Matrix.submatrixLinearMap_apply (R : Type u_1) {m : Type u_2} {n : Type u_3} {m' : Type u_4} {n' : Type u_5} {α : Type u_6} [Semiring R] [AddCommMonoid α] [Module R α] (row : m' → m) (col : n' → n) (A : Matrix m n α) : (submatrixLinearMap R row col) A = A.submatrix row col

theorem Matrix.trace_blockDiagonal_mul {o : Type u_1} {m : Type u_2} {R : Type u_3} [Fintype o] [DecidableEq o] [Fintype m] [NonUnitalNonAssocSemiring R] (B D : o → Matrix m m R) : (blockDiagonal B * blockDiagonal D).trace = ∑ b : o, (B b * D b).trace

The trace pairing of two block-diagonal matrices is the sum of the trace pairings of the corresponding diagonal blocks.

Basic operator type

@[reducible, inline]

abbrev MIPStarRE.Quantum.Op (d : Type u_1) : Type u_1

Square complex matrices as the finite-dimensional operator algebra.

Equations

• MIPStarRE.Quantum.Op d = Matrix d d ℂ

Kronecker product bookkeeping

theorem MIPStarRE.Quantum.kronecker_sub_right {d₁ : Type u_1} {d₂ : Type u_2} {A : Op d₁} {B₁ B₂ : Op d₂} : Matrix.kronecker A B₁ - Matrix.kronecker A B₂ = Matrix.kronecker A (B₁ - B₂)

Kronecker product is additive in the right factor, rewritten for subtraction.

theorem MIPStarRE.Quantum.kronecker_sub_left {d₁ : Type u_1} {d₂ : Type u_2} {A₁ A₂ : Op d₁} {B : Op d₂} : Matrix.kronecker A₁ B - Matrix.kronecker A₂ B = Matrix.kronecker (A₁ - A₂) B

Kronecker product is additive in the left factor, rewritten for subtraction.