mathlib3 documentation

monlib / quantum_graph.symm

@[simp]

theorem linear_equiv.symm_map_symm_apply (R : Type u_1) [is_R_or_C R] (M : Type u_2) [normed_add_comm_group M] [inner_product_space R M] [star_add_monoid M] [star_module R M] [finite_dimensional R M] (f : M →ₗ[R] M) :

⇑((linear_equiv.symm_map R M).symm) f = (⇑linear_map.adjoint f).real

@[simp]

theorem linear_equiv.symm_map_apply (R : Type u_1) [is_R_or_C R] (M : Type u_2) [normed_add_comm_group M] [inner_product_space R M] [star_add_monoid M] [star_module R M] [finite_dimensional R M] (f : M →ₗ[R] M) :

⇑(linear_equiv.symm_map R M) f = ⇑linear_map.adjoint f.real

noncomputable def linear_equiv.symm_map (R : Type u_1) [is_R_or_C R] (M : Type u_2) [normed_add_comm_group M] [inner_product_space R M] [star_add_monoid M] [star_module R M] [finite_dimensional R M] :

(M →ₗ[R] M) ≃ₗ[R] M →ₗ[R] M

Equations

linear_equiv.symm_map R M = {to_fun := λ (f : M →ₗ[R] M), ⇑linear_map.adjoint f.real, map_add' := _, map_smul' := _, inv_fun := λ (f : M →ₗ[R] M), (⇑linear_map.adjoint f).real, left_inv := _, right_inv := _}

theorem linear_equiv.symm_map_real {R : Type u_1} [is_R_or_C R] {M : Type u_2} [normed_add_comm_group M] [inner_product_space R M] [star_add_monoid M] [star_module R M] [finite_dimensional R M] :

↑(linear_equiv.symm_map R M).real = ↑((linear_equiv.symm_map R M).symm)

theorem linear_equiv.symm_map_rank_one_apply {n : Type u_1} [fintype n] [decidable_eq n] {s : n → Type u_2} [Π (i : n), fintype (s i)] [Π (i : n), decidable_eq (s i)] {ψ : Π (i : n), module.dual ℂ (matrix (s i) (s i) ℂ)} [hψ : ∀ (i : n), fact (ψ i).is_faithful_pos_map] (a b : Π (i : n), matrix (s i) (s i) ℂ) :

⇑(linear_equiv.symm_map ℂ (Π (i : n), matrix (s i) (s i) ℂ)) ↑(rank_one a b) = ↑(rank_one (⇑(module.dual.pi.is_faithful_pos_map.sig hψ (-1)) (has_star.star b)) (has_star.star a))

theorem linear_equiv.symm_map_symm_rank_one_apply {n : Type u_1} [fintype n] [decidable_eq n] {s : n → Type u_2} [Π (i : n), fintype (s i)] [Π (i : n), decidable_eq (s i)] {ψ : Π (i : n), module.dual ℂ (matrix (s i) (s i) ℂ)} [hψ : ∀ (i : n), fact (ψ i).is_faithful_pos_map] (a b : Π (i : n), matrix (s i) (s i) ℂ) :

⇑((linear_equiv.symm_map ℂ (Π (i : n), matrix (s i) (s i) ℂ)).symm) ↑(rank_one a b) = ↑(rank_one (has_star.star b) (⇑(module.dual.pi.is_faithful_pos_map.sig hψ (-1)) (has_star.star a)))

theorem pi.symm_map_eq {n : Type u_1} [fintype n] [decidable_eq n] {s : n → Type u_2} [Π (i : n), fintype (s i)] [Π (i : n), decidable_eq (s i)] {ψ : Π (i : n), module.dual ℂ (matrix (s i) (s i) ℂ)} [hψ : ∀ (i : n), fact (ψ i).is_faithful_pos_map] (f : (Π (i : n), matrix (s i) (s i) ℂ) →ₗ[ℂ ] Π (i : n), matrix (s i) (s i) ℂ) :

⇑(linear_equiv.symm_map ℂ (Π (i : n), matrix (s i) (s i) ℂ)) f = ↑(tensor_product.lid ℂ (Π (i : n), matrix (s i) (s i) ℂ)).comp (↑(tensor_product.comm ℂ (Π (i : n), matrix (s i) (s i) ℂ) ℂ).comp ((tensor_product.map 1 ((⇑linear_map.adjoint (algebra.linear_map ℂ (Π (i : n), matrix (s i) (s i) ℂ))).comp (linear_map.mul' ℂ (Π (i : n), matrix (s i) (s i) ℂ)))).comp (↑(tensor_product.assoc ℂ (Π (i : n), matrix (s i) (s i) ℂ) (Π (i : n), matrix (s i) (s i) ℂ) (Π (i : n), matrix (s i) (s i) ℂ)).comp ((tensor_product.map (tensor_product.map 1 f) 1).comp ((tensor_product.map ((⇑linear_map.adjoint (linear_map.mul' ℂ (Π (i : n), matrix (s i) (s i) ℂ))).comp (algebra.linear_map ℂ (Π (i : n), matrix (s i) (s i) ℂ))) 1).comp ↑((tensor_product.lid ℂ (Π (i : n), matrix (s i) (s i) ℂ)).symm))))))

theorem pi.symm_map_symm_eq {n : Type u_1} [fintype n] [decidable_eq n] {s : n → Type u_2} [Π (i : n), fintype (s i)] [Π (i : n), decidable_eq (s i)] {ψ : Π (i : n), module.dual ℂ (matrix (s i) (s i) ℂ)} [hψ : ∀ (i : n), fact (ψ i).is_faithful_pos_map] (f : (Π (i : n), matrix (s i) (s i) ℂ) →ₗ[ℂ ] Π (i : n), matrix (s i) (s i) ℂ) :

⇑((linear_equiv.symm_map ℂ (Π (i : n), matrix (s i) (s i) ℂ)).symm) f = ↑(tensor_product.lid ℂ (Π (i : n), matrix (s i) (s i) ℂ)).comp ((tensor_product.map ((⇑linear_map.adjoint (algebra.linear_map ℂ (Π (i : n), matrix (s i) (s i) ℂ))).comp (linear_map.mul' ℂ (Π (i : n), matrix (s i) (s i) ℂ))) 1).comp ((tensor_product.map (tensor_product.map 1 f) 1).comp (↑((tensor_product.assoc ℂ (Π (i : n), matrix (s i) (s i) ℂ) (Π (i : n), matrix (s i) (s i) ℂ) (Π (i : n), matrix (s i) (s i) ℂ)).symm).comp ((tensor_product.map 1 ((⇑linear_map.adjoint (linear_map.mul' ℂ (Π (i : n), matrix (s i) (s i) ℂ))).comp (algebra.linear_map ℂ (Π (i : n), matrix (s i) (s i) ℂ)))).comp (↑((tensor_product.comm ℂ (Π (i : n), matrix (s i) (s i) ℂ) ℂ).symm).comp ↑((tensor_product.lid ℂ (Π (i : n), matrix (s i) (s i) ℂ)).symm))))))

theorem pi.symm_map_tfae {n : Type u_1} [fintype n] [decidable_eq n] {s : n → Type u_2} [Π (i : n), fintype (s i)] [Π (i : n), decidable_eq (s i)] {ψ : Π (i : n), module.dual ℂ (matrix (s i) (s i) ℂ)} [hψ : ∀ (i : n), fact (ψ i).is_faithful_pos_map] (A : (Π (i : n), matrix (s i) (s i) ℂ) →ₗ[ℂ ] Π (i : n), matrix (s i) (s i) ℂ) :

[⇑(linear_equiv.symm_map ℂ (Π (i : n), matrix (s i) (s i) ℂ)) A = A, ⇑((linear_equiv.symm_map ℂ (Π (i : n), matrix (s i) (s i) ℂ)).symm) A = A, A.real = ⇑linear_map.adjoint A, ∀ (x : Π (i : n), matrix (s i) (s i) ℂ) (y : Π (i : n), matrix ((λ (i : n), s i) i) ((λ (i : n), s i) i) ℂ), ⇑(module.dual.pi ψ) (⇑A x * y) = ⇑(module.dual.pi ψ) (x * ⇑A y)].tfae

theorem commute_real_real {R : Type u_1} {A : Type u_2} [semiring R] [star_ring R] [add_comm_monoid A] [module R A] [star_add_monoid A] [star_module R A] (f g : A →ₗ[R] A) :

commute f.real g.real ↔ commute f g

theorem module.dual.pi.is_faithful_pos_map.sig_real {n : Type u_1} [fintype n] [decidable_eq n] {s : n → Type u_2} [Π (i : n), fintype (s i)] [Π (i : n), decidable_eq (s i)] {ψ : Π (i : n), module.dual ℂ (matrix (s i) (s i) ℂ)} [hψ : ∀ (i : n), fact (ψ i).is_faithful_pos_map] :

(module.dual.pi.is_faithful_pos_map.sig hψ 1).to_linear_map.real = (module.dual.pi.is_faithful_pos_map.sig hψ (-1)).to_linear_map

theorem pi.commute_sig_pos_neg {n : Type u_1} [fintype n] [decidable_eq n] {s : n → Type u_2} [Π (i : n), fintype (s i)] [Π (i : n), decidable_eq (s i)] {ψ : Π (i : n), module.dual ℂ (matrix (s i) (s i) ℂ)} [hψ : ∀ (i : n), fact (ψ i).is_faithful_pos_map] (r : ℝ) (x : (Π (i : n), matrix (s i) (s i) ℂ) →ₗ[ℂ ] Π (i : n), matrix (s i) (s i) ℂ) :

commute x (module.dual.pi.is_faithful_pos_map.sig hψ r).to_linear_map ↔ commute x (module.dual.pi.is_faithful_pos_map.sig hψ (-r)).to_linear_map

theorem pi.symm_map_apply_eq_symm_map_symm_apply_iff {n : Type u_1} [fintype n] [decidable_eq n] {s : n → Type u_2} [Π (i : n), fintype (s i)] [Π (i : n), decidable_eq (s i)] {ψ : Π (i : n), module.dual ℂ (matrix (s i) (s i) ℂ)} [hψ : ∀ (i : n), fact (ψ i).is_faithful_pos_map] (A : (Π (i : n), matrix (s i) (s i) ℂ) →ₗ[ℂ ] Π (i : n), matrix (s i) (s i) ℂ) :

⇑(linear_equiv.symm_map ℂ (Π (i : n), matrix (s i) (s i) ℂ)) A = ⇑((linear_equiv.symm_map ℂ (Π (i : n), matrix (s i) (s i) ℂ)).symm) A ↔ commute A (module.dual.pi.is_faithful_pos_map.sig hψ 1).to_linear_map

theorem Psi.real_apply {n : Type u_1} [fintype n] [decidable_eq n] {s : n → Type u_2} [Π (i : n), fintype (s i)] [Π (i : n), decidable_eq (s i)] {ψ : Π (i : n), module.dual ℂ (matrix (s i) (s i) ℂ)} [hψ : ∀ (i : n), fact (ψ i).is_faithful_pos_map] (r₁ r₂ : ℝ) (A : (Π (i : n), matrix (s i) (s i) ℂ) →ₗ[ℂ ] Π (i : n), matrix (s i) (s i) ℂ) :

⇑(module.dual.pi.is_faithful_pos_map.Psi hψ r₁ r₂) A.real = ⇑(tensor_product.map (module.dual.pi.is_faithful_pos_map.sig hψ (2 * r₁)).to_linear_map ((op.comp (module.dual.pi.is_faithful_pos_map.sig hψ (1 - 2 * r₂)).to_linear_map).comp unop)) (has_star.star (⇑(module.dual.pi.is_faithful_pos_map.Psi hψ r₁ r₂) A))

theorem Psi.adjoint_apply {n : Type u_1} [fintype n] [decidable_eq n] {s : n → Type u_2} [Π (i : n), fintype (s i)] [Π (i : n), decidable_eq (s i)] {ψ : Π (i : n), module.dual ℂ (matrix (s i) (s i) ℂ)} [hψ : ∀ (i : n), fact (ψ i).is_faithful_pos_map] (r₁ r₂ : ℝ) (A : (Π (i : n), matrix (s i) (s i) ℂ) →ₗ[ℂ ] Π (i : n), matrix (s i) (s i) ℂ) :

⇑(module.dual.pi.is_faithful_pos_map.Psi hψ r₁ r₂) (⇑linear_map.adjoint A) = ⇑(tensor_product.map (module.dual.pi.is_faithful_pos_map.sig hψ (r₁ - r₂)).to_linear_map (op.comp ((module.dual.pi.is_faithful_pos_map.sig hψ (r₁ - r₂)).to_linear_map.comp unop))) (⇑ten_swap (has_star.star (⇑(module.dual.pi.is_faithful_pos_map.Psi hψ r₁ r₂) A)))

theorem Psi.symm_map_apply {n : Type u_1} [fintype n] [decidable_eq n] {s : n → Type u_2} [Π (i : n), fintype (s i)] [Π (i : n), decidable_eq (s i)] {ψ : Π (i : n), module.dual ℂ (matrix (s i) (s i) ℂ)} [hψ : ∀ (i : n), fact (ψ i).is_faithful_pos_map] (r₁ r₂ : ℝ) (A : (Π (i : n), matrix (s i) (s i) ℂ) →ₗ[ℂ ] Π (i : n), matrix (s i) (s i) ℂ) :

⇑(module.dual.pi.is_faithful_pos_map.Psi hψ r₁ r₂) (⇑(linear_equiv.symm_map ℂ (Π (i : n), matrix (s i) (s i) ℂ)) A) = ⇑(tensor_product.map (module.dual.pi.is_faithful_pos_map.sig hψ (r₁ + r₂ - 1)).to_linear_map (op.comp ((module.dual.pi.is_faithful_pos_map.sig hψ (-r₁ - r₂)).to_linear_map.comp unop))) (⇑ten_swap (⇑(module.dual.pi.is_faithful_pos_map.Psi hψ r₁ r₂) A))

theorem Psi.symm_map_symm_apply {n : Type u_1} [fintype n] [decidable_eq n] {s : n → Type u_2} [Π (i : n), fintype (s i)] [Π (i : n), decidable_eq (s i)] {ψ : Π (i : n), module.dual ℂ (matrix (s i) (s i) ℂ)} [hψ : ∀ (i : n), fact (ψ i).is_faithful_pos_map] (r₁ r₂ : ℝ) (A : (Π (i : n), matrix (s i) (s i) ℂ) →ₗ[ℂ ] Π (i : n), matrix (s i) (s i) ℂ) :

⇑(module.dual.pi.is_faithful_pos_map.Psi hψ r₁ r₂) (⇑((linear_equiv.symm_map ℂ (Π (i : n), matrix (s i) (s i) ℂ)).symm) A) = ⇑(tensor_product.map (module.dual.pi.is_faithful_pos_map.sig hψ (r₁ + r₂)).to_linear_map (op.comp ((module.dual.pi.is_faithful_pos_map.sig hψ (1 - r₁ - r₂)).to_linear_map.comp unop))) (⇑ten_swap (⇑(module.dual.pi.is_faithful_pos_map.Psi hψ r₁ r₂) A))