Quantum graphs: quantum adjacency matrices

This file defines the quantum adjacency matrix of a quantum graph.

theorem Finset.sum_fin_one {α : Type u_1} [AddCommMonoid α] (f : Fin 1 → α) : ∑ i : Fin 1, f i = f 0

theorem sig_apply_posDef_matrix_hMul {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (t : ℝ) (x : Matrix n n ℂ) : (hφ.sig t) (⋯.rpow t * x) = x * ⋯.rpow t

theorem sig_apply_posDef_matrix_mul' {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (x : Matrix n n ℂ) : (hφ.sig 1) (φ.matrix * x) = x * φ.matrix

theorem sig_apply_matrix_hMul_posDef {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (t : ℝ) (x : Matrix n n ℂ) : (hφ.sig t) (x * ⋯.rpow (-t)) = ⋯.rpow (-t) * x

theorem sig_apply_matrix_hMul_posDef' {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (x : Matrix n n ℂ) : (hφ.sig (-1)) (x * φ.matrix) = φ.matrix * x

theorem sig_apply_matrix_hMul_posDef'' {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (x : Matrix n n ℂ) : (hφ.sig 1) (x * φ.matrix⁻¹) = φ.matrix⁻¹ * x

theorem sig_apply_basis {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (i : n × n) : (hφ.sig 1) (hφ.basis i) = φ.matrix⁻¹ * Matrix.stdBasisMatrix i.1 i.2 1 * ⋯.rpow (1 / 2)

theorem Qam.symm'_symm_real_apply_adjoint_tFAE {n : Type u_1} [Fintype n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (A : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ) : [(symmMap ℂ (Matrix n n ℂ) (Matrix n n ℂ)) A = A, (symmMap ℂ (Matrix n n ℂ) (Matrix n n ℂ)).symm A = A, A.real = LinearMap.adjoint A, ∀ (x y : Matrix n n ℂ), φ (A x * y) = φ (x * A y)].TFAE

theorem sig_comp_eq_iff {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (t : ℝ) (A B : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ) : (hφ.sig t).toLinearMap ∘ₗ A = B ↔ A = (hφ.sig (-t)).toLinearMap ∘ₗ B

theorem stdBasisMatrix_squash {n : Type u_1} [Fintype n] [DecidableEq n] (i j k l : n) (x : Matrix n n ℂ) : Matrix.stdBasisMatrix i j 1 * x * Matrix.stdBasisMatrix k l 1 = x j k • Matrix.stdBasisMatrix i l 1

theorem map_sig_mulLeft_injective {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (t s : ℝ) : Function.Injective ⇑(LinearMap.mulLeft ℂ (⋯.rpow t ⊗ₜ[ℂ] ↑(op ℂ) (⋯.rpow s)))

theorem map_sig_mulRight_injective {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (t s : ℝ) : Function.Injective ⇑(LinearMap.mulRight ℂ (⋯.rpow t ⊗ₜ[ℂ] ↑(op ℂ) (⋯.rpow s)))

theorem LinearMap.matrix.mulRight_adjoint {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (x : Matrix n n ℂ) : adjoint (mulRight ℂ x) = mulRight ℂ ((hφ.sig (-1)) x.conjTranspose)

theorem LinearMap.matrix.mulLeft_adjoint {n : Type u_1} [Fintype n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (x : Matrix n n ℂ) : adjoint (mulLeft ℂ x) = mulLeft ℂ x.conjTranspose