Frobenius equations

This file contains the proof of the Frobenius equations.

noncomputable def Module.Dual.tensorMul {n : Type u_1} {p : Type u_2} (φ₁ : Dual ℂ (Matrix n n ℂ)) (φ₂ : Dual ℂ (Matrix p p ℂ)) : Dual ℂ (TensorProduct ℂ (Matrix n n ℂ) (Matrix p p ℂ))

Tensor product of two matrix-valued module dual functionals.

Equations

• φ₁.tensorMul φ₂ = ↑(TensorProduct.lid ℂ ℂ) ∘ₗ TensorProduct.map φ₁ φ₂

theorem Module.Dual.tensorMul_apply {n : Type u_1} {p : Type u_2} (φ₁ : Dual ℂ (Matrix n n ℂ)) (φ₂ : Dual ℂ (Matrix p p ℂ)) (x : Matrix n n ℂ) (y : Matrix p p ℂ) : (φ₁.tensorMul φ₂) (x ⊗ₜ[ℂ] y) = φ₁ x * φ₂ y

theorem Module.Dual.tensorMul_apply' {n : Type u_1} {p : Type u_2} [Fintype n] [Fintype p] [DecidableEq n] [DecidableEq p] (φ₁ : Dual ℂ (Matrix n n ℂ)) (φ₂ : Dual ℂ (Matrix p p ℂ)) (x : TensorProduct ℂ (Matrix n n ℂ) (Matrix p p ℂ)) : (φ₁.tensorMul φ₂) x = ∑ i : n, ∑ j : n, ∑ k : p, ∑ l : p, TensorProduct.toKronecker x (i, k) (j, l) * (φ₁ (Matrix.stdBasisMatrix i j 1) * φ₂ (Matrix.stdBasisMatrix k l 1))

theorem Module.Dual.tensorMul_apply'' {n : Type u_1} {p : Type u_2} [Fintype n] [Fintype p] [DecidableEq n] [DecidableEq p] (φ₁ : Dual ℂ (Matrix n n ℂ)) (φ₂ : Dual ℂ (Matrix p p ℂ)) (a : Matrix (n × p) (n × p) ℂ) : (φ₁.tensorMul φ₂ ∘ₗ Matrix.kroneckerToTensorProduct) a = (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) φ₁.matrix φ₂.matrix * a).trace

theorem Module.Dual.tensorMul_matrix {n : Type u_1} {p : Type u_2} [Fintype n] [Fintype p] [DecidableEq n] [DecidableEq p] (φ₁ : Dual ℂ (Matrix n n ℂ)) (φ₂ : Dual ℂ (Matrix p p ℂ)) : matrix (φ₁.tensorMul φ₂ ∘ₗ Matrix.kroneckerToTensorProduct) = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) φ₁.matrix φ₂.matrix

instance Module.Dual.IsFaithfulPosMap.tensorMul {n : Type u_1} {p : Type u_2} [Fintype n] [Fintype p] [DecidableEq n] [DecidableEq p] {φ₁ : Dual ℂ (Matrix n n ℂ)} {φ₂ : Dual ℂ (Matrix p p ℂ)} [hφ₁ : φ₁.IsFaithfulPosMap] [hφ₂ : φ₂.IsFaithfulPosMap] : IsFaithfulPosMap (φ₁.tensorMul φ₂ ∘ₗ Matrix.kroneckerToTensorProduct)

Tensor products of faithful positive matrix functionals are faithful and positive.

theorem Matrix.kroneckerToTensorProduct_adjoint {n : Type u_1} {p : Type u_2} [Fintype n] [Fintype p] [DecidableEq n] [DecidableEq p] {φ : Module.Dual ℂ (Matrix n n ℂ)} {ψ : Module.Dual ℂ (Matrix p p ℂ)} [hφ : φ.IsFaithfulPosMap] [hψ : ψ.IsFaithfulPosMap] : TensorProduct.toKronecker = LinearMap.adjoint kroneckerToTensorProduct

theorem TensorProduct.toKronecker_adjoint {n : Type u_1} {p : Type u_2} [Fintype n] [Fintype p] [DecidableEq n] [DecidableEq p] {φ : Module.Dual ℂ (Matrix n n ℂ)} {ψ : Module.Dual ℂ (Matrix p p ℂ)} [hφ : φ.IsFaithfulPosMap] [hψ : ψ.IsFaithfulPosMap] : Matrix.kroneckerToTensorProduct = LinearMap.adjoint toKronecker

theorem Matrix.kroneckerToTensorProduct_comp_toKronecker {n : Type u_1} {p : Type u_2} [Fintype n] [Fintype p] [DecidableEq n] [DecidableEq p] : kroneckerToTensorProduct ∘ₗ TensorProduct.toKronecker = 1

@[reducible]

noncomputable def Module.Dual.isNormedAddCommGroupOfRing {n : Type u_1} [Fintype n] [DecidableEq n] (ψ : Dual ℂ (Matrix n n ℂ)) [ψ.IsFaithfulPosMap] : NormedAddCommGroupOfRing (Matrix n n ℂ)

The normed additive group of matrices induced by a faithful positive functional.

Equations

• ψ.isNormedAddCommGroupOfRing = { toRing := Matrix.instRing, toNorm := ψ.NormedAddCommGroup.toNorm, toMetricSpace := ψ.NormedAddCommGroup.toMetricSpace, dist_eq := ⋯ }

@[reducible]

noncomputable def Pi.module.Dual.isNormedAddCommGroupOfRing {k : Type u_1} [Fintype k] {s : k → Type u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] (ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)) [∀ (i : k), (ψ i).IsFaithfulPosMap] : NormedAddCommGroupOfRing (PiMat ℂ k s)

The normed additive commutative group structure induced by faithful block functionals.

Equations

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

noncomputable def matrixDirectSumFromTo {k : Type u_1} [DecidableEq k] {s : k → Type u_2} (i j : k) : Matrix (s i) (s i) ℂ →ₗ[ℂ] Matrix (s j) (s j) ℂ

Linear map from one matrix summand to another in a direct product of matrix blocks.

Equations

• matrixDirectSumFromTo i j = directSumFromTo i j

theorem matrixDirectSumFromTo_same {k : Type u_2} [DecidableEq k] {s : k → Type u_1} (i : k) : matrixDirectSumFromTo i i = 1

theorem LinearMap.pi_mul'_apply_includeBlock' {k : Type u_1} [DecidableEq k] {s : k → Type u_2} [(i : k) → Fintype (s i)] {i j : k} : mul' ℂ (PiMat ℂ k s) ∘ₗ TensorProduct.map Matrix.includeBlock Matrix.includeBlock = if i = j then Matrix.includeBlock ∘ₗ mul' ℂ (Matrix (s j) (s j) ℂ) ∘ₗ TensorProduct.map (matrixDirectSumFromTo i j) 1 else 0

noncomputable def directSumTensorMatrix {k : Type u_1} [Fintype k] [DecidableEq k] {s : k → Type u_2} : TensorProduct ℂ (PiMat ℂ k s) (PiMat ℂ k s) ≃ₗ[ℂ] (i : k × k) → TensorProduct ℂ (Matrix (s i.1) (s i.1) ℂ) (Matrix (s i.2) (s i.2) ℂ)

Linear equivalence splitting the tensor product of matrix-block products into block tensor products.

Equations

• directSumTensorMatrix = directSumTensor

@[simp]

theorem Module.Dual.IsFaithfulPosMap.sig_apply' {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] {r : ℝ} {x : Matrix n n ℂ} : (hφ.sig r) x = ⋯.rpow (-r) * x * ⋯.rpow r