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)

theorem Qam.completeGraph_eq {E₁ : Type u_3} {E₂ : Type u_4} [One E₁] [One E₂] [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] [InnerProductSpace ℂ E₁] [InnerProductSpace ℂ E₂] : Qam.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] : Qam.completeGraph A B = Algebra.linearMap ℂ A ∘ₗ Coalgebra.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] : Qam.completeGraph A B •ₛ Qam.completeGraph A B = Qam.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 (Qam.completeGraph E₁ E₂) = Qam.completeGraph E₂ E₁

theorem Qam.Nontracial.CompleteGraph.isSelfAdjoint {E : Type u_5} [One E] [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] : IsSelfAdjoint (Qam.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 (Qam.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) (Qam.completeGraph A B) = Qam.completeGraph B A

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

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

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

Equations

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

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

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

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

theorem Qam.Nontracial.trivialGraph {A : Type u_5} [ha : starAlgebra A] [hA : QuantumSet 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] [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] [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) : Qam.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 •ₛ Qam.completeGraph B A = x

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

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 ↔ Qam.complement' x •ₛ Qam.complement' x = Qam.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 (Qam.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₂) : Qam.complement' (Qam.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) ↔ Qam.complement' x •ₛ 1 = if α then 0 else 1

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

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

theorem QamReflexive.toQam {A : Type u_5} {ha : starAlgebra A} {hA : QuantumSet A} {x : A →ₗ[ℂ] A} [self : QamReflexive x] : x •ₛ x = x

theorem QamReflexive.toRefl {A : Type u_5} {ha : starAlgebra A} {hA : QuantumSet A} {x : A →ₗ[ℂ] A} [self : QamReflexive x] : x •ₛ 1 = 1

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

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

theorem QamIrreflexive.toQam {A : Type u_5} {ha : starAlgebra A} {hA : QuantumSet A} {x : A →ₗ[ℂ] A} [self : QamIrreflexive x] : x •ₛ x = x

theorem QamIrreflexive.toIrrefl {A : Type u_5} {ha : starAlgebra A} {hA : QuantumSet A} {x : A →ₗ[ℂ] A} [self : QamIrreflexive x] : x •ₛ 1 = 0

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 (Qam.complement' x) ↔ QamReflexive x

theorem Qam.complement'_is_reflexive_iff {A : Type u_5} [ha : starAlgebra A] [hA : QuantumSet A] (x : A →ₗ[ℂ] A) : QamReflexive (Qam.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

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 (Qam.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

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

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 (Qam.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 (Qam.reflexiveComplement x)

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

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

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

theorem Qam.completeGraph_reflexiveComplement_eq_trivialGraph {A : Type u_5} [ha : starAlgebra A] [hA : QuantumSet A] [QuantumSetDeltaForm A] : Qam.reflexiveComplement (Qam.completeGraph A A) = Qam.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₁) : Qam.complement' a = Qam.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 (Qam.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 (Qam.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 : ℝ) : (QuantumSet.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 : ℝ) : (QuantumSet.Psi t r).symm 1 = Qam.completeGraph A B