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₁

Equations

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

Instances For

source

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)

source

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

source

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

source

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₁

source

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

IsSelfAdjoint (completeGraph E E)

source

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)

source

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

source

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

source

theorem Qam.Nontracial.CompleteGraph.is_reflexive {A : Type u_3} [ha : starAlgebra A] [hA : QuantumSet A] :

completeGraph A A •ₛ 1 = 1

source

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

A →ₗ[ℂ ] A

Equations

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

Instances For

source

theorem Qam.trivialGraph_eq {A : Type u_5} [ha : starAlgebra A] [hA : QuantumSet A] [hA2 : QuantumSetDeltaForm A] :

trivialGraph A = (QuantumSetDeltaForm.delta A)⁻¹ • 1

source

theorem Qam.Nontracial.TrivialGraph.qam {A : Type u_5} [ha : starAlgebra A] [hA : QuantumSet A] [hA2 : QuantumSetDeltaForm A] :

Qam.trivialGraph A •ₛ Qam.trivialGraph A = Qam.trivialGraph A

source

theorem Qam.Nontracial.TrivialGraph.qam.is_self_adjoint {A : Type u_5} [ha : starAlgebra A] [hA : QuantumSet A] [hA2 : QuantumSetDeltaForm A] :

LinearMap.adjoint (Qam.trivialGraph A) = Qam.trivialGraph A

source

theorem Qam.Nontracial.trivialGraph {A : Type u_5} [ha : starAlgebra A] [hA : QuantumSet A] [hA2 : QuantumSetDeltaForm A] :

Qam.trivialGraph A •ₛ 1 = 1

source

theorem Qam.refl_idempotent_one_one_of_delta {A : Type u_5} [ha : starAlgebra A] [hA : QuantumSet A] [hA2 : QuantumSetDeltaForm A] :

1 •ₛ 1 = QuantumSetDeltaForm.delta A • 1

source

theorem Qam.Lm.Nontracial.is_unreflexive_iff_reflexive_add_one {A : Type u_5} [ha : starAlgebra A] [hA : QuantumSet A] [hA2 : QuantumSetDeltaForm A] (x : A →ₗ[ℂ ] A) :

x •ₛ 1 = 0 ↔ ((QuantumSetDeltaForm.delta A)⁻¹ • (x + 1)) •ₛ 1 = 1

source

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

source

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

source

noncomputable def Qam.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₁) :

E₂ →ₗ[ℂ ] E₁

Equations

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

Instances For

source

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

source

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)

source

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

source

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

source

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

Prop

toQam : x •ₛ x = x
toRefl : x •ₛ 1 = 1

Instances

source

theorem QamReflexive_iff {A : Type u_5} [ha : starAlgebra A] [hA : QuantumSet A] (x : A →ₗ[ℂ ] A) :

QamReflexive x ↔ x •ₛ x = x ∧ x •ₛ 1 = 1

source

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

Prop

toQam : x •ₛ x = x
toIrrefl : x •ₛ 1 = 0

Instances

source

theorem QamIrreflexive_iff {A : Type u_5} [ha : starAlgebra A] [hA : QuantumSet A] (x : A →ₗ[ℂ ] A) :

QamIrreflexive x ↔ x •ₛ x = x ∧ x •ₛ 1 = 0

source

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

QamIrreflexive (complement' x) ↔ QamReflexive x

source

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

QamReflexive (complement' x) ↔ QamIrreflexive x

source

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

A →ₗ[ℂ ] A

Equations

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

Instances For

source

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

source

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

A →ₗ[ℂ ] A

Equations

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

Instances For

source

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

A →ₗ[ℂ ] A

Equations

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

Instances For

source

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

LinearMap.IsReal (Qam.trivialGraph A)

source

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)

source

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)

source

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

irreflexiveComplement (irreflexiveComplement x) = x

source

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

reflexiveComplement (reflexiveComplement x) = x

source

theorem Qam.trivialGraph_reflexiveComplement_eq_completeGraph {A : Type u_5} [ha : starAlgebra A] [hA : QuantumSet A] [QuantumSetDeltaForm A] :

reflexiveComplement (trivialGraph A) = completeGraph A A

source

theorem Qam.completeGraph_reflexiveComplement_eq_trivialGraph {A : Type u_5} [ha : starAlgebra A] [hA : QuantumSet A] [QuantumSetDeltaForm A] :

reflexiveComplement (completeGraph A A) = trivialGraph A

source

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

source

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

source

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

source

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

source

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

Documentation

Monlib.QuantumGraph.Example

Basic examples on quantum adjacency matrices #