Quantum graphs as projections

This file contains the definition of a quantum graph as a projection, and the proof that the

def «termWithProjectionMatrixCoalgebraQuantum[_]_» : Lean.ParserDescr

Elaborate projection/QAM statements with the matrix coalgebra induced by φ.

Equations

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

def «tacticWithProjectionMatrixCoalgebraQuantumCtx[_]» : Lean.ParserDescr

Introduce the projection matrix coalgebra context induced by φ in a proof.

Equations

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

@[reducible, inline]

noncomputable abbrev FiniteDimensional.finrank (𝕜 : Type u_1) (E : Type u_2) [DivisionRing 𝕜] [AddCommGroup E] [Module 𝕜 E] : ℕ

Compatibility spelling for the old FiniteDimensional.finrank namespace.

Equations

• FiniteDimensional.finrank 𝕜 E = Module.finrank 𝕜 E

@[reducible, inline]

noncomputable abbrev Qam.reflIdempotent {p : Type u_1} [Fintype p] [DecidableEq p] {φ : Module.Dual ℂ (Matrix p p ℂ)} (hφ : φ.IsFaithfulPosMap) (A : Matrix p p ℂ →ₗ[ℂ] Matrix p p ℂ) : (Matrix p p ℂ →ₗ[ℂ] Matrix p p ℂ) →ₗ[ℂ] Matrix p p ℂ →ₗ[ℂ] Matrix p p ℂ

The reflexive idempotent product used in older Monlib quantum-graph files.

Equations

• Qam.reflIdempotent hφ A = schurMul A

theorem Qam.isReal_and_idempotent_iff_psi_orthogonal_projection {p : Type u_1} [Fintype p] [DecidableEq p] {φ : Module.Dual ℂ (Matrix p p ℂ)} (hφ : φ.IsFaithfulPosMap) (A : Matrix p p ℂ →ₗ[ℂ] Matrix p p ℂ) : (reflIdempotent hφ A) A = A ∧ LinearMap.IsReal A ↔ IsIdempotentElem ((hφ.psi 0 (1 / 2)) A) ∧ IsSelfAdjoint ((hφ.psi 0 (1 / 2)) A)

noncomputable def blockDiag'KroneckerEquiv {p : Type u_1} [Fintype p] [DecidableEq p] {n : p → Type u_2} [(i : p) → Fintype (n i)] [(i : p) → DecidableEq (n i)] {φ : (i : p) → Module.Dual ℂ (Matrix (n i) (n i) ℂ)} (hφ : ∀ (i : p), (φ i).IsFaithfulPosMap) : Matrix ((i : p) × n i × n i) ((i : p) × n i × n i) ℂ ≃ₗ[ℂ] TensorProduct ℂ { x : Matrix ((i : p) × n i) ((i : p) × n i) ℂ // x.IsBlockDiagonal } { x : Matrix ((i : p) × n i) ((i : p) × n i) ℂ // x.IsBlockDiagonal }

Linear equivalence from block-diagonal matrix coordinates to the tensor product of block-diagonal matrices.

Equations

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

theorem Matrix.conj_conjTranspose' {R : Type u_1} {n₁ : Type u_2} {n₂ : Type u_3} [InvolutiveStar R] (A : Matrix n₁ n₂ R) : A.conj.conjTranspose = A.transpose

theorem toMatrix_mulLeft_mulRight_adjoint {p : Type u_2} [Fintype p] [DecidableEq p] {n : p → Type u_1} [(i : p) → Fintype (n i)] [(i : p) → DecidableEq (n i)] {φ : (i : p) → Module.Dual ℂ (Matrix (n i) (n i) ℂ)} (hφ : ∀ (i : p), (φ i).IsFaithfulPosMap) (x y : (i : p) → Matrix (n i) (n i) ℂ) : (Module.Dual.pi.IsFaithfulPosMap.toMatrix ⋯) (LinearMap.mulLeft ℂ x * LinearMap.adjoint (LinearMap.mulRight ℂ y)) = Matrix.blockDiagonal' fun (i : p) => Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (x i) ((⋯.sig (1 / 2)) (y i)).conj

def Pi.LinearMap.apply {ι₁ : Type u_1} {ι₂ : Type u_2} {E₁ : ι₁ → Type u_3} [DecidableEq ι₁] [(i : ι₁) → AddCommMonoid (E₁ i)] [(i : ι₁) → Module ℂ (E₁ i)] {E₂ : ι₂ → Type u_4} [(i : ι₂) → AddCommMonoid (E₂ i)] [(i : ι₂) → Module ℂ (E₂ i)] (i : ι₁) (j : ι₂) : (((a : ι₁) → E₁ a) →ₗ[ℂ] (a : ι₂) → E₂ a) →ₗ[ℂ] E₁ i →ₗ[ℂ] E₂ j

Apply a linear map between dependent products to a selected input and output component.

Equations

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

@[simp]

theorem Pi.LinearMap.apply_apply_apply {ι₁ : Type u_1} {ι₂ : Type u_2} {E₁ : ι₁ → Type u_3} [DecidableEq ι₁] [(i : ι₁) → AddCommMonoid (E₁ i)] [(i : ι₁) → Module ℂ (E₁ i)] {E₂ : ι₂ → Type u_4} [(i : ι₂) → AddCommMonoid (E₂ i)] [(i : ι₂) → Module ℂ (E₂ i)] (i : ι₁) (j : ι₂) (x : ((a : ι₁) → E₁ a) →ₗ[ℂ] (a : ι₂) → E₂ a) (a : E₁ i) : ((apply i j) x) a = x ((LinearMap.single ℂ E₁ i) a) j

theorem rankOne_psi_transpose_to_lin {n : Type u_1} [DecidableEq n] [Fintype n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (x y : Matrix n n ℂ) : hφ.toMatrix.symm (TensorProduct.toKronecker ((TensorProduct.map 1 (Matrix.transposeAlgEquiv n ℂ ℂ).symm.toLinearMap) ((hφ.psi 0 (1 / 2)) ↑(((rankOne ℂ) x) y)))) = LinearMap.mulLeft ℂ x * LinearMap.adjoint (LinearMap.mulRight ℂ y)

theorem rankOne_toMatrix_transpose_psi_symm {p : Type u_1} [Fintype p] [DecidableEq p] {φ : Module.Dual ℂ (Matrix p p ℂ)} [hφ : φ.IsFaithfulPosMap] (x y : Matrix p p ℂ) : (hφ.psi 0 (1 / 2)).symm ((TensorProduct.map 1 (Matrix.transposeAlgEquiv p ℂ ℂ).toLinearMap) (Matrix.kroneckerToTensorProduct (hφ.toMatrix ↑(((rankOne ℂ) x) y)))) = LinearMap.mulLeft ℂ (x * φ.matrix) * LinearMap.adjoint (LinearMap.mulRight ℂ (φ.matrix * y))

theorem orthogonal_projection_iff_lm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] {p : E →ₗ[𝕜] E} : (∃ (U : Submodule 𝕜 E), ↑(orthogonalProjection' U) = p) ↔ IsSelfAdjoint p ∧ IsIdempotentElem p

theorem Matrix.conj_eq_transpose_conjTranspose {R : Type u_1} {n₁ : Type u_2} {n₂ : Type u_3} [Star R] (A : Matrix n₁ n₂ R) : A.conj = A.transpose.conjTranspose

theorem Matrix.conj_eq_conjTranspose_transpose {R : Type u_1} {n₁ : Type u_2} {n₂ : Type u_3} [Star R] (A : Matrix n₁ n₂ R) : A.conj = A.conjTranspose.transpose

theorem Matrix.star_transpose_eq_star_transpose {R : Type u_1} {n : Type u_2} [Star R] (A : Matrix n n R) : (star A).transpose = star A.transpose

noncomputable def oneMapTranspose {p : Type u_1} [Fintype p] [DecidableEq p] : TensorProduct ℂ (Matrix p p ℂ) (Matrix p p ℂ)ᵐᵒᵖ ≃⋆ₐ[ℂ] Matrix (p × p) (p × p) ℂ

Star algebra equivalence between a matrix tensor product and matrices on product indices.

Equations

• oneMapTranspose = StarAlgEquiv.ofAlgEquiv ((AlgEquiv.TensorProduct.map 1 (Matrix.transposeAlgEquiv p ℂ ℂ).symm).trans tensorToKronecker) ⋯

theorem oneMapTranspose_eq {p : Type u_1} [Fintype p] [DecidableEq p] (x : TensorProduct ℂ (Matrix p p ℂ) (Matrix p p ℂ)ᵐᵒᵖ) : oneMapTranspose x = TensorProduct.toKronecker ((TensorProduct.map 1 (Matrix.transposeAlgEquiv p ℂ ℂ).symm.toLinearMap) x)

theorem oneMapTranspose_symm_eq {p : Type u_1} [Fintype p] [DecidableEq p] (x : Matrix (p × p) (p × p) ℂ) : oneMapTranspose.symm x = (TensorProduct.map 1 (Matrix.transposeAlgEquiv p ℂ ℂ).toLinearMap) (Matrix.kroneckerToTensorProduct x)

theorem oneMapTranspose_apply {p : Type u_1} [Fintype p] [DecidableEq p] (x y : Matrix p p ℂ) : oneMapTranspose (x ⊗ₜ[ℂ] MulOpposite.op y) = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) x y.transpose

theorem toMatrix''_map_star {p : Type u_1} [Fintype p] [DecidableEq p] {φ : Module.Dual ℂ (Matrix p p ℂ)} [hφ : φ.IsFaithfulPosMap] (x : Matrix p p ℂ →ₗ[ℂ] Matrix p p ℂ) : hφ.toMatrix (LinearMap.adjoint x) = star (hφ.toMatrix x)

theorem toMatrix''_symm_map_star {p : Type u_1} [Fintype p] [DecidableEq p] {φ : Module.Dual ℂ (Matrix p p ℂ)} [hφ : φ.IsFaithfulPosMap] (x : Matrix (p × p) (p × p) ℂ) : hφ.toMatrix.symm (star x) = LinearMap.adjoint (hφ.toMatrix.symm x)

noncomputable def Qam.fdOrthogonalProjection {p : Type u_1} [Fintype p] [DecidableEq p] {φ : Module.Dual ℂ (Matrix p p ℂ)} [hφ : φ.IsFaithfulPosMap] (U : Submodule ℂ (Matrix p p ℂ)) : Matrix p p ℂ →ₗ[ℂ] Matrix p p ℂ

The orthogonal projection onto a submodule, using the finite-dimensional matrix context.

Equations

• Qam.fdOrthogonalProjection U = ↑(orthogonalProjection' U)

theorem Qam.fd_orthogonal_projection_iff_lm {p : Type u_1} [Fintype p] [DecidableEq p] {φ : Module.Dual ℂ (Matrix p p ℂ)} [hφ : φ.IsFaithfulPosMap] {q : Matrix p p ℂ →ₗ[ℂ] Matrix p p ℂ} : (∃ (U : Submodule ℂ (Matrix p p ℂ)), fdOrthogonalProjection U = q) ↔ IsSelfAdjoint q ∧ IsIdempotentElem q

theorem Qam.fdOrthogonalProjection_eq_sum_rankOne {p : Type u_1} [Fintype p] [DecidableEq p] {φ : Module.Dual ℂ (Matrix p p ℂ)} [hφ : φ.IsFaithfulPosMap] {ι : Type u_2} [Fintype ι] {U : Submodule ℂ (Matrix p p ℂ)} (b : OrthonormalBasis ι ℂ ↥U) : fdOrthogonalProjection U = ∑ i : ι, ↑(((rankOne ℂ) ↑(b i)) ↑(b i))

theorem Qam.idempotent_and_real_iff_exists_ortho_proj {p : Type u_1} [Fintype p] [DecidableEq p] {φ : Module.Dual ℂ (Matrix p p ℂ)} [hφ : φ.IsFaithfulPosMap] (A : Matrix p p ℂ →ₗ[ℂ] Matrix p p ℂ) : (reflIdempotent hφ A) A = A ∧ LinearMap.IsReal A ↔ ∃ (U : Submodule ℂ (Matrix p p ℂ)), fdOrthogonalProjection U = hφ.toMatrix.symm (TensorProduct.toKronecker ((TensorProduct.map 1 (Matrix.transposeAlgEquiv p ℂ ℂ).symm.toLinearMap) ((hφ.psi 0 (1 / 2)) A)))

noncomputable def Qam.submoduleOfIdempotentAndReal {p : Type u_1} [Fintype p] [DecidableEq p] {φ : Module.Dual ℂ (Matrix p p ℂ)} [hφ : φ.IsFaithfulPosMap] {A : Matrix p p ℂ →ₗ[ℂ] Matrix p p ℂ} (hA1 : (reflIdempotent hφ A) A = A) (hA2 : LinearMap.IsReal A) : Submodule ℂ (Matrix p p ℂ)

The submodule associated to an idempotent real quantum adjacency map.

Equations

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

theorem Qam.orthogonalProjection'_eq {p : Type u_1} [Fintype p] [DecidableEq p] {φ : Module.Dual ℂ (Matrix p p ℂ)} [hφ : φ.IsFaithfulPosMap] {A : Matrix p p ℂ →ₗ[ℂ] Matrix p p ℂ} (hA1 : (reflIdempotent hφ A) A = A) (hA2 : LinearMap.IsReal A) : fdOrthogonalProjection (submoduleOfIdempotentAndReal hA1 hA2) = hφ.toMatrix.symm (TensorProduct.toKronecker ((TensorProduct.map 1 (Matrix.transposeAlgEquiv p ℂ ℂ).symm.toLinearMap) ((hφ.psi 0 (1 / 2)) A)))

noncomputable def Qam.onbOfIdempotentAndReal {p : Type u_1} [Fintype p] [DecidableEq p] {φ : Module.Dual ℂ (Matrix p p ℂ)} [hφ : φ.IsFaithfulPosMap] {A : Matrix p p ℂ →ₗ[ℂ] Matrix p p ℂ} (hA1 : (reflIdempotent hφ A) A = A) (hA2 : LinearMap.IsReal A) : OrthonormalBasis (Fin (FiniteDimensional.finrank ℂ ↥(submoduleOfIdempotentAndReal hA1 hA2))) ℂ ↥(submoduleOfIdempotentAndReal hA1 hA2)

A canonical orthonormal basis for the submodule associated to an idempotent real QAM.

Equations

• Qam.onbOfIdempotentAndReal hA1 hA2 = stdOrthonormalBasis ℂ ↥(Qam.submoduleOfIdempotentAndReal hA1 hA2)

theorem Qam.IdempotentAndReal.eq {p : Type u_1} [Fintype p] [DecidableEq p] {φ : Module.Dual ℂ (Matrix p p ℂ)} [hφ : φ.IsFaithfulPosMap] {A : Matrix p p ℂ →ₗ[ℂ] Matrix p p ℂ} (hA1 : (reflIdempotent hφ A) A = A) (hA2 : LinearMap.IsReal A) : A = ∑ i : Fin (FiniteDimensional.finrank ℂ ↥(submoduleOfIdempotentAndReal hA1 hA2)), LinearMap.mulLeft ℂ (↑((onbOfIdempotentAndReal hA1 hA2) i) * φ.matrix) * LinearMap.adjoint (LinearMap.mulRight ℂ (φ.matrix * ↑((onbOfIdempotentAndReal hA1 hA2) i)))

class RealQam {p : Type u_1} [Fintype p] [DecidableEq p] {φ : Module.Dual ℂ (Matrix p p ℂ)} (hφ : φ.IsFaithfulPosMap) (A : Matrix p p ℂ →ₗ[ℂ] Matrix p p ℂ) : Prop

Quantum adjacency maps that are both Schur-idempotent and real.

• toIdempotent : (Qam.reflIdempotent hφ A) A = A

  The Schur idempotence condition.

• toIsReal : LinearMap.IsReal A

  The realness condition.

theorem RealQam_iff {p : Type u_1} [Fintype p] [DecidableEq p] {φ : Module.Dual ℂ (Matrix p p ℂ)} [hφ : φ.IsFaithfulPosMap] {A : Matrix p p ℂ →ₗ[ℂ] Matrix p p ℂ} : RealQam hφ A ↔ (Qam.reflIdempotent hφ A) A = A ∧ LinearMap.IsReal A

theorem RealQam.add_iff {p : Type u_1} [Fintype p] [DecidableEq p] {φ : Module.Dual ℂ (Matrix p p ℂ)} [hφ : φ.IsFaithfulPosMap] {A B : Matrix p p ℂ →ₗ[ℂ] Matrix p p ℂ} (hA : RealQam hφ A) (hB : RealQam hφ B) : RealQam hφ (A + B) ↔ (Qam.reflIdempotent hφ A) B + (Qam.reflIdempotent hφ B) A = 0

theorem RealQam.zero {p : Type u_1} [Fintype p] [DecidableEq p] {φ : Module.Dual ℂ (Matrix p p ℂ)} [hφ : φ.IsFaithfulPosMap] : RealQam hφ 0

The zero map as a real QAM.

@[reducible]

noncomputable instance RealQam.hasZero {p : Type u_1} [Fintype p] [DecidableEq p] {φ : Module.Dual ℂ (Matrix p p ℂ)} [hφ : φ.IsFaithfulPosMap] : Zero { x : Matrix p p ℂ →ₗ[ℂ] Matrix p p ℂ // RealQam hφ x }

Equations

• RealQam.hasZero = { zero := ⟨0, ⋯⟩ }

theorem Qam.reflIdempotent_zero {p : Type u_1} [Fintype p] [DecidableEq p] {φ : Module.Dual ℂ (Matrix p p ℂ)} [hφ : φ.IsFaithfulPosMap] (a : Matrix p p ℂ →ₗ[ℂ] Matrix p p ℂ) : (reflIdempotent hφ a) 0 = 0

theorem Qam.zero_reflIdempotent {p : Type u_1} [Fintype p] [DecidableEq p] {φ : Module.Dual ℂ (Matrix p p ℂ)} [hφ : φ.IsFaithfulPosMap] (a : Matrix p p ℂ →ₗ[ℂ] Matrix p p ℂ) : (reflIdempotent hφ 0) a = 0

@[reducible]

noncomputable def RealQam.edges {p : Type u_1} [Fintype p] [DecidableEq p] {φ : Module.Dual ℂ (Matrix p p ℂ)} [hφ : φ.IsFaithfulPosMap] {x : Matrix p p ℂ →ₗ[ℂ] Matrix p p ℂ} (hx : RealQam hφ x) : ℕ

Number of edges of a real QAM, computed as the rank of its associated submodule.

Equations

• hx.edges = FiniteDimensional.finrank ℂ ↥(Qam.submoduleOfIdempotentAndReal ⋯ ⋯)

@[reducible]

noncomputable def RealQam.edges' {p : Type u_1} [Fintype p] [DecidableEq p] {φ : Module.Dual ℂ (Matrix p p ℂ)} [hφ : φ.IsFaithfulPosMap] : { x : Matrix p p ℂ →ₗ[ℂ] Matrix p p ℂ // RealQam hφ x } → ℕ

Edge-count function on the subtype of real QAMs.

Equations

• RealQam.edges' x = FiniteDimensional.finrank ℂ ↥(Qam.submoduleOfIdempotentAndReal ⋯ ⋯)

theorem RealQam.edges_eq {p : Type u_1} [Fintype p] [DecidableEq p] {φ : Module.Dual ℂ (Matrix p p ℂ)} [hφ : φ.IsFaithfulPosMap] {A : Matrix p p ℂ →ₗ[ℂ] Matrix p p ℂ} (hA : RealQam hφ A) : ↑hA.edges = (A φ.matrix⁻¹).trace

theorem completeGraphRealQam {p : Type u_1} [Fintype p] [DecidableEq p] {φ : Module.Dual ℂ (Matrix p p ℂ)} [hφ : φ.IsFaithfulPosMap] : RealQam hφ (Qam.completeGraph (Matrix p p ℂ) (Matrix p p ℂ))

theorem Qam.completeGraph_edges {p : Type u_1} [Fintype p] [DecidableEq p] {φ : Module.Dual ℂ (Matrix p p ℂ)} [hφ : φ.IsFaithfulPosMap] : ⋯.edges = FiniteDimensional.finrank ℂ ↥⊤

theorem Qam.trivialGraphRealQam {p : Type u_1} [Fintype p] [DecidableEq p] {φ : Module.Dual ℂ (Matrix p p ℂ)} [hφ : φ.IsFaithfulPosMap] [Nonempty p] : RealQam hφ (trivialGraph (Matrix p p ℂ))

theorem Qam.trivialGraph_edges {p : Type u_1} [Fintype p] [DecidableEq p] {φ : Module.Dual ℂ (Matrix p p ℂ)} [hφ : φ.IsFaithfulPosMap] [Nonempty p] : ⋯.edges = 1

theorem RealQam.edges_eq_zero_iff {p : Type u_1} [Fintype p] [DecidableEq p] {φ : Module.Dual ℂ (Matrix p p ℂ)} [hφ : φ.IsFaithfulPosMap] {A : Matrix p p ℂ →ₗ[ℂ] Matrix p p ℂ} (hA : RealQam hφ A) : hA.edges = 0 ↔ A = 0

theorem psi_apply_complete_graph {p : Type u_1} [Fintype p] [DecidableEq p] {φ : Module.Dual ℂ (Matrix p p ℂ)} [hφ : φ.IsFaithfulPosMap] {t s : ℝ} : (hφ.psi t s) ↑(((rankOne ℂ) 1) 1) = 1

theorem AlgEquiv.TensorProduct.map_toLinearMap' {R : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} {V : Type u_5} [CommSemiring R] [Semiring S] [Semiring T] [Semiring U] [Semiring V] [Algebra R S] [Algebra R T] [Algebra R U] [Algebra R V] (f : S ≃ₐ[R] T) (g : U ≃ₐ[R] V) : (map f g).toLinearMap = _root_.TensorProduct.map f.toLinearMap g.toLinearMap

theorem AlgEquiv.toLinearMap_one {R : Type u_1} {S : Type u_2} [CommSemiring R] [Semiring S] [Algebra R S] : toLinearMap 1 = 1

theorem RealQam.edges_eq_dim_iff {p : Type u_1} [Fintype p] [DecidableEq p] {φ : Module.Dual ℂ (Matrix p p ℂ)} [hφ : φ.IsFaithfulPosMap] {A : Matrix p p ℂ →ₗ[ℂ] Matrix p p ℂ} (hA : RealQam hφ A) : hA.edges = FiniteDimensional.finrank ℂ ↥⊤ ↔ A = ↑(((rankOne ℂ) 1) 1)

theorem Complex.ofReal'_eq_isROrC_ofReal (a : ℝ) : ↑a = ↑a

theorem RealQam.edges_eq_one_iff {p : Type u_1} [Fintype p] [DecidableEq p] {φ : Module.Dual ℂ (Matrix p p ℂ)} [hφ : φ.IsFaithfulPosMap] {A : Matrix p p ℂ →ₗ[ℂ] Matrix p p ℂ} (hA : RealQam hφ A) : hA.edges = 1 ↔ ∃ (x : { x : Matrix p p ℂ // x ≠ 0 }), A = (1 / ↑‖↑x‖ ^ 2) • (LinearMap.mulLeft ℂ (↑x * φ.matrix) * LinearMap.adjoint (LinearMap.mulRight ℂ (φ.matrix * ↑x)))