Single-edged quantum graphs #
This file defines the single-edged quantum graph, and proves that it is a QAM.
noncomputable
def
qam_A
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
(hφ : φ.is_faithful_pos_map)
(x : {x // x ≠ 0}) :
theorem
qam_A.to_matrix
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(x : {x // x ≠ 0}) :
theorem
qam_A.ne_zero
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(x : {x // x ≠ 0}) :
given a non-zero matrix $x$, we always get $A(x)$ is non-zero
theorem
qam_A.smul
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(x : {x // x ≠ 0})
(α : ℂˣ) :
Given any non-zero matrix $x$ and non-zero $\alpha\in\mathbb{C}$ we have
$$A(\alpha x)=A(x),$$
in other words, it is not injective. However, it is_almost_injective (see qam_A.is_almost_injective).
theorem
qam_A.is_idempotent
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(x : {x // x ≠ 0}) :
theorem
Psi.one
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map] :
⇑(_.Psi 0 (1 / 2)) 1 = ⇑(tensor_product.map 1 (matrix.transpose_alg_equiv n ℂ ℂ).to_linear_map) (⇑matrix.kronecker_to_tensor_product (⇑(_.to_matrix) ↑(rank_one (φ.matrix)⁻¹ (φ.matrix)⁻¹)))
theorem
one_map_transpose_Psi_eq
{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 ℂ) :
⇑(tensor_product.map 1 (matrix.transpose_alg_equiv n ℂ ℂ).symm.to_linear_map) (⇑(_.Psi 0 (1 / 2)) A) = ⇑(tensor_product.map A 1) (⇑matrix.kronecker_to_tensor_product (⇑(_.to_matrix) ↑(rank_one (φ.matrix)⁻¹ (φ.matrix)⁻¹)))
theorem
qam_A.is_real
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(x : {x // x ≠ 0}) :
theorem
sig_eq_lmul_rmul
{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 = (linear_map.mul_left ℂ (_.rpow (-t))).comp (linear_map.mul_right ℂ (_.rpow t))
theorem
sig_comp_eq_iff_eq_sig_inv_comp
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(r : ℝ)
(a b : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) :
(_.sig r).to_linear_map.comp a = b ↔ a = (_.sig (-r)).to_linear_map.comp b
theorem
comp_sig_eq_iff_eq_comp_sig_inv
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(r : ℝ)
(a b : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ) :
a.comp (_.sig r).to_linear_map = b ↔ a = b.comp (_.sig (-r)).to_linear_map
theorem
sig_eq_self_iff_commute
{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_A.of_is_self_adjoint
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(x : {x // x ≠ 0})
(h : ⇑linear_map.adjoint (qam_A _ x) = qam_A _ x) :
theorem
qam_A.is_self_adjoint_of
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(x : {x // x ≠ 0})
(hx₁ : ↑x.is_almost_hermitian)
(hx₂ : commute φ.matrix ↑x) :
⇑linear_map.adjoint (qam_A _ x) = qam_A _ x
theorem
qam_A.is_self_adjoint_iff
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(x : {x // x ≠ 0}) :
theorem
qam_A.is_real_qam
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(x : {x // x ≠ 0}) :
theorem
matrix.pos_def.ne_zero
{n : Type u_1}
[fintype n]
[decidable_eq n]
[nontrivial n]
{Q : matrix n n ℂ}
(hQ : Q.pos_def) :
Q ≠ 0
theorem
qam_A.edges
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
(x : {x // x ≠ 0}) :
theorem
qam_A.is_irreflexive_iff
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
[nontrivial n]
(x : {x // x ≠ 0}) :
theorem
qam_A.is_reflexive_iff
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
[nontrivial n]
(x : {x // x ≠ 0}) :
theorem
qam_A.of_trivial_graph
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
[nontrivial n] :
theorem
qam.unique_one_edge_and_refl
{n : Type u_1}
[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 ℂ}
(hA : real_qam _ A) :
theorem
qam_A.isometric_star_alg_equiv_conj
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
[nontrivial n]
(x : {x // x ≠ 0})
{f : matrix n n ℂ ≃⋆ₐ[ℂ] matrix n n ℂ}
(hf : f.is_isometry) :
f.to_alg_equiv.to_linear_map.comp ((qam_A _ x).comp f.symm.to_alg_equiv.to_linear_map) = qam_A _ ⟨⇑f ↑x, _⟩
theorem
qam_A.iso_iff
{n : Type u_1}
[fintype n]
[decidable_eq n]
{φ : module.dual ℂ (matrix n n ℂ)}
[hφ : fact φ.is_faithful_pos_map]
[nontrivial n]
{x y : {x // x ≠ 0}} :