Single-edged quantum graphs

This file defines the single-edged quantum graph, and proves that it is a QAM.

noncomputable def qamA {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} (hφ : φ.IsFaithfulPosMap) (x : { x : Matrix n n ℂ // x ≠ 0 }) : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ

The rank-one quantum adjacency map associated to a nonzero matrix.

Equations

• qamA hφ x = (1 / ↑‖↑x‖ ^ 2) • (LinearMap.mulLeft ℂ (↑x * φ.matrix) * LinearMap.adjoint (LinearMap.mulRight ℂ (φ.matrix * ↑x)))

theorem qamA_eq {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (x : { x : Matrix n n ℂ // x ≠ 0 }) : qamA hφ x = (1 / ↑‖↑x‖ ^ 2) • (LinearMap.mulLeft ℂ (↑x * φ.matrix) * LinearMap.adjoint (LinearMap.mulRight ℂ (φ.matrix * ↑x)))

theorem qamA.toMatrix {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (x : { x : Matrix n n ℂ // x ≠ 0 }) : hφ.toMatrix (qamA hφ x) = (1 / ↑‖↑x‖ ^ 2) • Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (↑x * φ.matrix) (⋯.rpow (1 / 2) * ↑x * ⋯.rpow (1 / 2)).conj

@[reducible]

noncomputable instance hasSmul.unitsMatrixNeZero {n : Type u_1} : SMul ℂˣ { x : Matrix n n ℂ // x ≠ 0 }

Equations

• hasSmul.unitsMatrixNeZero = { smul := fun (α : ℂˣ) (x : { x : Matrix n n ℂ // x ≠ 0 }) => ⟨↑α • ↑x, ⋯⟩ }

theorem qamA.ne_zero {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (x : { x : Matrix n n ℂ // x ≠ 0 }) : qamA hφ x ≠ 0

given a non-zero matrix $x$, we always get $A(x)$ is non-zero

theorem qamA.smul {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (x : { x : Matrix n n ℂ // x ≠ 0 }) (α : ℂˣ) : qamA hφ (α • x) = qamA hφ x

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 qamA.is_idempotent {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (x : { x : Matrix n n ℂ // x ≠ 0 }) : (Qam.reflIdempotent hφ (qamA hφ x)) (qamA hφ x) = qamA hφ x

theorem Psi.one {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] : (hφ.psi 0 (1 / 2)) 1 = (TensorProduct.map 1 (Matrix.transposeAlgEquiv n ℂ ℂ).toLinearMap) (Matrix.kroneckerToTensorProduct (hφ.toMatrix ↑(((rankOne ℂ) φ.matrix⁻¹) φ.matrix⁻¹)))

theorem one_map_transpose_psi_eq {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (A : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ) : (TensorProduct.map 1 (Matrix.transposeAlgEquiv n ℂ ℂ).symm.toLinearMap) ((hφ.psi 0 (1 / 2)) A) = (TensorProduct.map A 1) (Matrix.kroneckerToTensorProduct (hφ.toMatrix ↑(((rankOne ℂ) φ.matrix⁻¹) φ.matrix⁻¹)))

theorem Psi.schurMul_faithful {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (r₁ r₂ : ℝ) (f g : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ) : (hφ.psi r₁ r₂) (f •ₛ g) = (hφ.psi r₁ r₂) f * (hφ.psi r₁ r₂) g

theorem qamA.isReal {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (x : { x : Matrix n n ℂ // x ≠ 0 }) : LinearMap.IsReal (qamA hφ x)

theorem sig_eq_lmul_rmul {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (t : ℝ) : (hφ.sig t).toLinearMap = LinearMap.mulLeft ℂ (⋯.rpow (-t)) ∘ₗ LinearMap.mulRight ℂ (⋯.rpow t)

theorem Qam.RankOne.symmetric_eq {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (x : Matrix n n ℂ) : (symmMap ℂ (Matrix n n ℂ) (Matrix n n ℂ)) ↑(((rankOne ℂ) x) x) = ↑(((rankOne ℂ) ((hφ.sig (-1)) x.conjTranspose)) x.conjTranspose)

theorem Qam.RankOne.symmetric'_eq {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (x : Matrix n n ℂ) : (symmMap ℂ (Matrix n n ℂ) (Matrix n n ℂ)).symm ↑(((rankOne ℂ) x) x) = ↑(((rankOne ℂ) x.conjTranspose) ((hφ.sig (-1)) x.conjTranspose))

theorem sig_comp_eq_iff_eq_sig_inv_comp {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (r : ℝ) (a b : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ) : (hφ.sig r).toLinearMap ∘ₗ a = b ↔ a = (hφ.sig (-r)).toLinearMap ∘ₗ b

theorem sig_eq_iff_eq_sig_inv {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (r : ℝ) (a b : Matrix n n ℂ) : (hφ.sig r) a = b ↔ a = (hφ.sig (-r)) b

theorem comp_sig_eq_iff_eq_comp_sig_inv {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (r : ℝ) (a b : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ) : a ∘ₗ (hφ.sig r).toLinearMap = b ↔ a = b ∘ₗ (hφ.sig (-r)).toLinearMap

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

theorem qamA.of_is_self_adjoint {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (x : { x : Matrix n n ℂ // x ≠ 0 }) (h : LinearMap.adjoint (qamA hφ x) = qamA hφ x) : (↑x).IsAlmostHermitian ∧ Commute φ.matrix ↑x

theorem qamA.is_self_adjoint_of {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (x : { x : Matrix n n ℂ // x ≠ 0 }) (hx₁ : (↑x).IsAlmostHermitian) (hx₂ : Commute φ.matrix ↑x) : LinearMap.adjoint (qamA hφ x) = qamA hφ x

theorem qamA.is_self_adjoint_iff {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (x : { x : Matrix n n ℂ // x ≠ 0 }) : LinearMap.adjoint (qamA hφ x) = qamA hφ x ↔ (↑x).IsAlmostHermitian ∧ Commute φ.matrix ↑x

theorem qamA.isRealQam {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (x : { x : Matrix n n ℂ // x ≠ 0 }) : RealQam hφ (qamA hφ x)

theorem Matrix.PosDef.ne_zero {n : Type u_1} [Finite n] [Nontrivial n] {Q : Matrix n n ℂ} (hQ : Q.PosDef) : Q ≠ 0

theorem qamA.edges {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (x : { x : Matrix n n ℂ // x ≠ 0 }) : ⋯.edges = 1

theorem qamA.is_irreflexive_iff {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] [Nontrivial n] (x : { x : Matrix n n ℂ // x ≠ 0 }) : (Qam.reflIdempotent hφ (qamA hφ x)) 1 = 0 ↔ (↑x).trace = 0

theorem qamA.is_almost_injective {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (x y : { x : Matrix n n ℂ // x ≠ 0 }) : qamA hφ x = qamA hφ y ↔ ∃ (α : ℂˣ), ↑x = ↑α • ↑y

theorem qamA.is_reflexive_iff {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] [Nontrivial n] (x : { x : Matrix n n ℂ // x ≠ 0 }) : (Qam.reflIdempotent hφ (qamA hφ x)) 1 = 1 ↔ ∃ (α : ℂˣ), ↑x = ↑α • φ.matrix⁻¹

theorem qamA.of_trivialGraph {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] [Nontrivial n] [Nonempty n] : qamA hφ ⟨φ.matrix⁻¹, ⋯⟩ = Qam.trivialGraph (Matrix n n ℂ)

theorem Qam.unique_one_edge_and_refl {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] [Nontrivial n] [Nonempty n] {A : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ} (hA : RealQam hφ A) : hA.edges = 1 ∧ (reflIdempotent hφ A) 1 = 1 ↔ A = trivialGraph (Matrix n n ℂ)

theorem qamA.isometric_starAlgEquiv_conj {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (x : { x : Matrix n n ℂ // x ≠ 0 }) {f : Matrix n n ℂ ≃⋆ₐ[ℂ] Matrix n n ℂ} : StarAlgEquiv.IsIsometry ⇑f → f.toAlgEquiv.toLinearMap ∘ₗ qamA hφ x ∘ₗ f.symm.toAlgEquiv.toLinearMap = qamA hφ ⟨f ↑x, ⋯⟩

theorem qamA.iso_iff {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] {x y : { x : Matrix n n ℂ // x ≠ 0 }} : Qam.Iso (qamA hφ x) (qamA hφ y) ↔ ∃ (U : ↥(Matrix.unitaryGroup n ℂ)), (∃ (β : ℂˣ), ↑x = (Matrix.innerAut U) (↑β • ↑y)) ∧ Commute φ.matrix ↑U