mathlib3 documentation

monlib / quantum_graph.schur_idempotent

Schur idempotent operator #

In this file we define the Schur idempotent operator and prove some basic properties.

@[protected, instance]

noncomputable def module.dual.is_normed_add_comm_group_of_ring {n : Type u_1} [fintype n] [decidable_eq n] {ψ : module.dual ℂ (matrix n n ℂ)} [hψ : fact ψ.is_faithful_pos_map] :

normed_add_comm_group_of_ring (matrix n n ℂ)

Equations

module.dual.is_normed_add_comm_group_of_ring = {to_has_norm := normed_add_comm_group.to_has_norm module.dual.is_faithful_pos_map.normed_add_comm_group, to_ring := matrix.ring complex.ring, to_metric_space := normed_add_comm_group.to_metric_space module.dual.is_faithful_pos_map.normed_add_comm_group, dist_eq := _}

@[protected, instance]

noncomputable def pi.module.dual.is_normed_add_comm_group_of_ring {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] :

normed_add_comm_group_of_ring (Π (i : n), matrix (s i) (s i) ℂ)

Equations

pi.module.dual.is_normed_add_comm_group_of_ring = {to_has_norm := normed_add_comm_group.to_has_norm module.dual.pi.normed_add_comm_group, to_ring := normed_add_comm_group_of_ring.to_ring pi.normed_add_comm_group_of_ring, to_metric_space := normed_add_comm_group.to_metric_space module.dual.pi.normed_add_comm_group, dist_eq := _}

noncomputable def schur_idempotent {B : Type u_1} [normed_add_comm_group_of_ring B] [inner_product_space ℂ B] [smul_comm_class ℂ B B] [is_scalar_tower ℂ B B] [finite_dimensional ℂ B] :

(B →ₗ[ℂ ] B) →ₗ[ℂ ] (B →ₗ[ℂ ] B) →ₗ[ℂ ] B →ₗ[ℂ ] B

Equations

schur_idempotent = {to_fun := λ (x : B →ₗ[ℂ ] B), {to_fun := λ (y : B →ₗ[ℂ ] B), (linear_map.mul' ℂ B).comp ((tensor_product.map x y).comp (⇑linear_map.adjoint (linear_map.mul' ℂ B))), map_add' := _, map_smul' := _}, map_add' := _, map_smul' := _}

theorem schur_idempotent.apply_rank_one {B : Type u_1} [normed_add_comm_group_of_ring B] [inner_product_space ℂ B] [smul_comm_class ℂ B B] [is_scalar_tower ℂ B B] [finite_dimensional ℂ B] (a b c d : B) :

⇑(⇑schur_idempotent ↑(rank_one a b)) ↑(rank_one c d) = ↑(rank_one (a * c) (b * d))

theorem schur_idempotent_one_one_right {B : Type u_1} [normed_add_comm_group_of_ring B] [inner_product_space ℂ B] [smul_comm_class ℂ B B] [is_scalar_tower ℂ B B] [finite_dimensional ℂ B] (A : B →ₗ[ℂ ] B) :

⇑(⇑schur_idempotent A) ↑(rank_one 1 1) = A

theorem schur_idempotent_one_one_left {B : Type u_1} [normed_add_comm_group_of_ring B] [inner_product_space ℂ B] [smul_comm_class ℂ B B] [is_scalar_tower ℂ B B] [finite_dimensional ℂ B] (A : B →ₗ[ℂ ] B) :

⇑(⇑schur_idempotent ↑(rank_one 1 1)) A = A

theorem lmul_adjoint {B : Type u_1} [normed_add_comm_group_of_ring B] [inner_product_space ℂ B] [smul_comm_class ℂ B B] [is_scalar_tower ℂ B B] [finite_dimensional ℂ B] [star_semigroup B] {ψ : module.dual ℂ B} (hψ : ∀ (a b : B), has_inner.inner a b = ⇑ψ (has_star.star a * b)) (a : B) :

⇑linear_map.adjoint (⇑lmul a) = ⇑lmul (has_star.star a)

theorem rmul_adjoint {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) ℂ) :

⇑linear_map.adjoint (⇑rmul a) = ⇑rmul (⇑(module.dual.pi.is_faithful_pos_map.sig hψ (-1)) (has_star.star a))

theorem continuous_linear_map.linear_map_adjoint {𝕜 : Type u_1} {B : Type u_2} {C : Type u_3} [is_R_or_C 𝕜] [normed_add_comm_group B] [normed_add_comm_group C] [inner_product_space 𝕜 B] [inner_product_space 𝕜 C] [finite_dimensional 𝕜 B] [finite_dimensional 𝕜 C] (x : B →L[𝕜] C) :

⇑linear_map.adjoint ↑x = ↑(⇑continuous_linear_map.adjoint x)

theorem schur_idempotent_adjoint {B : Type u_1} [normed_add_comm_group_of_ring B] [inner_product_space ℂ B] [smul_comm_class ℂ B B] [is_scalar_tower ℂ B B] [finite_dimensional ℂ B] (x y : B →ₗ[ℂ ] B) :

⇑linear_map.adjoint (⇑(⇑schur_idempotent x) y) = ⇑(⇑schur_idempotent (⇑linear_map.adjoint x)) (⇑linear_map.adjoint y)

theorem schur_idempotent_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] (x y : (Π (i : n), matrix (s i) (s i) ℂ) →ₗ[ℂ ] Π (i : n), matrix (s i) (s i) ℂ) :

(⇑(⇑schur_idempotent x) y).real = ⇑(⇑schur_idempotent y.real) x.real

theorem schur_idempotent_one_right_rank_one {B : Type u_1} [normed_add_comm_group_of_ring B] [inner_product_space ℂ B] [smul_comm_class ℂ B B] [is_scalar_tower ℂ B B] [finite_dimensional ℂ B] [star_semigroup B] {ψ : module.dual ℂ B} (hψ : ∀ (a b : B), has_inner.inner a b = ⇑ψ (has_star.star a * b)) (a b : B) :

⇑(⇑schur_idempotent ↑(rank_one a b)) 1 = ⇑lmul a * ⇑linear_map.adjoint (⇑lmul b)

theorem matrix.cast_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 j : n} (x : matrix (s i) (s i) ℂ) (h : i = j) (p q : s j) :

_.mp x p q = x (_.mpr p) (_.mpr q)

theorem matrix.cast_mul {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 j : n} (x y : matrix (s i) (s i) ℂ) (h : i = j) :

_.mp (x * y) = _.mp x * _.mp y

theorem module.dual.pi.is_faithful_pos_map.basis.apply_cast_eq_mp {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] {i j : n} (h : i = j) (p : s i × s i) :

_.mp (⇑(_.basis) p) = ⇑(_.basis) (_.mpr p)

theorem pi_lmul_to_matrix {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] (x : Π (i : n), matrix (s i) (s i) ℂ) :

⇑(module.dual.pi.is_faithful_pos_map.to_matrix _) (⇑lmul x) = matrix.block_diagonal' (λ (i : n), matrix.kronecker_map has_mul.mul (x i) 1)

theorem pi_rmul_to_matrix {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] (x : Π (i : n), matrix (s i) (s i) ℂ) :

⇑(module.dual.pi.is_faithful_pos_map.to_matrix _) (⇑rmul x) = matrix.block_diagonal' (λ (i : n), matrix.kronecker_map has_mul.mul 1 (⇑(_.sig (1 / 2)) (x i)).transpose)

theorem unitary.coe_pi {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)] (U : Π (i : n), ↥(matrix.unitary_group (s i) ℂ)) :

↑(unitary.pi U) = ↑U

theorem unitary.coe_pi_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)] (U : Π (i : n), ↥(matrix.unitary_group (s i) ℂ)) (i : n) :

↑U i = ⇑(U i)

theorem pi_inner_aut_to_matrix {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] (U : Π (i : n), ↥(matrix.unitary_group (s i) ℂ)) :

⇑(module.dual.pi.is_faithful_pos_map.to_matrix _) (unitary.inner_aut_star_alg ℂ (unitary.pi U)).to_alg_equiv.to_linear_map = matrix.block_diagonal' (λ (i : n), matrix.kronecker_map has_mul.mul ⇑(U i) (⇑(_.sig (-(1 / 2))) ⇑(U i)).conj)

theorem schur_idempotent_one_left_rank_one {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) ℂ) :

⇑(⇑schur_idempotent 1) ↑(rank_one a b) = ⇑rmul a * ⇑linear_map.adjoint (⇑rmul b)

theorem Psi.symm_map {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₂ : ℝ) (f g : (Π (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₂) (⇑(⇑schur_idempotent f) g) = ⇑(module.dual.pi.is_faithful_pos_map.Psi hψ r₁ r₂) f * ⇑(module.dual.pi.is_faithful_pos_map.Psi hψ r₁ r₂) g