mathlib3 documentation

monlib / quantum_graph.iso

Isomorphisms between quantum graphs #

This file defines isomorphisms between quantum graphs.

theorem inner_aut_adjoint_eq_iff {n : Type u_2} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] [nontrivial n] (U : ↥(matrix.unitary_group n ℂ)) :

⇑linear_map.adjoint (matrix.inner_aut U) = matrix.inner_aut (has_star.star U) ↔ commute φ.matrix ⇑U

theorem qam.mul'_adjoint_commutes_with_inner_aut_lm {n : Type u_2} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] [nontrivial n] {x : ↥(matrix.unitary_group n ℂ)} (hx : commute φ.matrix ⇑x) :

(tensor_product.map (matrix.inner_aut x) (matrix.inner_aut x)).comp (⇑linear_map.adjoint (linear_map.mul' ℂ (matrix n n ℂ))) = (⇑linear_map.adjoint (linear_map.mul' ℂ (matrix n n ℂ))).comp (matrix.inner_aut x)

theorem qam.unit_commutes_with_inner_aut_lm {n : Type u_2} [fintype n] [decidable_eq n] (U : ↥(matrix.unitary_group n ℂ)) :

(matrix.inner_aut U).comp (algebra.linear_map ℂ (matrix n n ℂ)) = algebra.linear_map ℂ (matrix n n ℂ)

theorem qam.mul'_commutes_with_inner_aut_lm {n : Type u_2} [fintype n] [decidable_eq n] (x : ↥(matrix.unitary_group n ℂ)) :

(linear_map.mul' ℂ (matrix n n ℂ)).comp (tensor_product.map (matrix.inner_aut x) (matrix.inner_aut x)) = (matrix.inner_aut x).comp (linear_map.mul' ℂ (matrix n n ℂ))

theorem qam.unit_adjoint_commutes_with_inner_aut_lm {n : Type u_2} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] [nontrivial n] {U : ↥(matrix.unitary_group n ℂ)} (hU : commute φ.matrix ⇑U) :

(⇑linear_map.adjoint (algebra.linear_map ℂ (matrix n n ℂ))).comp (matrix.inner_aut U) = ⇑linear_map.adjoint (algebra.linear_map ℂ (matrix n n ℂ))

theorem inner_aut_is_real {n : Type u_2} [fintype n] [decidable_eq n] (U : ↥(matrix.unitary_group n ℂ)) :

(matrix.inner_aut U).is_real

def star_alg_equiv.is_isometry {n : Type u_2} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (f : matrix n n ℂ ≃⋆ₐ[ℂ ] matrix n n ℂ) :

Prop

Equations

f.is_isometry = ∀ (x : matrix n n ℂ), ‖⇑f x‖ = ‖x‖

theorem inner_aut.to_matrix {n : Type u_2} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (U : ↥(matrix.unitary_group n ℂ)) :

⇑(_.to_matrix) (matrix.inner_aut U) = matrix.kronecker_map has_mul.mul ⇑U (⇑(_.sig (-(1 / 2))) ⇑U).conj

theorem unitary_commutes_with_hφ_matrix_iff_is_isometry {n : Type u_2} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] [nontrivial n] (U : ↥(matrix.unitary_group n ℂ)) :

commute φ.matrix ⇑U ↔ (matrix.inner_aut_star_alg U).is_isometry

theorem qam.symm_apply_star_alg_equiv_conj {n : Type u_2} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] [nontrivial n] {f : matrix n n ℂ ≃⋆ₐ[ℂ ] matrix n n ℂ} (hf : f.is_isometry) (A : matrix n n ℂ →ₗ[ℂ ] matrix n n ℂ) :

⇑(linear_equiv.symm_map ℂ (matrix n n ℂ)) (f.to_alg_equiv.to_linear_map.comp (A.comp f.symm.to_alg_equiv.to_linear_map)) = f.to_alg_equiv.to_linear_map.comp ((⇑(linear_equiv.symm_map ℂ (matrix n n ℂ)) A).comp f.symm.to_alg_equiv.to_linear_map)

theorem inner_aut.symmetric_eq {n : Type u_2} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] [nontrivial n] (A : matrix n n ℂ →ₗ[ℂ ] matrix n n ℂ) {U : ↥(matrix.unitary_group n ℂ)} (hU : commute φ.matrix ⇑U) :

⇑(linear_equiv.symm_map ℂ (matrix n n ℂ)) ((matrix.inner_aut U).comp (A.comp (matrix.inner_aut (has_star.star U)))) = (matrix.inner_aut U).comp ((⇑(linear_equiv.symm_map ℂ (matrix n n ℂ)) A).comp (matrix.inner_aut (has_star.star U)))

theorem star_alg_equiv.commutes_with_mul' {n : Type u_2} [fintype n] [decidable_eq n] (f : matrix n n ℂ ≃⋆ₐ[ℂ ] matrix n n ℂ) :

(linear_map.mul' ℂ (matrix n n ℂ)).comp (tensor_product.map f.to_alg_equiv.to_linear_map f.to_alg_equiv.to_linear_map) = f.to_alg_equiv.to_linear_map.comp (linear_map.mul' ℂ (matrix n n ℂ))

theorem star_alg_equiv.is_isometry.commutes_with_mul'_adjoint {n : Type u_2} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] [nontrivial n] {f : matrix n n ℂ ≃⋆ₐ[ℂ ] matrix n n ℂ} (hf : f.is_isometry) :

theorem qam.refl_idempotent_star_alg_equiv_conj {n : Type u_2} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] [nontrivial n] {f : matrix n n ℂ ≃⋆ₐ[ℂ ] matrix n n ℂ} (hf : f.is_isometry) (A B : matrix n n ℂ →ₗ[ℂ ] matrix n n ℂ) :

⇑(⇑(qam.refl_idempotent _) (f.to_alg_equiv.to_linear_map.comp (A.comp f.symm.to_alg_equiv.to_linear_map))) (f.to_alg_equiv.to_linear_map.comp (B.comp f.symm.to_alg_equiv.to_linear_map)) = f.to_alg_equiv.to_linear_map.comp ((⇑(⇑(qam.refl_idempotent _) A) B).comp f.symm.to_alg_equiv.to_linear_map)

theorem inner_aut.refl_idempotent {n : Type u_2} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] [nontrivial n] {U : ↥(matrix.unitary_group n ℂ)} (hU : commute φ.matrix ⇑U) (A B : matrix n n ℂ →ₗ[ℂ ] matrix n n ℂ) :

⇑(⇑(qam.refl_idempotent _) ((matrix.inner_aut U).comp (A.comp (matrix.inner_aut (has_star.star U))))) ((matrix.inner_aut U).comp (B.comp (matrix.inner_aut (has_star.star U)))) = (matrix.inner_aut U).comp ((⇑(⇑(qam.refl_idempotent _) A) B).comp (matrix.inner_aut (has_star.star U)))

theorem qam_star_alg_equiv_conj_iff {n : Type u_2} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] [nontrivial n] {f : matrix n n ℂ ≃⋆ₐ[ℂ ] matrix n n ℂ} (hf : f.is_isometry) (A : matrix n n ℂ →ₗ[ℂ ] matrix n n ℂ) :

qam φ (f.to_alg_equiv.to_linear_map.comp (A.comp f.symm.to_alg_equiv.to_linear_map)) ↔ qam φ A

theorem qam_symm_star_alg_equiv_conj_iff {n : Type u_2} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] [nontrivial n] {f : matrix n n ℂ ≃⋆ₐ[ℂ ] matrix n n ℂ} (hf : f.is_isometry) (A : matrix n n ℂ →ₗ[ℂ ] matrix n n ℂ) :

qam.is_symm (f.to_alg_equiv.to_linear_map.comp (A.comp f.symm.to_alg_equiv.to_linear_map)) ↔ qam.is_symm A

theorem qam_is_self_adjoint_star_alg_equiv_conj_iff {n : Type u_2} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] [nontrivial n] {f : matrix n n ℂ ≃⋆ₐ[ℂ ] matrix n n ℂ} (hf : f.is_isometry) (A : matrix n n ℂ →ₗ[ℂ ] matrix n n ℂ) :

is_self_adjoint (f.to_alg_equiv.to_linear_map.comp (A.comp f.symm.to_alg_equiv.to_linear_map)) ↔ is_self_adjoint A

theorem qam_ir_reflexive_star_alg_equiv_conj {n : Type u_2} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] [nontrivial n] {f : matrix n n ℂ ≃⋆ₐ[ℂ ] matrix n n ℂ} (hf : f.is_isometry) (A : matrix n n ℂ →ₗ[ℂ ] matrix n n ℂ) :

⇑(⇑(qam.refl_idempotent _) (f.to_alg_equiv.to_linear_map.comp (A.comp f.symm.to_alg_equiv.to_linear_map))) 1 = f.to_alg_equiv.to_linear_map.comp ((⇑(⇑(qam.refl_idempotent _) A) 1).comp f.symm.to_alg_equiv.to_linear_map)

theorem qam_ir_reflexive'_star_alg_equiv_conj {n : Type u_2} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] [nontrivial n] {f : matrix n n ℂ ≃⋆ₐ[ℂ ] matrix n n ℂ} (hf : f.is_isometry) (A : matrix n n ℂ →ₗ[ℂ ] matrix n n ℂ) :

⇑(⇑(qam.refl_idempotent _) 1) (f.to_alg_equiv.to_linear_map.comp (A.comp f.symm.to_alg_equiv.to_linear_map)) = f.to_alg_equiv.to_linear_map.comp ((⇑(⇑(qam.refl_idempotent _) 1) A).comp f.symm.to_alg_equiv.to_linear_map)

theorem inner_aut.qam {n : Type u_2} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] [nontrivial n] {U : ↥(matrix.unitary_group n ℂ)} (hU : commute φ.matrix ⇑U) (A : matrix n n ℂ →ₗ[ℂ ] matrix n n ℂ) :

qam φ ((matrix.inner_aut U).comp (A.comp (matrix.inner_aut (has_star.star U)))) ↔ qam φ A

theorem inner_aut.ir_reflexive {n : Type u_2} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] [nontrivial n] {U : ↥(matrix.unitary_group n ℂ)} (hU : commute φ.matrix ⇑U) (A : matrix n n ℂ →ₗ[ℂ ] matrix n n ℂ) :

⇑(⇑(qam.refl_idempotent _) ((matrix.inner_aut U).comp (A.comp (matrix.inner_aut (has_star.star U))))) 1 = (matrix.inner_aut U).comp ((⇑(⇑(qam.refl_idempotent _) A) 1).comp (matrix.inner_aut (has_star.star U)))

theorem inner_aut.qam_is_reflexive {n : Type u_2} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] [nontrivial n] {U : ↥(matrix.unitary_group n ℂ)} (hU : commute φ.matrix ⇑U) {A : matrix n n ℂ →ₗ[ℂ ] matrix n n ℂ} :

qam_lm_nontracial_is_reflexive ((matrix.inner_aut U).comp (A.comp (matrix.inner_aut (has_star.star U)))) ↔ qam_lm_nontracial_is_reflexive A

theorem inner_aut.qam_is_irreflexive {n : Type u_2} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] [nontrivial n] {U : ↥(matrix.unitary_group n ℂ)} (hU : commute φ.matrix ⇑U) {A : matrix n n ℂ →ₗ[ℂ ] matrix n n ℂ} :

qam_lm_nontracial_is_unreflexive ((matrix.inner_aut U).comp (A.comp (matrix.inner_aut (has_star.star U)))) ↔ qam_lm_nontracial_is_unreflexive A

def qam.iso {n : Type u_2} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} (A B : matrix n n ℂ →ₗ[ℂ ] matrix n n ℂ) :

Prop

Equations

qam.iso A B = ∃ (f : matrix n n ℂ ≃⋆ₐ[ℂ ] matrix n n ℂ), A.comp f.to_alg_equiv.to_linear_map = f.to_alg_equiv.to_linear_map.comp B ∧ ⇑f φ.matrix = φ.matrix

structure qam_iso {n : Type u_2} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] {A B : matrix n n ℂ →ₗ[ℂ ] matrix n n ℂ} (hA : qam φ A) (hB : qam φ B) :

Type u_2

to_star_alg_equiv : matrix n n ℂ ≃⋆ₐ[ℂ ] matrix n n ℂ
is_hom : Prop
is_iso : Prop

Instances for qam_iso

qam_iso.has_sizeof_inst

theorem qam.iso_iff {n : Type u_2} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] {A B : matrix n n ℂ →ₗ[ℂ ] matrix n n ℂ} [nontrivial n] :

qam.iso A B ↔ ∃ (U : ↥(matrix.unitary_group n ℂ)), A.comp (matrix.inner_aut U) = (matrix.inner_aut U).comp B ∧ commute φ.matrix ⇑U

theorem qam.iso_preserves_spectrum {n : Type u_2} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} (A B : matrix n n ℂ →ₗ[ℂ ] matrix n n ℂ) (h : qam.iso A B) :

spectrum ℂ A = spectrum ℂ B

theorem inner_aut_lm_rank_one {n : Type u_2} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] [nontrivial n] {U : ↥(matrix.unitary_group n ℂ)} (hU : commute φ.matrix ⇑U) (x y : matrix n n ℂ) :

(matrix.inner_aut U).comp (↑(rank_one x y).comp (matrix.inner_aut (has_star.star U))) = ↑(rank_one (⇑(matrix.inner_aut U) x) (⇑(matrix.inner_aut U) y))

theorem inner_aut_lm_basis_apply {n : Type u_2} [fintype n] [decidable_eq n] (U : ↥(matrix.unitary_group n ℂ)) (i j k l : n) :

⇑(matrix.inner_aut U) (matrix.std_basis_matrix i j 1) k l = matrix.kronecker_map has_mul.mul ⇑U (has_star.star ⇑U) (k, j) (i, l)

theorem qam.rank_one_to_matrix_of_star_alg_equiv_coord {n : Type u_2} [fintype n] [decidable_eq n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] (x y : matrix n n ℂ) (i j k l : n) :

⇑(_.to_matrix) ↑(rank_one x y) (i, j) (k, l) = matrix.kronecker_map has_mul.mul (x.mul (_.rpow (1 / 2))) (y.mul (_.rpow (1 / 2))).conj (i, k) (j, l)