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

Equations

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

@[simp]

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

@[simp]

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

@[reducible, inline]

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

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

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)] (x : TensorProduct ℂ (PiMat ℂ ι₁ p₁) (PiMat ℂ ι₂ p₂)) (i : ι₁ × ι₂) : PiMatTensorProductEquiv x i = TensorProduct.toKronecker (directSumTensorToFun x 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)] (x : PiMat ℂ (ι₁ × ι₂) fun (i : ι₁ × ι₂) => p₁ i.1 × p₂ i.2) : PiMatTensorProductEquiv.symm x = directSumTensorInvFun ((AlgEquiv.piCongrRight fun (i : ι₁ × ι₂) => tensorToKronecker.symm) x)

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] : (B →L[𝕜] B) ≃⋆ₐ[𝕜] B →ₗ[𝕜] B

Equations

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

@[reducible, inline]

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

Equations

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

theorem isIdempotentElem_iff {M : Type u_3} [Mul M] {p : M} : IsIdempotentElem p ↔ p * p = p

@[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 →ₗ[ℂ] ℂ

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)] (a✝ : PiMat ℂ ι p) : traceLinearMap a✝ = (Matrix.blockDiagonal'AlgHom a✝).trace

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} (hf : QuantumGraph (PiMat ℂ ι p) f) (t r : ℝ) : ∃ (u : (i : ι × ι) → Submodule ℂ (EuclideanSpace ℂ (p i.1 × p i.2))), ∀ (i : ι × ι), LinearMap.IsProj (u i) (PiMat_toEuclideanLM (PiMatTensorProductEquiv ((StarAlgEquiv.lTensor (PiMat ℂ ι p) (PiMat.transposeStarAlgEquiv ι p).symm) ((QuantumSet.Psi t r) f))) i)

noncomputable def QuantumGraph.PiMat_submodule {ι : 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 : ι × ι) : Submodule ℂ (EuclideanSpace ℂ (p i.1 × p i.2))

Equations

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

theorem QuantumGraph.PiMat_submoduleIsProj {ι : 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.PiMat_submodule t r i) (PiMat_toEuclideanLM (PiMatTensorProductEquiv ((StarAlgEquiv.lTensor (PiMat ℂ ι p) (PiMat.transposeStarAlgEquiv ι p).symm) ((QuantumSet.Psi t r) f))) i)

theorem QuantumGraph.PiMat_submoduleIsProj_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.PiMat_submodule t r i).subtype ∘ₗ ⋯.codRestrict = PiMat_toEuclideanLM (PiMatTensorProductEquiv ((StarAlgEquiv.lTensor (PiMat ℂ ι p) (PiMat.transposeStarAlgEquiv ι p).symm) ((QuantumSet.Psi t r) f))) i

noncomputable def QuantumGraph.dim_of_piMat_submodule {ι : 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) : ℕ

Equations

• hf.dim_of_piMat_submodule = ∑ i : ι × ι, Module.finrank ℂ ↥(hf.PiMat_submodule 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.dim_of_piMat_submodule_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.dim_of_piMat_submodule = 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

theorem QuantumGraph.dim_of_piMat_submodule_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] (hc : CoalgebraStruct.counit = PiMat.traceLinearMap) {f : PiMat ℂ ι p →ₗ[ℂ] PiMat ℂ ι p} (hf : QuantumGraph (PiMat ℂ ι p) f) : ↑hf.dim_of_piMat_submodule = 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.dim_of_piMat_submodule_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] (hc : CoalgebraStruct.counit = PiMat.traceLinearMap) {f : PiMat ℂ ι p →ₗ[ℂ] PiMat ℂ ι p} (hf : QuantumGraph (PiMat ℂ ι p) f) : ↑hf.dim_of_piMat_submodule = NumOfEdges f

theorem QuantumGraph.dim_of_piMat_submodule_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.dim_of_piMat_submodule = ∑ i : ι × ι, Fintype.card (p i.1) * Fintype.card (p i.2) ↔ f = Qam.completeGraph (PiMat ℂ ι p) (PiMat ℂ ι p)

theorem QuantumGraph.CompleteGraph_dim_of_piMat_submodule {ι : 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] : ⋯.dim_of_piMat_submodule = ∑ 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 ι] [DecidableEq ι] [(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_dim_of_piMat_submodule_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] (hφ₂ : (Module.Dual.pi φ).IsUnital) (hB : 1 < Module.finrank ℂ (PiMat ℂ ι p)) : ∃ (A : PiMat ℂ ι p →ₗ[ℂ] PiMat ℂ ι p) (hA : QuantumGraph (PiMat ℂ ι p) A), QuantumGraph.NumOfEdges A ≠ ↑hA.dim_of_piMat_submodule

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} (hA : Real (PiMat ℂ ι p) A) (i : ι × ι) : (LinearMap.toContinuousLinearMap (PiMat_toEuclideanLM (PiMatTensorProductEquiv ((StarAlgEquiv.lTensor (PiMat ℂ ι p) (PiMat.transposeStarAlgEquiv ι p).symm) ((QuantumSet.Psi 0 (1 / 2)) A))) i)).IsOrthogonalProjection

noncomputable def QuantumGraph.Real.PiMat_submodule {ι : 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 : ι × ι) : Submodule ℂ (EuclideanSpace ℂ (p i.1 × p i.2))

Equations

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

theorem QuantumGraph.Real.PiMat_submoduleOrthogonalProjection {ι : 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.PiMat_submodule i) = LinearMap.toContinuousLinearMap (PiMat_toEuclideanLM (PiMatTensorProductEquiv ((StarAlgEquiv.lTensor (PiMat ℂ ι p) (PiMat.transposeStarAlgEquiv ι p).symm) ((QuantumSet.Psi 0 (1 / 2)) A))) i)

noncomputable def QuantumGraph.Real.PiMat_orthonormalBasis {ι : 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.PiMat_submodule i))) ℂ ↥(hA.PiMat_submodule i)

Equations

• hA.PiMat_orthonormalBasis i = stdOrthonormalBasis ℂ ↥(hA.PiMat_submodule 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] [DecidableEq n] [Fintype m] [DecidableEq m] (x : EuclideanSpace ℂ n) (y : EuclideanSpace ℂ m) : toEuclideanLin (vecMulVec x y) = ↑(((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) = Matrix.reshape (Matrix.vecMulVec x y)

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)

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)

Equations

• x.chooseFinset = (fun (S : Finset (M × N)) (x : x = ∑ i ∈ S, i.1 ⊗ₜ[R] i.2) => S) (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.prod_choose {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

Equations

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

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

theorem 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.prod_choose_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.prod_choose s).1 ⊗ₜ[ℂ] (x.prod_choose 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) : let S := fun (i : ι × ι) (j : Fin (Module.finrank ℂ ↥(hA.PiMat_submodule i))) => (↑((hA.PiMat_orthonormalBasis i) j)).prod_choose; A = ↑(∑ i : ι × ι, ∑ j : Fin (Module.finrank ℂ ↥(hA.PiMat_submodule 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 (star (S i j l).1)))) ((modAut (-(1 / 2))) (Matrix.includeBlock (Matrix.vecMulVec (S i j s).2 (star (S i j l).2)).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)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] (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} [Fintype ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] (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_dim_of_piMat_submodule {ι : 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)] : ⋯.dim_of_piMat_submodule = 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

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) ℂ)} (hU : (piInnerAut U) (Module.Dual.pi.matrixBlock φ) = Module.Dual.pi.matrixBlock φ) : LinearMap.adjoint (piInnerAut U).toLinearMap = (piInnerAut U).symm.toLinearMap

def 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} (hA : Real (PiMat ℂ ι p) A) {U : (i : ι) → ↥(Matrix.unitaryGroup (p i) ℂ)} (hU : (piInnerAut U) (Module.Dual.pi.matrixBlock φ) = Module.Dual.pi.matrixBlock φ) : Real (PiMat ℂ ι p) ((piInnerAut U).toLinearMap ∘ₗ A ∘ₗ LinearMap.adjoint (piInnerAut U).toLinearMap)

Equations

• ⋯ = ⋯

@[reducible, inline]

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

Equations

• Matrix.UnitaryGroup.toEuclideanLinearEquiv A = Matrix.UnitaryGroup.toLinearEquiv A

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

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

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 = (↑A).mulVec x

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

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

@[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)

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' ((↑(U i.1)).mulVec x ⊗ₜ[ℂ] (↑(U i.2)).conj.mulVec y)

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' ((↑(U i.1)).mulVec (x.prod_choose j).1 ⊗ₜ[ℂ] (↑(U i.2)).conj.mulVec (x.prod_choose j).2)

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' ((↑(U i.1)).conjTranspose.mulVec x ⊗ₜ[ℂ] (↑(U i.2)).transpose.mulVec y)

theorem QuantumGraph.Real.PiMat_submodule_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.PiMat_submodule i = hB.PiMat_submodule 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' (A.mulVec x ⊗ₜ[ℂ] B.mulVec y))

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.mul_vecMulVec {n : Type u_3} {m : Type u_4} {R : Type u_5} [Fintype m] [Semiring R] (A : Matrix n m R) (x : m → R) (y : n → R) : A * vecMulVec x y = vecMulVec (A.mulVec x) y

theorem Matrix.vecMulVec_mul {n : Type u_3} {m : Type u_4} {R : Type u_5} [Fintype n] [CommSemiring R] (x : m → R) (y : n → R) (A : Matrix n m R) : vecMulVec x y * A = vecMulVec x (A.transpose.mulVec y)

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} {𝕜 : Type u_4} [Fintype n] [RCLike 𝕜] [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} [Fintype ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] {r : ℝ} : starAlgebra.modAut r = AlgEquiv.piCongrRight fun (x : ι) => starAlgebra.modAut r

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 ι] [DecidableEq ι] [(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 ι] [DecidableEq ι] [(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} [Fintype ι] [(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) ℂ)} {r : ℝ} (h : ∀ (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) ℂ)} (hU : (piInnerAut U) (Module.Dual.pi.matrixBlock φ) = Module.Dual.pi.matrixBlock φ) : let S := fun (i : ι × ι) (j : Fin (Module.finrank ℂ ↥(hA.PiMat_submodule i))) => (↑((hA.PiMat_orthonormalBasis i) j)).prod_choose; (piInnerAut U).toLinearMap ∘ₗ A ∘ₗ LinearMap.adjoint (piInnerAut U).toLinearMap = ↑(∑ i : ι × ι, ∑ j : Fin (Module.finrank ℂ ↥(hA.PiMat_submodule 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) (star ((↑(U i.1)).mulVec (S i j l).1))))) ((modAut (-(1 / 2))) (Matrix.includeBlock (Matrix.vecMulVec ((↑(U i.2)).conj.mulVec (S i j s).2) (star ((↑(U i.2)).conj.mulVec (S i j l).2))).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 : ι × ι) : ⋯.PiMat_submodule i = Submodule.map (unitaryTensorEuclidean U i) (hA.PiMat_submodule 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} [Fintype ι] [DecidableEq ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] (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} [Fintype ι] [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] (r : ℝ) (j : ι) (x : PiMat ℂ ι p) : (starAlgebra.modAut r) ((LinearMap.proj j) x) = (LinearMap.proj j) ((starAlgebra.modAut r) x)

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

theorem Matrix.vecMulVec_zero {m : Type u_3} {n : Type u_4} {α : Type u_5} [MulZeroClass α] (w : m → α) : vecMulVec w 0 = 0

theorem Matrix.zero_vecMulVec {m : Type u_3} {n : Type u_4} {α : Type u_5} [MulZeroClass α] (w : n → α) : vecMulVec 0 w = 0

theorem QuantumGraph.Real.PiMat_submodule_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.PiMat_submodule i = ⊥ ↔ LinearMap.proj i.1 ∘ₗ A ∘ₗ LinearMap.adjoint (LinearMap.proj i.2) = 0

theorem QuantumGraph.Real.PiMat_submodule_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.PiMat_submodule 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.of_linearEquiv {𝕜 : 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

Equations

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

theorem LinearIsometryEquiv.of_linearEquiv_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) : (of_linearEquiv f hf) x = f x

noncomputable def TensorProduct.comm_linearIsometryEquiv (𝕜 : 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

Equations

• TensorProduct.comm_linearIsometryEquiv 𝕜 E F = LinearIsometryEquiv.of_linearEquiv (TensorProduct.comm 𝕜 E F) ⋯

theorem TensorProduct.comm_linearIsometryEquiv_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) : (comm_linearIsometryEquiv 𝕜 E F) (x ⊗ₜ[𝕜] y) = y ⊗ₜ[𝕜] x

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

Equations

• EuclideanSpace.tensor_comm = (euclideanSpaceTensor'.symm.trans (TensorProduct.comm_linearIsometryEquiv ℂ (EuclideanSpace ℂ n) (EuclideanSpace ℂ m))).trans euclideanSpaceTensor'

theorem EuclideanSpace.tensor_comm_apply {n : Type u_3} {m : Type u_4} [Fintype n] [Fintype m] [DecidableEq n] [DecidableEq m] (x : EuclideanSpace ℂ n) (y : EuclideanSpace ℂ m) : tensor_comm (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) (hf₂ : LinearMap.adjoint f = f) (i : ι × ι) : Module.finrank ℂ ↥(hf.PiMat_submodule i) = Module.finrank ℂ ↥(hf.PiMat_submodule i.swap)

theorem QuantumGraph.Real.PiMat_submodule_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) (hA₂ : LinearMap.adjoint A = A) (i : ι × ι) : hA.PiMat_submodule i = ⊥ ↔ hA.PiMat_submodule 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.PiMat_submodule_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) (hA₂ : LinearMap.adjoint A = A) (i : ι × ι) : hA.PiMat_submodule i = ⊤ ↔ hA.PiMat_submodule i.swap = ⊤