mathlib3 documentation

monlib / quantum_graph.example

Basic examples on quantum adjacency matrices #

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

source
noncomputable def qam.complete_graph (E : Type u_1) [has_one E] [normed_add_comm_group E] [inner_product_space ℂ E] :
E →ₗ[ℂ] E
Equations
source
theorem qam.complete_graph_eq {E : Type u_1} [has_one E] [normed_add_comm_group E] [inner_product_space ℂ E] :
qam.complete_graph E = ↑(rank_one 1 1)
source
theorem qam.complete_graph_eq' {p : Type u_1} [fintype p] [decidable_eq p] {φ : module.dual ℂ (matrix p p ℂ)} [hφ : fact φ.is_faithful_pos_map] :
qam.complete_graph (matrix p p ℂ) = (algebra.linear_map ℂ (matrix p p ℂ)).comp (⇑linear_map.adjoint (algebra.linear_map ℂ (matrix p p ℂ)))
source
theorem pi.qam.complete_graph_eq' {p : Type u_1} [fintype p] [decidable_eq p] {n : p → Type u_2} [Π (i : p), fintype (n i)] [Π (i : p), decidable_eq (n i)] {φ : Π (i : p), module.dual ℂ (matrix (n i) (n i) ℂ)} [hφ : ∀ (i : p), fact (φ i).is_faithful_pos_map] :
qam.complete_graph (Π (i : p), matrix (n i) (n i) ℂ) = (algebra.linear_map ℂ (Π (i : p), matrix (n i) (n i) ℂ)).comp (⇑linear_map.adjoint (algebra.linear_map ℂ (Π (i : p), matrix (n i) (n i) ℂ)))
source
theorem qam.nontracial.complete_graph.qam {E : Type u_1} [normed_add_comm_group_of_ring E] [inner_product_space ℂ E] [finite_dimensional ℂ E] [is_scalar_tower ℂ E E] [smul_comm_class ℂ E E] :
⇑(⇑schur_idempotent (qam.complete_graph E)) (qam.complete_graph E) = qam.complete_graph E
source
theorem qam.nontracial.complete_graph.is_self_adjoint {E : Type u_1} [has_one E] [normed_add_comm_group E] [inner_product_space ℂ E] [finite_dimensional ℂ E] :
is_self_adjoint (qam.complete_graph E)
source
theorem qam.nontracial.complete_graph.is_real {p : Type u_1} [fintype p] [decidable_eq p] {φ : module.dual ℂ (matrix p p ℂ)} [hφ : fact φ.is_faithful_pos_map] :
(qam.complete_graph (matrix p p ℂ)).is_real
source
theorem qam.nontracial.complete_graph.is_symm {p : Type u_1} [fintype p] [decidable_eq p] {φ : module.dual ℂ (matrix p p ℂ)} [hφ : fact φ.is_faithful_pos_map] :
⇑(linear_equiv.symm_map ℂ (matrix p p ℂ)) (qam.complete_graph (matrix p p ℂ)) = qam.complete_graph (matrix p p ℂ)
source
theorem pi.qam.nontracial.complete_graph.is_real {p : Type u_1} [fintype p] [decidable_eq p] {n : p → Type u_2} [Π (i : p), fintype (n i)] [Π (i : p), decidable_eq (n i)] {φ : Π (i : p), module.dual ℂ (matrix (n i) (n i) ℂ)} [hφ : ∀ (i : p), fact (φ i).is_faithful_pos_map] :
(qam.complete_graph (Π (i : p), matrix (n i) (n i) ℂ)).is_real
source
theorem pi.qam.nontracial.complete_graph.is_symm {p : Type u_1} [fintype p] [decidable_eq p] {n : p → Type u_2} [Π (i : p), fintype (n i)] [Π (i : p), decidable_eq (n i)] {φ : Π (i : p), module.dual ℂ (matrix (n i) (n i) ℂ)} [hφ : ∀ (i : p), fact (φ i).is_faithful_pos_map] :
⇑(linear_equiv.symm_map ℂ (Π (i : p), matrix (n i) (n i) ℂ)) (qam.complete_graph (Π (i : p), matrix (n i) (n i) ℂ)) = qam.complete_graph (Π (i : p), matrix (n i) (n i) ℂ)
source
theorem qam.nontracial.complete_graph.is_reflexive {E : Type u_1} [normed_add_comm_group_of_ring E] [inner_product_space ℂ E] [finite_dimensional ℂ E] [is_scalar_tower ℂ E E] [smul_comm_class ℂ E E] :
⇑(⇑schur_idempotent (qam.complete_graph E)) 1 = 1
source
theorem linear_map.mul'_comp_mul'_adjoint_of_delta_form {p : Type u_1} [fintype p] [decidable_eq p] {φ : module.dual ℂ (matrix p p ℂ)} {δ : ℂ} [hφ : fact φ.is_faithful_pos_map] (hφ₂ : (φ.matrix)⁻¹.trace = δ) :
(linear_map.mul' ℂ (matrix p p ℂ)).comp (⇑linear_map.adjoint (linear_map.mul' ℂ (matrix p p ℂ))) = δ • 1
source
theorem linear_map.pi_mul'_comp_mul'_adjoint_of_delta_form {p : Type u_1} [fintype p] [decidable_eq p] {n : p → Type u_2} [Π (i : p), fintype (n i)] [Π (i : p), decidable_eq (n i)] {φ : Π (i : p), module.dual ℂ (matrix (n i) (n i) ℂ)} [∀ (i : p), nontrivial (n i)] {δ : ℂ} [hφ : ∀ (i : p), fact (φ i).is_faithful_pos_map] (hφ₂ : ∀ (i : p), ((φ i).matrix)⁻¹.trace = δ) :
(linear_map.mul' ℂ (Π (i : p), matrix (n i) (n i) ℂ)).comp (⇑linear_map.adjoint (linear_map.mul' ℂ (Π (i : p), matrix (n i) (n i) ℂ))) = δ • 1
source
theorem qam.nontracial.delta_ne_zero {p : Type u_1} [fintype p] [decidable_eq p] [nonempty p] {φ : module.dual ℂ (matrix p p ℂ)} {δ : ℂ} [hφ : fact φ.is_faithful_pos_map] (hφ₂ : (φ.matrix)⁻¹.trace = δ) :
δ ≠ 0
source
theorem pi.qam.nontracial.delta_ne_zero {p : Type u_1} [fintype p] [decidable_eq p] {n : p → Type u_2} [Π (i : p), fintype (n i)] [Π (i : p), decidable_eq (n i)] {φ : Π (i : p), module.dual ℂ (matrix (n i) (n i) ℂ)} [nonempty p] [∀ (i : p), nontrivial (n i)] {δ : ℂ} [hφ : ∀ (i : p), fact (φ i).is_faithful_pos_map] (hφ₂ : ∀ (i : p), ((φ i).matrix)⁻¹.trace = δ) :
δ ≠ 0
source
@[instance]
noncomputable def qam.nontracial.mul'_comp_mul'_adjoint.invertible {p : Type u_1} [fintype p] [decidable_eq p] [nonempty p] {φ : module.dual ℂ (matrix p p ℂ)} {δ : ℂ} [hφ : fact φ.is_faithful_pos_map] (hφ₂ : (φ.matrix)⁻¹.trace = δ) :
invertible ((linear_map.mul' ℂ (matrix p p ℂ)).comp (⇑linear_map.adjoint (linear_map.mul' ℂ (matrix p p ℂ))))
Equations
source
@[instance]
noncomputable def pi.qam.nontracial.mul'_comp_mul'_adjoint.invertible {p : Type u_1} [fintype p] [decidable_eq p] {n : p → Type u_2} [Π (i : p), fintype (n i)] [Π (i : p), decidable_eq (n i)] {φ : Π (i : p), module.dual ℂ (matrix (n i) (n i) ℂ)} [nonempty p] [∀ (i : p), nontrivial (n i)] {δ : ℂ} [hφ : ∀ (i : p), fact (φ i).is_faithful_pos_map] (hφ₂ : ∀ (i : p), ((φ i).matrix)⁻¹.trace = δ) :
invertible ((linear_map.mul' ℂ (Π (i : p), matrix (n i) (n i) ℂ)).comp (⇑linear_map.adjoint (linear_map.mul' ℂ (Π (i : p), matrix (n i) (n i) ℂ))))
Equations
source
noncomputable def qam.trivial_graph {p : Type u_1} [fintype p] [decidable_eq p] [nonempty p] {φ : module.dual ℂ (matrix p p ℂ)} {δ : ℂ} (hφ : fact φ.is_faithful_pos_map) (hφ₂ : (φ.matrix)⁻¹.trace = δ) :
matrix p p ℂ →ₗ[ℂ] matrix p p ℂ
Equations
source
noncomputable def pi.qam.trivial_graph {p : Type u_1} [fintype p] [decidable_eq p] {n : p → Type u_2} [Π (i : p), fintype (n i)] [Π (i : p), decidable_eq (n i)] {φ : Π (i : p), module.dual ℂ (matrix (n i) (n i) ℂ)} [nonempty p] [∀ (i : p), nontrivial (n i)] {δ : ℂ} (hφ : ∀ (i : p), fact (φ i).is_faithful_pos_map) (hφ₂ : ∀ (i : p), ((φ i).matrix)⁻¹.trace = δ) :
(Π (i : p), matrix (n i) (n i) ℂ) →ₗ[ℂ] Π (i : p), matrix (n i) (n i) ℂ
Equations
source
theorem qam.trivial_graph_eq {p : Type u_1} [fintype p] [decidable_eq p] [nonempty p] {φ : module.dual ℂ (matrix p p ℂ)} [hφ : fact φ.is_faithful_pos_map] {δ : ℂ} (hφ₂ : (φ.matrix)⁻¹.trace = δ) :
qam.trivial_graph hφ hφ₂ = δ⁻¹ • 1
source
theorem pi.qam.trivial_graph_eq {p : Type u_1} [fintype p] [decidable_eq p] {n : p → Type u_2} [Π (i : p), fintype (n i)] [Π (i : p), decidable_eq (n i)] {φ : Π (i : p), module.dual ℂ (matrix (n i) (n i) ℂ)} [nonempty p] [∀ (i : p), nontrivial (n i)] {δ : ℂ} [hφ : ∀ (i : p), fact (φ i).is_faithful_pos_map] (hφ₂ : ∀ (i : p), ((φ i).matrix)⁻¹.trace = δ) :
pi.qam.trivial_graph hφ hφ₂ = δ⁻¹ • 1
source
theorem qam.nontracial.trivial_graph.qam {p : Type u_1} [fintype p] [decidable_eq p] [nonempty p] {φ : module.dual ℂ (matrix p p ℂ)} [hφ : fact φ.is_faithful_pos_map] {δ : ℂ} (hφ₂ : (φ.matrix)⁻¹.trace = δ) :
⇑(⇑schur_idempotent (qam.trivial_graph hφ hφ₂)) (qam.trivial_graph hφ hφ₂) = qam.trivial_graph hφ hφ₂
source
theorem pi.qam.nontracial.trivial_graph.qam {p : Type u_1} [fintype p] [decidable_eq p] {n : p → Type u_2} [Π (i : p), fintype (n i)] [Π (i : p), decidable_eq (n i)] {φ : Π (i : p), module.dual ℂ (matrix (n i) (n i) ℂ)} [nonempty p] [∀ (i : p), nontrivial (n i)] {δ : ℂ} [hφ : ∀ (i : p), fact (φ i).is_faithful_pos_map] (hφ₂ : ∀ (i : p), ((φ i).matrix)⁻¹.trace = δ) :
⇑(⇑schur_idempotent (pi.qam.trivial_graph hφ hφ₂)) (pi.qam.trivial_graph hφ hφ₂) = pi.qam.trivial_graph hφ hφ₂
source
theorem qam.nontracial.trivial_graph.qam.is_self_adjoint {p : Type u_1} [fintype p] [decidable_eq p] [nonempty p] {φ : module.dual ℂ (matrix p p ℂ)} [hφ : fact φ.is_faithful_pos_map] {δ : ℂ} (hφ₂ : (φ.matrix)⁻¹.trace = δ) :
⇑linear_map.adjoint (qam.trivial_graph hφ hφ₂) = qam.trivial_graph hφ hφ₂
source
theorem pi.qam.nontracial.trivial_graph.qam.is_self_adjoint {p : Type u_1} [fintype p] [decidable_eq p] {n : p → Type u_2} [Π (i : p), fintype (n i)] [Π (i : p), decidable_eq (n i)] {φ : Π (i : p), module.dual ℂ (matrix (n i) (n i) ℂ)} [nonempty p] [∀ (i : p), nontrivial (n i)] {δ : ℂ} [hφ : ∀ (i : p), fact (φ i).is_faithful_pos_map] (hφ₂ : ∀ (i : p), ((φ i).matrix)⁻¹.trace = δ) :
⇑linear_map.adjoint (pi.qam.trivial_graph hφ hφ₂) = pi.qam.trivial_graph hφ hφ₂
source
theorem qam.nontracial.trivial_graph {p : Type u_1} [fintype p] [decidable_eq p] [nonempty p] {φ : module.dual ℂ (matrix p p ℂ)} [hφ : fact φ.is_faithful_pos_map] {δ : ℂ} (hφ₂ : (φ.matrix)⁻¹.trace = δ) :
⇑(⇑schur_idempotent (qam.trivial_graph hφ hφ₂)) 1 = 1
source
theorem pi.qam.nontracial.trivial_graph {p : Type u_1} [fintype p] [decidable_eq p] {n : p → Type u_2} [Π (i : p), fintype (n i)] [Π (i : p), decidable_eq (n i)] {φ : Π (i : p), module.dual ℂ (matrix (n i) (n i) ℂ)} [nonempty p] [∀ (i : p), nontrivial (n i)] {δ : ℂ} [hφ : ∀ (i : p), fact (φ i).is_faithful_pos_map] (hφ₂ : ∀ (i : p), ((φ i).matrix)⁻¹.trace = δ) :
⇑(⇑schur_idempotent (pi.qam.trivial_graph hφ hφ₂)) 1 = 1
source
theorem qam.refl_idempotent_one_one_of_delta {p : Type u_1} [fintype p] [decidable_eq p] [nonempty p] {φ : module.dual ℂ (matrix p p ℂ)} [hφ : fact φ.is_faithful_pos_map] {δ : ℂ} (hφ₂ : (φ.matrix)⁻¹.trace = δ) :
⇑(⇑schur_idempotent 1) 1 = δ • 1
source
theorem pi.qam.refl_idempotent_one_one_of_delta {p : Type u_1} [fintype p] [decidable_eq p] {n : p → Type u_2} [Π (i : p), fintype (n i)] [Π (i : p), decidable_eq (n i)] {φ : Π (i : p), module.dual ℂ (matrix (n i) (n i) ℂ)} [nonempty p] [∀ (i : p), nontrivial (n i)] {δ : ℂ} [hφ : ∀ (i : p), fact (φ i).is_faithful_pos_map] (hφ₂ : ∀ (i : p), ((φ i).matrix)⁻¹.trace = δ) :
⇑(⇑schur_idempotent 1) 1 = δ • 1
source
theorem qam.lm.nontracial.is_unreflexive_iff_reflexive_add_one {p : Type u_1} [fintype p] [decidable_eq p] [nonempty p] {φ : module.dual ℂ (matrix p p ℂ)} [hφ : fact φ.is_faithful_pos_map] {δ : ℂ} (hφ₂ : (φ.matrix)⁻¹.trace = δ) (x : matrix p p ℂ →ₗ[ℂ] matrix p p ℂ) :
⇑(⇑schur_idempotent x) 1 = 0 ↔ ⇑(⇑schur_idempotent (δ⁻¹ • (x + 1))) 1 = 1
source
theorem pi.qam.lm.nontracial.is_unreflexive_iff_reflexive_add_one {p : Type u_1} [fintype p] [decidable_eq p] {n : p → Type u_2} [Π (i : p), fintype (n i)] [Π (i : p), decidable_eq (n i)] {φ : Π (i : p), module.dual ℂ (matrix (n i) (n i) ℂ)} [nonempty p] [∀ (i : p), nontrivial (n i)] {δ : ℂ} [hφ : ∀ (i : p), fact (φ i).is_faithful_pos_map] (hφ₂ : ∀ (i : p), ((φ i).matrix)⁻¹.trace = δ) (x : (Π (i : p), matrix (n i) (n i) ℂ) →ₗ[ℂ] Π (i : p), matrix (n i) (n i) ℂ) :
⇑(⇑schur_idempotent x) 1 = 0 ↔ ⇑(⇑schur_idempotent (δ⁻¹ • (x + 1))) 1 = 1
source
theorem qam.refl_idempotent_complete_graph_left {E : Type u_1} [normed_add_comm_group_of_ring E] [inner_product_space ℂ E] [finite_dimensional ℂ E] [is_scalar_tower ℂ E E] [smul_comm_class ℂ E E] (x : E →ₗ[ℂ] E) :
⇑(⇑schur_idempotent (qam.complete_graph E)) x = x
source
theorem qam.refl_idempotent_complete_graph_right {E : Type u_1} [normed_add_comm_group_of_ring E] [inner_product_space ℂ E] [finite_dimensional ℂ E] [is_scalar_tower ℂ E E] [smul_comm_class ℂ E E] (x : E →ₗ[ℂ] E) :
⇑(⇑schur_idempotent x) (qam.complete_graph E) = x
source
noncomputable def qam.complement' {E : Type u_1} [normed_add_comm_group_of_ring E] [inner_product_space ℂ E] [finite_dimensional ℂ E] [is_scalar_tower ℂ E E] [smul_comm_class ℂ E E] (x : E →ₗ[ℂ] E) :
E →ₗ[ℂ] E
Equations
source
theorem qam.nontracial.complement'.qam {E : Type u_1} [normed_add_comm_group_of_ring E] [inner_product_space ℂ E] [finite_dimensional ℂ E] [is_scalar_tower ℂ E E] [smul_comm_class ℂ E E] (x : E →ₗ[ℂ] E) :
⇑(⇑schur_idempotent x) x = x ↔ ⇑(⇑schur_idempotent (qam.complement' x)) (qam.complement' x) = qam.complement' x
source
theorem qam.nontracial.complement'.qam.is_real {p : Type u_1} [fintype p] [decidable_eq p] {φ : module.dual ℂ (matrix p p ℂ)} [hφ : fact φ.is_faithful_pos_map] (x : matrix p p ℂ →ₗ[ℂ] matrix p p ℂ) :
x.is_real ↔ (qam.complement' x).is_real
source
theorem pi.qam.nontracial.complement'.qam.is_real {p : Type u_1} [fintype p] [decidable_eq p] {n : p → Type u_2} [Π (i : p), fintype (n i)] [Π (i : p), decidable_eq (n i)] {φ : Π (i : p), module.dual ℂ (matrix (n i) (n i) ℂ)} [hφ : ∀ (i : p), fact (φ i).is_faithful_pos_map] (x : (Π (i : p), matrix (n i) (n i) ℂ) →ₗ[ℂ] Π (i : p), matrix (n i) (n i) ℂ) :
x.is_real ↔ (qam.complement' x).is_real
source
theorem qam.complement'_complement' {E : Type u_1} [normed_add_comm_group_of_ring E] [inner_product_space ℂ E] [finite_dimensional ℂ E] [is_scalar_tower ℂ E E] [smul_comm_class ℂ E E] (x : E →ₗ[ℂ] E) :
qam.complement' (qam.complement' x) = x
source
theorem qam.nontracial.complement'.ir_reflexive {E : Type u_1} [normed_add_comm_group_of_ring E] [inner_product_space ℂ E] [finite_dimensional ℂ E] [is_scalar_tower ℂ E E] [smul_comm_class ℂ E E] (x : E →ₗ[ℂ] E) (α : Prop) [decidable α] :
⇑(⇑schur_idempotent x) 1 = ite α 1 0 ↔ ⇑(⇑schur_idempotent (qam.complement' x)) 1 = ite α 0 1
source
def qam_reflexive {E : Type u_1} [normed_add_comm_group_of_ring E] [inner_product_space ℂ E] [finite_dimensional ℂ E] [is_scalar_tower ℂ E E] [smul_comm_class ℂ E E] (x : E →ₗ[ℂ] E) :
Prop
Equations
source
def qam_irreflexive {E : Type u_1} [normed_add_comm_group_of_ring E] [inner_product_space ℂ E] [finite_dimensional ℂ E] [is_scalar_tower ℂ E E] [smul_comm_class ℂ E E] (x : E →ₗ[ℂ] E) :
Prop
Equations
source
theorem qam.complement'_is_irreflexive_iff {E : Type u_1} [normed_add_comm_group_of_ring E] [inner_product_space ℂ E] [finite_dimensional ℂ E] [is_scalar_tower ℂ E E] [smul_comm_class ℂ E E] (x : E →ₗ[ℂ] E) :
qam_irreflexive (qam.complement' x) ↔ qam_reflexive x
source
theorem qam.complement'_is_reflexive_iff {E : Type u_1} [normed_add_comm_group_of_ring E] [inner_product_space ℂ E] [finite_dimensional ℂ E] [is_scalar_tower ℂ E E] [smul_comm_class ℂ E E] (x : E →ₗ[ℂ] E) :
qam_reflexive (qam.complement' x) ↔ qam_irreflexive x
source
noncomputable def qam.complement'' {p : Type u_1} [fintype p] [decidable_eq p] [nonempty p] {φ : module.dual ℂ (matrix p p ℂ)} {δ : ℂ} (hφ : fact φ.is_faithful_pos_map) (hφ₂ : (φ.matrix)⁻¹.trace = δ) (x : matrix p p ℂ →ₗ[ℂ] matrix p p ℂ) :
matrix p p ℂ →ₗ[ℂ] matrix p p ℂ
Equations
source
noncomputable def pi.qam.complement'' {p : Type u_1} [fintype p] [decidable_eq p] {n : p → Type u_2} [Π (i : p), fintype (n i)] [Π (i : p), decidable_eq (n i)] {φ : Π (i : p), module.dual ℂ (matrix (n i) (n i) ℂ)} [nonempty p] [∀ (i : p), nontrivial (n i)] {δ : ℂ} (hφ : ∀ (i : p), fact (φ i).is_faithful_pos_map) (hφ₂ : ∀ (i : p), ((φ i).matrix)⁻¹.trace = δ) (x : (Π (i : p), matrix (n i) (n i) ℂ) →ₗ[ℂ] Π (i : p), matrix (n i) (n i) ℂ) :
(Π (i : p), matrix (n i) (n i) ℂ) →ₗ[ℂ] Π (i : p), matrix (n i) (n i) ℂ
Equations
source
theorem single_schur_idempotent_real {p : Type u_1} [fintype p] [decidable_eq p] {φ : module.dual ℂ (matrix p p ℂ)} [hφ : fact φ.is_faithful_pos_map] (x y : matrix p p ℂ →ₗ[ℂ] matrix p p ℂ) :
(⇑(⇑schur_idempotent x) y).real = ⇑(⇑schur_idempotent y.real) x.real
source
theorem schur_idempotent_reflexive_of_is_real {p : Type u_1} [fintype p] [decidable_eq p] {φ : module.dual ℂ (matrix p p ℂ)} [hφ : fact φ.is_faithful_pos_map] {x : matrix p p ℂ →ₗ[ℂ] matrix p p ℂ} (hx : x.is_real) :
⇑(⇑schur_idempotent x) 1 = 1 ↔ ⇑(⇑schur_idempotent 1) x = 1
source
theorem pi.schur_idempotent_reflexive_of_is_real {p : Type u_1} [fintype p] [decidable_eq p] {n : p → Type u_2} [Π (i : p), fintype (n i)] [Π (i : p), decidable_eq (n i)] {φ : Π (i : p), module.dual ℂ (matrix (n i) (n i) ℂ)} [hφ : ∀ (i : p), fact (φ i).is_faithful_pos_map] {x : (Π (i : p), matrix (n i) (n i) ℂ) →ₗ[ℂ] Π (i : p), matrix (n i) (n i) ℂ} (hx : x.is_real) :
⇑(⇑schur_idempotent x) 1 = 1 ↔ ⇑(⇑schur_idempotent 1) x = 1
source
theorem qam.complement''_is_irreflexive_iff {p : Type u_1} [fintype p] [decidable_eq p] [nonempty p] {φ : module.dual ℂ (matrix p p ℂ)} {δ : ℂ} [hφ : fact φ.is_faithful_pos_map] (hφ₂ : (φ.matrix)⁻¹.trace = δ) {x : matrix p p ℂ →ₗ[ℂ] matrix p p ℂ} (hx : x.is_real) :
qam_irreflexive (qam.complement'' hφ hφ₂ x) ↔ qam_reflexive x
source
theorem pi.qam.complement''_is_irreflexive_iff {p : Type u_1} [fintype p] [decidable_eq p] {n : p → Type u_2} [Π (i : p), fintype (n i)] [Π (i : p), decidable_eq (n i)] {φ : Π (i : p), module.dual ℂ (matrix (n i) (n i) ℂ)} [nonempty p] [∀ (i : p), nontrivial (n i)] {δ : ℂ} [hφ : ∀ (i : p), fact (φ i).is_faithful_pos_map] (hφ₂ : ∀ (i : p), ((φ i).matrix)⁻¹.trace = δ) {x : (Π (i : p), matrix (n i) (n i) ℂ) →ₗ[ℂ] Π (i : p), matrix (n i) (n i) ℂ} (hx : x.is_real) :
qam_irreflexive (pi.qam.complement'' hφ hφ₂ x) ↔ qam_reflexive x
source
noncomputable def pi.qam.irreflexive_complement {p : Type u_1} [fintype p] [decidable_eq p] {n : p → Type u_2} [Π (i : p), fintype (n i)] [Π (i : p), decidable_eq (n i)] {φ : Π (i : p), module.dual ℂ (matrix (n i) (n i) ℂ)} [nonempty p] [∀ (i : p), nontrivial (n i)] {δ : ℂ} (hφ : ∀ (i : p), fact (φ i).is_faithful_pos_map) (hφ₂ : ∀ (i : p), ((φ i).matrix)⁻¹.trace = δ) (x : (Π (i : p), matrix (n i) (n i) ℂ) →ₗ[ℂ] Π (i : p), matrix (n i) (n i) ℂ) :
(Π (i : p), matrix (n i) (n i) ℂ) →ₗ[ℂ] Π (i : p), matrix (n i) (n i) ℂ
Equations
source
noncomputable def pi.qam.reflexive_complement {p : Type u_1} [fintype p] [decidable_eq p] {n : p → Type u_2} [Π (i : p), fintype (n i)] [Π (i : p), decidable_eq (n i)] {φ : Π (i : p), module.dual ℂ (matrix (n i) (n i) ℂ)} [nonempty p] [∀ (i : p), nontrivial (n i)] {δ : ℂ} (hφ : ∀ (i : p), fact (φ i).is_faithful_pos_map) (hφ₂ : ∀ (i : p), ((φ i).matrix)⁻¹.trace = δ) (x : (Π (i : p), matrix (n i) (n i) ℂ) →ₗ[ℂ] Π (i : p), matrix (n i) (n i) ℂ) :
(Π (i : p), matrix (n i) (n i) ℂ) →ₗ[ℂ] Π (i : p), matrix (n i) (n i) ℂ
Equations
source
theorem qam.nontracial.trivial_graph.is_real {p : Type u_1} [fintype p] [decidable_eq p] [nonempty p] {φ : module.dual ℂ (matrix p p ℂ)} [hφ : fact φ.is_faithful_pos_map] {δ : ℂ} (hφ₂ : (φ.matrix)⁻¹.trace = δ) :
(qam.trivial_graph hφ hφ₂).is_real
source
theorem pi.qam.nontracial.trivial_graph.is_real {p : Type u_1} [fintype p] [decidable_eq p] {n : p → Type u_2} [Π (i : p), fintype (n i)] [Π (i : p), decidable_eq (n i)] {φ : Π (i : p), module.dual ℂ (matrix (n i) (n i) ℂ)} [nonempty p] [∀ (i : p), nontrivial (n i)] {δ : ℂ} [hφ : ∀ (i : p), fact (φ i).is_faithful_pos_map] (hφ₂ : ∀ (i : p), ((φ i).matrix)⁻¹.trace = δ) :
(pi.qam.trivial_graph hφ hφ₂).is_real
source
theorem pi.qam.irreflexive_complement.is_real {p : Type u_1} [fintype p] [decidable_eq p] {n : p → Type u_2} [Π (i : p), fintype (n i)] [Π (i : p), decidable_eq (n i)] {φ : Π (i : p), module.dual ℂ (matrix (n i) (n i) ℂ)} [nonempty p] [∀ (i : p), nontrivial (n i)] {δ : ℂ} [hφ : ∀ (i : p), fact (φ i).is_faithful_pos_map] (hφ₂ : ∀ (i : p), ((φ i).matrix)⁻¹.trace = δ) {x : (Π (i : p), matrix (n i) (n i) ℂ) →ₗ[ℂ] Π (i : p), matrix (n i) (n i) ℂ} (hx : x.is_real) :
(pi.qam.irreflexive_complement hφ hφ₂ x).is_real
source
theorem pi.qam.reflexive_complement.is_real {p : Type u_1} [fintype p] [decidable_eq p] {n : p → Type u_2} [Π (i : p), fintype (n i)] [Π (i : p), decidable_eq (n i)] {φ : Π (i : p), module.dual ℂ (matrix (n i) (n i) ℂ)} [nonempty p] [∀ (i : p), nontrivial (n i)] {δ : ℂ} [hφ : ∀ (i : p), fact (φ i).is_faithful_pos_map] (hφ₂ : ∀ (i : p), ((φ i).matrix)⁻¹.trace = δ) {x : (Π (i : p), matrix (n i) (n i) ℂ) →ₗ[ℂ] Π (i : p), matrix (n i) (n i) ℂ} (hx : x.is_real) :
(pi.qam.reflexive_complement hφ hφ₂ x).is_real
source
theorem pi.qam.irreflexive_complement_irreflexive_complement {p : Type u_1} [fintype p] [decidable_eq p] {n : p → Type u_2} [Π (i : p), fintype (n i)] [Π (i : p), decidable_eq (n i)] {φ : Π (i : p), module.dual ℂ (matrix (n i) (n i) ℂ)} [nonempty p] [∀ (i : p), nontrivial (n i)] {δ : ℂ} [hφ : ∀ (i : p), fact (φ i).is_faithful_pos_map] (hφ₂ : ∀ (i : p), ((φ i).matrix)⁻¹.trace = δ) {x : (Π (i : p), matrix (n i) (n i) ℂ) →ₗ[ℂ] Π (i : p), matrix (n i) (n i) ℂ} :
pi.qam.irreflexive_complement hφ hφ₂ (pi.qam.irreflexive_complement hφ hφ₂ x) = x
source
theorem pi.qam.reflexive_complement_reflexive_complement {p : Type u_1} [fintype p] [decidable_eq p] {n : p → Type u_2} [Π (i : p), fintype (n i)] [Π (i : p), decidable_eq (n i)] {φ : Π (i : p), module.dual ℂ (matrix (n i) (n i) ℂ)} [nonempty p] [∀ (i : p), nontrivial (n i)] {δ : ℂ} [hφ : ∀ (i : p), fact (φ i).is_faithful_pos_map] (hφ₂ : ∀ (i : p), ((φ i).matrix)⁻¹.trace = δ) {x : (Π (i : p), matrix (n i) (n i) ℂ) →ₗ[ℂ] Π (i : p), matrix (n i) (n i) ℂ} :
pi.qam.reflexive_complement hφ hφ₂ (pi.qam.reflexive_complement hφ hφ₂ x) = x
source
theorem pi.qam.trivial_graph_reflexive_complement_eq_complete_graph {p : Type u_1} [fintype p] [decidable_eq p] {n : p → Type u_2} [Π (i : p), fintype (n i)] [Π (i : p), decidable_eq (n i)] {φ : Π (i : p), module.dual ℂ (matrix (n i) (n i) ℂ)} [nonempty p] [∀ (i : p), nontrivial (n i)] {δ : ℂ} [hφ : ∀ (i : p), fact (φ i).is_faithful_pos_map] (hφ₂ : ∀ (i : p), ((φ i).matrix)⁻¹.trace = δ) :
pi.qam.reflexive_complement hφ hφ₂ (pi.qam.trivial_graph hφ hφ₂) = qam.complete_graph (Π (i : p), matrix (n i) (n i) ℂ)
source
theorem pi.qam.complete_graph_reflexive_complement_eq_trivial_graph {p : Type u_1} [fintype p] [decidable_eq p] {n : p → Type u_2} [Π (i : p), fintype (n i)] [Π (i : p), decidable_eq (n i)] {φ : Π (i : p), module.dual ℂ (matrix (n i) (n i) ℂ)} [nonempty p] [∀ (i : p), nontrivial (n i)] {δ : ℂ} [hφ : ∀ (i : p), fact (φ i).is_faithful_pos_map] (hφ₂ : ∀ (i : p), ((φ i).matrix)⁻¹.trace = δ) :
pi.qam.reflexive_complement hφ hφ₂ (qam.complete_graph (Π (i : p), matrix (n i) (n i) ℂ)) = pi.qam.trivial_graph hφ hφ₂
source
theorem qam.complement'_eq {E : Type u_1} [normed_add_comm_group_of_ring E] [inner_product_space ℂ E] [finite_dimensional ℂ E] [is_scalar_tower ℂ E E] [smul_comm_class ℂ E E] (a : E →ₗ[ℂ] E) :
qam.complement' a = qam.complete_graph E - a
source
theorem pi.qam.irreflexive_complement_is_irreflexive_qam_iff_irreflexive_qam {p : Type u_1} [fintype p] [decidable_eq p] {n : p → Type u_2} [Π (i : p), fintype (n i)] [Π (i : p), decidable_eq (n i)] {φ : Π (i : p), module.dual ℂ (matrix (n i) (n i) ℂ)} [nonempty p] [∀ (i : p), nontrivial (n i)] {δ : ℂ} [hφ : ∀ (i : p), fact (φ i).is_faithful_pos_map] (hφ₂ : ∀ (i : p), ((φ i).matrix)⁻¹.trace = δ) {x : (Π (i : p), matrix (n i) (n i) ℂ) →ₗ[ℂ] Π (i : p), matrix (n i) (n i) ℂ} (hx : x.is_real) :
qam_irreflexive (pi.qam.irreflexive_complement hφ hφ₂ x) ↔ qam_irreflexive x
source
theorem pi.qam.reflexive_complment_is_reflexive_qam_iff_reflexive_qam {p : Type u_1} [fintype p] [decidable_eq p] {n : p → Type u_2} [Π (i : p), fintype (n i)] [Π (i : p), decidable_eq (n i)] {φ : Π (i : p), module.dual ℂ (matrix (n i) (n i) ℂ)} [nonempty p] [∀ (i : p), nontrivial (n i)] {δ : ℂ} [hφ : ∀ (i : p), fact (φ i).is_faithful_pos_map] (hφ₂ : ∀ (i : p), ((φ i).matrix)⁻¹.trace = δ) {x : (Π (i : p), matrix (n i) (n i) ℂ) →ₗ[ℂ] Π (i : p), matrix (n i) (n i) ℂ} (hx : x.is_real) :
qam_reflexive (pi.qam.reflexive_complement hφ hφ₂ x) ↔ qam_reflexive x