LeanPool.Monlib4.QuantumGraph.PiMat

Imported Lean Pool material for LeanPool.Monlib4.QuantumGraph.PiMat.

def «tacticWithPiQuantumCtx[_]» : Lean.ParserDescr

Introduce the quantum-set instances for a product of matrix blocks in a proof.

Equations

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

def «tacticWithMatrixQuantumCtx[_]» : Lean.ParserDescr

Introduce the quantum-set instances for a single matrix algebra in a proof.

Equations

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

noncomputable def PiMat.transposeStarAlgEquiv (ι : Type u_3) (p : ι → Type u_4) [(i : ι) → Fintype (p i)] : PiMat ℂ ι p ≃⋆ₐ[ℂ] (PiMat ℂ ι p)ᵐᵒᵖ

Transpose each matrix block of a PiMat as a star-algebra equivalence to the opposite algebra.

Equations

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

@[simp]

theorem PiMat.transposeStarAlgEquiv_apply (ι : Type u_3) (p : ι → Type u_4) [(i : ι) → Fintype (p i)] (x : PiMat ℂ ι p) : (transposeStarAlgEquiv ι p) x = MulOpposite.op fun (i : ι) => Matrix.transpose (x i)

@[simp]

theorem PiMat.transposeStarAlgEquiv_symm_apply (ι : Type u_3) (p : ι → Type u_4) [(i : ι) → Fintype (p i)] (x : (PiMat ℂ ι p)ᵐᵒᵖ) (i : ι) : (transposeStarAlgEquiv ι p).symm x i = Matrix.transpose (MulOpposite.unop x i)

@[reducible, inline]

noncomputable abbrev Matrix.toEuclideanStarAlgEquiv {n : Type u_3} [Fintype n] [DecidableEq n] : Matrix n n ℂ ≃⋆ₐ[ℂ] EuclideanSpace ℂ n →ₗ[ℂ] EuclideanSpace ℂ n

Matrix algebra as endomorphisms of Euclidean space, as a star-algebra equivalence.

Equations

• Matrix.toEuclideanStarAlgEquiv = StarAlgEquiv.ofAlgEquiv (AlgEquiv.ofLinearEquiv Matrix.toEuclideanLin ⋯ ⋯) ⋯

theorem Matrix.toEuclideanStarAlgEquiv_coe {n : Type u_3} [Fintype n] [DecidableEq n] : ⇑toEuclideanStarAlgEquiv = ⇑toEuclideanLin

noncomputable def PiMatTensorProductEquiv {ι₁ : Type u_3} {ι₂ : Type u_4} {p₁ : ι₁ → Type u_5} {p₂ : ι₂ → Type u_6} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] [(i : ι₁) → Fintype (p₁ i)] [(i : ι₁) → DecidableEq (p₁ i)] [(i : ι₂) → Fintype (p₂ i)] [(i : ι₂) → DecidableEq (p₂ i)] : TensorProduct ℂ (PiMat ℂ ι₁ p₁) (PiMat ℂ ι₂ p₂) ≃⋆ₐ[ℂ] PiMat ℂ (ι₁ × ι₂) fun (i : ι₁ × ι₂) => p₁ i.1 × p₂ i.2

Tensor-product equivalence for direct products of matrix algebras.

Equations

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

@[simp]

theorem PiMatTensorProductEquiv_apply {ι₁ : Type u_3} {ι₂ : Type u_4} {p₁ : ι₁ → Type u_5} {p₂ : ι₂ → Type u_6} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] [(i : ι₁) → Fintype (p₁ i)] [(i : ι₁) → DecidableEq (p₁ i)] [(i : ι₂) → Fintype (p₂ i)] [(i : ι₂) → DecidableEq (p₂ i)] (a✝ : TensorProduct ℂ ((i : ι₁) → Mat ℂ (p₁ i)) ((i : ι₂) → Mat ℂ (p₂ i))) (i : ι₁ × ι₂) : PiMatTensorProductEquiv a✝ i = TensorProduct.toKronecker (directSumTensorToFun a✝ i)

@[simp]

theorem PiMatTensorProductEquiv_symm_apply {ι₁ : Type u_3} {ι₂ : Type u_4} {p₁ : ι₁ → Type u_5} {p₂ : ι₂ → Type u_6} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] [(i : ι₁) → Fintype (p₁ i)] [(i : ι₁) → DecidableEq (p₁ i)] [(i : ι₂) → Fintype (p₂ i)] [(i : ι₂) → DecidableEq (p₂ i)] (a✝ : PiMat ℂ (ι₁ × ι₂) fun (i : ι₁ × ι₂) => p₁ i.1 × p₂ i.2) : PiMatTensorProductEquiv.symm a✝ = directSumTensorInvFun ((AlgEquiv.piCongrRight fun (i : ι₁ × ι₂) => tensorToKronecker.symm) a✝)

theorem PiMatTensorProductEquiv_tmul_apply {ι₁ : Type u_3} {ι₂ : Type u_4} {p₁ : ι₁ → Type u_5} {p₂ : ι₂ → Type u_6} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] [(i : ι₁) → Fintype (p₁ i)] [(i : ι₁) → DecidableEq (p₁ i)] [(i : ι₂) → Fintype (p₂ i)] [(i : ι₂) → DecidableEq (p₂ i)] (x : PiMat ℂ ι₁ p₁) (y : PiMat ℂ ι₂ p₂) (r : ι₁ × ι₂) (a b : p₁ r.1 × p₂ r.2) : PiMatTensorProductEquiv (x ⊗ₜ[ℂ] y) r a b = x r.1 a.1 b.1 * y r.2 a.2 b.2

theorem PiMatTensorProductEquiv_tmul {ι₁ : Type u_3} {ι₂ : Type u_4} {p₁ : ι₁ → Type u_5} {p₂ : ι₂ → Type u_6} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] [(i : ι₁) → Fintype (p₁ i)] [(i : ι₁) → DecidableEq (p₁ i)] [(i : ι₂) → Fintype (p₂ i)] [(i : ι₂) → DecidableEq (p₂ i)] (x : PiMat ℂ ι₁ p₁) (y : PiMat ℂ ι₂ p₂) : PiMatTensorProductEquiv (x ⊗ₜ[ℂ] y) = fun (r : ι₁ × ι₂) => Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (x r.1) (y r.2)

theorem PiMatTensorProductEquiv_tmul_apply' {ι₁ : Type u_3} {ι₂ : Type u_4} {p₁ : ι₁ → Type u_5} {p₂ : ι₂ → Type u_6} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] [(i : ι₁) → Fintype (p₁ i)] [(i : ι₁) → DecidableEq (p₁ i)] [(i : ι₂) → Fintype (p₂ i)] [(i : ι₂) → DecidableEq (p₂ i)] (x : PiMat ℂ ι₁ p₁) (y : PiMat ℂ ι₂ p₂) (r : ι₁ × ι₂) (a c : p₁ r.1) (b d : p₂ r.2) : PiMatTensorProductEquiv (x ⊗ₜ[ℂ] y) r (a, b) (c, d) = x r.1 a c * y r.2 b d

noncomputable def ContinuousLinearMap.toLinearMapStarAlgEquiv {𝕜 : Type u_3} {B : Type u_4} [RCLike 𝕜] [NormedAddCommGroup B] [InnerProductSpace 𝕜 B] [FiniteDimensional 𝕜 B] [CompleteSpace B] : (B →L[𝕜] B) ≃⋆ₐ[𝕜] B →ₗ[𝕜] B

The forgetful equivalence from continuous endomorphisms to linear endomorphisms, as a star algebra equivalence.

Equations

• ContinuousLinearMap.toLinearMapStarAlgEquiv = StarAlgEquiv.ofAlgEquiv ContinuousLinearMap.toLinearMapAlgEquiv ⋯

@[reducible, inline]

noncomputable abbrev PiMatToEuclideanLM {ι : Type u_1} {p : ι → Type u_2} [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] : PiMat ℂ ι p ≃⋆ₐ[ℂ] (i : ι) → EuclideanSpace ℂ (p i) →ₗ[ℂ] EuclideanSpace ℂ (p i)

Convert each block of a PiMat to a Euclidean-space linear map.

Equations

• PiMatToEuclideanLM = StarAlgEquiv.piCongrRight fun (x : ι) => Matrix.toEuclideanStarAlgEquiv

@[reducible, inline]

noncomputable abbrev PiMat.traceLinearMap {ι : Type u_1} {p : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] : PiMat ℂ ι p →ₗ[ℂ] ℂ

Trace functional on a product of matrix blocks.

Equations

• PiMat.traceLinearMap = Matrix.traceLinearMap ((i : ι) × p i) ℂ ℂ ∘ₗ Matrix.blockDiagonal'AlgHom.toLinearMap

@[simp]

theorem PiMat.traceLinearMap_apply {ι : Type u_1} {p : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] (x : PiMat ℂ ι p) : traceLinearMap x = (Matrix.blockDiagonal'AlgHom x).trace

@[reducible]

noncomputable def PiMat.finiteDimensionalHilbertCoalgebraStruct {ι : Type u_1} {p : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] : CoalgebraStruct ℂ (PiMat ℂ ι p)

Coalgebra structure on a finite product of matrix blocks.

Equations

• PiMat.finiteDimensionalHilbertCoalgebraStruct = Coalgebra.ofFiniteDimensionalHilbertAlgebra.toCoalgebraStruct

theorem QuantumGraph.PiMat_existsSubmoduleIsProj {ι : Type u_1} {p : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] {f : PiMat ℂ ι p →ₗ[ℂ] PiMat ℂ ι p} : QuantumGraph (PiMat ℂ ι p) f → ∀ (t r : ℝ), ∃ (u : (i : ι × ι) → Submodule ℂ (EuclideanSpace ℂ (p i.1 × p i.2))), ∀ (i : ι × ι), LinearMap.IsProj (u i) (PiMatToEuclideanLM (PiMatTensorProductEquiv ((StarAlgEquiv.lTensor (PiMat ℂ ι p) (PiMat.transposeStarAlgEquiv ι p).symm) ((QuantumSet.Psi t r) f))) i)

noncomputable def QuantumGraph.PiMatSubmodule {ι : Type u_1} {p : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] {f : PiMat ℂ ι p →ₗ[ℂ] PiMat ℂ ι p} : QuantumGraph (PiMat ℂ ι p) f → ℝ → ℝ → (i : ι × ι) → Submodule ℂ (EuclideanSpace ℂ (p i.1 × p i.2))

Submodules associated to the block components of a PiMat quantum graph.

Equations

• hf.PiMatSubmodule t r = Classical.choose ⋯

theorem QuantumGraph.PiMatSubmoduleIsProj {ι : Type u_1} {p : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] {f : PiMat ℂ ι p →ₗ[ℂ] PiMat ℂ ι p} (hf : QuantumGraph (PiMat ℂ ι p) f) (t r : ℝ) (i : ι × ι) : LinearMap.IsProj (hf.PiMatSubmodule t r i) (PiMatToEuclideanLM (PiMatTensorProductEquiv ((StarAlgEquiv.lTensor (PiMat ℂ ι p) (PiMat.transposeStarAlgEquiv ι p).symm) ((QuantumSet.Psi t r) f))) i)

theorem QuantumGraph.PiMatSubmoduleIsProj_codRestrict {ι : Type u_1} {p : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] {f : PiMat ℂ ι p →ₗ[ℂ] PiMat ℂ ι p} (hf : QuantumGraph (PiMat ℂ ι p) f) (t r : ℝ) (i : ι × ι) : (hf.PiMatSubmodule t r i).subtype ∘ₗ ⋯.codRestrict = PiMatToEuclideanLM (PiMatTensorProductEquiv ((StarAlgEquiv.lTensor (PiMat ℂ ι p) (PiMat.transposeStarAlgEquiv ι p).symm) ((QuantumSet.Psi t r) f))) i

noncomputable def QuantumGraph.dimOfPiMatSubmodule {ι : Type u_1} {p : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] {f : PiMat ℂ ι p →ₗ[ℂ] PiMat ℂ ι p} : QuantumGraph (PiMat ℂ ι p) f → ℕ

Sum of the dimensions of the block submodules associated to a PiMat quantum graph.

Equations

• hf.dimOfPiMatSubmodule = ∑ i : ι × ι, Module.finrank ℂ ↥(hf.PiMatSubmodule 0 (1 / 2) i)

theorem PiMat.traceLinearMap_comp_piMatTensorProductEquiv_eq {ι : Type u_1} {p : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] : traceLinearMap ∘ₗ PiMatTensorProductEquiv.toLinearMap = LinearMap.mul' ℂ ℂ ∘ₗ TensorProduct.map traceLinearMap traceLinearMap

theorem PiMat.transposeStarAlgEquiv_symm_is_tracePreserving {ι : Type u_1} {p : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] (x : (PiMat ℂ ι p)ᵐᵒᵖ) : traceLinearMap ((transposeStarAlgEquiv ι p).symm x) = traceLinearMap (MulOpposite.unop x)

theorem PiMat.traceLinearMap_comp_transposeStarAlgEquiv_symm {ι : Type u_1} {p : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] : traceLinearMap ∘ₗ (transposeStarAlgEquiv ι p).symm.toLinearMap = traceLinearMap ∘ₗ ↑(unop ℂ)

theorem QuantumGraph.dimOfPiMatSubmodule_eq_trace {ι : Type u_1} {p : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] {f : PiMat ℂ ι p →ₗ[ℂ] PiMat ℂ ι p} (hf : QuantumGraph (PiMat ℂ ι p) f) : ↑hf.dimOfPiMatSubmodule = PiMat.traceLinearMap (PiMatTensorProductEquiv ((StarAlgEquiv.lTensor (PiMat ℂ ι p) (PiMat.transposeStarAlgEquiv ι p).symm) ((QuantumSet.Psi 0 (1 / 2)) f)))

theorem Coalgebra.counit_mulOpposite {A : Type u_3} [Semiring A] [Algebra ℂ A] [CoalgebraStruct ℂ A] : counit = counit ∘ₗ ↑(unop ℂ)

theorem StarAlgEquiv.lTensor_toLinearMap {R : Type u_3} {A : Type u_4} {B : Type u_5} {C : Type u_6} [RCLike R] [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebra R B] [Algebra R C] [StarAddMonoid A] [StarAddMonoid B] [StarAddMonoid C] [StarModule R A] [StarModule R B] [StarModule R C] [Module.Finite R A] [Module.Finite R B] [Module.Finite R C] (f : A ≃⋆ₐ[R] B) : (lTensor C f).toLinearMap = LinearMap.lTensor C f.toLinearMap

@[implicit_reducible]

noncomputable instance TensorProduct.instCoalgebraStruct' {R : Type u_3} {S : Type u_4} {A : Type u_5} {B : Type u_6} [CommSemiring R] [CommSemiring S] [AddCommMonoid A] [AddCommMonoid B] [Algebra R S] [Module R A] [Module S A] [Module R B] [CoalgebraStruct R B] [CoalgebraStruct S A] [IsScalarTower R S A] : CoalgebraStruct S (TensorProduct R A B)

Equations

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

theorem TensorProduct.instCoalgebraStruct'_counit {R : Type u_3} {S : Type u_4} {A : Type u_5} {B : Type u_6} [CommSemiring R] [CommSemiring S] [AddCommMonoid A] [AddCommMonoid B] [Algebra R S] [Module R A] [Module S A] [Module R B] [CoalgebraStruct R B] [CoalgebraStruct S A] [IsScalarTower R S A] : CoalgebraStruct.counit = ↑(AlgebraTensorModule.rid R S S) ∘ₗ AlgebraTensorModule.map CoalgebraStruct.counit CoalgebraStruct.counit

theorem QuantumGraph.dimOfPiMatSubmodule_eq_trace_counit {ι : Type u_1} {p : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] : CoalgebraStruct.counit = PiMat.traceLinearMap → ∀ {f : PiMat ℂ ι p →ₗ[ℂ] PiMat ℂ ι p} (hf : QuantumGraph (PiMat ℂ ι p) f), ↑hf.dimOfPiMatSubmodule = CoalgebraStruct.counit ((QuantumSet.Psi 0 (1 / 2)) f)

theorem Coalgebra.counit_self_tensor_mulOpposite_eq_bra_one {A : Type u_3} [NormedAddCommGroupOfRing A] [InnerProductSpace ℂ A] [SMulCommClass ℂ A A] [IsScalarTower ℂ A A] [FiniteDimensional ℂ A] : counit = ↑((bra ℂ) 1)

theorem QuantumGraph.NumOfEdges_apply {A : Type u_3} [starAlgebra A] [QuantumSet A] (f : A →ₗ[ℂ] A) : NumOfEdges f = inner ℂ 1 (f 1)

theorem QuantumGraph.dimOfPiMatSubmodule_eq_numOfEdges_of_trace_counit {ι : Type u_1} {p : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] : CoalgebraStruct.counit = PiMat.traceLinearMap → ∀ {f : PiMat ℂ ι p →ₗ[ℂ] PiMat ℂ ι p} (hf : QuantumGraph (PiMat ℂ ι p) f), ↑hf.dimOfPiMatSubmodule = NumOfEdges f

theorem QuantumGraph.dimOfPiMatSubmodule_eq_rank_top_iff {ι : Type u_1} {p : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] {f : PiMat ℂ ι p →ₗ[ℂ] PiMat ℂ ι p} (hf : QuantumGraph (PiMat ℂ ι p) f) : hf.dimOfPiMatSubmodule = ∑ i : ι × ι, Fintype.card (p i.1) * Fintype.card (p i.2) ↔ f = Qam.completeGraph (PiMat ℂ ι p) (PiMat ℂ ι p)

theorem QuantumGraph.CompleteGraph_dimOfPiMatSubmodule {ι : Type u_1} {p : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] : ⋯.dimOfPiMatSubmodule = ∑ i : ι × ι, Fintype.card (p i.1) * Fintype.card (p i.2)

theorem Algebra.linearMap_adjoint_eq_dual {ι : Type u_1} {p : ι → Type u_2} [Fintype ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] : LinearMap.adjoint (Algebra.linearMap ℂ (PiMat ℂ ι p)) = Module.Dual.pi φ

theorem exists_dimOfPiMatSubmodule_ne_inner_one_map_one_of_IsFaithfulState {ι : Type u_1} {p : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] : (Module.Dual.pi φ).IsUnital → 1 < Module.finrank ℂ (PiMat ℂ ι p) → ∃ (A : PiMat ℂ ι p →ₗ[ℂ] PiMat ℂ ι p) (hA : QuantumGraph (PiMat ℂ ι p) A), QuantumGraph.NumOfEdges A ≠ ↑hA.dimOfPiMatSubmodule

theorem QuantumGraph.Real.PiMat_isOrthogonalProjection {ι : Type u_1} {p : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] {A : PiMat ℂ ι p →ₗ[ℂ] PiMat ℂ ι p} : Real (PiMat ℂ ι p) A → ∀ (i : ι × ι), (LinearMap.toContinuousLinearMap (PiMatToEuclideanLM (PiMatTensorProductEquiv ((StarAlgEquiv.lTensor (PiMat ℂ ι p) (PiMat.transposeStarAlgEquiv ι p).symm) ((QuantumSet.Psi 0 (1 / 2)) A))) i)).IsOrthogonalProjection

noncomputable def QuantumGraph.Real.PiMatSubmodule {ι : Type u_1} {p : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] {A : PiMat ℂ ι p →ₗ[ℂ] PiMat ℂ ι p} : Real (PiMat ℂ ι p) A → (i : ι × ι) → Submodule ℂ (EuclideanSpace ℂ (p i.1 × p i.2))

Block submodules associated to a real PiMat quantum graph.

Equations

• hA.PiMatSubmodule i = Classical.choose ⋯

theorem QuantumGraph.Real.PiMatSubmoduleOrthogonalProjection {ι : Type u_1} {p : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] {A : PiMat ℂ ι p →ₗ[ℂ] PiMat ℂ ι p} (hA : Real (PiMat ℂ ι p) A) (i : ι × ι) : orthogonalProjection' (hA.PiMatSubmodule i) = LinearMap.toContinuousLinearMap (PiMatToEuclideanLM (PiMatTensorProductEquiv ((StarAlgEquiv.lTensor (PiMat ℂ ι p) (PiMat.transposeStarAlgEquiv ι p).symm) ((QuantumSet.Psi 0 (1 / 2)) A))) i)

noncomputable def QuantumGraph.Real.PiMatOrthonormalBasis {ι : Type u_1} {p : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] {A : PiMat ℂ ι p →ₗ[ℂ] PiMat ℂ ι p} (hA : Real (PiMat ℂ ι p) A) (i : ι × ι) : OrthonormalBasis (Fin (Module.finrank ℂ ↥(hA.PiMatSubmodule i))) ℂ ↥(hA.PiMatSubmodule i)

Orthonormal basis of a block submodule associated to a real PiMat quantum graph.

Equations

• hA.PiMatOrthonormalBasis i = stdOrthonormalBasis ℂ ↥(hA.PiMatSubmodule i)

theorem EuclideanSpace.prod_exists_finset {n : Type u_3} {m : Type u_4} [Fintype n] [DecidableEq n] [Fintype m] [DecidableEq m] (x : EuclideanSpace ℂ (n × m)) : ∃ (S : Finset (EuclideanSpace ℂ n × EuclideanSpace ℂ m)), x = ∑ s ∈ S, euclideanSpaceTensor' (s.1 ⊗ₜ[ℂ] s.2)

theorem QuantumSet.PiMat_n {ι : Type u_1} {p : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] : n (PiMat ℂ ι p) = ((i : ι) × p i × p i)

@[simp]

theorem Matrix.ite_kronecker {α : Type u_3} {n : Type u_4} {m : Type u_5} {p : Type u_6} {q : Type u_7} [MulZeroClass α] (x₁ : Matrix n m α) (x₂ : Matrix p q α) (P : Prop) [Decidable P] : kroneckerMap (fun (x1 x2 : α) => x1 * x2) (if P then x₁ else 0) x₂ = if P then kroneckerMap (fun (x1 x2 : α) => x1 * x2) x₁ x₂ else 0

@[simp]

theorem Matrix.dite_kronecker {α : Type u_3} {n : Type u_4} {m : Type u_5} {p : Type u_6} {q : Type u_7} [MulZeroClass α] (P : Prop) [Decidable P] (x₁ : P → Matrix n m α) (x₂ : Matrix p q α) : kroneckerMap (fun (x1 x2 : α) => x1 * x2) (if p : P then x₁ p else 0) x₂ = if p_1 : P then kroneckerMap (fun (x1 x2 : α) => x1 * x2) (x₁ p_1) x₂ else 0

@[simp]

theorem Matrix.kronecker_ite {α : Type u_3} {n : Type u_4} {m : Type u_5} {p : Type u_6} {q : Type u_7} [MulZeroClass α] (x₁ : Matrix n m α) (x₂ : Matrix p q α) (P : Prop) [Decidable P] : kroneckerMap (fun (x1 x2 : α) => x1 * x2) x₁ (if P then x₂ else 0) = if P then kroneckerMap (fun (x1 x2 : α) => x1 * x2) x₁ x₂ else 0

@[simp]

theorem Matrix.kronecker_dite {α : Type u_3} {n : Type u_4} {m : Type u_5} {p : Type u_6} {q : Type u_7} [MulZeroClass α] (x₁ : Matrix n m α) (P : Prop) [Decidable P] (x₂ : P → Matrix p q α) : kroneckerMap (fun (x1 x2 : α) => x1 * x2) x₁ (if p : P then x₂ p else 0) = if p_1 : P then kroneckerMap (fun (x1 x2 : α) => x1 * x2) x₁ (x₂ p_1) else 0

theorem Matrix.vecMulVec_kronecker_vecMulVec {α : Type u_3} {n : Type u_4} {m : Type u_5} {p : Type u_6} {q : Type u_7} [CommSemiring α] (x : n → α) (y : m → α) (z : p → α) (w : q → α) : kroneckerMap (fun (x1 x2 : α) => x1 * x2) (vecMulVec x y) (vecMulVec z w) = vecMulVec (reshape (vecMulVec x z)) (reshape (vecMulVec y w))

@[simp]

theorem Matrix.vecMulVec_toEuclideanLin {n : Type u_3} {m : Type u_4} [Fintype n] [Fintype m] [DecidableEq m] (x : EuclideanSpace ℂ n) (y : EuclideanSpace ℂ m) : toEuclideanLin (vecMulVec x.ofLp y.ofLp) = ↑(((rankOne ℂ) x) (star y))

theorem EuclideanSpaceTensor_apply_eq_reshape_vecMulVec {n : Type u_3} {m : Type u_4} [Fintype n] [DecidableEq n] [Fintype m] [DecidableEq m] (x : EuclideanSpace ℂ n) (y : EuclideanSpace ℂ m) : (euclideanSpaceTensor' (x ⊗ₜ[ℂ] y)).ofLp = Matrix.reshape (Matrix.vecMulVec x.ofLp y.ofLp)

theorem Matrix.vecMulVec_conj {α : Type u_3} {n : Type u_4} {m : Type u_5} [CommSemiring α] [StarMul α] (x : n → α) (y : m → α) : (vecMulVec x y).conj = vecMulVec (star x) (star y)

theorem rankOne_euclideanSpaceTensor_eq_toEuclideanLin_vecMulVec {n : Type u_3} {m : Type u_4} [Fintype n] [DecidableEq n] [Fintype m] [DecidableEq m] (x y : EuclideanSpace ℂ n) (z w : EuclideanSpace ℂ m) : ((rankOne ℂ) (euclideanSpaceTensor' (x ⊗ₜ[ℂ] z))) (euclideanSpaceTensor' (y ⊗ₜ[ℂ] w)) = LinearMap.toContinuousLinearMap (Matrix.toEuclideanLin (Matrix.vecMulVec (Matrix.reshape (Matrix.vecMulVec x.ofLp z.ofLp)) (Matrix.reshape (Matrix.vecMulVec (star y.ofLp) (star w.ofLp)))))

theorem Matrix.includeBlock_apply_block {R : Type u_3} {k : Type u_4} [CommSemiring R] [DecidableEq k] {s : k → Type u_5} {i : k} (x : Matrix (s i) (s i) R) (j : k) : includeBlock x j = if h : i = j then ⋯.mp x else 0

noncomputable def TensorProduct.chooseFinset {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (x : TensorProduct R M N) : Finset (M × N)

A chosen finite support representation of a tensor.

Equations

• x.chooseFinset = Classical.choose ⋯

theorem TensorProduct.chooseFinset_spec {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (x : TensorProduct R M N) : x = ∑ s ∈ x.chooseFinset, s.1 ⊗ₜ[R] s.2

noncomputable def EuclideanSpace.prodChoose {n : Type u_3} {m : Type u_4} [Fintype n] [DecidableEq n] [Fintype m] [DecidableEq m] (x : EuclideanSpace ℂ (n × m)) : n × m → EuclideanSpace ℂ n × EuclideanSpace ℂ m

A product-coordinate decomposition of Euclidean space vectors.

Equations

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

theorem EuclideanSpace.sum_apply {n : Type u_3} {𝕜 : Type u_4} [RCLike 𝕜] {ι : Type u_5} (s : Finset ι) (x : ι → EuclideanSpace 𝕜 n) (j : n) : (∑ i ∈ s, x i).ofLp j = ∑ i ∈ s, (x i).ofLp j

theorem Module.Basis.tensorProduct_repr_tmul_apply' {R : Type u_3} {M : Type u_4} {N : Type u_5} {ι : Type u_6} {κ : Type u_7} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (b : Basis ι R M) (c : Basis κ R N) (m : M) (n : N) (i : ι × κ) : ((b.tensorProduct c).repr (m ⊗ₜ[R] n)) i = (c.repr n) i.2 * (b.repr m) i.1

theorem EuclideanSpace.prodChoose_spec {n : Type u_3} {m : Type u_4} [Fintype n] [DecidableEq n] [Fintype m] [DecidableEq m] (x : EuclideanSpace ℂ (n × m)) : x = ∑ s : n × m, euclideanSpaceTensor' ((x.prodChoose s).1 ⊗ₜ[ℂ] (x.prodChoose s).2)

theorem QuantumGraph.Real.PiMat_eq {ι : Type u_1} {p : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] {A : PiMat ℂ ι p →ₗ[ℂ] PiMat ℂ ι p} (hA : Real (PiMat ℂ ι p) A) : have S := fun (i : ι × ι) (j : Fin (Module.finrank ℂ ↥(hA.PiMatSubmodule i))) => (↑((hA.PiMatOrthonormalBasis i) j)).prodChoose; A = ↑(∑ i : ι × ι, ∑ j : Fin (Module.finrank ℂ ↥(hA.PiMatSubmodule i)), ∑ s : p i.1 × p i.2, ∑ l : p i.1 × p i.2, ((rankOne ℂ) (Matrix.includeBlock (Matrix.vecMulVec (S i j s).1.ofLp (star (S i j l).1.ofLp)))) ((modAut (-(1 / 2))) (Matrix.includeBlock (Matrix.vecMulVec (S i j s).2.ofLp (star (S i j l).2.ofLp)).conj)))

theorem QuantumGraph.trivialGraph {ι : Type u_1} {p : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] {d : ℂ} [Nonempty ι] [hφ₂ : Fact (∀ (i : ι), (φ i).matrix⁻¹.trace = d)] [∀ (i : ι), Nontrivial (p i)] : QuantumGraph (PiMat ℂ ι p) (Qam.trivialGraph (PiMat ℂ ι p))

theorem PiMat.piAlgEquiv_trace_apply {ι : Type u_1} {p : ι → Type u_2} [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] (f : (i : ι) → Matrix (p i) (p i) ℂ ≃ₐ[ℂ] Matrix (p i) (p i) ℂ) (x : PiMat ℂ ι p) (a : ι) : ((AlgEquiv.piCongrRight f) x a).trace = Matrix.trace (x a)

theorem PiMat.modAut_trace_apply {ι : Type u_1} {p : ι → Type u_2} [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] [Finite ι] (r : ℝ) (x : PiMat ℂ ι p) (a : ι) : Matrix.trace ((starAlgebra.modAut r) x a) = Matrix.trace (x a)

theorem PiMat.orthonormalBasis_trace {ι : Type u_1} {p : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] (a : n (PiMat ℂ ι p)) (i : ι) : Matrix.trace (onb a i) = if a.fst = i then ⋯.rpow (-(1 / 2)) a.snd.2 a.snd.1 else 0

theorem QuantumGraph.trivialGraph_dimOfPiMatSubmodule {ι : Type u_1} {p : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] {d : ℂ} [Nonempty ι] [hφ₂ : Fact (∀ (i : ι), (φ i).matrix⁻¹.trace = d)] [∀ (i : ι), Nontrivial (p i)] : ⋯.dimOfPiMatSubmodule = Fintype.card ι

theorem StarAlgEquiv.piCongrRight_symm {R : Type u_3} {ι : Type u_4} {A₁ : ι → Type u_5} {A₂ : ι → Type u_6} [(i : ι) → Add (A₁ i)] [(i : ι) → Add (A₂ i)] [(i : ι) → Mul (A₁ i)] [(i : ι) → Mul (A₂ i)] [(i : ι) → Star (A₁ i)] [(i : ι) → Star (A₂ i)] [(i : ι) → SMul R (A₁ i)] [(i : ι) → SMul R (A₂ i)] (e : (i : ι) → A₁ i ≃⋆ₐ[R] A₂ i) : (piCongrRight e).symm = piCongrRight fun (i : ι) => (e i).symm

theorem Matrix.k {n : Type u_3} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [φ.IsFaithfulPosMap] : QuantumSet.k (Matrix n n ℂ) = 0

theorem unitary.mul_inv_eq_iff {A : Type u_3} [Monoid A] [StarMul A] (U : ↥(unitary A)) (x y : A) : x * ↑U⁻¹ = y ↔ x = y * ↑U

@[reducible, inline]

noncomputable abbrev piInnerAut {ι : Type u_1} {p : ι → Type u_2} [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] (U : (i : ι) → ↥(Matrix.unitaryGroup (p i) ℂ)) : PiMat ℂ ι p ≃⋆ₐ[ℂ] PiMat ℂ ι p

Blockwise inner automorphism of a PiMat.

Equations

• piInnerAut U = StarAlgEquiv.piCongrRight fun (i : ι) => Matrix.innerAutStarAlg (U i)

theorem piInnerAut_apply_dualMatrix_iff' {ι : Type u_1} {p : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} {U : (i : ι) → ↥(Matrix.unitaryGroup (p i) ℂ)} : (piInnerAut U) (Module.Dual.pi.matrixBlock φ) = Module.Dual.pi.matrixBlock φ ↔ ∀ (i : ι), (Matrix.innerAutStarAlg (U i)) (φ i).matrix = (φ i).matrix

theorem piInnerAut_apply_dualMatrix_iff {ι : Type u_1} {p : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} {U : (i : ι) → ↥(Matrix.unitaryGroup (p i) ℂ)} : (piInnerAut U) (Module.Dual.pi.matrixBlock φ) = Module.Dual.pi.matrixBlock φ ↔ ∀ (a : ι), ↑(U a) * (φ a).matrix = (φ a).matrix * ↑(U a)

theorem innerAutStarAlg_adjoint_eq_symm_of {ι : Type u_1} {p : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] {U : (i : ι) → ↥(Matrix.unitaryGroup (p i) ℂ)} : (piInnerAut U) (Module.Dual.pi.matrixBlock φ) = Module.Dual.pi.matrixBlock φ → LinearMap.adjoint (piInnerAut U).toLinearMap = (piInnerAut U).symm.toLinearMap

theorem QuantumGraph.Real.piMat_conj_unitary {ι : Type u_1} {p : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] {A : PiMat ℂ ι p →ₗ[ℂ] PiMat ℂ ι p} : Real (PiMat ℂ ι p) A → ∀ {U : (i : ι) → ↥(Matrix.unitaryGroup (p i) ℂ)}, (piInnerAut U) (Module.Dual.pi.matrixBlock φ) = Module.Dual.pi.matrixBlock φ → Real (PiMat ℂ ι p) ((piInnerAut U).toLinearMap ∘ₗ A ∘ₗ LinearMap.adjoint (piInnerAut U).toLinearMap)

Real quantum graphs on PiMat are preserved by blockwise unitary conjugation.

@[reducible, inline]

noncomputable abbrev Matrix.UnitaryGroup.toEuclideanLinearEquiv {n : Type u_3} [Fintype n] [DecidableEq n] (A : ↥(unitaryGroup n ℂ)) : EuclideanSpace ℂ n ≃ₗ[ℂ] EuclideanSpace ℂ n

A unitary matrix as a linear equivalence of Euclidean space.

Equations

• Matrix.UnitaryGroup.toEuclideanLinearEquiv A = (WithLp.linearEquiv 2 ℂ (n → ℂ)).trans ((Matrix.UnitaryGroup.toLinearEquiv A).trans (WithLp.linearEquiv 2 ℂ (n → ℂ)).symm)

theorem Matrix.UnitaryGroup.toEuclideanLinearEquiv_apply {n : Type u_3} [Fintype n] [DecidableEq n] (A : ↥(unitaryGroup n ℂ)) (v : EuclideanSpace ℂ n) : (toEuclideanLinearEquiv A) v = WithLp.toLp 2 ((↑A).mulVec v.ofLp)

noncomputable def Matrix.UnitaryGroup.toEuclideanLinearIsometryEquiv {n : Type u_3} [Fintype n] [DecidableEq n] (A : ↥(unitaryGroup n ℂ)) : EuclideanSpace ℂ n ≃ₗᵢ[ℂ] EuclideanSpace ℂ n

A unitary matrix as a linear isometry equivalence of Euclidean space.

Equations

• Matrix.UnitaryGroup.toEuclideanLinearIsometryEquiv A = { toLinearEquiv := Matrix.UnitaryGroup.toEuclideanLinearEquiv A, norm_map' := ⋯ }

theorem Matrix.UnitaryGroup.toEuclideanLinearIsometryEquiv_apply {n : Type u_3} [Fintype n] [DecidableEq n] (A : ↥(unitaryGroup n ℂ)) (x : EuclideanSpace ℂ n) : (toEuclideanLinearIsometryEquiv A) x = WithLp.toLp 2 ((↑A).mulVec x.ofLp)

theorem Matrix.UnitaryGroup.toEuclideanLinearIsometryEquiv_symm_apply {n : Type u_3} [Fintype n] [DecidableEq n] (A : ↥(unitaryGroup n ℂ)) (x : EuclideanSpace ℂ n) : (toEuclideanLinearIsometryEquiv A).symm x = WithLp.toLp 2 ((↑A⁻¹).mulVec x.ofLp)

theorem Matrix.UnitaryGroup.toEuclideanLinearIsometryEquiv_apply' {n : Type u_3} [Fintype n] [DecidableEq n] (A : ↥(unitaryGroup n ℂ)) (x : EuclideanSpace ℂ n) : (toEuclideanLinearIsometryEquiv A).symm x = WithLp.toLp 2 ((↑A).conjTranspose.mulVec x.ofLp)

@[reducible, inline]

noncomputable abbrev unitaryTensorEuclidean {ι : Type u_1} {p : ι → Type u_2} [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] (U : (i : ι) → ↥(Matrix.unitaryGroup (p i) ℂ)) (i : ι × ι) : EuclideanSpace ℂ (p i.1 × p i.2) ≃ₗᵢ[ℂ] EuclideanSpace ℂ (p i.1 × p i.2)

Tensor-product Euclidean isometry induced by a pair of blockwise unitaries.

Equations

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

theorem unitaryTensorEuclidean_apply {ι : Type u_1} {p : ι → Type u_2} [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {U : (i : ι) → ↥(Matrix.unitaryGroup (p i) ℂ)} (i : ι × ι) (x : EuclideanSpace ℂ (p i.1)) (y : EuclideanSpace ℂ (p i.2)) : (unitaryTensorEuclidean U i) (euclideanSpaceTensor' (x ⊗ₜ[ℂ] y)) = euclideanSpaceTensor' (WithLp.toLp 2 ((↑(U i.1)).mulVec x.ofLp) ⊗ₜ[ℂ] WithLp.toLp 2 ((↑(U i.2)).conj.mulVec y.ofLp))

theorem unitaryTensorEuclidean_apply' {ι : Type u_1} {p : ι → Type u_2} [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {U : (i : ι) → ↥(Matrix.unitaryGroup (p i) ℂ)} (i : ι × ι) (x : EuclideanSpace ℂ (p i.1 × p i.2)) : (unitaryTensorEuclidean U i) x = ∑ j : p i.1 × p i.2, euclideanSpaceTensor' (WithLp.toLp 2 ((↑(U i.1)).mulVec (x.prodChoose j).1.ofLp) ⊗ₜ[ℂ] WithLp.toLp 2 ((↑(U i.2)).conj.mulVec (x.prodChoose j).2.ofLp))

theorem unitaryTensorEuclidean_symm_apply {ι : Type u_1} {p : ι → Type u_2} [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {U : (i : ι) → ↥(Matrix.unitaryGroup (p i) ℂ)} (i : ι × ι) (x : EuclideanSpace ℂ (p i.1)) (y : EuclideanSpace ℂ (p i.2)) : (unitaryTensorEuclidean U i).symm (euclideanSpaceTensor' (x ⊗ₜ[ℂ] y)) = euclideanSpaceTensor' (WithLp.toLp 2 ((↑(U i.1)).conjTranspose.mulVec x.ofLp) ⊗ₜ[ℂ] WithLp.toLp 2 ((↑(U i.2)).transpose.mulVec y.ofLp))

theorem QuantumGraph.Real.PiMatSubmodule_eq_submodule_iff {ι : Type u_1} {p : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] {A B : PiMat ℂ ι p →ₗ[ℂ] PiMat ℂ ι p} (hA : Real (PiMat ℂ ι p) A) (hB : Real (PiMat ℂ ι p) B) : (∀ (i : ι × ι), hA.PiMatSubmodule i = hB.PiMatSubmodule i) ↔ A = B

theorem Matrix.kronecker_mulVec_euclideanSpaceTensor' {n : Type u_3} {m : Type u_4} [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (A : Matrix n n ℂ) (B : Matrix m m ℂ) (x : EuclideanSpace ℂ n) (y : EuclideanSpace ℂ m) : (kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A B).mulVec ((WithLp.equiv 2 (n × m → ℂ)) (euclideanSpaceTensor' (x ⊗ₜ[ℂ] y))) = (WithLp.equiv 2 ((i : n × m) → (fun (x : n × m) => ℂ) i)) (euclideanSpaceTensor' (WithLp.toLp 2 (A.mulVec x.ofLp) ⊗ₜ[ℂ] WithLp.toLp 2 (B.mulVec y.ofLp)))

theorem StarAlgEquiv.piCongrRight_apply_includeBlock {ι : Type u_3} {p : ι → Type u_4} [(i : ι) → Fintype (p i)] [DecidableEq ι] (f : (i : ι) → Matrix (p i) (p i) ℂ ≃⋆ₐ[ℂ] Matrix (p i) (p i) ℂ) (i : ι) (x : Matrix (p i) (p i) ℂ) : (piCongrRight fun (a : ι) => f a) (Matrix.includeBlock x) = Matrix.includeBlock ((f i) x)

theorem Matrix.innerAutStarAlg_apply_vecMulVec {n : Type u_3} {𝕜 : Type u_4} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] (U : ↥(unitaryGroup n 𝕜)) (x y : n → 𝕜) : (innerAutStarAlg U) (vecMulVec x y) = vecMulVec ((↑U).mulVec x) ((↑U).conj.mulVec y)

theorem Matrix.innerAutStarAlg_apply_vecMulVec_star {n : Type u_3} {𝕜 : Type u_4} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] (U : ↥(unitaryGroup n 𝕜)) (x y : n → 𝕜) : (innerAutStarAlg U) (vecMulVec x (star y)) = vecMulVec ((↑U).mulVec x) (star ((↑U).mulVec y))

theorem Matrix.innerAutStarAlg_apply_star_vecMulVec {n : Type u_3} {𝕜 : Type u_4} [Fintype n] [Field 𝕜] [StarRing 𝕜] [DecidableEq n] (U : ↥(unitaryGroup n 𝕜)) (x y : n → 𝕜) : (innerAutStarAlg U) (vecMulVec (star x) y) = (vecMulVec ((↑U).conj.mulVec x) (star ((↑U).conj.mulVec y))).conj

theorem Matrix.PosSemidef.eq_iff_sq_eq_sq {n : Type u_3} [Fintype n] [DecidableEq n] {A : Matrix n n ℂ} (hA : A.PosSemidef) {B : Matrix n n ℂ} (hB : B.PosSemidef) : A ^ 2 = B ^ 2 ↔ A = B

theorem innerAutStarAlg_apply_dualMatrix_eq_iff_eq_sqrt {ι : Type u_1} {p : ι → Type u_2} [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] {i : ι} (U : ↥(Matrix.unitaryGroup (p i) ℂ)) : (Matrix.innerAutStarAlg U) (φ i).matrix = (φ i).matrix ↔ (Matrix.innerAutStarAlg U) (⋯.rpow (1 / 2)) = ⋯.rpow (1 / 2)

theorem PiMat.modAut {ι : Type u_1} {p : ι → Type u_2} [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] [Finite ι] (r : ℝ) (x : PiMat ℂ ι p) (i : ι) : (starAlgebra.modAut r) x i = (sig ⋯ r) (x i)

theorem Matrix.counit_eq_dual {n : Type u_3} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [φ.IsFaithfulPosMap] : CoalgebraStruct.counit = φ

theorem PiMat.counit_eq_dual {ι : Type u_1} {p : ι → Type u_2} [Fintype ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] : CoalgebraStruct.counit = Module.Dual.pi φ

theorem modAut_eq_id_iff {ι : Type u_1} {p : ι → Type u_2} [Fintype ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] (r : ℝ) : modAut r = 1 ↔ r = 0 ∨ Module.Dual.IsTracial CoalgebraStruct.counit

theorem unitary.mul_inj {A : Type u_3} [Monoid A] [StarMul A] (U : ↥(unitary A)) (x y : A) : ↑U * x = ↑U * y ↔ x = y

theorem piInnerAut_modAut_commutes_of {ι : Type u_1} {p : ι → Type u_2} [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] [Finite ι] {U : (i : ι) → ↥(Matrix.unitaryGroup (p i) ℂ)} {r : ℝ} : (∀ (i : ι), (Matrix.innerAutStarAlg (U i)) (⋯.rpow r) = ⋯.rpow r) → ∀ (x : PiMat ℂ ι p), (piInnerAut U) ((modAut (-r)) x) = (modAut (-r)) ((piInnerAut U) x)

theorem QuantumGraph.Real.PiMat_applyConjInnerAut {ι : Type u_1} {p : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] {A : PiMat ℂ ι p →ₗ[ℂ] PiMat ℂ ι p} (hA : Real (PiMat ℂ ι p) A) {U : (i : ι) → ↥(Matrix.unitaryGroup (p i) ℂ)} : (piInnerAut U) (Module.Dual.pi.matrixBlock φ) = Module.Dual.pi.matrixBlock φ → have S := fun (i : ι × ι) (j : Fin (Module.finrank ℂ ↥(hA.PiMatSubmodule i))) => (↑((hA.PiMatOrthonormalBasis i) j)).prodChoose; (piInnerAut U).toLinearMap ∘ₗ A ∘ₗ LinearMap.adjoint (piInnerAut U).toLinearMap = ↑(∑ i : ι × ι, ∑ j : Fin (Module.finrank ℂ ↥(hA.PiMatSubmodule i)), ∑ s : p i.1 × p i.2, ∑ l : p i.1 × p i.2, ((rankOne ℂ) (Matrix.includeBlock (Matrix.vecMulVec ((↑(U i.1)).mulVec (S i j s).1.ofLp) (star ((↑(U i.1)).mulVec (S i j l).1.ofLp))))) ((modAut (-(1 / 2))) (Matrix.includeBlock (Matrix.vecMulVec ((↑(U i.2)).conj.mulVec (S i j s).2.ofLp) (star ((↑(U i.2)).conj.mulVec (S i j l).2.ofLp))).conj)))

theorem QuantumGraph.Real.PiMat_conj_unitary_submodule_eq_map {ι : Type u_1} {p : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] {A : PiMat ℂ ι p →ₗ[ℂ] PiMat ℂ ι p} (hA : Real (PiMat ℂ ι p) A) {U : (i : ι) → ↥(Matrix.unitaryGroup (p i) ℂ)} (hU : (piInnerAut U) (Module.Dual.pi.matrixBlock φ) = Module.Dual.pi.matrixBlock φ) (i : ι × ι) : ⋯.PiMatSubmodule i = Submodule.map (↑(unitaryTensorEuclidean U i).toLinearEquiv) (hA.PiMatSubmodule i)

theorem orthogonalProjection'_bot {𝕜 : Type u_3} {E : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : orthogonalProjection' ⊥ = 0

theorem LinearMap.proj_apply_includeBlock {ι : Type u_1} {p : ι → Type u_2} [DecidableEq ι] (i j : ι) (x : Matrix (p j) (p j) ℂ) : (proj i) (Matrix.includeBlock x) = if h : j = i then ⋯.mpr x else 0

theorem PiMat.modAut_includeBlock {ι : Type u_1} {p : ι → Type u_2} [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] [Finite ι] (r : ℝ) (j : ι) (x : Matrix (p j) (p j) ℂ) : (starAlgebra.modAut r) (Matrix.includeBlock x) = Matrix.includeBlock ((starAlgebra.modAut r) x)

theorem PiMat.modAut_proj {ι : Type u_1} {p : ι → Type u_2} [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] [Finite ι] (r : ℝ) (j : ι) (x : PiMat ℂ ι p) : (starAlgebra.modAut r) ((LinearMap.proj j) x) = (LinearMap.proj j) ((starAlgebra.modAut r) x)

theorem EuclideanSpace.prodChoose_zero_fst {n : Type u_3} {m : Type u_4} [Fintype n] [DecidableEq n] [Fintype m] [DecidableEq m] (i : n × m) : (prodChoose 0 i).1 = 0

theorem QuantumGraph.Real.PiMatSubmodule_eq_bot_iff_proj_comp_adjoint_proj_eq_zero {ι : Type u_1} {p : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] {A : PiMat ℂ ι p →ₗ[ℂ] PiMat ℂ ι p} (hA : Real (PiMat ℂ ι p) A) {i : ι × ι} : hA.PiMatSubmodule i = ⊥ ↔ LinearMap.proj i.1 ∘ₗ A ∘ₗ LinearMap.adjoint (LinearMap.proj i.2) = 0

theorem QuantumGraph.Real.PiMatSubmodule_eq_top_iff_proj_comp_adjoint_proj_eq_rankOne_one_one {ι : Type u_1} {p : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] {A : PiMat ℂ ι p →ₗ[ℂ] PiMat ℂ ι p} (hA : Real (PiMat ℂ ι p) A) {i : ι × ι} : hA.PiMatSubmodule i = ⊤ ↔ LinearMap.proj i.1 ∘ₗ A ∘ₗ LinearMap.adjoint (LinearMap.proj i.2) = ↑(((rankOne ℂ) 1) 1)

theorem Matrix.trace_eq_linearMap_trace {n : Type u_3} [Fintype n] [DecidableEq n] (y : Matrix n n ℂ) : y.trace = (LinearMap.trace ℂ (EuclideanSpace ℂ n)) (toEuclideanLin y)

theorem Matrix.trace_piMatTensorProductEquiv_apply_lTensor_transpose {ι : Type u_3} [Fintype ι] [DecidableEq ι] {p : ι → Type u_4} [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] (x : TensorProduct ℂ (PiMat ℂ ι p) (PiMat ℂ ι p)ᵐᵒᵖ) (i : ι × ι) : trace (PiMatTensorProductEquiv ((StarAlgEquiv.lTensor (PiMat ℂ ι p) (PiMat.transposeStarAlgEquiv ι p).symm) x) i) = trace (PiMatTensorProductEquiv ((LinearMap.lTensor (PiMat ℂ ι p) ↑(unop ℂ)) x) i)

theorem Matrix.trace_piMatTensorProductEquiv_lTensor_unop_map_modAut {ι : Type u_1} {p : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] (x : TensorProduct ℂ (PiMat ℂ ι p) (PiMat ℂ ι p)ᵐᵒᵖ) (i : ι × ι) : trace (PiMatTensorProductEquiv ((LinearMap.lTensor (PiMat ℂ ι p) ↑(unop ℂ)) ((TensorProduct.map (modAut (0 - 1 / 2)).toLinearMap (AlgEquiv.op (modAut (0 - 1 / 2))).toLinearMap) x)) i) = trace (PiMatTensorProductEquiv ((LinearMap.lTensor (PiMat ℂ ι p) ↑(unop ℂ)) x) i)

theorem Matrix.trace_piMatTensorProductEquiv_lTensor_unop_tenSwap {ι : Type u_1} {p : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] (x : TensorProduct ℂ (PiMat ℂ ι p) (PiMat ℂ ι p)ᵐᵒᵖ) (i : ι × ι) : trace (PiMatTensorProductEquiv ((LinearMap.lTensor (PiMat ℂ ι p) ↑(unop ℂ)) ((tenSwap ℂ) x)) i) = trace (PiMatTensorProductEquiv ((LinearMap.lTensor (PiMat ℂ ι p) ↑(unop ℂ)) x) i.swap)

def LinearIsometryEquiv.ofLinearEquiv {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (f : E ≃ₗ[𝕜] F) (hf : LinearMap.adjoint ↑f = ↑f.symm) : E ≃ₗᵢ[𝕜] F

Build a linear isometry equivalence from a linear equivalence whose adjoint is its inverse.

Equations

• LinearIsometryEquiv.ofLinearEquiv f hf = { toLinearEquiv := f, norm_map' := ⋯ }

theorem LinearIsometryEquiv.ofLinearEquiv_apply {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (f : E ≃ₗ[𝕜] F) (hf : LinearMap.adjoint ↑f = ↑f.symm) (x : E) : (ofLinearEquiv f hf) x = f x

noncomputable def TensorProduct.commLinearIsometryEquiv (𝕜 : Type u_3) (E : Type u_4) (F : Type u_5) [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] : TensorProduct 𝕜 E F ≃ₗᵢ[𝕜] TensorProduct 𝕜 F E

Tensor-product commutativity as a linear isometry equivalence.

Equations

• TensorProduct.commLinearIsometryEquiv 𝕜 E F = LinearIsometryEquiv.ofLinearEquiv (TensorProduct.comm 𝕜 E F) ⋯

theorem TensorProduct.commLinearIsometryEquiv_apply {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (x : E) (y : F) : (commLinearIsometryEquiv 𝕜 E F) (x ⊗ₜ[𝕜] y) = y ⊗ₜ[𝕜] x

noncomputable def EuclideanSpace.tensorComm {n : Type u_3} {m : Type u_4} [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] : EuclideanSpace ℂ (n × m) ≃ₗᵢ[ℂ] EuclideanSpace ℂ (m × n)

Commute the factors of Euclidean space indexed by a product.

Equations

• EuclideanSpace.tensorComm = (euclideanSpaceTensor'.symm.trans (TensorProduct.commLinearIsometryEquiv ℂ (EuclideanSpace ℂ n) (EuclideanSpace ℂ m))).trans euclideanSpaceTensor'

theorem EuclideanSpace.tensorComm_apply {n : Type u_3} {m : Type u_4} [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (x : EuclideanSpace ℂ n) (y : EuclideanSpace ℂ m) : tensorComm (euclideanSpaceTensor' (x ⊗ₜ[ℂ] y)) = euclideanSpaceTensor' (y ⊗ₜ[ℂ] x)

theorem QuantumGraph.Real.piMat_submodule_finrank_eq_swap_of_adjoint {ι : Type u_1} {p : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] {f : PiMat ℂ ι p →ₗ[ℂ] PiMat ℂ ι p} (hf : Real (PiMat ℂ ι p) f) : LinearMap.adjoint f = f → ∀ (i : ι × ι), Module.finrank ℂ ↥(hf.PiMatSubmodule i) = Module.finrank ℂ ↥(hf.PiMatSubmodule i.swap)

theorem QuantumGraph.Real.PiMatSubmodule_eq_bot_iff_swap_eq_bot_of_adjoint {ι : Type u_1} {p : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] {A : PiMat ℂ ι p →ₗ[ℂ] PiMat ℂ ι p} (hA : Real (PiMat ℂ ι p) A) : LinearMap.adjoint A = A → ∀ (i : ι × ι), hA.PiMatSubmodule i = ⊥ ↔ hA.PiMatSubmodule i.swap = ⊥

theorem Submodule.finrank_eq_iff_eq_top {K : Type u_3} {V : Type u_4} [DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {S : Submodule K V} : Module.finrank K ↥S = Module.finrank K V ↔ S = ⊤

theorem QuantumGraph.Real.PiMatSubmodule_eq_top_iff_swap_eq_top_of_adjoint {ι : Type u_1} {p : ι → Type u_2} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] {A : PiMat ℂ ι p →ₗ[ℂ] PiMat ℂ ι p} (hA : Real (PiMat ℂ ι p) A) : LinearMap.adjoint A = A → ∀ (i : ι × ι), hA.PiMatSubmodule i = ⊤ ↔ hA.PiMatSubmodule i.swap = ⊤