Basic examples on quantum adjacency matrices

This file contains elementary examples of quantum adjacency matrices, such as the complete graph and the trivial graph.

noncomputable def Qam.completeGraph (E₁ : Type u_3) (E₂ : Type u_4) [One E₁] [One E₂] [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] [InnerProductSpace ℂ E₁] [InnerProductSpace ℂ E₂] : E₂ →ₗ[ℂ] E₁

The complete quantum adjacency map between two Hilbert spaces with chosen units.

Equations

• Qam.completeGraph E₁ E₂ = ↑(((rankOne ℂ) 1) 1)

theorem Qam.completeGraph_eq {E₁ : Type u_3} {E₂ : Type u_4} [One E₁] [One E₂] [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] [InnerProductSpace ℂ E₁] [InnerProductSpace ℂ E₂] : completeGraph E₁ E₂ = ↑(((rankOne ℂ) 1) 1)

theorem Qam.completeGraph_eq' {A : Type u_3} {B : Type u_4} [ha : starAlgebra A] [hb : starAlgebra B] [hA : QuantumSet A] [hB : QuantumSet B] : completeGraph A B = Algebra.linearMap ℂ A ∘ₗ CoalgebraStruct.counit

theorem Qam.Nontracial.CompleteGraph.qam {A : Type u_3} {B : Type u_4} [ha : starAlgebra A] [hb : starAlgebra B] [hA : QuantumSet A] [hB : QuantumSet B] : completeGraph A B •ₛ completeGraph A B = completeGraph A B

theorem Qam.Nontracial.CompleteGraph.adjoint_eq {E₁ : Type u_5} {E₂ : Type u_6} [NormedAddCommGroupOfRing E₁] [NormedAddCommGroupOfRing E₂] [InnerProductSpace ℂ E₁] [InnerProductSpace ℂ E₂] [FiniteDimensional ℂ E₁] [FiniteDimensional ℂ E₂] [IsScalarTower ℂ E₁ E₁] [IsScalarTower ℂ E₂ E₂] [SMulCommClass ℂ E₁ E₁] [SMulCommClass ℂ E₂ E₂] : LinearMap.adjoint (completeGraph E₁ E₂) = completeGraph E₂ E₁

theorem Qam.Nontracial.CompleteGraph.isSelfAdjoint {E : Type u_5} [One E] [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] : IsSelfAdjoint (completeGraph E E)

theorem Qam.Nontracial.CompleteGraph.isReal {A : Type u_3} {B : Type u_4} [ha : starAlgebra A] [hb : starAlgebra B] [hA : QuantumSet A] [hB : QuantumSet B] : LinearMap.IsReal (completeGraph A B)

theorem Qam.Nontracial.CompleteGraph.symm_eq {A : Type u_3} {B : Type u_4} [ha : starAlgebra A] [hb : starAlgebra B] [hA : QuantumSet A] [hB : QuantumSet B] : (symmMap ℂ B A) (completeGraph A B) = completeGraph B A

theorem Qam.Nontracial.CompleteGraph.is_symm {A : Type u_3} [ha : starAlgebra A] [hA : QuantumSet A] : (symmMap ℂ A A) (completeGraph A A) = completeGraph A A

theorem Qam.Nontracial.CompleteGraph.is_reflexive {A : Type u_3} [ha : starAlgebra A] [hA : QuantumSet A] : completeGraph A A •ₛ 1 = 1

noncomputable def Qam.trivialGraph (A : Type u_5) [starAlgebra A] [CoalgebraStruct ℂ A] [QuantumSet A] [QuantumSetDeltaForm A] : A →ₗ[ℂ] A

The trivial quantum graph on a quantum set with delta form.

Equations

• Qam.trivialGraph A = ⅟(LinearMap.mul' ℂ A ∘ₗ CoalgebraStruct.comul)

theorem Qam.trivialGraph_eq {A : Type u_5} [ha : starAlgebra A] [hA : QuantumSet A] [hAc : CoalgebraStruct ℂ A] [hA2 : QuantumSetDeltaForm A] : trivialGraph A = (QuantumSetDeltaForm.delta A)⁻¹ • 1

theorem Qam.Nontracial.TrivialGraph.qam {A : Type u_5} [ha : starAlgebra A] [hA : QuantumSet A] [hAc : CoalgebraStruct ℂ A] [hA2 : QuantumSetDeltaForm A] : Qam.trivialGraph A •ₛ Qam.trivialGraph A = Qam.trivialGraph A

theorem Qam.Nontracial.TrivialGraph.qam.is_self_adjoint {A : Type u_5} [ha : starAlgebra A] [hA : QuantumSet A] [hAc : CoalgebraStruct ℂ A] [hA2 : QuantumSetDeltaForm A] : LinearMap.adjoint (Qam.trivialGraph A) = Qam.trivialGraph A

theorem Qam.Nontracial.trivialGraph {A : Type u_5} [ha : starAlgebra A] [hA : QuantumSet A] [hAc : CoalgebraStruct ℂ A] [hA2 : QuantumSetDeltaForm A] : Qam.trivialGraph A •ₛ 1 = 1

theorem Qam.refl_idempotent_one_one_of_delta {A : Type u_5} [ha : starAlgebra A] [hA : QuantumSet A] [hAc : CoalgebraStruct ℂ A] [hA2 : QuantumSetDeltaForm A] : 1 •ₛ 1 = QuantumSetDeltaForm.delta A • 1

theorem Qam.Lm.Nontracial.is_unreflexive_iff_reflexive_add_one {A : Type u_5} [ha : starAlgebra A] [hA : QuantumSet A] [hAc : CoalgebraStruct ℂ A] [hA2 : QuantumSetDeltaForm A] (x : A →ₗ[ℂ] A) : x •ₛ 1 = 0 ↔ ((QuantumSetDeltaForm.delta A)⁻¹ • (x + 1)) •ₛ 1 = 1

theorem Qam.refl_idempotent_completeGraph_left {B : Type u_4} [hb : starAlgebra B] [hB : QuantumSet B] {A : Type u_5} [ha : starAlgebra A] [hA : QuantumSet A] (x : A →ₗ[ℂ] B) : completeGraph B A •ₛ x = x

theorem Qam.refl_idempotent_completeGraph_right {B : Type u_4} [hb : starAlgebra B] [hB : QuantumSet B] {A : Type u_5} [ha : starAlgebra A] [hA : QuantumSet A] (x : A →ₗ[ℂ] B) : x •ₛ completeGraph B A = x

noncomputable def Qam.complement' {E₁ : Type u_6} {E₂ : Type u_7} [One E₁] [One E₂] [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] [InnerProductSpace ℂ E₁] [InnerProductSpace ℂ E₂] (x : E₂ →ₗ[ℂ] E₁) : E₂ →ₗ[ℂ] E₁

The complement of a quantum adjacency map, relative to the complete graph.

Equations

• Qam.complement' x = Qam.completeGraph E₁ E₂ - x

theorem Qam.Nontracial.Complement'.qam {B : Type u_4} [hb : starAlgebra B] [hB : QuantumSet B] {A : Type u_5} [ha : starAlgebra A] [hA : QuantumSet A] (x : A →ₗ[ℂ] B) : x •ₛ x = x ↔ complement' x •ₛ complement' x = complement' x

theorem Qam.Nontracial.Complement'.qam.isReal {B : Type u_4} [hb : starAlgebra B] [hB : QuantumSet B] {A : Type u_5} [ha : starAlgebra A] [hA : QuantumSet A] (x : A →ₗ[ℂ] B) : LinearMap.IsReal x ↔ LinearMap.IsReal (complement' x)

theorem Qam.complement'_complement' {E₁ : Type u_6} {E₂ : Type u_7} [NormedAddCommGroupOfRing E₁] [NormedAddCommGroupOfRing E₂] [InnerProductSpace ℂ E₁] [InnerProductSpace ℂ E₂] [FiniteDimensional ℂ E₁] [FiniteDimensional ℂ E₂] [IsScalarTower ℂ E₁ E₁] [IsScalarTower ℂ E₂ E₂] [SMulCommClass ℂ E₁ E₁] [SMulCommClass ℂ E₂ E₂] (x : E₁ →ₗ[ℂ] E₂) : complement' (complement' x) = x

theorem Qam.Nontracial.Complement'.ir_reflexive {A : Type u_5} [ha : starAlgebra A] [hA : QuantumSet A] (x : A →ₗ[ℂ] A) (α : Prop) [Decidable α] : (x •ₛ 1 = if α then 1 else 0) ↔ complement' x •ₛ 1 = if α then 0 else 1

class QamReflexive {A : Type u_5} [ha : starAlgebra A] [hA : QuantumSet A] (x : A →ₗ[ℂ] A) : Prop

A quantum adjacency map that is idempotent and reflexive.

• toQam : x •ₛ x = x

  Idempotence under Schur multiplication.

• toRefl : x •ₛ 1 = 1

  Reflexivity condition.

theorem QamReflexive_iff {A : Type u_5} [ha : starAlgebra A] [hA : QuantumSet A] (x : A →ₗ[ℂ] A) : QamReflexive x ↔ x •ₛ x = x ∧ x •ₛ 1 = 1

class QamIrreflexive {A : Type u_5} [ha : starAlgebra A] [hA : QuantumSet A] (x : A →ₗ[ℂ] A) : Prop

A quantum adjacency map that is idempotent and irreflexive.

• toQam : x •ₛ x = x

  Idempotence under Schur multiplication.

• toIrrefl : x •ₛ 1 = 0

  Irreflexivity condition.

theorem QamIrreflexive_iff {A : Type u_5} [ha : starAlgebra A] [hA : QuantumSet A] (x : A →ₗ[ℂ] A) : QamIrreflexive x ↔ x •ₛ x = x ∧ x •ₛ 1 = 0

theorem Qam.complement'_is_irreflexive_iff {A : Type u_5} [ha : starAlgebra A] [hA : QuantumSet A] (x : A →ₗ[ℂ] A) : QamIrreflexive (complement' x) ↔ QamReflexive x

theorem Qam.complement'_is_reflexive_iff {A : Type u_5} [ha : starAlgebra A] [hA : QuantumSet A] (x : A →ₗ[ℂ] A) : QamReflexive (complement' x) ↔ QamIrreflexive x

noncomputable def Qam.complement'' {A : Type u_5} [ha : starAlgebra A] [hA : QuantumSet A] [QuantumSetDeltaForm A] (x : A →ₗ[ℂ] A) : A →ₗ[ℂ] A

Complement relative to the trivial graph.

Equations

• Qam.complement'' x = x - Qam.trivialGraph A

theorem Qam.complement''_is_irreflexive_iff {A : Type u_5} [ha : starAlgebra A] [hA : QuantumSet A] [hA2 : QuantumSetDeltaForm A] {x : A →ₗ[ℂ] A} (hx : LinearMap.IsReal x) : QamIrreflexive (complement'' x) ↔ QamReflexive x

noncomputable def Qam.irreflexiveComplement {A : Type u_5} [ha : starAlgebra A] [hA : QuantumSet A] [QuantumSetDeltaForm A] (x : A →ₗ[ℂ] A) : A →ₗ[ℂ] A

Complement operation producing the irreflexive complement.

Equations

• Qam.irreflexiveComplement x = Qam.completeGraph A A - Qam.trivialGraph A - x

noncomputable def Qam.reflexiveComplement {A : Type u_5} [ha : starAlgebra A] [hA : QuantumSet A] [QuantumSetDeltaForm A] (x : A →ₗ[ℂ] A) : A →ₗ[ℂ] A

Complement operation producing the reflexive complement.

Equations

• Qam.reflexiveComplement x = Qam.completeGraph A A + Qam.trivialGraph A - x

theorem Qam.Nontracial.trivialGraph.isReal {A : Type u_5} [ha : starAlgebra A] [hA : QuantumSet A] [hA2 : QuantumSetDeltaForm A] : LinearMap.IsReal (Qam.trivialGraph A)

theorem Qam.irreflexiveComplement.isReal {A : Type u_5} [ha : starAlgebra A] [hA : QuantumSet A] [hA2 : QuantumSetDeltaForm A] {x : A →ₗ[ℂ] A} (hx : LinearMap.IsReal x) : LinearMap.IsReal (irreflexiveComplement x)

theorem Qam.reflexiveComplement.isReal {A : Type u_5} [ha : starAlgebra A] [hA : QuantumSet A] [hA2 : QuantumSetDeltaForm A] {x : A →ₗ[ℂ] A} (hx : LinearMap.IsReal x) : LinearMap.IsReal (reflexiveComplement x)

theorem Qam.irreflexiveComplement_irreflexiveComplement {A : Type u_5} [ha : starAlgebra A] [hA : QuantumSet A] [QuantumSetDeltaForm A] {x : A →ₗ[ℂ] A} : irreflexiveComplement (irreflexiveComplement x) = x

theorem Qam.reflexiveComplement_reflexiveComplement {A : Type u_5} [ha : starAlgebra A] [hA : QuantumSet A] [QuantumSetDeltaForm A] {x : A →ₗ[ℂ] A} : reflexiveComplement (reflexiveComplement x) = x

theorem Qam.trivialGraph_reflexiveComplement_eq_completeGraph {A : Type u_5} [ha : starAlgebra A] [hA : QuantumSet A] [QuantumSetDeltaForm A] : reflexiveComplement (trivialGraph A) = completeGraph A A

theorem Qam.completeGraph_reflexiveComplement_eq_trivialGraph {A : Type u_5} [ha : starAlgebra A] [hA : QuantumSet A] [QuantumSetDeltaForm A] : reflexiveComplement (completeGraph A A) = trivialGraph A

theorem Qam.complement'_eq {E₁ : Type u_6} {E₂ : Type u_7} [NormedAddCommGroupOfRing E₁] [NormedAddCommGroupOfRing E₂] [InnerProductSpace ℂ E₁] [InnerProductSpace ℂ E₂] [FiniteDimensional ℂ E₁] [FiniteDimensional ℂ E₂] [IsScalarTower ℂ E₁ E₁] [IsScalarTower ℂ E₂ E₂] [SMulCommClass ℂ E₁ E₁] [SMulCommClass ℂ E₂ E₂] (a : E₂ →ₗ[ℂ] E₁) : complement' a = completeGraph E₁ E₂ - a

theorem Qam.irreflexiveComplement_is_irreflexive_qam_iff_irreflexive_qam {A : Type u_5} [ha : starAlgebra A] [hA : QuantumSet A] [hA2 : QuantumSetDeltaForm A] {x : A →ₗ[ℂ] A} (hx : LinearMap.IsReal x) : QamIrreflexive (irreflexiveComplement x) ↔ QamIrreflexive x

theorem Qam.reflexive_complment_is_reflexive_qam_iff_reflexive_qam {A : Type u_5} [ha : starAlgebra A] [hA : QuantumSet A] [hA2 : QuantumSetDeltaForm A] {x : A →ₗ[ℂ] A} (hx : LinearMap.IsReal x) : QamReflexive (reflexiveComplement x) ↔ QamReflexive x

theorem QuantumSet.Psi_apply_completeGraph {A : Type u_6} {B : Type u_7} [starAlgebra A] [starAlgebra B] [QuantumSet A] [QuantumSet B] (t r : ℝ) : (Psi t r) (Qam.completeGraph A B) = 1

theorem QuantumSet.Psi_symm_one {A : Type u_6} {B : Type u_7} [starAlgebra A] [starAlgebra B] [QuantumSet A] [QuantumSet B] (t r : ℝ) : (Psi t r).symm 1 = Qam.completeGraph A B