Linear functionals

This file contains results for linear functionals on the set of $n \times n$ matrices $M_n$ over $\mathbb{C}$.

Main results

• module.dual.apply
• module.dual.is_pos_map_iff
• module.dual.is_faithful_pos_map_iff
• module.dual.is_tracial_faithful_pos_map_iff
• module.dual.is_faithful_pos_map_iff_is_inner

theorem includeBlock_apply_mul {R : Type u_1} {k : Type u_2} {s : k → Type u_3} [CommSemiring R] [DecidableEq k] [(i : k) → Fintype (s i)] {i j : k} (x : Matrix (s i) (s i) R) (y : Matrix (s j) (s j) R) (p q : s j) : (Matrix.includeBlock x j * y) p q = if i = j then (Matrix.includeBlock x j * y) p q else 0

theorem includeBlock_mul_apply {R : Type u_1} {k : Type u_2} {s : k → Type u_3} [CommSemiring R] [DecidableEq k] [(i : k) → Fintype (s i)] {i j : k} (x : Matrix (s j) (s j) R) (y : Matrix (s i) (s i) R) (p q : s j) : (x * Matrix.includeBlock y j) p q = if i = j then (x * Matrix.includeBlock y j) p q else 0

def Module.Dual.matrix {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u_2} [CommSemiring R] (φ : Dual R (Matrix n n R)) : Matrix n n R

the matrix of a linear map φ : M_n →ₗ[R] R is given by ∑ i j, stdBasisMatrix j i (φ (stdBasisMatrix i j 1)).

Equations

• φ.matrix = ∑ i : n, ∑ j : n, Matrix.stdBasisMatrix j i (φ (Matrix.stdBasisMatrix i j 1))

theorem Module.Dual.apply {n : Type u_2} [Fintype n] [DecidableEq n] {R : Type u_1} [CommSemiring R] (φ : Dual R (Matrix n n R)) (a : Matrix n n R) : φ a = (φ.matrix * a).trace

given any linear functional φ : M_n →ₗ[R] R, we get φ a = (φ.matrix ⬝ a).trace.

def Module.Dual.pi {R : Type u_1} [CommSemiring R] {k : Type u_2} [Fintype k] {s : k → Type u_3} (φ : (i : k) → Dual R (Matrix (s i) (s i) R)) : Dual R (PiMat R k s)

we linear maps φ_i : M_[n_i] →ₗ[R] R, we define its direct sum as the linear map (Π i, M_[n_i]) →ₗ[R] R.

Equations

• Module.Dual.pi φ = { toFun := fun (a : PiMat R k s) => ∑ i : k, (φ i) (a i), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Module.Dual.pi_apply {R : Type u_1} [CommSemiring R] {k : Type u_2} [Fintype k] {s : k → Type u_3} (φ : (i : k) → Dual R (Matrix (s i) (s i) R)) (a : PiMat R k s) : (pi φ) a = ∑ i : k, (φ i) (a i)

def Module.Dual.pi_of {R : Type u_1} [CommSemiring R] {k : Type u_2} [Fintype k] [DecidableEq k] {s : k → Type u_3} (φ : Dual R (PiMat R k s)) (i : k) : Dual R (Matrix (s i) (s i) R)

Equations

• φ.pi_of x✝ = φ ∘ₗ Matrix.includeBlock

@[simp]

theorem Module.Dual.pi_of_apply {R : Type u_1} [CommSemiring R] {k : Type u_2} [Fintype k] [DecidableEq k] {s : k → Type u_3} (φ : Dual R (PiMat R k s)) (i : k) (a✝ : Matrix (s i) (s i) R) : (φ.pi_of i) a✝ = φ (Matrix.includeBlock a✝)

theorem Module.Dual.pi.apply {R : Type u_3} [CommSemiring R] {k : Type u_1} [Fintype k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] (φ : (i : k) → Dual R (Matrix (s i) (s i) R)) (x : PiMat R k s) : (pi φ) x = ∑ i : k, ((φ i).matrix * x i).trace

for direct sums, we get φ x = ∑ i, ((φ i).matrix ⬝ x i).trace

theorem Module.Dual.eq_pi_of_pi {R : Type u_3} [CommSemiring R] {k : Type u_1} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] (φ : (i : k) → Dual R (Matrix (s i) (s i) R)) : φ = (pi φ).pi_of

theorem Module.Dual.eq_pi_pi_of {R : Type u_3} [CommSemiring R] {k : Type u_1} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] (φ : Dual R (PiMat R k s)) : φ = pi φ.pi_of

theorem Module.Dual.pi.apply' {R : Type u_3} [CommSemiring R] {k : Type u_1} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] (φ : (i : k) → Dual R (Matrix (s i) (s i) R)) (x : PiMat R k s) : (pi φ) x = ∑ i : k, (Matrix.blockDiagonal' (Matrix.includeBlock (φ i).matrix) * Matrix.blockDiagonal' x).trace

theorem Module.Dual.pi_apply'' {R : Type u_3} [CommSemiring R] {k : Type u_1} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] (φ : Dual R (PiMat R k s)) (x : PiMat R k s) : φ x = ∑ i : k, ((φ.pi_of i).matrix * x i).trace

theorem Module.Dual.apply_eq_of {n : Type u_2} [Fintype n] [DecidableEq n] {R : Type u_1} [CommSemiring R] (φ : Dual R (Matrix n n R)) (x : Matrix n n R) (h : ∀ (a : Matrix n n R), φ a = (x * a).trace) : x = φ.matrix

theorem Module.Dual.eq_trace_unique {n : Type u_2} [Fintype n] [DecidableEq n] {R : Type u_1} [CommSemiring R] (φ : Dual R (Matrix n n R)) : ∃! Q : Matrix n n R, ∀ (a : Matrix n n R), φ a = (Q * a).trace

Any linear functional $f$ on $M_n$ is given by a unique matrix $Q \in M_n$ such that $f(x)=\operatorname{Tr}(Qx)$ for any $x \in M_n$.

def Module.Dual.pi' {R : Type u_1} [CommSemiring R] {k : Type u_2} [Fintype k] [DecidableEq k] {s : k → Type u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] (φ : (i : k) → Dual R (Matrix (s i) (s i) R)) : Dual R (Matrix.BlockDiagonals R k s)

Equations

• Module.Dual.pi' φ = Module.Dual.pi φ ∘ₗ Matrix.isBlockDiagonalPiAlgEquiv.toLinearMap

theorem Module.Dual.pi.apply_single_block {R : Type u_3} [CommSemiring R] {k : Type u_1} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] (φ : (i : k) → Matrix (s i) (s i) R →ₗ[R] R) (x : (i : k) → Matrix (s i) (s i) R) (i : k) : (pi φ) (Matrix.includeBlock (x i)) = (φ i) (x i)

⨁_i φ_i ι_i (x_i) = φ_i (x_i)

theorem Module.Dual.pi.apply_single_block' {R : Type u_3} [CommSemiring R] {k : Type u_1} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] (φ : (i : k) → Matrix (s i) (s i) R →ₗ[R] R) {i : k} (x : Matrix (s i) (s i) R) : (pi φ) (Matrix.includeBlock x) = (φ i) x

def Module.Dual.IsPosMap {𝕜 : Type u_1} [RCLike 𝕜] {A : Type u_2} [NonUnitalSemiring A] [StarRing A] [Module 𝕜 A] (φ : Dual 𝕜 A) : Prop

A linear functional $φ$ on $M_n$ is positive if $0 ≤ φ (x^*x)$ for all $x \in M_n$.

Equations

• φ.IsPosMap = ∀ (a : A), 0 ≤ φ (star a * a)

theorem Matrix.nonneg_iff {k : Type u_1} [Fintype k] [DecidableEq k] {x : Matrix k k ℂ} : 0 ≤ x ↔ ∃ (y : Matrix k k ℂ), x = star y * y

theorem PiMat.nonneg_iff {k : Type u_1} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {x : PiMat ℂ k s} : 0 ≤ x ↔ ∃ (y : PiMat ℂ k s), x = star y * y

theorem dual_isPosMap_of_linearMap_isPosMap {𝕜 : Type u_2} [RCLike 𝕜] {A : Type u_1} [NonUnitalSemiring A] [StarRing A] [Module 𝕜 A] [PartialOrder A] [StarOrderedRing A] {φ : Module.Dual 𝕜 A} (h : LinearMap.IsPosMap φ) : φ.IsPosMap

theorem Module.Dual.piIsPosMap_iff {𝕜 : Type u_3} [RCLike 𝕜] {k : Type u_1} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] (φ : Dual 𝕜 (PiMat 𝕜 k s)) : φ.IsPosMap ↔ ∀ (i : k), (φ.pi_of i).IsPosMap

theorem Module.Dual.pi_isPosMap_iff {𝕜 : Type u_3} [RCLike 𝕜] {k : Type u_1} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] (φ : (i : k) → Dual 𝕜 (Matrix (s i) (s i) 𝕜)) : (pi φ).IsPosMap ↔ ∀ (i : k), (φ i).IsPosMap

def Module.Dual.IsUnital {R : Type u_1} [CommSemiring R] {A : Type u_2} [AddCommMonoid A] [Module R A] [One A] (φ : Dual R A) : Prop

A linear functional $φ$ on $M_n$ is unital if $φ(1) = 1$.

Equations

• φ.IsUnital = (φ 1 = 1)

class Module.Dual.IsState {𝕜 : Type u_1} [RCLike 𝕜] {A : Type u_2} [Semiring A] [StarRing A] [Module 𝕜 A] (φ : Dual 𝕜 A) : Prop

A linear functional is called a state if it is positive and unital

• toIsPosMap : φ.IsPosMap
• toIsUnital : φ.IsUnital

theorem Module.Dual.IsState_iff {𝕜 : Type u_2} [RCLike 𝕜] {A : Type u_1} [Semiring A] [StarRing A] [Module 𝕜 A] (φ : Dual 𝕜 A) : φ.IsState ↔ φ.IsPosMap ∧ φ.IsUnital

theorem Module.Dual.isPosMap_of_matrix {n : Type u_2} [Fintype n] [DecidableEq n] {𝕜 : Type u_1} [RCLike 𝕜] (φ : Dual 𝕜 (Matrix n n 𝕜)) : φ.IsPosMap ↔ ∀ (a : Matrix n n 𝕜), a.PosSemidef → 0 ≤ φ a

def Module.Dual.IsFaithful {𝕜 : Type u_1} [RCLike 𝕜] {A : Type u_2} [NonUnitalSemiring A] [StarRing A] [Module 𝕜 A] (φ : Dual 𝕜 A) : Prop

A linear functional $f$ on $M_n$ is said to be faithful if $f(x^*x)=0$ if and only if $x=0$ for any $x \in M_n$.

Equations

• φ.IsFaithful = ∀ (a : A), φ (star a * a) = 0 ↔ a = 0

theorem Matrix.includeBlock_eq_zero {R : Type u_3} [CommSemiring R] {k : Type u_1} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {i : k} {x : Matrix (s i) (s i) R} : includeBlock x = 0 ↔ x = 0

theorem Module.Dual.piIsFaithful_iff {𝕜 : Type u_3} [RCLike 𝕜] {k : Type u_1} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {φ : Dual 𝕜 (PiMat 𝕜 k s)} (hφ : φ.IsPosMap) : φ.IsFaithful ↔ ∀ (i : k), (φ.pi_of i).IsFaithful

theorem Module.Dual.isFaithful_of_matrix {n : Type u_2} [Fintype n] [DecidableEq n] {𝕜 : Type u_1} [RCLike 𝕜] (φ : Dual 𝕜 (Matrix n n 𝕜)) : φ.IsFaithful ↔ ∀ (a : Matrix n n 𝕜), a.PosSemidef → (φ a = 0 ↔ a = 0)

theorem Module.Dual.isPosMap_iff_of_matrix {n : Type u_1} [Fintype n] [DecidableEq n] (φ : Dual ℂ (Matrix n n ℂ)) : φ.IsPosMap ↔ φ.matrix.PosSemidef

A linear functional $f$ is positive if and only if there exists a unique positive semi-definite matrix $Q\in M_n$ such $f(x)=\operatorname{Tr}(Qx)$ for all $x\in M_n$.

theorem Module.Dual.isState_iff_of_matrix {n : Type u_1} [Fintype n] [DecidableEq n] (φ : Dual ℂ (Matrix n n ℂ)) : φ.IsState ↔ φ.matrix.PosSemidef ∧ φ.matrix.trace = 1

A linear functional $f$ is a state if and only if there exists a unique positive semi-definite matrix $Q\in M_n$ such that its trace equals $1$ and $f(x)=\operatorname{Tr}(Qx)$ for all $x\in M_n$.

theorem Module.Dual.IsPosMap.isFaithful_iff_of_matrix {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Dual ℂ (Matrix n n ℂ)} (hs : φ.IsPosMap) : φ.IsFaithful ↔ φ.matrix.PosDef

A positive linear functional $f$ is faithful if and only if there exists a positive definite matrix such that $f(x)=\operatorname{Tr}(Qx)$ for all $x\in M_n$.

class Module.Dual.IsFaithfulPosMap {𝕜 : Type u_1} [RCLike 𝕜] {A : Type u_2} [NonUnitalSemiring A] [StarRing A] [Module 𝕜 A] (φ : Dual 𝕜 A) : Prop

• toIsPosMap : φ.IsPosMap
• toIsFaithful : φ.IsFaithful

theorem Module.Dual.IsFaithfulPosMap_iff {𝕜 : Type u_2} [RCLike 𝕜] {A : Type u_1} [NonUnitalSemiring A] [StarRing A] [Module 𝕜 A] (φ : Dual 𝕜 A) : φ.IsFaithfulPosMap ↔ φ.IsPosMap ∧ φ.IsFaithful

theorem Module.Dual.isFaithfulPosMap_iff_of_matrix {n : Type u_1} [Fintype n] [DecidableEq n] (φ : Dual ℂ (Matrix n n ℂ)) : φ.IsFaithfulPosMap ↔ φ.matrix.PosDef

A linear functional $φ$ is a faithful and positive if and only if there exists a unique positive definite matrix $Q$ such that $φ(x)=\operatorname{Tr}(Qx)$ for all $x\in M_n$.

theorem Module.Dual.IsState.isFaithful_iff_of_matrix {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Dual ℂ (Matrix n n ℂ)} (hs : φ.IsState) : φ.IsFaithful ↔ φ.matrix.PosDef ∧ φ.matrix.trace = 1

A state is faithful $f$ if and only if there exists a unique positive definite matrix $Q\in M_n$ with trace equal to $1$ and $f(x)=\operatorname{Tr}(Qx)$ for all $x \in M_n$.

theorem Module.Dual.isFaithful_state_iff_of_matrix {n : Type u_1} [Fintype n] [DecidableEq n] (φ : Dual ℂ (Matrix n n ℂ)) : φ.IsState ∧ φ.IsFaithful ↔ φ.matrix.PosDef ∧ φ.matrix.trace = 1

def Module.Dual.IsTracial {𝕜 : Type u_1} [RCLike 𝕜] {A : Type u_2} [NonUnitalSemiring A] [Module 𝕜 A] (φ : Dual 𝕜 A) : Prop

A linear functional $f$ is tracial if and only if $f(xy)=f(yx)$ for all $x,y$.

Equations

• φ.IsTracial = ∀ (x y : A), φ (x * y) = φ (y * x)

theorem Module.Dual.isTracial_pos_map_iff_of_matrix {n : Type u_1} [Fintype n] [DecidableEq n] (φ : Dual ℂ (Matrix n n ℂ)) : φ.IsPosMap ∧ φ.IsTracial ↔ ∃ (α : NNReal), φ.matrix = ↑↑α • 1

A linear functional is tracial and positive if and only if there exists a non-negative real $α$ such that $f\colon x \mapsto \alpha \operatorname{Tr}(x)$.

theorem Module.Dual.isTracial_pos_map_iff'_of_matrix {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] (φ : Dual ℂ (Matrix n n ℂ)) : φ.IsPosMap ∧ φ.IsTracial ↔ ∃! α : NNReal, φ.matrix = ↑↑α • 1

A linear functional is tracial and positive if and only if there exists a unique non-negative real $α$ such that $f\colon x \mapsto \alpha \operatorname{Tr}(x)$.

theorem Module.Dual.isTracial_faithful_pos_map_iff_of_matrix {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] (φ : Dual ℂ (Matrix n n ℂ)) : φ.IsFaithfulPosMap ∧ φ.IsTracial ↔ ∃! α : { x : NNReal // 0 < x }, φ.matrix = ↑↑↑α • 1

A linear functional $f$ is tracial positive and faithful if and only if there exists a positive real number $\alpha$ such that $f\colon x\mapsto \alpha \operatorname{Tr}(x)$.

theorem Matrix.ext_iff_trace' {R : Type u_1} {m : Type u_2} {n : Type u_3} [Semiring R] [StarRing R] [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (A B : Matrix m n R) : (∀ (x : Matrix m n R), (x.conjTranspose * A).trace = (x.conjTranspose * B).trace) ↔ A = B

theorem Module.Dual.isReal_iff {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Dual ℂ (Matrix n n ℂ)} : LinearMap.IsReal φ ↔ φ.matrix.IsHermitian

theorem Module.Dual.IsPosMap.isReal {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Dual ℂ (Matrix n n ℂ)} (hφ : φ.IsPosMap) : LinearMap.IsReal φ

theorem Module.Dual.pi.IsPosMap.isReal {k : Type u_1} [Fintype k] [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {ψ : (i : k) → Dual ℂ (Matrix (s i) (s i) ℂ)} (hψ : ∀ (i : k), (ψ i).IsPosMap) : LinearMap.IsReal (pi ψ)

def IsInner {𝕜 : Type u_1} [RCLike 𝕜] {H : Type u_2} [AddCommMonoid H] [Module 𝕜 H] (φ : H × H → 𝕜) : Prop

A function $H \times H \to 𝕜$ defines an inner product if it satisfies the following.

Equations

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

theorem Module.Dual.isFaithfulPosMap_iff_isInner_of_matrix {n : Type u_1} [Fintype n] [DecidableEq n] (φ : Dual ℂ (Matrix n n ℂ)) : φ.IsFaithfulPosMap ↔ IsInner fun (xy : Matrix n n ℂ × Matrix n n ℂ) => φ (xy.1.conjTranspose * xy.2)

A linear functional $f$ on $M_n$ is positive and faithful if and only if $(x,y)\mapsto f(x^*y)$ defines an inner product on $M_n$.

theorem Module.Dual.isFaithfulPosMap_of_matrix_tfae {n : Type u_1} [Fintype n] [DecidableEq n] (φ : Dual ℂ (Matrix n n ℂ)) : [φ.IsFaithfulPosMap, φ.matrix.PosDef, IsInner fun (xy : Matrix n n ℂ × Matrix n n ℂ) => φ (xy.1.conjTranspose * xy.2)].TFAE

@[reducible]

noncomputable def Module.Dual.NormedAddCommGroup {n : Type u_1} [Fintype n] [DecidableEq n] (φ : Dual ℂ (Matrix n n ℂ)) [hφ : φ.IsFaithfulPosMap] : _root_.NormedAddCommGroup (Matrix n n ℂ)

Equations

• φ.NormedAddCommGroup = InnerProductSpace.Core.toNormedAddCommGroup

@[reducible]

noncomputable def Module.Dual.InnerProductSpace {n : Type u_1} [Fintype n] [DecidableEq n] (φ : Dual ℂ (Matrix n n ℂ)) [hφ : φ.IsFaithfulPosMap] : _root_.InnerProductSpace ℂ (Matrix n n ℂ)

Equations

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

@[reducible]

noncomputable def Module.Dual.PiNormedAddCommGroup {k : Type u_1} [Fintype k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {φ : (i : k) → Dual ℂ (Matrix (s i) (s i) ℂ)} [_hφ : ∀ (i : k), (φ i).IsFaithfulPosMap] : _root_.NormedAddCommGroup (PiMat ℂ k s)

Equations

• Module.Dual.PiNormedAddCommGroup = PiLp.normedAddCommGroup 2 fun (j : k) => Mat ℂ (s j)

@[reducible]

noncomputable def Module.Dual.pi.InnerProductSpace {k : Type u_1} [Fintype k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {φ : (i : k) → Dual ℂ (Matrix (s i) (s i) ℂ)} [hφ : ∀ (i : k), (φ i).IsFaithfulPosMap] : _root_.InnerProductSpace ℂ (PiMat ℂ k s)

Equations

• Module.Dual.pi.InnerProductSpace = PiLp.innerProductSpace fun (j : k) => Mat ℂ (s j)