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 : ι) : (PiMat.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) : (PiMat.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] : ⇑Matrix.toEuclideanStarAlgEquiv = ⇑Matrix.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 : p₁ r.1 × p₂ r.2) (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 : p₁ r.1) (c : p₁ r.1) (b : p₂ r.2) (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), PiMat.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 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 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 : QuantumGraph.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 : QuantumGraph.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 : QuantumGraph.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 : QuantumGraph.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] : Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) (if P then x₁ else 0) x₂ = if P then Matrix.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 α) : Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) (if p : P then x₁ p else 0) x₂ = if p_1 : P then Matrix.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] : Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) x₁ (if P then x₂ else 0) = if P then Matrix.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 α) : Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) x₁ (if p : P then x₂ p else 0) = if p_1 : P then Matrix.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 → α) : Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) (Matrix.vecMulVec x y) (Matrix.vecMulVec z w) = Matrix.vecMulVec (Matrix.reshape (Matrix.vecMulVec x z)) (Matrix.reshape (Matrix.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) : Matrix.toEuclideanLin (Matrix.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 → α) : (Matrix.vecMulVec x y).conj = Matrix.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 : QuantumGraph.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 ((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) : (StarAlgEquiv.piCongrRight e).symm = StarAlgEquiv.piCongrRight fun (i : ι) => (e i).symm

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

theorem unitary.mul_inv_eq_iff {A : Type u_3} [Monoid A] [StarMul A] (U : ↥(unitary A)) (x : A) (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 : QuantumGraph.Real (PiMat ℂ ι p) A) {U : (i : ι) → ↥(Matrix.unitaryGroup (p i) ℂ)} (hU : (piInnerAut U) (Module.Dual.pi.matrixBlock φ) = Module.Dual.pi.matrixBlock φ) : QuantumGraph.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 : ↥(Matrix.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 : ↥(Matrix.unitaryGroup n ℂ)) (v : EuclideanSpace ℂ n) : (Matrix.UnitaryGroup.toEuclideanLinearEquiv A) v = (↑A).mulVec v

noncomputable def Matrix.UnitaryGroup.toEuclideanLinearIsometryEquiv {n : Type u_3} [Fintype n] [DecidableEq n] (A : ↥(Matrix.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 : ↥(Matrix.unitaryGroup n ℂ)) (x : EuclideanSpace ℂ n) : (Matrix.UnitaryGroup.toEuclideanLinearIsometryEquiv A) x = (↑A).mulVec x

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

theorem Matrix.UnitaryGroup.toEuclideanLinearIsometryEquiv_apply' {n : Type u_3} [Fintype n] [DecidableEq n] (A : ↥(Matrix.unitaryGroup n ℂ)) (x : EuclideanSpace ℂ n) : (Matrix.UnitaryGroup.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 : PiMat ℂ ι p →ₗ[ℂ] PiMat ℂ ι p} {B : PiMat ℂ ι p →ₗ[ℂ] PiMat ℂ ι p} (hA : QuantumGraph.Real (PiMat ℂ ι p) A) (hB : QuantumGraph.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) : (Matrix.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) ℂ) : (StarAlgEquiv.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 * Matrix.vecMulVec x y = Matrix.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) : Matrix.vecMulVec x y * A = Matrix.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 : ↥(Matrix.unitaryGroup n 𝕜)) (x : n → 𝕜) (y : n → 𝕜) : (Matrix.innerAutStarAlg U) (Matrix.vecMulVec x y) = Matrix.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 : ↥(Matrix.unitaryGroup n 𝕜)) (x : n → 𝕜) (y : n → 𝕜) : (Matrix.innerAutStarAlg U) (Matrix.vecMulVec x (star y)) = Matrix.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 : ↥(Matrix.unitaryGroup n 𝕜)) (x : n → 𝕜) (y : n → 𝕜) : (Matrix.innerAutStarAlg U) (Matrix.vecMulVec (star x) y) = (Matrix.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 : ℝ} : modAut r = AlgEquiv.piCongrRight fun (x : ι) => modAut r

theorem Matrix.counit_eq_dual {n : Type u_3} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [φ.IsFaithfulPosMap] : Coalgebra.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] : Coalgebra.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 Coalgebra.counit

theorem unitary.mul_inj {A : Type u_3} [Monoid A] [StarMul A] (U : ↥(unitary A)) (x : A) (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 : QuantumGraph.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 : QuantumGraph.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)