mathlib3 documentation

monlib / quantum_graph.qam_A_example

Examples of single-edged quantum graph #

This file contains examples of single-edged quantum graphs over M₂(ℂ). The main result is that all single-edged quantum graphs over M₂(ℂ) are isomorphic each other.

source
def trace_module_dual {𝕜 : Type u_1} {n : Type u_2} [fintype n] [is_R_or_C 𝕜] :
module.dual 𝕜 (matrix n n 𝕜)
Equations
source
@[instance]
def trace_is_faithful_pos_map {n : Type u_1} [fintype n] {𝕜 : Type u_2} [is_R_or_C 𝕜] :
fact trace_module_dual.is_faithful_pos_map
source
theorem trace_module_dual_matrix {n : Type u_1} [fintype n] [decidable_eq n] :
trace_module_dual.matrix = 1
source
theorem pos_def_one_rpow (n : Type u_1) [fintype n] [decidable_eq n] (r : ℝ) :
matrix.pos_def_one.rpow r = 1
source
theorem matrix.std_basis_matrix.transpose {R : Type u_1} {n : Type u_2} {m : Type u_3} [decidable_eq n] [decidable_eq m] [semiring R] (i : n) (j : m) :
(matrix.std_basis_matrix i j 1).transpose = matrix.std_basis_matrix j i 1
source
def pi_prod_unit_equiv_pi {R : Type u_1} {n : Type u_2} [semiring R] :
(n × unit → R) ≃ₗ[R] n → R

obviously, n × unit → R is linearly equiv to n → R

Equations
source
def matrix.of_col {R : Type u_1} {n : Type u_2} [semiring R] :
matrix n unit R ≃ₗ[R] n → R

matrix.col written as a linear equivalence

Equations
source
def matrix_prod_unit_right {R : Type u_1} {n : Type u_2} {m : Type u_3} [semiring R] :
matrix n (m × unit) R ≃ₗ[R] matrix n m R

obviously, matrix n (m × unit) is linearly equivalent to matrix n m R

Equations
source
theorem col_mul_col_conj_transpose_is_kronecker_of_vectors {R : Type u_1} {m : Type u_2} {n : Type u_3} {p : Type u_4} {q : Type u_5} [semiring R] [has_star R] (x : matrix m n R) (y : matrix p q R) :
(matrix.col (⇑matrix.reshape x)).mul (matrix.col (⇑matrix.reshape y)).conj_transpose = ⇑(matrix.reshape.symm) (⇑matrix.of_col (⇑matrix_prod_unit_right (matrix.kronecker_map has_mul.mul (matrix.col (⇑matrix.reshape x)) (matrix.col (⇑matrix.reshape y.conj)))))

vec_mul_vec (reshape x) (star (reshape y)) written as a kronecker product of their corresponding vectors (via reshape).

source
theorem star_alg_equiv.eq_comp_iff {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} {E₃ : Type u_4} [comm_semiring R] [semiring E₂] [semiring E₃] [add_comm_monoid E₁] [algebra R E₂] [algebra R E₃] [module R E₁] [has_star E₂] [has_star E₃] (f : E₂ ≃⋆ₐ[R] E₃) (x : E₁ →ₗ[R] E₂) (y : E₁ →ₗ[R] E₃) :
f.to_alg_equiv.to_linear_map.comp x = y ↔ x = f.symm.to_alg_equiv.to_linear_map.comp y
source
theorem ite_comp {R : Type u_1} {U : Type u_2} {V : Type u_3} {W : Type u_4} [semiring R] [add_comm_monoid U] [add_comm_monoid V] [add_comm_monoid W] [module R U] [module R V] [module R W] {P : Prop} [decidable P] {x y : W →ₗ[R] U} {f : V →ₗ[R] W} :
(ite P x y).comp f = ite P (x.comp f) (y.comp f)
source
theorem comp_ite {R : Type u_1} {U : Type u_2} {V : Type u_3} {W : Type u_4} [semiring R] [add_comm_monoid U] [add_comm_monoid V] [add_comm_monoid W] [module R U] [module R V] [module R W] {P : Prop} [decidable P] {x y : W →ₗ[R] U} {f : U →ₗ[R] V} :
f.comp (ite P x y) = ite P (f.comp x) (f.comp y)
source
theorem star_alg_equiv.comp_symm_self {R : Type u_1} {U : Type u_2} {V : Type u_3} [comm_semiring R] [semiring U] [semiring V] [algebra R U] [algebra R V] [has_star U] [has_star V] {f : U ≃⋆ₐ[R] V} :
f.to_alg_equiv.to_linear_map.comp f.symm.to_alg_equiv.to_linear_map = 1
source
theorem star_alg_equiv.symm_comp_self {R : Type u_1} {U : Type u_2} {V : Type u_3} [comm_semiring R] [semiring U] [semiring V] [algebra R U] [algebra R V] [has_star U] [has_star V] {f : U ≃⋆ₐ[R] V} :
f.symm.to_alg_equiv.to_linear_map.comp f.to_alg_equiv.to_linear_map = 1
source
theorem qam.iso_preserves_ir_reflexive {n : Type u_1} [fintype n] [decidable_eq n] [nontrivial n] {φ : module.dual ℂ (matrix n n ℂ)} [hφ : fact φ.is_faithful_pos_map] {x y : matrix n n ℂ →ₗ[ℂ] matrix n n ℂ} (hxhy : qam.iso x y) (ir_reflexive : Prop) [decidable ir_reflexive] :
⇑(⇑(qam.refl_idempotent _) x) 1 = ite ir_reflexive 1 0 ↔ ⇑(⇑(qam.refl_idempotent _) y) 1 = ite ir_reflexive 1 0
source
def function.is_almost_injective {A : Type u_1} {B : Type u_2} (f : A → B) [has_smul ℂˣ A] :
Prop

a function f : A → B is almost injective if for all $x, y \in A$, if $f(x)=f(y)$ then there exists some $0\neq\alpha \in \mathbb{C}$ such that $x = \alpha y$ (in other words, $x$ and $y$ are co-linear)

Equations
source
theorem matrix.is_almost_hermitian.spectrum {n : Type u_1} [fintype n] [decidable_eq n] {x : matrix n n ℂ} (hx : x.is_almost_hermitian) :
spectrum ℂ (⇑matrix.to_lin' x) = {x_1 : ℂ | ∃ (i : n), hx.eigenvalues i = x_1}
source
theorem matrix.is_hermitian.eigenvalues_eq_zero_iff {n : Type u_1} [fintype n] [decidable_eq n] {x : matrix n n ℂ} (hx : x.is_hermitian) :
coe ∘ hx.eigenvalues = 0 ↔ x = 0
source
theorem spectra_fin_two {x : matrix (fin 2) (fin 2) ℂ} (hx : x.is_almost_hermitian) :
hx.spectra = {hx.eigenvalues 0, hx.eigenvalues 1}
source
theorem spectra_fin_two' {x : matrix (fin 2) (fin 2) ℂ} (hx : x.is_almost_hermitian) :
hx.spectra = ↑[hx.eigenvalues 0, hx.eigenvalues 1]
source
theorem spectra_fin_two'' {α : Type u_1} (a : fin 2 → α) :
multiset.map a finset.univ.val = {a 0, a 1}
source
theorem list.coe_inj {α : Type u_1} (l₁ l₂ : list α) :
↑l₁ = ↑l₂ ↔ l₁ ~ l₂
source
theorem spectra_fin_two_ext_aux {A : Type u_1} (α β γ : A) :
{α, α} = {β, γ} ↔ α = β ∧ α = γ
source
theorem spectra_fin_two_ext {α : Type u_1} (α₁ α₂ β₁ β₂ : α) :
{α₁, α₂} = {β₁, β₂} ↔ α₁ = β₁ ∧ α₂ = β₂ ∨ α₁ = β₂ ∧ α₂ = β₁
source
@[instance]
def multiset.has_smul {α : Type u_1} [has_smul ℂ α] :
has_smul ℂ (multiset α)
Equations
source
theorem multiset.smul_fin_two {α : Type u_1} [has_smul ℂ α] (a b : α) (c : ℂ) :
c • {a, b} = {c • a, c • b}
source
theorem is_almost_hermitian.smul_eq {n : Type u_1} [fintype n] [decidable_eq n] {x : matrix n n ℂ} (hx : x.is_almost_hermitian) (c : ℂ) :
_.scalar • _.matrix = c • x
source
theorem spectra_fin_two_ext_of_traceless {α₁ α₂ β₁ β₂ : ℂ} (hα₂ : α₂ ≠ 0) (hβ₂ : β₂ ≠ 0) (h₁ : α₁ = -α₂) (h₂ : β₁ = -β₂) :
∃ (c : ℂˣ), {α₁, α₂} = ↑c • {β₁, β₂}
source
theorem matrix.is_almost_hermitian.trace {n : Type u_1} [fintype n] [decidable_eq n] {x : matrix n n ℂ} (hx : x.is_almost_hermitian) :
x.trace = finset.univ.sum (λ (i : n), hx.eigenvalues i)
source
noncomputable def matrix.is_almost_hermitian.eigenvector_matrix {n : Type u_1} [fintype n] [decidable_eq n] {x : matrix n n ℂ} (hx : x.is_almost_hermitian) :
matrix n n ℂ
Equations
source
theorem matrix.is_almost_hermitian.eigenvector_matrix_eq {n : Type u_1} [fintype n] [decidable_eq n] {x : matrix n n ℂ} (hx : x.is_almost_hermitian) :
hx.eigenvector_matrix = _.eigenvector_matrix
source
theorem matrix.is_almost_hermitian.eigenvector_matrix_mem_unitary_group {n : Type u_1} [fintype n] [decidable_eq n] {x : matrix n n ℂ} (hx : x.is_almost_hermitian) :
hx.eigenvector_matrix ∈ matrix.unitary_group n ℂ
source
theorem matrix.is_almost_hermitian.spectral_theorem' {n : Type u_1} [fintype n] [decidable_eq n] {x : matrix n n ℂ} (hx : x.is_almost_hermitian) :
x = hx.scalar • ⇑(matrix.inner_aut ⟨_.eigenvector_matrix, _⟩) (matrix.diagonal (coe ∘ _.eigenvalues))
source
theorem matrix.is_almost_hermitian.eigenvalues_eq {n : Type u_1} [fintype n] [decidable_eq n] {x : matrix n n ℂ} (hx : x.is_almost_hermitian) :
hx.eigenvalues = hx.scalar • coe ∘ _.eigenvalues
source
theorem matrix.is_almost_hermitian.spectral_theorem {n : Type u_1} [fintype n] [decidable_eq n] {x : matrix n n ℂ} (hx : x.is_almost_hermitian) :
x = ⇑(matrix.inner_aut ⟨hx.eigenvector_matrix, _⟩) (matrix.diagonal hx.eigenvalues)
source
theorem matrix.is_almost_hermitian.eigenvalues_eq_zero_iff {n : Type u_1} [fintype n] [decidable_eq n] {x : matrix n n ℂ} (hx : x.is_almost_hermitian) :
hx.eigenvalues = 0 ↔ x = 0
source
theorem matrix.diagonal_eq_zero_iff {n : Type u_1} [fintype n] [decidable_eq n] {x : n → ℂ} :
matrix.diagonal x = 0 ↔ x = 0
source
theorem qam_A.fin_two_iso (x y : {x // x ≠ 0}) (hx1 : is_self_adjoint (qam_A _ x)) (hx2 : ⇑(⇑(qam.refl_idempotent _) (qam_A _ x)) 1 = 0) (hy1 : is_self_adjoint (qam_A _ y)) (hy2 : ⇑(⇑(qam.refl_idempotent _) (qam_A _ y)) 1 = 0) :
qam.iso (qam_A _ x) (qam_A _ y)
source
theorem qam.fin_two_iso_of_single_edge {A B : matrix (fin 2) (fin 2) ℂ →ₗ[ℂ] matrix (fin 2) (fin 2) ℂ} (hx0 : real_qam _ A) (hy0 : real_qam _ B) (hx : hx0.edges = 1) (hy : hy0.edges = 1) (hx1 : is_self_adjoint A) (hx2 : ⇑(⇑(qam.refl_idempotent _) A) 1 = 0) (hy1 : is_self_adjoint B) (hy2 : ⇑(⇑(qam.refl_idempotent _) B) 1 = 0) :
qam.iso A B