Quantum graphs: quantum adjacency matrices #
This file defines the quantum adjacency matrix of a quantum graph.
noncomputable
def
qam.refl_idempotent
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
(hφ : φ.is_faithful_pos_map) :
Equations
- qam.refl_idempotent hφ = let _inst : fact φ.is_faithful_pos_map := _ in schur_idempotent
theorem
qam.rank_one.refl_idempotent_eq
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(a b c d : matrix n n ℂ) :
theorem
finset.sum_fin_one
{α : Type u_1}
[add_comm_monoid α]
(f : fin 1 → α) :
finset.univ.sum (λ (i : fin 1), f i) = f 0
theorem
rank_one_real_apply
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(a b : matrix n n ℂ) :
↑(rank_one a b).real = ↑(rank_one a.conj_transpose (⇑(_.sig (-1)) b.conj_transpose))
theorem
qam.rank_one.symmetric_eq
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(a b : matrix n n ℂ) :
⇑(linear_equiv.symm_map ℂ (matrix n n ℂ)) ↑(rank_one a b) = ↑(rank_one (⇑(_.sig (-1)) b.conj_transpose) a.conj_transpose)
theorem
qam.rank_one.symmetric'_eq
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(a b : matrix n n ℂ) :
⇑((linear_equiv.symm_map ℂ (matrix n n ℂ)).symm) ↑(rank_one a b) = ↑(rank_one b.conj_transpose (⇑(_.sig (-1)) a.conj_transpose))
theorem
qam.symm_adjoint_eq_symm'_of_adjoint
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(x : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) :
⇑linear_map.adjoint (⇑(linear_equiv.symm_map ℂ (matrix n n ℂ)) x) = ⇑((linear_equiv.symm_map ℂ (matrix n n ℂ)).symm) (⇑linear_map.adjoint x)
theorem
linear_map.adjoint_real_eq
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(f : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) :
(⇑linear_map.adjoint f).real = (_.sig 1).to_linear_map.comp ((⇑linear_map.adjoint f.real).comp (_.sig (-1)).to_linear_map)
theorem
module.dual.is_faithful_pos_map.sig_trans_sig
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(x y : ℝ) :
theorem
module.dual.is_faithful_pos_map.sig_comp_sig
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(x y : ℝ) :
(_.sig x).to_linear_map.comp (_.sig y).to_linear_map = (_.sig (x + y)).to_linear_map
theorem
module.dual.is_faithful_pos_map.sig_zero'
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map] :
theorem
linear_map.is_real.adjoint_is_real_iff_commute_with_sig
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
{f : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ}
(hf : f.is_real) :
(⇑linear_map.adjoint f).is_real ↔ commute f (_.sig 1).to_linear_map
theorem
sig_apply_pos_def_matrix_mul'
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(x : matrix n n ℂ) :
theorem
sig_apply_matrix_mul_pos_def'
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(x : matrix n n ℂ) :
theorem
qam.symm'_symm_real_eq_adjoint_tfae
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(A : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) :
theorem
sig_comp_eq_iff
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(t : ℝ)
(A B : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) :
(_.sig t).to_linear_map.comp A = B ↔ A = (_.sig (-t)).to_linear_map.comp B
theorem
module.dual.is_faithful_pos_map.sig_real
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
{t : ℝ} :
(_.sig t).to_linear_map.real = (_.sig (-t)).to_linear_map
theorem
qam.commute_with_sig_iff_symm_eq_symm'
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
{A : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ} :
theorem
qam.commute_with_sig_of_symm
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
{A : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ}
(hA : ⇑(linear_equiv.symm_map ℂ (matrix n n ℂ)) A = A) :
commute A (_.sig 1).to_linear_map
theorem
qam.symm_one
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map] :
def
qam.is_self_adjoint
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(x : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) :
Prop
Equations
- qam.is_self_adjoint x = (⇑linear_map.adjoint x = x)
def
qam.is_symm
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(x : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) :
Prop
Equations
- qam.is_symm x = (⇑(linear_equiv.symm_map ℂ (matrix n n ℂ)) x = x)
def
qam_lm_nontracial_is_reflexive
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(x : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) :
Prop
Equations
- qam_lm_nontracial_is_reflexive x = (⇑(⇑(qam.refl_idempotent qam_lm_nontracial_is_reflexive._proof_1) x) 1 = 1)
def
qam_lm_nontracial_is_unreflexive
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(x : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) :
Prop
Equations
- qam_lm_nontracial_is_unreflexive x = (⇑(⇑(qam.refl_idempotent qam_lm_nontracial_is_unreflexive._proof_1) x) 1 = 0)
theorem
std_basis_matrix_squash
{n : Type u_1}
[fintype n]
[decidable_eq n]
(i j k l : n)
(x : matrix n n ℂ) :
((matrix.std_basis_matrix i j 1).mul x).mul (matrix.std_basis_matrix k l 1) = x j k • matrix.std_basis_matrix i l 1
theorem
rank_one_lm_smul
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
(x y : E)
(r : 𝕜) :
rank_one_lm x (r • y) = ⇑(star_ring_end 𝕜) r • rank_one_lm x y
theorem
smul_rank_one_lm
{𝕜 : Type u_1}
{E : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group E]
[inner_product_space 𝕜 E]
(x y : E)
(r : 𝕜) :
rank_one_lm (r • x) y = r • rank_one_lm x y
theorem
Psi.symmetric
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(a : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ)
(t s : ℝ) :
theorem
Psi.symmetric'
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(a : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ)
(t s : ℝ) :
theorem
ten_swap_sig
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(x y : ℝ) :
ten_swap.comp (tensor_product.map (_.sig x).to_linear_map (sigop _ y)) = (tensor_product.map (_.sig y).to_linear_map (sigop _ x)).comp ten_swap
theorem
Psi.adjoint
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(a : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ)
(t s : ℝ) :
⇑(_.Psi t s) (⇑linear_map.adjoint a) = ⇑(tensor_product.map (_.sig (t - s)).to_linear_map (sigop _ (t - s))) (⇑ten_swap (has_star.star (⇑(_.Psi t s) a)))
theorem
qam.reflexive_eq_rank_one
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(a b : matrix n n ℂ) :
⇑(⇑(qam.refl_idempotent _) ↑(rank_one a b)) 1 = linear_map.mul_left ℂ (a.mul b.conj_transpose)
theorem
qam.reflexive'_eq_rank_one
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(a b : matrix n n ℂ) :
⇑(⇑(qam.refl_idempotent _) 1) ↑(rank_one a b) = linear_map.mul_right ℂ ((⇑(_.sig (-1)) b.conj_transpose).mul a)
theorem
map_sig_star
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(t s : ℝ)
(x : tensor_product ℂ (matrix n n ℂ) (matrix n n ℂ)ᵐᵒᵖ) :
has_star.star (⇑(tensor_product.map (_.sig t).to_linear_map (sigop _ s)) x) = ⇑(tensor_product.map (_.sig (-t)).to_linear_map (sigop _ (-s))) (has_star.star x)
theorem
op_sig_unop_comp
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(t s : ℝ) :
theorem
map_sig_injective
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(t s : ℝ) :
function.injective ⇑(tensor_product.map (_.sig t).to_linear_map (sigop _ s))
theorem
map_sig_eq
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(t s : ℝ) :
theorem
map_sig_mul_left_injective
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(t s : ℝ) :
theorem
map_sig_mul_right_injective
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(t s : ℝ) :
theorem
linear_map.matrix.mul_right_adjoint
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(x : matrix n n ℂ) :
⇑linear_map.adjoint (linear_map.mul_right ℂ x) = linear_map.mul_right ℂ (⇑(_.sig (-1)) x.conj_transpose)
theorem
linear_map.matrix.mul_left_adjoint
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(x : matrix n n ℂ) :
theorem
qam.ir_refl_iff_ir_refl'_of_real
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
{A : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ}
(hA : A.is_real)
(p : Prop)
[decidable p] :
theorem
qam.real_of_self_adjoint_symm
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(A : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ)
(h1 : ⇑linear_map.adjoint A = A)
(h2 : ⇑(linear_equiv.symm_map ℂ (matrix n n ℂ)) A = A) :
A.is_real
theorem
qam.self_adjoint_of_symm_real
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(A : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ)
(h1 : ⇑(linear_equiv.symm_map ℂ (matrix n n ℂ)) A = A)
(h2 : A.is_real) :
⇑linear_map.adjoint A = A
theorem
qam.symm_of_real_self_adjoint
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(A : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ)
(h1 : A.is_real)
(h2 : ⇑linear_map.adjoint A = A) :
theorem
qam.self_adjoint_symm_real_tfae
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(A : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) :
theorem
Psi.real
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(A : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ)
(t s : ℝ) :
⇑(_.Psi t s) A.real = ⇑(tensor_product.map (_.sig (2 * t)).to_linear_map (sigop _ (1 - 2 * s))) (has_star.star (⇑(_.Psi t s) A))
theorem
sigop_zero
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map] :
theorem
qam.is_real_and_idempotent_iff_Psi_orthogonal_projection
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(A : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) :
theorem
sig_map_sigop_comp_Psi
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(t s r q : ℝ) :
theorem
sig_map_sigop_apply_Psi
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(t s r q : ℝ)
(A : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) :