Isomorphisms between quantum graphs

This file defines isomorphisms between quantum graphs.

theorem innerAut_adjoint_eq_iff {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] [Nontrivial n] (U : ↥(Matrix.unitaryGroup n ℂ)) : LinearMap.adjoint (Matrix.innerAut U) = Matrix.innerAut (star U) ↔ Commute φ.matrix ↑U

theorem Qam.mul'_adjoint_commutes_with_innerAut_lm {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] [Nontrivial n] {x : ↥(Matrix.unitaryGroup n ℂ)} (hx : Commute φ.matrix ↑x) : TensorProduct.map (Matrix.innerAut x) (Matrix.innerAut x) ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ Matrix.innerAut x

theorem Qam.unit_commutes_with_innerAut_lm {n : Type u_1} [Fintype n] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n ℂ)) : Matrix.innerAut U ∘ₗ Algebra.linearMap ℂ (Matrix n n ℂ) = Algebra.linearMap ℂ (Matrix n n ℂ)

theorem Qam.mul'_commutes_with_innerAut_lm {n : Type u_1} [Fintype n] [DecidableEq n] (x : ↥(Matrix.unitaryGroup n ℂ)) : LinearMap.mul' ℂ (Matrix n n ℂ) ∘ₗ TensorProduct.map (Matrix.innerAut x) (Matrix.innerAut x) = Matrix.innerAut x ∘ₗ LinearMap.mul' ℂ (Matrix n n ℂ)

theorem Qam.unit_adjoint_commutes_with_innerAut_lm {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] [Nontrivial n] {U : ↥(Matrix.unitaryGroup n ℂ)} (hU : Commute φ.matrix ↑U) : CoalgebraStruct.counit ∘ₗ Matrix.innerAut U = CoalgebraStruct.counit

theorem innerAutIsReal {n : Type u_1} [Fintype n] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n ℂ)) : LinearMap.IsReal (Matrix.innerAut U)

@[reducible]

def StarAlgEquiv.IsIsometry {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (f : α → β) : Prop

Alias of Isometry.

---

An isometry (also known as isometric embedding) is a map preserving the edistance between pseudoemetric spaces, or equivalently the distance between pseudometric space.

Equations

• @StarAlgEquiv.IsIsometry = @Isometry

theorem InnerAut.toMatrix {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (U : ↥(Matrix.unitaryGroup n ℂ)) : hφ.toMatrix (Matrix.innerAut U) = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (↑U) ((modAut (-(1 / 2))) ↑U).conj

theorem unitary_commutes_with_hφ_matrix_iff_isIsometry {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} (hφ : φ.IsFaithfulPosMap) [Nontrivial n] (U : ↥(Matrix.unitaryGroup n ℂ)) : Commute φ.matrix ↑U ↔ StarAlgEquiv.IsIsometry ⇑(Matrix.innerAutStarAlg U)

theorem Qam.symm_apply_starAlgEquiv_conj {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] [Nontrivial n] {f : Matrix n n ℂ ≃⋆ₐ[ℂ] Matrix n n ℂ} (hf : StarAlgEquiv.IsIsometry ⇑f) (A : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ) : (symmMap ℂ (Matrix n n ℂ) (Matrix n n ℂ)) (f.toLinearMap ∘ₗ A ∘ₗ f.symm.toLinearMap) = f.toLinearMap ∘ₗ (symmMap ℂ (Matrix n n ℂ) (Matrix n n ℂ)) A ∘ₗ f.symm.toLinearMap

theorem InnerAut.symmetric_eq {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] [Nontrivial n] (A : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ) {U : ↥(Matrix.unitaryGroup n ℂ)} (hU : Commute φ.matrix ↑U) : (symmMap ℂ (Matrix n n ℂ) (Matrix n n ℂ)) (Matrix.innerAut U ∘ₗ A ∘ₗ Matrix.innerAut (star U)) = Matrix.innerAut U ∘ₗ (symmMap ℂ (Matrix n n ℂ) (Matrix n n ℂ)) A ∘ₗ Matrix.innerAut (star U)

theorem StarAlgEquiv.commutes_with_mul' {n : Type u_1} [Fintype n] (f : Matrix n n ℂ ≃⋆ₐ[ℂ] Matrix n n ℂ) : LinearMap.mul' ℂ (Matrix n n ℂ) ∘ₗ _root_.TensorProduct.map f.toLinearMap f.toLinearMap = f.toLinearMap ∘ₗ LinearMap.mul' ℂ (Matrix n n ℂ)

theorem StarAlgEquiv.IsIsometry.commutes_with_mul'_adjoint {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] [Nontrivial n] {f : Matrix n n ℂ ≃⋆ₐ[ℂ] Matrix n n ℂ} (hf : IsIsometry ⇑f) : _root_.TensorProduct.map f.toLinearMap f.toLinearMap ∘ₗ LinearMap.adjoint (LinearMap.mul' ℂ (Matrix n n ℂ)) = LinearMap.adjoint (LinearMap.mul' ℂ (Matrix n n ℂ)) ∘ₗ f.toLinearMap

theorem Qam.reflIdempotent_starAlgEquiv_conj {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] [Nontrivial n] {f : Matrix n n ℂ ≃⋆ₐ[ℂ] Matrix n n ℂ} (hf : StarAlgEquiv.IsIsometry ⇑f) (A B : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ) : (f.toLinearMap ∘ₗ A ∘ₗ f.symm.toLinearMap) •ₛ f.toLinearMap ∘ₗ B ∘ₗ f.symm.toLinearMap = f.toLinearMap ∘ₗ (A •ₛ B) ∘ₗ f.symm.toLinearMap

theorem InnerAut.reflIdempotent {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] [Nontrivial n] {U : ↥(Matrix.unitaryGroup n ℂ)} (hU : Commute φ.matrix ↑U) (A B : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ) : (Matrix.innerAut U ∘ₗ A ∘ₗ Matrix.innerAut (star U)) •ₛ Matrix.innerAut U ∘ₗ B ∘ₗ Matrix.innerAut (star U) = Matrix.innerAut U ∘ₗ (A •ₛ B) ∘ₗ Matrix.innerAut (star U)

def Qam.Iso {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} (A B : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ) : Prop

Isomorphism relation between two matrix quantum adjacency maps.

Equations

• Qam.Iso A B = ∃ (f : Matrix n n ℂ ≃⋆ₐ[ℂ] Matrix n n ℂ), A ∘ₗ f.toLinearMap = f.toLinearMap ∘ₗ B ∧ f φ.matrix = φ.matrix

theorem Qam.iso_iff {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] {A B : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ} [Nontrivial n] : Iso A B ↔ ∃ (U : ↥(Matrix.unitaryGroup n ℂ)), A ∘ₗ Matrix.innerAut U = Matrix.innerAut U ∘ₗ B ∧ Commute φ.matrix ↑U

theorem Qam.iso_preserves_spectrum {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} (A B : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ) (h : Iso A B) : spectrum ℂ A = spectrum ℂ B

theorem innerAut_lm_rankOne {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] [Nontrivial n] {U : ↥(Matrix.unitaryGroup n ℂ)} (hU : Commute φ.matrix ↑U) (x y : Matrix n n ℂ) : Matrix.innerAut U ∘ₗ ↑(((rankOne ℂ) x) y) ∘ₗ Matrix.innerAut (star U) = ↑(((rankOne ℂ) ((Matrix.innerAut U) x)) ((Matrix.innerAut U) y))

theorem innerAut_lm_basis_apply {n : Type u_1} [Fintype n] [DecidableEq n] (U : ↥(Matrix.unitaryGroup n ℂ)) (i j k l : n) : (Matrix.innerAut U) (Matrix.stdBasisMatrix i j 1) k l = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (↑U) (star ↑U) (k, j) (i, l)

theorem Module.Dual.IsFaithfulPosMap.basis_eq_onb_toBasis {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] : hφ.basis = hφ.orthonormalBasis.toBasis

theorem Qam.rankOne_toMatrix_of_star_algEquiv_coord {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (x y : Matrix n n ℂ) (i j k l : n) : hφ.toMatrix ↑(((rankOne ℂ) x) y) (i, j) (k, l) = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (x * ⋯.rpow (1 / 2)) (y * ⋯.rpow (1 / 2)).conj (i, k) (j, l)