theorem lmul_toMatrix {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (x : Matrix n n ℂ) : onb.toMatrix (lmul x) = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) x 1

theorem rmul_toMatrix {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (x : Matrix n n ℂ) : onb.toMatrix (rmul x) = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) 1 ((modAut (1 / 2)) x).transpose

theorem Matrix.stdBasisMatrix_transpose {R : Type u_2} {n : Type u_3} {p : Type u_4} [DecidableEq n] [DecidableEq p] [Zero R] {i : n} {j : p} {α : R} : (stdBasisMatrix i j α).transpose = stdBasisMatrix j i α

theorem Module.Dual.IsFaithfulPosMap.inner_coord' {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (y : Matrix n n ℂ) (i j : n) : inner (onb (i, j)) y = (y * ⋯.rpow (1 / 2)) i j

@[reducible, inline]

abbrev Matrix.transposeStarAlgEquiv (ι : Type u_2) [Fintype ι] [DecidableEq ι] : Matrix ι ι ℂ ≃⋆ₐ[ℂ] (Matrix ι ι ℂ)ᵐᵒᵖ

Equations

• Matrix.transposeStarAlgEquiv ι = StarAlgEquiv.ofAlgEquiv (Matrix.transposeAlgEquiv ι ℂ ℂ) ⋯

theorem Matrix.transposeStarAlgEquiv_apply {ι : Type u_2} [Fintype ι] [DecidableEq ι] (x : Matrix ι ι ℂ) : (transposeStarAlgEquiv ι) x = MulOpposite.op x.transpose

theorem Matrix.transposeStarAlgEquiv_symm_apply {ι : Type u_2} [Fintype ι] [DecidableEq ι] (x : (Matrix ι ι ℂ)ᵐᵒᵖ) : (transposeStarAlgEquiv ι).symm x = (MulOpposite.unop x).transpose

theorem QuantumSet.Psi_symm_transpose_kroneckerToTensor_toMatrix_rankOne {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (x y : Matrix n n ℂ) : (Psi 0 (1 / 2)).symm ((StarAlgEquiv.lTensor (Matrix n n ℂ) (Matrix.transposeStarAlgEquiv n)) (kroneckerToTensor (onb.toMatrix ↑(((rankOne ℂ) x) y)))) = lmul (x * φ.matrix) * LinearMap.adjoint (rmul (φ.matrix * y))

theorem QuantumGraph.Real.matrix_isOrthogonalProjection {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] {A : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ} (hA : Real (Matrix n n ℂ) A) : (ContinuousLinearMap.toLinearMapAlgEquiv.symm (onb.toMatrix.symm (tensorToKronecker ((StarAlgEquiv.lTensor (Matrix n n ℂ) (Matrix.transposeStarAlgEquiv n).symm) ((QuantumSet.Psi 0 (1 / 2)) A))))).IsOrthogonalProjection

noncomputable def QuantumGraph.Real.matrix_submodule {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] {A : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ} (hA : Real (Matrix n n ℂ) A) : Submodule ℂ (Matrix n n ℂ)

Equations

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

theorem QuantumGraph.Real.matrix_orthogonalProjection_eq {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] {A : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ} (hA : Real (Matrix n n ℂ) A) : orthogonalProjection' hA.matrix_submodule = ContinuousLinearMap.toLinearMapAlgEquiv.symm (onb.toMatrix.symm (tensorToKronecker ((StarAlgEquiv.lTensor (Matrix n n ℂ) (Matrix.transposeStarAlgEquiv n).symm) ((QuantumSet.Psi 0 (1 / 2)) A))))

theorem StarAlgEquiv.lTensor_symm {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [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).symm = lTensor C f.symm

theorem QuantumGraph.Real.matrix_eq_of_orthonormalBasis {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] {A : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ} (hA : Real (Matrix n n ℂ) A) {ι : Type u_2} [DecidableEq ι] [Fintype ι] (u : OrthonormalBasis ι ℂ ↥hA.matrix_submodule) : A = ∑ i : ι, lmul (↑(u i) * φ.matrix) * LinearMap.adjoint (rmul (φ.matrix * ↑(u i)))

theorem QuantumGraph.Real.matrix_submodule_exists_orthonormalBasis {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] {A : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ} (hA : Real (Matrix n n ℂ) A) : ∃ (u : OrthonormalBasis (Fin (Module.finrank ℂ ↥hA.matrix_submodule)) ℂ ↥hA.matrix_submodule), A = ∑ i : Fin (Module.finrank ℂ ↥hA.matrix_submodule), lmul (↑(u i) * φ.matrix) * LinearMap.adjoint (rmul (φ.matrix * ↑(u i)))

@[reducible, inline]

noncomputable abbrev QuantumGraph.Real.of_norm_one_matrix {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (u : { x : Matrix n n ℂ // ‖x‖ = 1 }) : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ

Equations

• QuantumGraph.Real.of_norm_one_matrix u = lmul (↑u * φ.matrix) * LinearMap.adjoint (rmul (φ.matrix * ↑u))

theorem OrthonormalBasis.norm_eq_one {ι : Type u_2} {𝕜 : Type u_3} {E : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] [DecidableEq ι] (u : OrthonormalBasis ι 𝕜 E) (i : ι) : ‖u i‖ = 1

theorem orthogonalProjection'_of_finrank_eq_one {𝕜 : Type u_2} {E : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U : Submodule 𝕜 E} (hU : Module.finrank 𝕜 ↥U = 1) : ∃ (v : { x : E // ‖x‖ = 1 }), orthogonalProjection' U = ((rankOne 𝕜) ↑v) ↑v

theorem QuantumSet.Psi_apply_matrix_one {n : Type u_2} [DecidableEq n] [Fintype n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] : (Psi 0 (1 / 2)) 1 = (StarAlgEquiv.lTensor (Matrix n n ℂ) (Matrix.transposeStarAlgEquiv n)) (kroneckerToTensor (onb.toMatrix ↑(((rankOne ℂ) φ.matrix⁻¹) φ.matrix⁻¹)))

theorem Module.Dual.IsFaithfulPosMap.inner_dualMatrix_right {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (x : Matrix n n ℂ) : inner x φ.matrix⁻¹ = star x.trace

theorem QuantumGraph.Real.of_norm_one_matrix_is_irreflexive_iff {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] [Nontrivial n] (x : { x : Matrix n n ℂ // ‖x‖ = 1 }) : of_norm_one_matrix x •ₛ 1 = 0 ↔ (↑x).trace = 0

noncomputable def normalize_of_ne_zero {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {a : E} (ha : a ≠ 0) : { x : E // ‖x‖ = 1 }

Equations

• normalize_of_ne_zero ha = ⟨(1 / ↑‖a‖) • a, ⋯⟩

theorem Module.Dual.IsFaithfulPosMap.norm_sq_dualMatrix_inv {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] : ↑‖φ.matrix⁻¹‖ ^ 2 = φ.matrix⁻¹.trace

theorem QuantumGraph.Real.of_norm_one_matrix_eq_trivialGraph {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] [Nontrivial n] : of_norm_one_matrix (normalize_of_ne_zero ⋯) = Qam.trivialGraph (Matrix n n ℂ)

theorem QuantumGraph.Real.of_norm_one_matrix_is_reflexive_iff {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] [Nontrivial n] (x : { x : Matrix n n ℂ // ‖x‖ = 1 }) : of_norm_one_matrix x •ₛ 1 = 1 ↔ ∃ (α : ℂˣ), ↑x = ↑α • φ.matrix⁻¹

theorem Matrix.traceLinearMap_comp_tensorToKronecker {n : Type u_2} [DecidableEq n] [Fintype n] : traceLinearMap (n × n) ℂ ℂ ∘ₗ TensorProduct.toKronecker = LinearMap.mul' ℂ ℂ ∘ₗ TensorProduct.map (traceLinearMap n ℂ ℂ) (traceLinearMap n ℂ ℂ)

theorem traceLinearMap_comp_transposeStarAlgEquiv_symm {n : Type u_2} [DecidableEq n] [Fintype n] : Matrix.traceLinearMap n ℂ ℂ ∘ₗ (Matrix.transposeStarAlgEquiv n).symm.toLinearMap = Matrix.traceLinearMap n ℂ ℂ ∘ₗ ↑(unop ℂ)

theorem QuantumGraph.NumOfEdges_eq {A : Type u_2} [starAlgebra A] [QuantumSet A] (B : A →ₗ[ℂ] A) : NumOfEdges B = inner 1 (B 1)

theorem QuantumGraph.Real.matrix_submodule_finrank_eq_numOfEdges_of_counit_eq_trace {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (hc : CoalgebraStruct.counit = Matrix.traceLinearMap n ℂ ℂ) {A : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ} (hA : Real (Matrix n n ℂ) A) : ↑(Module.finrank ℂ ↥hA.matrix_submodule) = NumOfEdges A

theorem Matrix.traceLinearMap_dualMatrix_eq {n : Type u_2} [DecidableEq n] [Fintype n] : Module.Dual.matrix (traceLinearMap n ℂ ℂ) = 1

theorem QuantumGraph.Real.of_norm_one_matrix_eq_of_norm_one_matrix_iff {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] {x y : { x : Matrix n n ℂ // ‖x‖ = 1 }} : of_norm_one_matrix x = of_norm_one_matrix y ↔ ∃ (α : ℂˣ), ↑x = ↑α • ↑y

theorem QuantumGraph.Real.reflexive_matrix_numOfEdges_eq_one_iff_eq_trivialGraph_of_counit_eq_trace {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] [Nontrivial n] (hc : CoalgebraStruct.counit = Matrix.traceLinearMap n ℂ ℂ) {A : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ} (hA : Real (Matrix n n ℂ) A) (hA₂ : A •ₛ 1 = 1) : NumOfEdges A = 1 ↔ A = Qam.trivialGraph (Matrix n n ℂ)

theorem counit_eq_traceLinearMap_of_counit_eq_piMat_traceLinearMap {ι : Type u_2} [DecidableEq ι] [Fintype ι] {p : ι → Type u_3} [(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) (i : ι) : CoalgebraStruct.counit = Matrix.traceLinearMap (p i) ℂ ℂ

theorem QuantumGraph.Real.PiMatFinTwo_same_isSelfAdjoint_reflexive_and_numOfEdges_eq_one {n : Type u_1} [Fintype n] [DecidableEq n] {φ : (i : Fin 2) → Module.Dual ℂ (Matrix (PiFinTwo_same n i) (PiFinTwo_same n i) ℂ)} [hφ : ∀ (i : Fin 2), (φ i).IsFaithfulPosMap] [Nontrivial n] {A : PiMat ℂ (Fin 2) (PiFinTwo_same n) →ₗ[ℂ] PiMat ℂ (Fin 2) (PiFinTwo_same n)} (hc : CoalgebraStruct.counit = PiMat.traceLinearMap) (hA : Real (PiMat ℂ (Fin 2) (PiFinTwo_same n)) A) (hA₂ : LinearMap.adjoint A = A) (hA₃ : A •ₛ 1 = 1) (hA₄ : NumOfEdges A = 1) : A = LinearMap.adjoint (LinearMap.proj 0) ∘ₗ Qam.trivialGraph (Mat ℂ (PiFinTwo_same n 0)) ∘ₗ LinearMap.proj 0 ∨ A = LinearMap.adjoint (LinearMap.proj 1) ∘ₗ Qam.trivialGraph (Mat ℂ (PiFinTwo_same n 1)) ∘ₗ LinearMap.proj 1

class QuantumGraph.equiv {A : Type u_2} {B : Type u_3} [starAlgebra A] [QuantumSet A] [starAlgebra B] [QuantumSet B] (x : A →ₗ[ℂ] A) (y : B →ₗ[ℂ] B) (f : A ≃⋆ₐ[ℂ] B) : Prop

• isIsometry : Isometry ⇑f
• prop : f.toLinearMap ∘ₗ x = y ∘ₗ f.toLinearMap

theorem QuantumGraph.equiv_prop {A : Type u_2} {B : Type u_3} [starAlgebra A] [QuantumSet A] [starAlgebra B] [QuantumSet B] (x : A →ₗ[ℂ] A) (y : B →ₗ[ℂ] B) {f : A ≃⋆ₐ[ℂ] B} (hf : equiv x y f) : f.toLinearMap ∘ₗ x = y ∘ₗ f.toLinearMap

theorem QuantumGraph.equiv_prop' {A : Type u_2} {B : Type u_3} [starAlgebra A] [QuantumSet A] [starAlgebra B] [QuantumSet B] (x : A →ₗ[ℂ] A) (y : B →ₗ[ℂ] B) {f : A ≃⋆ₐ[ℂ] B} (hf : equiv x y f) : f.toLinearMap ∘ₗ x ∘ₗ LinearMap.adjoint f.toLinearMap = y

theorem Pi.eq_sum_single_proj (R : Type u_2) {ι : Type u_3} [Semiring R] [Fintype ι] [DecidableEq ι] {φ : ι → Type u_4} [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (x : (i : ι) → φ i) : x = ∑ i : ι, single i (x i)

def PiMat_finTwo_same_swapStarAlgEquiv {n : Type u_2} [Fintype n] [DecidableEq n] : PiMat ℂ (Fin 2) (PiFinTwo_same n) ≃⋆ₐ[ℂ] PiMat ℂ (Fin 2) (PiFinTwo_same n)

Equations

• PiMat_finTwo_same_swapStarAlgEquiv = StarAlgEquiv.ofAlgEquiv PiMat_finTwo_same_swapAlgEquiv ⋯

theorem PiMat_finTwo_same_swapStarAlgEquiv_apply {n : Type u_2} [Fintype n] [DecidableEq n] (x : PiMat ℂ (Fin 2) (PiFinTwo_same n)) : PiMat_finTwo_same_swapStarAlgEquiv x = Pi.single 0 (x 1) + Pi.single 1 (x 0)

theorem PiMat_finTwo_same_swapStarAlgEquiv_toAlgEquiv {n : Type u_2} [Fintype n] [DecidableEq n] : PiMat_finTwo_same_swapStarAlgEquiv.toAlgEquiv = PiMat_finTwo_same_swapAlgEquiv

theorem PiMat_finTwo_same_swapStarAlgEquiv_symm {n : Type u_2} [Fintype n] [DecidableEq n] : PiMat_finTwo_same_swapStarAlgEquiv.symm = PiMat_finTwo_same_swapStarAlgEquiv

theorem PiMat_finTwo_same_swapStarAlgEquiv_isometry {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] : LinearMap.adjoint PiMat_finTwo_same_swapStarAlgEquiv.toLinearMap = PiMat_finTwo_same_swapStarAlgEquiv.symm.toLinearMap

theorem PiMat_finTwo_same_swapStarAlgEquiv_comp_linearMapSingle_zero {n : Type u_2} [Fintype n] [DecidableEq n] : PiMat_finTwo_same_swapStarAlgEquiv.toLinearMap ∘ₗ LinearMap.single ℂ (fun (j : Fin 2) => Mat ℂ (PiFinTwo_same n j)) 0 = LinearMap.single ℂ (fun (j : Fin 2) => Mat ℂ (PiFinTwo_same n j)) 1

theorem PiMat_finTwo_same_swapStarAlgEquiv_comp_linearMapSingle_one {n : Type u_2} [Fintype n] [DecidableEq n] : PiMat_finTwo_same_swapStarAlgEquiv.toLinearMap ∘ₗ LinearMap.single ℂ (fun (j : Fin 2) => Mat ℂ (PiFinTwo_same n j)) 1 = LinearMap.single ℂ (fun (j : Fin 2) => Mat ℂ (PiFinTwo_same n j)) 0

theorem PiMat_finTwo_same_proj_zero_comp_swapStarAlgEquiv {n : Type u_2} [Fintype n] [DecidableEq n] : LinearMap.proj 0 ∘ₗ PiMat_finTwo_same_swapStarAlgEquiv.toLinearMap = LinearMap.proj 1

theorem PiMat_finTwo_same_proj_one_comp_swapStarAlgEquiv {n : Type u_2} [Fintype n] [DecidableEq n] : LinearMap.proj 1 ∘ₗ PiMat_finTwo_same_swapStarAlgEquiv.toLinearMap = LinearMap.proj 0

theorem QuantumGraph.Real.piMatFinTwo_same_eq_zero_of_isSelfAdjoint_and_reflexive_and_numOfEdges_eq_one {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] [Nontrivial n] (hc : CoalgebraStruct.counit = PiMat.traceLinearMap) {A : PiMat ℂ (Fin 2) (PiFinTwo_same n) →ₗ[ℂ] PiMat ℂ (Fin 2) (PiFinTwo_same n)} (hA : Real (PiMat ℂ (Fin 2) (PiFinTwo_same n)) A) (hA₂ : LinearMap.adjoint A = A) (hA₃ : A •ₛ 1 = 1) (hA₄ : NumOfEdges A = 1) : A = 0