LeanPool.Monlib4.QuantumGraph.Matrix

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

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

Elaborate a matrix quantum-graph statement with its finite-dimensional coalgebra.

Equations

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

def «tacticWithMatrixCoalgebraQuantumCtx[_]» : Lean.ParserDescr

Introduce the matrix quantum-set and finite-dimensional coalgebra instances in a proof.

Equations

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

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.single_transpose {R : Type u_2} {n : Type u_3} {p : Type u_4} [DecidableEq n] [DecidableEq p] [Zero R] {i : n} {j : p} {α : R} : (single i j α).transpose = single j i α

theorem Module.Dual.IsFaithfulPosMap.inner_coord_onb {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]

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

Matrix transpose as a star-algebra equivalence to the opposite algebra.

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.matrixSubmodule {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 ℂ)

The submodule corresponding to a real matrix quantum graph.

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.matrixSubmodule = 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] (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} [Fintype ι] (u : OrthonormalBasis ι ℂ ↥hA.matrixSubmodule) : A = ∑ i : ι, lmul (↑(u i) * φ.matrix) * LinearMap.adjoint (rmul (φ.matrix * ↑(u i)))

theorem QuantumGraph.Real.matrixSubmodule_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.matrixSubmodule)) ℂ ↥hA.matrixSubmodule), A = ∑ i : Fin (Module.finrank ℂ ↥hA.matrixSubmodule), lmul (↑(u i) * φ.matrix) * LinearMap.adjoint (rmul (φ.matrix * ↑(u i)))

@[reducible, inline]

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

Rank-one real quantum graph generated by a norm-one matrix.

Equations

• QuantumGraph.Real.ofNormOneMatrix = fun (u : { x : Matrix n n ℂ // ‖x‖ = 1 }) => lmul (↑u * φ.matrix) * LinearMap.adjoint (rmul (φ.matrix * ↑u))

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.ofNormOneMatrix_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 }) : ofNormOneMatrix x •ₛ 1 = 0 ↔ (↑x).trace = 0

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

Normalize a nonzero vector to a unit vector.

Equations

• normalizeOfNeZero 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.ofNormOneMatrix_eq_trivialGraph {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] [Nontrivial n] : ofNormOneMatrix (normalizeOfNeZero ⋯) = Qam.trivialGraph (Matrix n n ℂ)

theorem QuantumGraph.Real.ofNormOneMatrix_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 }) : ofNormOneMatrix 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.matrixSubmodule_finrank_eq_numOfEdges_of_counit_eq_trace {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] : CoalgebraStruct.counit = Matrix.traceLinearMap n ℂ ℂ → ∀ {A : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ} (hA : Real (Matrix n n ℂ) A), ↑(Module.finrank ℂ ↥hA.matrixSubmodule) = NumOfEdges A

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

theorem QuantumGraph.Real.ofNormOneMatrix_eq_ofNormOneMatrix_iff {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] {x y : { x : Matrix n n ℂ // ‖x‖ = 1 }} : ofNormOneMatrix x = ofNormOneMatrix 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] : CoalgebraStruct.counit = Matrix.traceLinearMap n ℂ ℂ → ∀ {A : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ} (hA : Real (Matrix n n ℂ) A), 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] : CoalgebraStruct.counit = PiMat.traceLinearMap → ∀ (i : ι), CoalgebraStruct.counit = Matrix.traceLinearMap (p i) ℂ ℂ

theorem QuantumGraph.Real.numOfEdges_ne_one_of_isSelfAdjoint_and_reflexive {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Nontrivial ι] {p : ι → Type u_3} [(i : ι) → Fintype (p i)] [(i : ι) → DecidableEq (p i)] [∀ (i : ι), Nonempty (p i)] {φ : (i : ι) → Module.Dual ℂ (Matrix (p i) (p i) ℂ)} [hφ : ∀ (i : ι), (φ i).IsFaithfulPosMap] : CoalgebraStruct.counit = PiMat.traceLinearMap → ∀ {A : PiMat ℂ ι p →ₗ[ℂ] PiMat ℂ ι p} (hA : Real (PiMat ℂ ι p) A), LinearMap.adjoint A = A → A •ₛ 1 = 1 → NumOfEdges A ≠ 1

A reflexive self-adjoint quantum graph on at least two nonzero matrix blocks cannot have exactly one edge when the counit is the trace.

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 (PiFinTwoSame n i) (PiFinTwoSame n i) ℂ)} [hφ : ∀ (i : Fin 2), (φ i).IsFaithfulPosMap] [Nontrivial n] : CoalgebraStruct.counit = PiMat.traceLinearMap → ∀ {A : PiMat ℂ (Fin 2) (PiFinTwoSame n) →ₗ[ℂ] PiMat ℂ (Fin 2) (PiFinTwoSame n)} (hA : Real (PiMat ℂ (Fin 2) (PiFinTwoSame n)) A), LinearMap.adjoint A = A → A •ₛ 1 = 1 → NumOfEdges A = 1 → A = LinearMap.adjoint (LinearMap.proj 0) ∘ₗ Qam.trivialGraph (Mat ℂ (PiFinTwoSame n 0)) ∘ₗ LinearMap.proj 0 ∨ A = LinearMap.adjoint (LinearMap.proj 1) ∘ₗ Qam.trivialGraph (Mat ℂ (PiFinTwoSame 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

Isomorphism data between two quantum graphs via a star-algebra equivalence.

• isIsometry : Isometry ⇑f

  The equivalence is isometric.

• prop : f.toLinearMap ∘ₗ x = y ∘ₗ f.toLinearMap

  The equivalence intertwines the adjacency maps.

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)

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

Swap the two equal blocks of a Fin 2-indexed PiMat as a star-algebra equivalence.

Equations

• PiMatFinTwoSameSwapStarAlgEquiv = StarAlgEquiv.ofAlgEquiv PiMatFinTwoSameSwapAlgEquiv ⋯

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

theorem PiMatFinTwoSameSwapStarAlgEquiv_toAlgEquiv {n : Type u_2} [Fintype n] [DecidableEq n] : PiMatFinTwoSameSwapStarAlgEquiv.toAlgEquiv = PiMatFinTwoSameSwapAlgEquiv

theorem PiMatFinTwoSameSwapStarAlgEquiv_symm {n : Type u_2} [Fintype n] [DecidableEq n] : PiMatFinTwoSameSwapStarAlgEquiv.symm = PiMatFinTwoSameSwapStarAlgEquiv

@[reducible, inline]

abbrev PiFinTwoSameFunctional {n : Type u_2} (φ : Module.Dual ℂ (Matrix n n ℂ)) (i : Fin 2) : Module.Dual ℂ (Matrix (PiFinTwoSame n i) (PiFinTwoSame n i) ℂ)

The constant two-block functional used for two identical matrix summands.

Equations

• PiFinTwoSameFunctional φ x✝ = φ

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

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

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

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

theorem PiMat_finTwo_same_proj_one_comp_swapStarAlgEquiv {n : Type u_2} [Fintype n] [DecidableEq n] : LinearMap.proj 1 ∘ₗ PiMatFinTwoSameSwapStarAlgEquiv.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] : CoalgebraStruct.counit = PiMat.traceLinearMap → ∀ {A : PiMat ℂ (Fin 2) (PiFinTwoSame n) →ₗ[ℂ] PiMat ℂ (Fin 2) (PiFinTwoSame n)} (hA : Real (PiMat ℂ (Fin 2) (PiFinTwoSame n)) A), LinearMap.adjoint A = A → A •ₛ 1 = 1 → NumOfEdges A = 1 → A = 0