Theory Von_Neumann_Algebras
section ‹‹Von_Neumann_Algebras› -- Von Neumann algebras and the double commutant theorem›
theory Von_Neumann_Algebras
imports Hilbert_Space_Tensor_Product
begin
unbundle cblinfun_syntax
subsection ‹Commutants›
definition ‹commutant F = {x. ∀y∈F. x o⇩C⇩L y = y o⇩C⇩L x}›
lemma sandwich_unitary_commutant:
fixes U :: ‹'a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space›
assumes [simp]: ‹unitary U›
shows ‹sandwich U ` commutant X = commutant (sandwich U ` X)›
proof (rule Set.set_eqI)
fix x
let ?comm = ‹λa b. a o⇩C⇩L b = b o⇩C⇩L a›
have ‹x ∈ sandwich U ` commutant X ⟷ sandwich (U*) x ∈ commutant X›
apply (subst inj_image_mem_iff[symmetric, where f=‹sandwich (U*)›])
by (auto intro!: inj_sandwich_isometry simp: image_image
simp flip: cblinfun_apply_cblinfun_compose sandwich_compose)
also have ‹… ⟷ (∀y∈X. ?comm (sandwich (U*) x) y)›
by (simp add: commutant_def)
also have ‹… ⟷ (∀y∈X. ?comm x (sandwich U y))›
apply (rule ball_cong, simp)
apply (simp add: sandwich_apply)
by (smt (verit) assms cblinfun_assoc_left(1) cblinfun_compose_id_left cblinfun_compose_id_right unitaryD1 unitaryD2)
also have ‹… ⟷ (∀y∈sandwich U ` X. ?comm x y)›
by fast
also have ‹… ⟷ x ∈ commutant (sandwich U ` X)›
by (simp add: commutant_def)
finally show ‹(x ∈ (*⇩V) (sandwich U) ` commutant X) ⟷ (x ∈ commutant ((*⇩V) (sandwich U) ` X))›
by -
qed
lemma commutant_tensor1: ‹commutant (range (λa. a ⊗⇩o id_cblinfun)) = range (λb. id_cblinfun ⊗⇩o b)›
proof (rule Set.set_eqI, rule iffI)
fix x :: ‹('a × 'b) ell2 ⇒⇩C⇩L ('a × 'b) ell2›
fix γ :: 'a
assume ‹x ∈ commutant (range (λa. a ⊗⇩o id_cblinfun))›
then have comm: ‹(a ⊗⇩o id_cblinfun) *⇩V x *⇩V ψ = x *⇩V (a ⊗⇩o id_cblinfun) *⇩V ψ› for a ψ
by (metis (mono_tags, lifting) commutant_def mem_Collect_eq rangeI cblinfun_apply_cblinfun_compose)
define op where ‹op = classical_operator (λi. Some (γ,i::'b))›
have [simp]: ‹classical_operator_exists (λi. Some (γ,i))›
apply (rule classical_operator_exists_inj)
using inj_map_def by blast
define x' where ‹x' = op* o⇩C⇩L x o⇩C⇩L op›
have x': ‹cinner (ket j) (x' *⇩V ket l) = cinner (ket (γ,j)) (x *⇩V ket (γ,l))› for j l
by (simp add: x'_def op_def classical_operator_ket cinner_adj_right)
have ‹cinner (ket (i,j)) (x *⇩V ket (k,l)) = cinner (ket (i,j)) ((id_cblinfun ⊗⇩o x') *⇩V ket (k,l))› for i j k l
proof -
have ‹cinner (ket (i,j)) (x *⇩V ket (k,l))
= cinner ((butterfly (ket i) (ket γ) ⊗⇩o id_cblinfun) *⇩V ket (γ,j)) (x *⇩V (butterfly (ket k) (ket γ) ⊗⇩o id_cblinfun) *⇩V ket (γ,l))›
by (auto simp: tensor_op_ket tensor_ell2_ket)
also have ‹… = cinner (ket (γ,j)) ((butterfly (ket γ) (ket i) ⊗⇩o id_cblinfun) *⇩V x *⇩V (butterfly (ket k) (ket γ) ⊗⇩o id_cblinfun) *⇩V ket (γ,l))›
by (metis (no_types, lifting) cinner_adj_left butterfly_adjoint id_cblinfun_adjoint tensor_op_adjoint)
also have ‹… = cinner (ket (γ,j)) (x *⇩V (butterfly (ket γ) (ket i) ⊗⇩o id_cblinfun o⇩C⇩L butterfly (ket k) (ket γ) ⊗⇩o id_cblinfun) *⇩V ket (γ,l))›
unfolding comm by (simp add: cblinfun_apply_cblinfun_compose)
also have ‹… = cinner (ket i) (ket k) * cinner (ket (γ,j)) (x *⇩V ket (γ,l))›
by (simp add: comp_tensor_op tensor_op_ket tensor_op_scaleC_left cinner_ket tensor_ell2_ket)
also have ‹… = cinner (ket i) (ket k) * cinner (ket j) (x' *⇩V ket l)›
by (simp add: x')
also have ‹… = cinner (ket (i,j)) ((id_cblinfun ⊗⇩o x') *⇩V ket (k,l))›
apply (simp add: tensor_op_ket)
by (simp flip: tensor_ell2_ket)
finally show ?thesis by -
qed
then have ‹x = (id_cblinfun ⊗⇩o x')›
by (auto intro!: equal_ket cinner_ket_eqI)
then show ‹x ∈ range (λb. id_cblinfun ⊗⇩o b)›
by auto
next
fix x :: ‹('a × 'b) ell2 ⇒⇩C⇩L ('a × 'b) ell2›
assume ‹x ∈ range (λb. id_cblinfun ⊗⇩o b)›
then obtain b where x: ‹x = id_cblinfun ⊗⇩o b›
by auto
then show ‹x ∈ commutant (range (λa. a ⊗⇩o id_cblinfun))›
by (auto simp: x commutant_def comp_tensor_op)
qed
lemma csubspace_commutant[simp]: ‹csubspace (commutant X)›
by (auto simp add: complex_vector.subspace_def commutant_def cblinfun_compose_add_right cblinfun_compose_add_left)
lemma closed_commutant[simp]: ‹closed (commutant X)›
proof (subst closed_sequential_limits, intro allI impI, erule conjE)
fix s :: ‹nat ⇒ _› and l
assume s_comm: ‹∀n. s n ∈ commutant X›
assume ‹s ⇢ l›
have ‹l o⇩C⇩L x - x o⇩C⇩L l = 0› if ‹x ∈ X› for x
proof -
from ‹s ⇢ l›
have ‹(λn. s n o⇩C⇩L x - x o⇩C⇩L s n) ⇢ l o⇩C⇩L x - x o⇩C⇩L l›
apply (rule isCont_tendsto_compose[rotated])
by (intro continuous_intros)
then have ‹(λ_. 0) ⇢ l o⇩C⇩L x - x o⇩C⇩L l›
using s_comm that by (auto simp add: commutant_def)
then show ?thesis
by (simp add: LIMSEQ_const_iff that)
qed
then show ‹l ∈ commutant X›
by (simp add: commutant_def)
qed
lemma closed_csubspace_commutant[simp]: ‹closed_csubspace (commutant X)›
apply (rule closed_csubspace.intro) by simp_all
lemma commutant_mult: ‹a o⇩C⇩L b ∈ commutant X› if ‹a ∈ commutant X› and ‹b ∈ commutant X›
using that
apply (auto simp: commutant_def cblinfun_compose_assoc)
by (simp flip: cblinfun_compose_assoc)
lemma double_commutant_grows[simp]: ‹X ⊆ commutant (commutant X)›
by (auto simp add: commutant_def)
lemma commutant_antimono: ‹X ⊆ Y ⟹ commutant X ⊇ commutant Y›
by (auto simp add: commutant_def)
lemma triple_commutant[simp]: ‹commutant (commutant (commutant X)) = commutant X›
by (auto simp: commutant_def)
lemma commutant_adj: ‹adj ` commutant X = commutant (adj ` X)›
apply (auto intro!: image_eqI double_adj[symmetric] simp: commutant_def simp flip: adj_cblinfun_compose)
by (metis adj_cblinfun_compose double_adj)
lemma commutant_empty[simp]: ‹commutant {} = UNIV›
by (simp add: commutant_def)
lemma commutant_weak_star_closed[simp]: ‹closedin weak_star_topology (commutant X)›
proof -
have comm_inter: ‹commutant X = (⋂x∈X. commutant {x})›
by (auto simp: commutant_def)
have comm_x: ‹commutant {x} = (λy. x o⇩C⇩L y - y o⇩C⇩L x) -` {0}› for x :: ‹'a ⇒⇩C⇩L 'a›
by (auto simp add: commutant_def vimage_def)
have cont: ‹continuous_map weak_star_topology weak_star_topology (λy. x o⇩C⇩L y - y o⇩C⇩L x)› for x :: ‹'a ⇒⇩C⇩L 'a›
apply (rule continuous_intros)
by (simp_all add: continuous_map_left_comp_weak_star continuous_map_right_comp_weak_star)
have ‹closedin weak_star_topology ((λy. x o⇩C⇩L y - y o⇩C⇩L x) -` {0})› for x :: ‹'a ⇒⇩C⇩L 'a›
using closedin_vimage[where U=‹weak_star_topology› and S=‹{0}› and T=weak_star_topology]
using cont by (auto simp add: closedin_Hausdorff_singleton)
then show ?thesis
apply (cases ‹X = {}›)
using closedin_topspace[of weak_star_topology]
by (auto simp add: comm_inter comm_x)
qed
lemma cspan_in_double_commutant: ‹cspan X ⊆ commutant (commutant X)›
by (simp add: complex_vector.span_minimal)
lemma weak_star_closure_in_double_commutant: ‹weak_star_topology closure_of X ⊆ commutant (commutant X)›
by (simp add: closure_of_minimal)
lemma weak_star_closure_cspan_in_double_commutant: ‹weak_star_topology closure_of cspan X ⊆ commutant (commutant X)›
by (simp add: closure_of_minimal cspan_in_double_commutant)
lemma commutant_memberI:
assumes ‹⋀y. y ∈ X ⟹ x o⇩C⇩L y = y o⇩C⇩L x›
shows ‹x ∈ commutant X›
using assms by (simp add: commutant_def)
lemma commutant_sot_closed: ‹closedin cstrong_operator_topology (commutant A)›
proof (cases ‹A = {}›)
case True
then show ?thesis
apply simp
by (metis closedin_topspace cstrong_operator_topology_topspace)
next
case False
have closed_a: ‹closedin cstrong_operator_topology (commutant {a})› for a :: ‹'a ⇒⇩C⇩L 'a›
proof -
have comm_a: ‹commutant {a} = (λb. a o⇩C⇩L b - b o⇩C⇩L a) -` {0}›
by (auto simp: commutant_def)
have closed_0: ‹closedin cstrong_operator_topology {0}›
apply (rule closedin_Hausdorff_singleton)
by simp_all
have cont: ‹continuous_map cstrong_operator_topology cstrong_operator_topology (λb. a o⇩C⇩L b - b o⇩C⇩L a)›
by (intro continuous_intros continuous_map_left_comp_sot continuous_map_right_comp_sot)
show ?thesis
using closedin_vimage[OF closed_0 cont]
by (simp add: comm_a)
qed
have *: ‹commutant A = (⋂a∈A. commutant {a})›
by (auto simp add: commutant_def)
show ?thesis
by (auto intro!: closedin_Inter simp: * False closed_a)
qed
lemma commutant_tensor1': ‹commutant (range (λa. id_cblinfun ⊗⇩o a)) = range (λb. b ⊗⇩o id_cblinfun)›
proof -
have ‹commutant (range (λa. id_cblinfun ⊗⇩o a)) = commutant (sandwich swap_ell2 ` range (λa. a ⊗⇩o id_cblinfun))›
by (metis (no_types, lifting) image_cong range_composition swap_tensor_op_sandwich)
also have ‹… = sandwich swap_ell2 ` commutant (range (λa. a ⊗⇩o id_cblinfun))›
by (simp add: sandwich_unitary_commutant)
also have ‹… = sandwich swap_ell2 ` range (λa. id_cblinfun ⊗⇩o a)›
by (simp add: commutant_tensor1)
also have ‹… = range (λb. b ⊗⇩o id_cblinfun)›
by force
finally show ?thesis
by -
qed
lemma closed_map_sot_tensor_op_id_right:
‹closed_map cstrong_operator_topology cstrong_operator_topology (λa. a ⊗⇩o id_cblinfun :: ('a × 'b) ell2 ⇒⇩C⇩L ('a × 'b) ell2)›
proof (unfold closed_map_def, intro allI impI)
fix U :: ‹('a ell2 ⇒⇩C⇩L 'a ell2) set›
assume closed_U: ‹closedin cstrong_operator_topology U›
have aux1: ‹range f ⊆ X ⟷ (∀x. f x ∈ X)› for f :: ‹'x ⇒ 'y› and X
by blast
have ‹l ∈ (λa. a ⊗⇩o id_cblinfun) ` U› if range: ‹range (λx. f x) ⊆ (λa. a ⊗⇩o id_cblinfun) ` U›
and limit: ‹limitin cstrong_operator_topology f l F› and ‹F ≠ ⊥›
for f and l :: ‹('a × 'b) ell2 ⇒⇩C⇩L ('a × 'b) ell2› and F :: ‹(('a × 'b) ell2 ⇒⇩C⇩L ('a × 'b) ell2) filter›
proof -
from range obtain f' where f'U: ‹range f' ⊆ U› and f_def: ‹f y = f' y ⊗⇩o id_cblinfun› for y
apply atomize_elim
apply (subst aux1)
apply (rule choice2)
by auto
have ‹l ∈ commutant (range (λa. id_cblinfun ⊗⇩o a))›
proof (rule commutant_memberI)
fix c :: ‹('a × 'b) ell2 ⇒⇩C⇩L ('a × 'b) ell2›
assume ‹c ∈ range (λa. id_cblinfun ⊗⇩o a)›
then obtain c' where c_def: ‹c = id_cblinfun ⊗⇩o c'›
by blast
from limit have 1: ‹limitin cstrong_operator_topology ((λz. z o⇩C⇩L c) o f) (l o⇩C⇩L c) F›
apply(rule continuous_map_limit[rotated])
by (simp add: continuous_map_right_comp_sot)
from limit have 2: ‹limitin cstrong_operator_topology ((λz. c o⇩C⇩L z) o f) (c o⇩C⇩L l) F›
apply(rule continuous_map_limit[rotated])
by (simp add: continuous_map_left_comp_sot)
have 3: ‹f x o⇩C⇩L c = c o⇩C⇩L f x› for x
by (simp add: f_def c_def comp_tensor_op)
from 1 2 show ‹l o⇩C⇩L c = c o⇩C⇩L l›
unfolding 3 o_def
by (meson hausdorff_sot limitin_Hausdorff_unique that(3))
qed
then have ‹l ∈ range (λa. a ⊗⇩o id_cblinfun)›
by (simp add: commutant_tensor1')
then obtain l' where l_def: ‹l = l' ⊗⇩o id_cblinfun›
by blast
have ‹limitin cstrong_operator_topology f' l' F›
proof (rule limitin_cstrong_operator_topology[THEN iffD2], rule allI)
fix ψ fix b :: 'b
have ‹((λx. f x *⇩V (ψ ⊗⇩s ket b)) ⤏ l *⇩V (ψ ⊗⇩s ket b)) F›
using limitin_cstrong_operator_topology that(2) by auto
then have ‹((λx. (f' x *⇩V ψ) ⊗⇩s ket b) ⤏ (l' *⇩V ψ) ⊗⇩s ket b) F›
by (simp add: f_def l_def tensor_op_ell2)
then have ‹((λx. (tensor_ell2_right (ket b))* *⇩V ((f' x *⇩V ψ) ⊗⇩s ket b))
⤏ (tensor_ell2_right (ket b))* *⇩V ((l' *⇩V ψ) ⊗⇩s ket b)) F›
apply (rule cblinfun.tendsto[rotated])
by simp
then show ‹((λx. f' x *⇩V ψ) ⤏ l' *⇩V ψ) F›
by (simp add: tensor_ell2_right_adj_apply)
qed
with closed_U f'U ‹F ≠ ⊥› have ‹l' ∈ U›
by (simp add: Misc_Tensor_Product.limitin_closedin)
then show ‹l ∈ (λa. a ⊗⇩o id_cblinfun) ` U›
by (simp add: l_def)
qed
then show ‹closedin cstrong_operator_topology ((λa. a ⊗⇩o id_cblinfun :: ('a × 'b) ell2 ⇒⇩C⇩L ('a × 'b) ell2) ` U)›
apply (rule_tac closedin_if_converge_inside)
by simp_all
qed
lemma id_in_commutant[iff]: ‹id_cblinfun ∈ commutant A›
by (simp add: commutant_memberI)
lemma double_commutant_hull: ‹commutant (commutant X) = (λX. commutant (commutant X) = X) hull X›
by (smt (verit) commutant_antimono double_commutant_grows hull_unique triple_commutant)
lemma commutant_adj_closed: ‹(⋀x. x ∈ X ⟹ x* ∈ X) ⟹ x ∈ commutant X ⟹ x* ∈ commutant X›
by (metis (no_types, opaque_lifting) commutant_adj commutant_antimono double_adj imageI subset_iff)
lemma double_commutant_Un_left: ‹commutant (commutant (commutant (commutant X) ∪ Y)) = commutant (commutant (X ∪ Y))›
apply (simp add: double_commutant_hull cong: arg_cong[where f=‹Hull.hull _›])
using hull_Un_left by fastforce
lemma double_commutant_Un_right: ‹commutant (commutant (X ∪ commutant (commutant Y))) = commutant (commutant (X ∪ Y))›
by (metis Un_ac(3) double_commutant_Un_left)
lemma amplification_double_commutant_commute:
‹commutant (commutant ((λa. a ⊗⇩o id_cblinfun) ` X))
= (λa. a ⊗⇩o id_cblinfun) ` commutant (commutant X)›
proof -
define π :: ‹('a ell2 ⇒⇩C⇩L 'a ell2) ⇒ (('a × 'b) ell2 ⇒⇩C⇩L ('a × 'b) ell2)› where
‹π a = a ⊗⇩o id_cblinfun› for a
define U :: ‹'b ⇒ 'a ell2 ⇒⇩C⇩L ('a × 'b) ell2› where ‹U i = tensor_ell2_right (ket i)› for i :: 'b
write commutant (‹_''› [120] 120)
write id_cblinfun (‹𝟭›)
have *: ‹(π ` X)'' ⊆ range π› for X
proof (rule subsetI)
fix x assume asm: ‹x ∈ (π ` X)''›
fix t
define y where ‹y = U t* o⇩C⇩L x o⇩C⇩L U t›
have ‹ket (k,l) ∙⇩C (x *⇩V ket (m,n)) = ket (k,l) ∙⇩C (π y *⇩V ket (m,n))› for k l m n
proof -
have comm: ‹x o⇩C⇩L (U i o⇩C⇩L U j*) = (U i o⇩C⇩L U j*) o⇩C⇩L x› for i j
proof -
have ‹U i o⇩C⇩L U j* = id_cblinfun ⊗⇩o butterfly (ket i) (ket j)›
by (simp add: U_def tensor_ell2_right_butterfly)
also have ‹… ∈ (π ` X)'›
by (simp add: π_def commutant_def comp_tensor_op)
finally show ?thesis
using asm
by (simp add: commutant_def)
qed
have ‹ket (k,l) ∙⇩C (x *⇩V ket (m,n)) = ket k ∙⇩C (U l* *⇩V x *⇩V U n *⇩V ket m)›
by (simp add: cinner_adj_right U_def tensor_ell2_ket)
also have ‹… = ket k ∙⇩C (U l* *⇩V x *⇩V U n *⇩V U t* *⇩V U t *⇩V ket m)›
using U_def by fastforce
also have ‹… = ket k ∙⇩C (U l* *⇩V U n *⇩V U t* *⇩V x *⇩V U t *⇩V ket m)›
using simp_a_oCL_b'[OF comm]
by simp
also have ‹… = of_bool (l=n) * (ket k ∙⇩C (U t* *⇩V x *⇩V U t *⇩V ket m))›
using U_def by fastforce
also have ‹… = of_bool (l=n) * (ket k ∙⇩C (y *⇩V ket m))›
using y_def by force
also have ‹… = ket (k,l) ∙⇩C (π y *⇩V ket (m,n))›
by (simp add: π_def tensor_op_ell2 flip: tensor_ell2_ket)
finally show ?thesis
by -
qed
then have ‹x = π y›
by (metis cinner_ket_eqI equal_ket surj_pair)
then show ‹x ∈ range π›
by simp
qed
have **: ‹π ` (Y ') = (π ` Y)' ∩ range π› for Y
using inj_tensor_left[of id_cblinfun]
apply (auto simp add: commutant_def π_def comp_tensor_op
intro!: image_eqI)
using injD by fastforce
have 1: ‹(π ` X)'' ⊆ π ` (X '')› for X
proof -
have ‹(π ` X)'' ⊆ (π ` X)'' ∩ range π›
by (simp add: "*")
also have ‹… ⊆ ((π ` X)' ∩ range π)' ∩ range π›
by (simp add: commutant_antimono inf.coboundedI1)
also have ‹… = π ` (X '')›
by (simp add: ** )
finally show ?thesis
by -
qed
have ‹x o⇩C⇩L y = y o⇩C⇩L x› if ‹x ∈ π ` (X '')› and ‹y ∈ (π ` X)'› for x y
proof (intro equal_ket cinner_ket_eqI)
fix i j :: ‹'a × 'b›
from that obtain w where ‹w ∈ X ''› and x_def: ‹x = w ⊗⇩o 𝟭›
by (auto simp: π_def)
obtain i1 i2 where i_def: ‹i = (i1, i2)› by force
obtain j1 j2 where j_def: ‹j = (j1, j2)› by force
define y⇩0 where ‹y⇩0 = U i2* o⇩C⇩L y o⇩C⇩L U j2›
have ‹y⇩0 ∈ X '›
proof (rule commutant_memberI)
fix z assume ‹z ∈ X›
then have ‹z ⊗⇩o 𝟭 ∈ π ` X›
by (auto simp: π_def)
have ‹y⇩0 o⇩C⇩L z = U i2* o⇩C⇩L y o⇩C⇩L (z ⊗⇩o 𝟭) o⇩C⇩L U j2›
by (auto intro!: equal_ket simp add: y⇩0_def U_def tensor_op_ell2)
also have ‹… = U i2* o⇩C⇩L (z ⊗⇩o 𝟭) o⇩C⇩L y o⇩C⇩L U j2›
using ‹z ⊗⇩o 𝟭 ∈ π ` X› and ‹y ∈ (π ` X)'›
apply (auto simp add: commutant_def)
by (simp add: cblinfun_compose_assoc)
also have ‹… = z o⇩C⇩L y⇩0›
by (auto intro!: equal_ket cinner_ket_eqI
simp add: y⇩0_def U_def tensor_op_ell2 tensor_op_adjoint simp flip: cinner_adj_left)
finally show ‹y⇩0 o⇩C⇩L z = z o⇩C⇩L y⇩0›
by -
qed
have ‹ket i ∙⇩C ((x o⇩C⇩L y) *⇩V ket j) = ket i1 ∙⇩C (U i2* *⇩V (w ⊗⇩o 𝟭) *⇩V y *⇩V U j2 *⇩V ket j1)›
by (simp add: U_def i_def j_def tensor_ell2_ket cinner_adj_right x_def)
also have ‹… = ket i1 ∙⇩C (U i2* *⇩V (w ⊗⇩o 𝟭) *⇩V (U i2 o⇩C⇩L U i2*) *⇩V y *⇩V U j2 *⇩V ket j1)›
by (simp add: U_def tensor_ell2_right_butterfly tensor_op_adjoint tensor_op_ell2
flip: cinner_adj_left)
also have ‹… = ket i1 ∙⇩C (w *⇩V y⇩0 *⇩V ket j1)›
by (simp add: y⇩0_def tensor_op_adjoint tensor_op_ell2 U_def flip: cinner_adj_left)
also have ‹… = ket i1 ∙⇩C (y⇩0 *⇩V w *⇩V ket j1)›
using ‹y⇩0 ∈ X '› ‹w ∈ X ''›
apply (subst (asm) (2) commutant_def)
using lift_cblinfun_comp(4) by force
also have ‹… = ket i1 ∙⇩C (U i2* *⇩V y *⇩V (U j2 o⇩C⇩L U j2*) *⇩V (w ⊗⇩o 𝟭) *⇩V U j2 *⇩V ket j1)›
by (simp add: y⇩0_def tensor_op_adjoint tensor_op_ell2 U_def flip: cinner_adj_left)
also have ‹… = ket i1 ∙⇩C (U i2* *⇩V y *⇩V (w ⊗⇩o 𝟭) *⇩V U j2 *⇩V ket j1)›
by (simp add: U_def tensor_ell2_right_butterfly tensor_op_adjoint tensor_op_ell2
flip: cinner_adj_left)
also have ‹… = ket i ∙⇩C ((y o⇩C⇩L x) *⇩V ket j)›
by (simp add: U_def i_def j_def tensor_ell2_ket cinner_adj_right x_def)
finally show ‹ket i ∙⇩C ((x o⇩C⇩L y) *⇩V ket j) = ket i ∙⇩C ((y o⇩C⇩L x) *⇩V ket j)›
by -
qed
then have 2: ‹(π ` X)'' ⊇ π ` (X '')›
by (auto intro!: commutant_memberI)
from 1 2 show ?thesis
by (auto simp flip: π_def)
qed
lemma amplification_double_commutant_commute':
‹commutant (commutant ((λa. id_cblinfun ⊗⇩o a) ` X))
= (λa. id_cblinfun ⊗⇩o a) ` commutant (commutant X)›
proof -
have ‹commutant (commutant ((λa. id_cblinfun ⊗⇩o a) ` X))
= commutant (commutant (sandwich swap_ell2 ` (λa. a ⊗⇩o id_cblinfun) ` X))›
by (simp add: swap_tensor_op_sandwich image_image)
also have ‹… = sandwich swap_ell2 ` commutant (commutant ((λa. a ⊗⇩o id_cblinfun) ` X))›
by (simp add: sandwich_unitary_commutant)
also have ‹… = sandwich swap_ell2 ` (λa. a ⊗⇩o id_cblinfun) ` commutant (commutant X)›
by (simp add: amplification_double_commutant_commute)
also have ‹… = (λa. id_cblinfun ⊗⇩o a) ` commutant (commutant X)›
by (simp add: swap_tensor_op_sandwich image_image)
finally show ?thesis
by -
qed
lemma commutant_cspan: ‹commutant (cspan A) = commutant A›
by (meson basic_trans_rules(24) commutant_antimono complex_vector.span_superset cspan_in_double_commutant dual_order.trans)
lemma double_commutant_grows': ‹x ∈ X ⟹ x ∈ commutant (commutant X)›
using double_commutant_grows by blast
subsection ‹Double commutant theorem›
fun inflation_op' :: ‹nat ⇒ ('a ell2 ⇒⇩C⇩L 'b ell2) list ⇒ ('a×nat) ell2 ⇒⇩C⇩L ('b×nat) ell2› where
‹inflation_op' n Nil = 0›
| ‹inflation_op' n (a#as) = (a ⊗⇩o butterfly (ket n) (ket n)) + inflation_op' (n+1) as›
abbreviation ‹inflation_op ≡ inflation_op' 0›
fun inflation_state' :: ‹nat ⇒ 'a ell2 list ⇒ ('a×nat) ell2› where
‹inflation_state' n Nil = 0›
| ‹inflation_state' n (a#as) = (a ⊗⇩s ket n) + inflation_state' (n+1) as›
abbreviation ‹inflation_state ≡ inflation_state' 0›
fun inflation_space' :: ‹nat ⇒ 'a ell2 ccsubspace list ⇒ ('a×nat) ell2 ccsubspace› where
‹inflation_space' n Nil = 0›
| ‹inflation_space' n (S#Ss) = (S ⊗⇩S ccspan {ket n}) + inflation_space' (n+1) Ss›
abbreviation ‹inflation_space ≡ inflation_space' 0›
definition inflation_carrier :: ‹nat ⇒ ('a×nat) ell2 ccsubspace› where
‹inflation_carrier n = inflation_space (replicate n ⊤)›
definition inflation_op_carrier :: ‹nat ⇒ (('a×nat) ell2 ⇒⇩C⇩L ('b×nat) ell2) set› where
‹inflation_op_carrier n = { Proj (inflation_carrier n) o⇩C⇩L a o⇩C⇩L Proj (inflation_carrier n) | a. True }›
lemma inflation_op_compose_outside: ‹inflation_op' m ops o⇩C⇩L (a ⊗⇩o butterfly (ket n) (ket n)) = 0› if ‹n < m›
using that apply (induction ops arbitrary: m)
by (auto simp: cblinfun_compose_add_left comp_tensor_op cinner_ket)
lemma inflation_op_compose_outside_rev: ‹(a ⊗⇩o butterfly (ket n) (ket n)) o⇩C⇩L inflation_op' m ops = 0› if ‹n < m›
using that apply (induction ops arbitrary: m)
by (auto simp: cblinfun_compose_add_right comp_tensor_op cinner_ket)
lemma Proj_inflation_carrier: ‹Proj (inflation_carrier n) = inflation_op (replicate n id_cblinfun)›
proof -
have ‹Proj (inflation_space' m (replicate n ⊤)) = inflation_op' m (replicate n id_cblinfun)› for m
proof (induction n arbitrary: m)
case 0
then show ?case
by simp
next
case (Suc n)
have *: ‹orthogonal_spaces ((⊤ :: 'b ell2 ccsubspace) ⊗⇩S ccspan {ket m}) (inflation_space' (Suc m) (replicate n ⊤))›
by (auto simp add: orthogonal_projectors_orthogonal_spaces Suc tensor_ccsubspace_via_Proj
Proj_on_own_range is_Proj_tensor_op inflation_op_compose_outside_rev butterfly_is_Proj
simp flip: butterfly_eq_proj)
show ?case
apply (simp add: Suc * Proj_sup)
by (metis (no_types, opaque_lifting) Proj_is_Proj Proj_on_own_range Proj_top
butterfly_eq_proj is_Proj_tensor_op norm_ket tensor_ccsubspace_via_Proj)
qed
then show ?thesis
by (force simp add: inflation_carrier_def)
qed
lemma inflation_op_carrierI:
assumes ‹Proj (inflation_carrier n) o⇩C⇩L a o⇩C⇩L Proj (inflation_carrier n) = a›
shows ‹a ∈ inflation_op_carrier n›
using assms by (auto intro!: exI[of _ a] simp add: inflation_op_carrier_def)
lemma inflation_op_compose: ‹inflation_op' n ops1 o⇩C⇩L inflation_op' n ops2 = inflation_op' n (map2 cblinfun_compose ops1 ops2)›
proof (induction ops2 arbitrary: ops1 n)
case Nil
then show ?case by simp
next
case (Cons op ops2)
note IH = this
fix ops1 :: ‹('c ell2 ⇒⇩C⇩L 'b ell2) list›
show ‹inflation_op' n ops1 o⇩C⇩L inflation_op' n (op # ops2) =
inflation_op' n (map2 (o⇩C⇩L) ops1 (op # ops2))›
proof (cases ops1)
case Nil
then show ?thesis
by simp
next
case (Cons a list)
then show ?thesis
by (simp add: cblinfun_compose_add_right cblinfun_compose_add_left tensor_op_ell2
inflation_op_compose_outside comp_tensor_op inflation_op_compose_outside_rev
flip: IH)
qed
qed
lemma inflation_op_in_carrier: ‹inflation_op ops ∈ inflation_op_carrier n› if ‹length ops ≤ n›
apply (rule inflation_op_carrierI)
using that
by (simp add: Proj_inflation_carrier inflation_op_carrier_def inflation_op_compose
zip_replicate1 zip_replicate2 o_def)
lemma inflation_op'_apply_tensor_outside: ‹n < m ⟹ inflation_op' m as *⇩V (v ⊗⇩s ket n) = 0›
apply (induction as arbitrary: m)
by (auto simp: cblinfun.add_left tensor_op_ell2 cinner_ket)
lemma inflation_op'_compose_tensor_outside: ‹n < m ⟹ inflation_op' m as o⇩C⇩L tensor_ell2_right (ket n) = 0›
apply (rule cblinfun_eqI)
by (simp add: inflation_op'_apply_tensor_outside)
lemma inflation_state'_apply_tensor_outside: ‹n < m ⟹ (a ⊗⇩o butterfly ψ (ket n)) *⇩V inflation_state' m vs = 0›
apply (induction vs arbitrary: m)
by (auto simp: cblinfun.add_right tensor_op_ell2 cinner_ket)
lemma inflation_op_apply_inflation_state: ‹inflation_op' n ops *⇩V inflation_state' n vecs = inflation_state' n (map2 cblinfun_apply ops vecs)›
proof (induction vecs arbitrary: ops n)
case Nil
then show ?case by simp
next
case (Cons v vecs)
note IH = this
fix ops :: ‹('b ell2 ⇒⇩C⇩L 'a ell2) list›
show ‹inflation_op' n ops *⇩V inflation_state' n (v # vecs) =
inflation_state' n (map2 (*⇩V) ops (v # vecs))›
proof (cases ops)
case Nil
then show ?thesis
by simp
next
case (Cons a list)
then show ?thesis
by (simp add: cblinfun.add_right cblinfun.add_left tensor_op_ell2
inflation_op'_apply_tensor_outside inflation_state'_apply_tensor_outside
flip: IH)
qed
qed
lemma inflation_state_in_carrier: ‹inflation_state vecs ∈ space_as_set (inflation_carrier n)› if ‹length vecs + m ≤ n›
apply (rule space_as_setI_via_Proj)
using that
by (simp add: Proj_inflation_carrier inflation_op_apply_inflation_state zip_replicate1 o_def)
lemma inflation_op'_apply_tensor_outside': ‹n ≥ length as + m ⟹ inflation_op' m as *⇩V (v ⊗⇩s ket n) = 0›
apply (induction as arbitrary: m)
by (auto simp: cblinfun.add_left tensor_op_ell2 cinner_ket)
lemma Proj_inflation_carrier_outside: ‹Proj (inflation_carrier n) *⇩V (ψ ⊗⇩s ket i) = 0› if ‹i ≥ n›
by (simp add: Proj_inflation_carrier inflation_op'_apply_tensor_outside' that)
lemma inflation_state'_is_orthogonal_outside: ‹n < m ⟹ is_orthogonal (a ⊗⇩s ket n) (inflation_state' m vs)›
apply (induction vs arbitrary: m)
by (auto simp: cinner_add_right)
lemma inflation_op_adj: ‹(inflation_op' n ops)* = inflation_op' n (map adj ops)›
apply (induction ops arbitrary: n)
by (simp_all add: adj_plus tensor_op_adjoint)
lemma inflation_state0:
assumes ‹⋀v. v ∈ set f ⟹ v = 0›
shows ‹inflation_state' n f = 0›
using assms apply (induction f arbitrary: n)
apply simp
using tensor_ell2_0_left by force
lemma inflation_state_plus:
assumes ‹length f = length g›
shows ‹inflation_state' n f + inflation_state' n g = inflation_state' n (map2 plus f g)›
using assms apply (induction f g arbitrary: n rule: list_induct2)
by (auto simp: algebra_simps tensor_ell2_add1)
lemma inflation_state_minus:
assumes ‹length f = length g›
shows ‹inflation_state' n f - inflation_state' n g = inflation_state' n (map2 minus f g)›
using assms apply (induction f g arbitrary: n rule: list_induct2)
by (auto simp: algebra_simps tensor_ell2_diff1)
lemma inflation_state_scaleC:
shows ‹c *⇩C inflation_state' n f = inflation_state' n (map (scaleC c) f)›
apply (induction f arbitrary: n)
by (auto simp: algebra_simps tensor_ell2_scaleC1)
lemma inflation_op_compose_tensor_ell2_right:
assumes ‹i ≥ n› and ‹i < n + length f›
shows ‹inflation_op' n f o⇩C⇩L tensor_ell2_right (ket i) = tensor_ell2_right (ket i) o⇩C⇩L (f!(i-n))›
proof (insert assms, induction f arbitrary: n)
case Nil
then show ?case
by simp
next
case (Cons a f)
show ?case
proof (cases ‹i = n›)
case True
have ‹a ⊗⇩o butterfly (ket n) (ket n) o⇩C⇩L tensor_ell2_right (ket n) = tensor_ell2_right (ket n) o⇩C⇩L a›
apply (rule cblinfun_eqI)
by (simp add: tensor_op_ell2 cinner_ket)
with True show ?thesis
by (simp add: cblinfun_compose_add_left inflation_op'_compose_tensor_outside)
next
case False
with Cons.prems have 1: ‹Suc n ≤ i›
by presburger
have 2: ‹a ⊗⇩o butterfly (ket n) (ket n) o⇩C⇩L tensor_ell2_right (ket i) = 0›
apply (rule cblinfun_eqI)
using False by (simp add: tensor_op_ell2 cinner_ket)
show ?thesis
using Cons.prems 1
by (simp add: cblinfun_compose_add_left Cons.IH[where n=‹Suc n›] 2)
qed
qed
lemma inflation_op_apply:
assumes ‹i ≥ n› and ‹i < n + length f›
shows ‹inflation_op' n f *⇩V (ψ ⊗⇩s ket i) = (f!(i-n) *⇩V ψ) ⊗⇩s ket i›
by (simp add: inflation_op_compose_tensor_ell2_right assms
flip: tensor_ell2_right_apply cblinfun_apply_cblinfun_compose)
lemma norm_inflation_state:
‹norm (inflation_state' n f) = sqrt (∑v←f. (norm v)⇧2)›
proof -
have ‹(norm (inflation_state' n f))⇧2 = (∑v←f. (norm v)⇧2)›
proof (induction f arbitrary: n)
case Nil
then show ?case by simp
next
case (Cons v f)
have ‹(norm (inflation_state' n (v # f)))⇧2 = (norm (v ⊗⇩s ket n + inflation_state' (Suc n) f))⇧2›
by simp
also have ‹… = (norm (v ⊗⇩s ket n))⇧2 + (norm (inflation_state' (Suc n) f))⇧2›
apply (rule pythagorean_theorem)
apply (rule inflation_state'_is_orthogonal_outside)
by simp
also have ‹… = (norm (v ⊗⇩s ket n))⇧2 + (∑v←f. (norm v)⇧2)›
by (simp add: Cons.IH)
also have ‹… = (norm v)⇧2 + (∑v←f. (norm v)⇧2)›
by (simp add: norm_tensor_ell2)
also have ‹… = (∑v←v#f. (norm v)⇧2)›
by simp
finally show ?case
by -
qed
then show ?thesis
by (simp add: real_sqrt_unique)
qed
lemma cstrong_operator_topology_in_closure_algebraicI:
assumes space: ‹csubspace A›
assumes mult: ‹⋀a a'. a ∈ A ⟹ a' ∈ A ⟹ a o⇩C⇩L a' ∈ A›
assumes one: ‹id_cblinfun ∈ A›
assumes main: ‹⋀n S. S ≤ inflation_carrier n ⟹ (⋀a. a ∈ A ⟹ inflation_op (replicate n a) *⇩S S ≤ S) ⟹
inflation_op (replicate n b) *⇩S S ≤ S›
shows ‹b ∈ cstrong_operator_topology closure_of A›
proof (rule cstrong_operator_topology_in_closureI)
fix F :: ‹'a ell2 set› and ε :: real
assume ‹finite F› and ‹ε > 0›
obtain f where ‹set f = F› and ‹distinct f›
using ‹finite F› finite_distinct_list by blast
define n M' M where ‹n = length f›
and ‹M' = ((λa. inflation_state (map (cblinfun_apply a) f)) ` A)›
and ‹M = ccspan M'›
have M_carrier: ‹M ≤ inflation_carrier n›
proof -
have ‹M' ⊆ space_as_set (inflation_carrier n)›
by (auto intro!: inflation_state_in_carrier simp add: M'_def n_def)
then show ?thesis
by (simp add: M_def ccspan_leqI)
qed
have ‹inflation_op (replicate n a) *⇩S M ≤ M› if ‹a ∈ A› for a
proof (unfold M_def, rule cblinfun_image_ccspan_leqI)
fix v assume ‹v ∈ M'›
then obtain a' where ‹a' ∈ A› and v_def: ‹v = inflation_state (map (cblinfun_apply a') f)›
using M'_def by blast
then have ‹inflation_op (replicate n a) *⇩V v = inflation_state (map ((*⇩V) (a o⇩C⇩L a')) f)›
by (simp add: v_def n_def inflation_op_apply_inflation_state map2_map_map
flip: cblinfun_apply_cblinfun_compose map_replicate_const)
also have ‹… ∈ M'›
using M'_def ‹a' ∈ A› ‹a ∈ A› mult
by simp
also have ‹… ⊆ space_as_set (ccspan M')›
by (simp add: ccspan_superset)
finally show ‹inflation_op (replicate n a) *⇩V v ∈ space_as_set (ccspan M')›
by -
qed
then have b_invariant: ‹inflation_op (replicate n b) *⇩S M ≤ M›
using M_carrier by (simp add: main)
have f_M: ‹inflation_state f ∈ space_as_set M›
proof -
have ‹inflation_state f = inflation_state (map (cblinfun_apply id_cblinfun) f)›
by simp
also have ‹… ∈ M'›
using M'_def one by blast
also have ‹… ⊆ space_as_set M›
by (simp add: M_def ccspan_superset)
finally show ?thesis
by -
qed
have ‹csubspace M'›
proof (rule complex_vector.subspaceI)
fix c x y
show ‹0 ∈ M'›
apply (auto intro!: image_eqI[where x=0] simp add: M'_def)
apply (subst inflation_state0)
by (auto simp add: space complex_vector.subspace_0)
show ‹x ∈ M' ⟹ y ∈ M' ⟹ x + y ∈ M'›
by (auto intro!: image_eqI[where x=‹_ + _›]
simp add: M'_def inflation_state_plus map2_map_map
cblinfun.add_left[abs_def] space complex_vector.subspace_add)
show ‹c *⇩C x ∈ M' › if ‹x ∈ M'›
proof -
from that
obtain a where ‹a ∈ A› and ‹x = inflation_state (map ((*⇩V) a) f)›
by (auto simp add: M'_def)
then have ‹c *⇩C x = inflation_state (map ((*⇩V) (c *⇩C a)) f)›
by (simp add: inflation_state_scaleC o_def scaleC_cblinfun.rep_eq)
moreover have ‹c *⇩C a ∈ A›
by (simp add: ‹a ∈ A› space complex_vector.subspace_scale)
ultimately show ?thesis
unfolding M'_def
by (rule image_eqI)
qed
qed
then have M_closure_M': ‹space_as_set M = closure M'›
by (metis M_def ccspan.rep_eq complex_vector.span_eq_iff)
have ‹inflation_state (map (cblinfun_apply b) f) ∈ space_as_set M›
proof -
have ‹map2 (*⇩V) (replicate n b) f = map ((*⇩V) b) f›
using map2_map_map[where h=cblinfun_apply and g=id and f=‹λ_. b› and xs=f]
by (simp add: n_def flip: map_replicate_const)
then have ‹inflation_state (map (cblinfun_apply b) f) = inflation_op (replicate n b) *⇩V inflation_state f›
by (simp add: inflation_op_apply_inflation_state)
also have ‹… ∈ space_as_set (inflation_op (replicate n b) *⇩S M)›
by (simp add: f_M cblinfun_apply_in_image')
also have ‹… ⊆ space_as_set M›
using b_invariant less_eq_ccsubspace.rep_eq by blast
finally show ?thesis
by -
qed
then obtain m where ‹m ∈ M'› and m_close: ‹norm (m - inflation_state (map (cblinfun_apply b) f)) ≤ ε›
apply atomize_elim
apply (simp add: M_closure_M' closure_approachable dist_norm)
using ‹ε > 0› by fastforce
from ‹m ∈ M'›
obtain a where ‹a ∈ A› and m_def: ‹m = inflation_state (map (cblinfun_apply a) f)›
by (auto simp add: M'_def)
have ‹(∑v←f. (norm ((a - b) *⇩V v))⇧2) ≤ ε⇧2›
proof -
have ‹(∑v←f. (norm ((a - b) *⇩V v))⇧2) = (norm (inflation_state (map (cblinfun_apply (a - b)) f)))⇧2›
apply (simp add: norm_inflation_state o_def)
apply (subst real_sqrt_pow2)
apply (rule sum_list_nonneg)
by (auto simp: sum_list_nonneg)
also have ‹… = (norm (m - inflation_state (map (cblinfun_apply b) f)))⇧2›
by (simp add: m_def inflation_state_minus map2_map_map cblinfun.diff_left[abs_def])
also have ‹… ≤ ε⇧2›
by (simp add: m_close power_mono)
finally show ?thesis
by -
qed
then have ‹(norm ((a - b) *⇩V v))⇧2 ≤ ε⇧2› if ‹v ∈ F› for v
using that apply (simp flip: sum.distinct_set_conv_list add: ‹distinct f›)
by (smt (verit) ‹finite F› ‹set f = F› sum_nonneg_leq_bound zero_le_power2)
then show ‹∃a∈A. ∀f∈F. norm ((b - a) *⇩V f) ≤ ε›
using ‹0 < ε› ‹a ∈ A›
by (metis cblinfun.real.diff_left norm_minus_commute power2_le_imp_le power_eq_0_iff power_zero_numeral realpow_pos_nth_unique zero_compare_simps(12))
qed
lemma commutant_inflation:
fixes n
defines ‹⋀X. commutant' X ≡ commutant X ∩ inflation_op_carrier n›
shows ‹(λa. inflation_op (replicate n a)) ` commutant (commutant A)
⊆ commutant' (commutant' ((λa. inflation_op (replicate n a)) ` A))›
proof (unfold commutant'_def, rule subsetI, rule IntI)
fix b
assume ‹b ∈ (λa. inflation_op (replicate n a)) ` commutant (commutant A)›
then obtain b0 where b_def: ‹b = inflation_op (replicate n b0)› and b0_A'': ‹b0 ∈ commutant (commutant A)›
by auto
show ‹b ∈ inflation_op_carrier n›
by (simp add: b_def inflation_op_in_carrier)
show ‹b ∈ commutant (commutant ((λa. inflation_op (replicate n a)) ` A) ∩ inflation_op_carrier n)›
proof (rule commutant_memberI)
fix c
assume ‹c ∈ commutant ((λa. inflation_op (replicate n a)) ` A) ∩ inflation_op_carrier n›
then have c_comm: ‹c ∈ commutant ((λa. inflation_op (replicate n a)) ` A)›
and c_carr: ‹c ∈ inflation_op_carrier n›
by auto
define c' where ‹c' i j = (tensor_ell2_right (ket i))* o⇩C⇩L c o⇩C⇩L tensor_ell2_right (ket j)› for i j
have ‹c' i j o⇩C⇩L a = a o⇩C⇩L c' i j› if ‹a ∈ A› and ‹i < n› and ‹j < n› for a i j
proof -
from c_comm have ‹c o⇩C⇩L inflation_op (replicate n a) = inflation_op (replicate n a) o⇩C⇩L c›
using that by (auto simp: commutant_def)
then have ‹(tensor_ell2_right (ket i))* o⇩C⇩L c o⇩C⇩L (inflation_op (replicate n a) o⇩C⇩L tensor_ell2_right (ket j))
= (inflation_op (replicate n (a*)) o⇩C⇩L (tensor_ell2_right (ket i)))* o⇩C⇩L c o⇩C⇩L tensor_ell2_right (ket j)›
apply (simp add: inflation_op_adj)
by (metis (no_types, lifting) lift_cblinfun_comp(2))
then show ?thesis
apply (subst (asm) inflation_op_compose_tensor_ell2_right)
apply (simp, simp add: that)
apply (subst (asm) inflation_op_compose_tensor_ell2_right)
apply (simp, simp add: that)
by (simp add: that c'_def cblinfun_compose_assoc)
qed
then have ‹c' i j ∈ commutant A› if ‹i < n› and ‹j < n› for i j
using that by (simp add: commutant_memberI)
with b0_A'' have b0_c': ‹b0 o⇩C⇩L c' i j = c' i j o⇩C⇩L b0› if ‹i < n› and ‹j < n› for i j
using that by (simp add: commutant_def)
from c_carr obtain c'' where c'': ‹c = Proj (inflation_carrier n) o⇩C⇩L c'' o⇩C⇩L Proj (inflation_carrier n)›
by (auto simp add: inflation_op_carrier_def)
have c0: ‹c *⇩V (ψ ⊗⇩s ket i) = 0› if ‹i ≥ n› for i ψ
using that by (simp add: c'' Proj_inflation_carrier_outside)
have cadj0: ‹c* *⇩V (ψ ⊗⇩s ket j) = 0› if ‹j ≥ n› for j ψ
using that by (simp add: c'' adj_Proj Proj_inflation_carrier_outside)
have ‹inflation_op (replicate n b0) o⇩C⇩L c = c o⇩C⇩L inflation_op (replicate n b0)›
proof (rule equal_ket, rule cinner_ket_eqI)
fix ii jj
obtain i' j' :: 'a and i j :: nat where ii_def: ‹ii = (i',i)› and jj_def: ‹jj = (j',j)›
by force
show ‹ket ii ∙⇩C ((inflation_op (replicate n b0) o⇩C⇩L c) *⇩V ket jj) =
ket ii ∙⇩C ((c o⇩C⇩L inflation_op (replicate n b0)) *⇩V ket jj)›
proof (cases ‹i < n ∧ j < n›)
case True
have ‹ket ii ∙⇩C ((inflation_op (replicate n b0) o⇩C⇩L c) *⇩V ket jj) = ((b0* *⇩V ket i') ⊗⇩s ket i) ∙⇩C (c *⇩V ket j' ⊗⇩s ket j)›
using True by (simp add: ii_def jj_def inflation_op_adj inflation_op_apply flip: tensor_ell2_inner_prod
flip: tensor_ell2_ket cinner_adj_left[where G=‹inflation_op _›])
also have ‹… = (ket i' ⊗⇩s ket i) ∙⇩C (c *⇩V (b0 *⇩V ket j') ⊗⇩s ket j)›
using b0_c' apply (simp add: c'_def flip: tensor_ell2_right_apply cinner_adj_right)
by (metis (no_types, lifting) True simp_a_oCL_b')
also have ‹… = ket ii ∙⇩C ((c o⇩C⇩L inflation_op (replicate n b0)) *⇩V ket jj)›
by (simp add: True ii_def jj_def inflation_op_adj inflation_op_apply flip: tensor_ell2_inner_prod
flip: tensor_ell2_ket cinner_adj_left[where G=‹inflation_op _›])
finally show ?thesis
by -
next
case False
then show ?thesis
apply (auto simp add: ii_def jj_def inflation_op_adj c0 inflation_op'_apply_tensor_outside'
simp flip: tensor_ell2_ket cinner_adj_left[where G=‹inflation_op _›])
by (simp add: cadj0 flip: cinner_adj_left[where G=c])
qed
qed
then show ‹b o⇩C⇩L c = c o⇩C⇩L b›
by (simp add: b_def)
qed
qed
lemma double_commutant_theorem_aux:
fixes A :: ‹('a ell2 ⇒⇩C⇩L 'a ell2) set›
assumes ‹csubspace A›
assumes ‹⋀a a'. a ∈ A ⟹ a' ∈ A ⟹ a o⇩C⇩L a' ∈ A›
assumes ‹id_cblinfun ∈ A›
assumes ‹⋀a. a ∈ A ⟹ a* ∈ A›
shows ‹commutant (commutant A) = cstrong_operator_topology closure_of A›
proof (intro Set.set_eqI iffI)
show ‹x ∈ commutant (commutant A)› if ‹x ∈ cstrong_operator_topology closure_of A› for x
using closure_of_minimal commutant_sot_closed double_commutant_grows that by blast
next
show ‹b ∈ cstrong_operator_topology closure_of A› if b_A'': ‹b ∈ commutant (commutant A)› for b
proof (rule cstrong_operator_topology_in_closure_algebraicI)
show ‹csubspace A› and ‹a ∈ A ⟹ a' ∈ A ⟹ a o⇩C⇩L a' ∈ A› and ‹id_cblinfun ∈ A› for a a'
using assms by auto
fix n M
assume asm: ‹a ∈ A ⟹ inflation_op (replicate n a) *⇩S M ≤ M› for a
assume M_carrier: ‹M ≤ inflation_carrier n›
define commutant' where ‹commutant' X = commutant X ∩ inflation_op_carrier n› for X :: ‹(('a × nat) ell2 ⇒⇩C⇩L ('a × nat) ell2) set›
define An where ‹An = (λa. inflation_op (replicate n a)) ` A›
have *: ‹Proj M o⇩C⇩L (inflation_op (replicate n a) o⇩C⇩L Proj M) = inflation_op (replicate n a) o⇩C⇩L Proj M› if ‹a ∈ A› for a
apply (rule Proj_compose_cancelI)
using asm that by (simp add: cblinfun_compose_image)
have ‹Proj M o⇩C⇩L inflation_op (replicate n a) = inflation_op (replicate n a) o⇩C⇩L Proj M› if ‹a ∈ A› for a
proof -
have ‹Proj M o⇩C⇩L inflation_op (replicate n a) = (inflation_op (replicate n (a*)) o⇩C⇩L Proj M)*›
by (simp add: inflation_op_adj adj_Proj)
also have ‹… = (Proj M o⇩C⇩L inflation_op (replicate n (a*)) o⇩C⇩L Proj M)*›
apply (subst *[symmetric])
by (simp_all add: that assms flip: cblinfun_compose_assoc)
also have ‹… = Proj M o⇩C⇩L inflation_op (replicate n a) o⇩C⇩L Proj M›
by (simp add: inflation_op_adj adj_Proj cblinfun_compose_assoc)
also have ‹… = inflation_op (replicate n a) o⇩C⇩L Proj M›
apply (subst *[symmetric])
by (simp_all add: that flip: cblinfun_compose_assoc)
finally show ?thesis
by -
qed
then have ‹Proj M ∈ commutant' An›
using M_carrier
apply (auto intro!: inflation_op_carrierI simp add: An_def commutant_def commutant'_def)
by (metis Proj_compose_cancelI Proj_range adj_Proj adj_cblinfun_compose)
from b_A'' have ‹inflation_op (replicate n b) ∈ commutant' (commutant' An)›
using commutant_inflation[of n A, folded commutant'_def]
by (auto simp add: An_def commutant'_def)
with ‹Proj M ∈ commutant' An›
have *: ‹inflation_op (replicate n b) o⇩C⇩L Proj M = Proj M o⇩C⇩L inflation_op (replicate n b)›
by (simp add: commutant_def commutant'_def)
show ‹inflation_op (replicate n b) *⇩S M ≤ M›
proof -
have ‹inflation_op (replicate n b) *⇩S M = (inflation_op (replicate n b) o⇩C⇩L Proj M) *⇩S ⊤›
by (metis lift_cblinfun_comp(3) Proj_range)
also have ‹… = (Proj M o⇩C⇩L inflation_op (replicate n b)) *⇩S ⊤›
by (simp add: * )
also have ‹… ≤ M›
by (metis lift_cblinfun_comp(3) Proj_image_leq)
finally show ?thesis
by -
qed
qed
qed
lemma double_commutant_theorem_aux2:
fixes A :: ‹('a::{chilbert_space,not_singleton} ⇒⇩C⇩L 'a) set›
assumes subspace: ‹csubspace A›
assumes mult: ‹⋀a a'. a ∈ A ⟹ a' ∈ A ⟹ a o⇩C⇩L a' ∈ A›
assumes id: ‹id_cblinfun ∈ A›
assumes adj: ‹⋀a. a ∈ A ⟹ a* ∈ A›
shows ‹commutant (commutant A) = cstrong_operator_topology closure_of A›
proof -
define A' :: ‹('a chilbert2ell2 ell2 ⇒⇩C⇩L 'a chilbert2ell2 ell2) set›
where ‹A' = sandwich (ell2_to_hilbert*) ` A›
have subspace: ‹csubspace A'›
using subspace by (auto intro!: complex_vector.linear_subspace_image simp: A'_def)
have mult: ‹⋀a a'. a ∈ A' ⟹ a' ∈ A' ⟹ a o⇩C⇩L a' ∈ A'›
using mult by (auto simp add: A'_def sandwich_arg_compose unitary_ell2_to_hilbert)
have id: ‹id_cblinfun ∈ A'›
using id by (auto intro!: image_eqI simp add: A'_def sandwich_isometry_id unitary_ell2_to_hilbert)
have adj: ‹⋀a. a ∈ A' ⟹ a* ∈ A'›
using adj by (auto intro!: image_eqI simp: A'_def simp flip: sandwich_apply_adj)
have homeo: ‹homeomorphic_map cstrong_operator_topology cstrong_operator_topology
((*⇩V) (sandwich ell2_to_hilbert))›
by (auto intro!: continuous_intros homeomorphic_maps_imp_map[where g=‹sandwich (ell2_to_hilbert*)›]
simp: homeomorphic_maps_def unitary_ell2_to_hilbert
simp flip: cblinfun_apply_cblinfun_compose sandwich_compose)
have ‹commutant (commutant A') = cstrong_operator_topology closure_of A'›
using subspace mult id adj by (rule double_commutant_theorem_aux)
then have ‹sandwich ell2_to_hilbert ` commutant (commutant A') = sandwich ell2_to_hilbert ` (cstrong_operator_topology closure_of A')›
by simp
then show ?thesis
by (simp add: A'_def unitary_ell2_to_hilbert sandwich_unitary_commutant image_image homeo
flip: cblinfun_apply_cblinfun_compose sandwich_compose
homeomorphic_map_closure_of[where Y=cstrong_operator_topology])
qed
lemma double_commutant_theorem:
fixes A :: ‹('a::{chilbert_space} ⇒⇩C⇩L 'a) set›
assumes subspace: ‹csubspace A›
assumes mult: ‹⋀a a'. a ∈ A ⟹ a' ∈ A ⟹ a o⇩C⇩L a' ∈ A›
assumes id: ‹id_cblinfun ∈ A›
assumes adj: ‹⋀a. a ∈ A ⟹ a* ∈ A›
shows ‹commutant (commutant A) = cstrong_operator_topology closure_of A›
proof (cases ‹UNIV = {0::'a}›)
case True
then have ‹(x :: 'a) = 0› for x
by auto
then have UNIV_0: ‹UNIV = {0 :: 'a⇒⇩C⇩L'a}›
by (auto intro!: cblinfun_eqI)
have ‹0 ∈ commutant (commutant A)›
using complex_vector.subspace_0 csubspace_commutant by blast
then have 1: ‹commutant (commutant A) = UNIV›
using UNIV_0
by force
have ‹0 ∈ A›
by (simp add: assms(1) complex_vector.subspace_0)
then have ‹0 ∈ cstrong_operator_topology closure_of A›
by (simp add: assms(1) complex_vector.subspace_0)
then have 2: ‹cstrong_operator_topology closure_of A = UNIV›
using UNIV_0
by force
from 1 2 show ?thesis
by simp
next
case False
note aux2 = double_commutant_theorem_aux2[where 'a=‹'z::{chilbert_space,not_singleton}›, rule_format, internalize_sort ‹'z::{chilbert_space,not_singleton}›]
have hilbert: ‹class.chilbert_space (*⇩R) (*⇩C) (+) (0::'a) (-) uminus dist norm sgn uniformity open (∙⇩C)›
by (rule chilbert_space_class.chilbert_space_axioms)
from False
have not_singleton: ‹class.not_singleton TYPE('a)›
by (rule class_not_singletonI_monoid_add)
show ?thesis
apply (rule aux2)
using assms hilbert not_singleton by auto
qed
hide_fact double_commutant_theorem_aux double_commutant_theorem_aux2
lemma double_commutant_theorem_span:
fixes A :: ‹('a::{chilbert_space} ⇒⇩C⇩L 'a) set›
assumes mult: ‹⋀a a'. a ∈ A ⟹ a' ∈ A ⟹ a o⇩C⇩L a' ∈ A›
assumes id: ‹id_cblinfun ∈ A›
assumes adj: ‹⋀a. a ∈ A ⟹ a* ∈ A›
shows ‹commutant (commutant A) = cstrong_operator_topology closure_of (cspan A)›
proof -
have ‹commutant (commutant A) = commutant (commutant (cspan A))›
by (simp add: commutant_cspan)
also have ‹… = cstrong_operator_topology closure_of (cspan A)›
apply (rule double_commutant_theorem)
using assms
apply (auto simp: cspan_compose_closed cspan_adj_closed)
using complex_vector.span_clauses(1) by blast
finally show ?thesis
by -
qed
subsection ‹Von Neumann Algebras›
definition one_algebra :: ‹('a ⇒⇩C⇩L 'a::chilbert_space) set› where
‹one_algebra = range (λc. c *⇩C id_cblinfun)›
definition von_neumann_algebra where ‹von_neumann_algebra A ⟷ (∀a∈A. a* ∈ A) ∧ commutant (commutant A) = A›
definition von_neumann_factor where ‹von_neumann_factor A ⟷ von_neumann_algebra A ∧ A ∩ commutant A = one_algebra›
lemma von_neumann_algebraI: ‹(⋀a. a∈A ⟹ a* ∈ A) ⟹ commutant (commutant A) ⊆ A ⟹ von_neumann_algebra A› for 𝔉
apply (auto simp: von_neumann_algebra_def)
using double_commutant_grows by blast
lemma von_neumann_factorI:
assumes ‹von_neumann_algebra A›
assumes ‹A ∩ commutant A ⊆ one_algebra›
shows ‹von_neumann_factor A›
proof -
have 1: ‹A ⊇ one_algebra›
apply (subst asm_rl[of ‹A = commutant (commutant A)›])
using assms(1) von_neumann_algebra_def apply blast
by (auto simp: commutant_def one_algebra_def)
have 2: ‹commutant A ⊇ one_algebra›
by (auto simp: commutant_def one_algebra_def)
from 1 2 assms show ?thesis
by (auto simp add: von_neumann_factor_def)
qed
lemma commutant_UNIV: ‹commutant (UNIV :: ('a ⇒⇩C⇩L 'a::chilbert_space) set) = one_algebra›
proof -
have 1: ‹c *⇩C id_cblinfun ∈ commutant UNIV› for c
by (simp add: commutant_def)
moreover have 2: ‹x ∈ range (λc. c *⇩C id_cblinfun)› if x_comm: ‹x ∈ commutant UNIV› for x :: ‹'a ⇒⇩C⇩L 'a›
proof -
obtain B :: ‹'a set› where ‹is_onb B›
using is_onb_some_chilbert_basis by blast
have ‹∃c. x *⇩V ψ = c *⇩C ψ› for ψ
proof -
have ‹norm (x *⇩V ψ) = norm ((x o⇩C⇩L selfbutter (sgn ψ)) *⇩V ψ)›
by (simp add: cnorm_eq_1)
also have ‹… = norm ((selfbutter (sgn ψ) o⇩C⇩L x) *⇩V ψ)›
using x_comm by (simp add: commutant_def del: butterfly_apply)
also have ‹… = norm (proj ψ *⇩V (x *⇩V ψ))›
by (simp add: butterfly_sgn_eq_proj)
finally have ‹x *⇩V ψ ∈ space_as_set (ccspan {ψ})›
by (metis norm_Proj_apply)
then show ?thesis
by (auto simp add: ccspan_finite complex_vector.span_singleton)
qed
then obtain f where f: ‹x *⇩V ψ = f ψ *⇩C ψ› for ψ
apply atomize_elim apply (rule choice) by auto
have ‹f ψ = f φ› if ‹ψ ∈ B› and ‹φ ∈ B› for ψ φ
proof (cases ‹ψ = φ›)
case True
then show ?thesis by simp
next
case False
with that ‹is_onb B›
have [simp]: ‹ψ ∙⇩C φ = 0›
by (auto simp: is_onb_def is_ortho_set_def)
then have [simp]: ‹φ ∙⇩C ψ = 0›
using is_orthogonal_sym by blast
from that ‹is_onb B› have [simp]: ‹ψ ≠ 0›
by (auto simp: is_onb_def)
from that ‹is_onb B› have [simp]: ‹φ ≠ 0›
by (auto simp: is_onb_def)
have ‹f (ψ+φ) *⇩C ψ + f (ψ+φ) *⇩C φ = f (ψ+φ) *⇩C (ψ + φ)›
by (simp add: complex_vector.vector_space_assms(1))
also have ‹… = x *⇩V (ψ + φ)›
by (simp add: f)
also have ‹… = x *⇩V ψ + x *⇩V φ›
by (simp add: cblinfun.add_right)
also have ‹… = f ψ *⇩C ψ + f φ *⇩C φ›
by (simp add: f)
finally have *: ‹f (ψ + φ) *⇩C ψ + f (ψ + φ) *⇩C φ = f ψ *⇩C ψ + f φ *⇩C φ›
by -
have ‹f (ψ + φ) = f ψ›
using *[THEN arg_cong[where f=‹cinner ψ›]]
by (simp add: cinner_add_right)
moreover have ‹f (ψ + φ) = f φ›
using *[THEN arg_cong[where f=‹cinner φ›]]
by (simp add: cinner_add_right)
ultimately show ‹f ψ = f φ›
by simp
qed
then obtain c where ‹f ψ = c› if ‹ψ ∈ B› for ψ
by meson
then have ‹x *⇩V ψ = (c *⇩C id_cblinfun) *⇩V ψ› if ‹ψ ∈ B› for ψ
by (simp add: f that)
then have ‹x = c *⇩C id_cblinfun›
apply (rule cblinfun_eq_gen_eqI[where G=B])
using ‹is_onb B› by (auto simp: is_onb_def)
then show ‹x ∈ range (λc. c *⇩C id_cblinfun)›
by (auto)
qed
from 1 2 show ?thesis
by (auto simp: one_algebra_def)
qed
lemma von_neumann_algebra_UNIV: ‹von_neumann_algebra UNIV›
by (auto simp: von_neumann_algebra_def commutant_def)
lemma von_neumann_factor_UNIV: ‹von_neumann_factor UNIV›
by (simp add: von_neumann_factor_def commutant_UNIV von_neumann_algebra_UNIV)
lemma von_neumann_algebra_UNION:
assumes ‹⋀x. x ∈ X ⟹ von_neumann_algebra (A x)›
shows ‹von_neumann_algebra (commutant (commutant (⋃x∈X. A x)))›
proof (rule von_neumann_algebraI)
show ‹commutant (commutant (commutant (commutant (⋃x∈X. A x))))
⊆ commutant (commutant (⋃x∈X. A x))›
by (meson commutant_antimono double_commutant_grows)
next
fix a
assume ‹a ∈ commutant (commutant (⋃x∈X. A x))›
then have ‹a* ∈ adj ` commutant (commutant (⋃x∈X. A x))›
by simp
also have ‹… = commutant (commutant (⋃x∈X. adj ` A x))›
by (simp add: commutant_adj image_UN)
also have ‹… ⊆ commutant (commutant (⋃x∈X. A x))›
using assms by (auto simp: von_neumann_algebra_def intro!: commutant_antimono)
finally show ‹a* ∈ commutant (commutant (⋃x∈X. A x))›
by -
qed
lemma von_neumann_algebra_union:
assumes ‹von_neumann_algebra A›
assumes ‹von_neumann_algebra B›
shows ‹von_neumann_algebra (commutant (commutant (A ∪ B)))›
using von_neumann_algebra_UNION[where X=‹{True,False}› and A=‹λx. if x then A else B›]
by (auto simp: assms Un_ac(3))
lemma von_neumann_algebra_commutant: ‹von_neumann_algebra (commutant A)› if ‹von_neumann_algebra A›
proof (rule von_neumann_algebraI)
show ‹a* ∈ commutant A› if ‹a ∈ commutant A› for a
by (smt (verit) Set.basic_monos(7) ‹von_neumann_algebra A› commutant_adj commutant_antimono double_adj image_iff image_subsetI that von_neumann_algebra_def)
show ‹commutant (commutant (commutant A)) ⊆ commutant A ›
by simp
qed
lemma von_neumann_algebra_def_sot:
‹von_neumann_algebra 𝔉 ⟷
(∀a∈𝔉. a* ∈ 𝔉) ∧ csubspace 𝔉 ∧ (∀a∈𝔉. ∀b∈𝔉. a o⇩C⇩L b ∈ 𝔉) ∧ id_cblinfun ∈ 𝔉 ∧
closedin cstrong_operator_topology 𝔉›
proof (unfold von_neumann_algebra_def, intro iffI conjI; elim conjE; assumption?)
assume comm: ‹commutant (commutant 𝔉) = 𝔉›
from comm show ‹closedin cstrong_operator_topology 𝔉›
by (metis commutant_sot_closed)
from comm show ‹csubspace 𝔉›
by (metis csubspace_commutant)
from comm show ‹∀a∈𝔉. ∀b∈𝔉. a o⇩C⇩L b ∈ 𝔉›
using commutant_mult by blast
from comm show ‹id_cblinfun ∈ 𝔉›
by blast
next
assume adj: ‹∀a∈𝔉. a* ∈ 𝔉›
assume subspace: ‹csubspace 𝔉›
assume closed: ‹closedin cstrong_operator_topology 𝔉›
assume mult: ‹∀a∈𝔉. ∀b∈𝔉. a o⇩C⇩L b ∈ 𝔉›
assume id: ‹id_cblinfun ∈ 𝔉›
have ‹commutant (commutant 𝔉) = cstrong_operator_topology closure_of 𝔉›
apply (rule double_commutant_theorem)
thm double_commutant_theorem[of 𝔉]
using subspace subspace mult id adj
by simp_all
also from closed have ‹… = 𝔉›
by (simp add: closure_of_eq)
finally show ‹commutant (commutant 𝔉) = 𝔉›
by -
qed
lemma double_commutant_hull':
assumes ‹⋀x. x ∈ X ⟹ x* ∈ X›
shows ‹commutant (commutant X) = von_neumann_algebra hull X›
proof (rule antisym)
show ‹commutant (commutant X) ⊆ von_neumann_algebra hull X›
apply (subst double_commutant_hull)
apply (rule hull_antimono)
by (simp add: von_neumann_algebra_def)
show ‹von_neumann_algebra hull X ⊆ commutant (commutant X)›
apply (rule hull_minimal)
by (simp_all add: von_neumann_algebra_def assms commutant_adj_closed)
qed
lemma commutant_one_algebra: ‹commutant one_algebra = UNIV›
by (metis commutant_UNIV commutant_empty triple_commutant)
definition tensor_vn (infixr "⊗⇩v⇩N" 70) where
‹tensor_vn X Y = commutant (commutant ((λa. a ⊗⇩o id_cblinfun) ` X ∪ (λa. id_cblinfun ⊗⇩o a) ` Y))›
lemma von_neumann_algebra_adj_image: ‹von_neumann_algebra X ⟹ adj ` X = X›
by (auto simp: von_neumann_algebra_def intro!: image_eqI[where x=‹_*›])
lemma von_neumann_algebra_tensor_vn:
assumes ‹von_neumann_algebra X›
assumes ‹von_neumann_algebra Y›
shows ‹von_neumann_algebra (X ⊗⇩v⇩N Y)›
proof (rule von_neumann_algebraI)
have ‹adj ` (X ⊗⇩v⇩N Y) = commutant (commutant ((λa. a ⊗⇩o id_cblinfun) ` adj ` X ∪ (λa. id_cblinfun ⊗⇩o a) ` adj ` Y))›
by (simp add: tensor_vn_def commutant_adj image_image image_Un tensor_op_adjoint)
also have ‹… = commutant (commutant ((λa. a ⊗⇩o id_cblinfun) ` X ∪ (λa. id_cblinfun ⊗⇩o a) ` Y))›
using assms by (simp add: von_neumann_algebra_adj_image)
also have ‹… = X ⊗⇩v⇩N Y›
by (simp add: tensor_vn_def)
finally show ‹a* ∈ X ⊗⇩v⇩N Y› if ‹a ∈ X ⊗⇩v⇩N Y› for a
using that by blast
show ‹commutant (commutant (X ⊗⇩v⇩N Y)) ⊆ X ⊗⇩v⇩N Y›
by (simp add: tensor_vn_def)
qed
lemma tensor_vn_one_one[simp]: ‹one_algebra ⊗⇩v⇩N one_algebra = one_algebra›
apply (simp add: tensor_vn_def one_algebra_def image_image
tensor_op_scaleC_left tensor_op_scaleC_right)
by (simp add: commutant_one_algebra commutant_UNIV flip: one_algebra_def)
lemma sandwich_swap_tensor_vn: ‹sandwich swap_ell2 ` (X ⊗⇩v⇩N Y) = Y ⊗⇩v⇩N X›
by (simp add: tensor_vn_def sandwich_unitary_commutant image_Un image_image Un_commute)
lemma tensor_vn_one_left: ‹one_algebra ⊗⇩v⇩N X = (λx. id_cblinfun ⊗⇩o x) ` X› if ‹von_neumann_algebra X›
proof -
have ‹one_algebra ⊗⇩v⇩N X = commutant
(commutant ((λa. id_cblinfun ⊗⇩o a) ` X))›
apply (simp add: tensor_vn_def one_algebra_def image_image)
by (metis (no_types, lifting) Un_commute Un_empty_right commutant_UNIV commutant_empty double_commutant_Un_right image_cong one_algebra_def tensor_id tensor_op_scaleC_left)
also have ‹… = (λa. id_cblinfun ⊗⇩o a) ` commutant (commutant X)›
by (simp add: amplification_double_commutant_commute')
also have ‹… = (λa. id_cblinfun ⊗⇩o a) ` X›
using that von_neumann_algebra_def by blast
finally show ?thesis
by -
qed
lemma tensor_vn_one_right: ‹X ⊗⇩v⇩N one_algebra = (λx. x ⊗⇩o id_cblinfun) ` X› if ‹von_neumann_algebra X›
proof -
have ‹X ⊗⇩v⇩N one_algebra = sandwich swap_ell2 ` (one_algebra ⊗⇩v⇩N X)›
by (simp add: sandwich_swap_tensor_vn)
also have ‹… = sandwich swap_ell2 ` (λx. id_cblinfun ⊗⇩o x) ` X›
by (simp add: tensor_vn_one_left that)
also have ‹… = (λx. x ⊗⇩o id_cblinfun) ` X›
by (simp add: image_image)
finally show ?thesis
by -
qed
lemma double_commutant_in_vn_algI: ‹commutant (commutant X) ⊆ Y›
if ‹von_neumann_algebra Y› and ‹X ⊆ Y›
by (metis commutant_antimono that(1) that(2) von_neumann_algebra_def)
lemma von_neumann_algebra_compose:
assumes ‹von_neumann_algebra M›
assumes ‹x ∈ M› and ‹y ∈ M›
shows ‹x o⇩C⇩L y ∈ M›
using assms apply (auto simp: von_neumann_algebra_def commutant_def)
by (metis (no_types, lifting) assms(1) commutant_mult von_neumann_algebra_def)
lemma von_neumann_algebra_id:
assumes ‹von_neumann_algebra M›
shows ‹id_cblinfun ∈ M›
using assms by (auto simp: von_neumann_algebra_def)
lemma tensor_vn_UNIV[simp]: ‹UNIV ⊗⇩v⇩N UNIV = (UNIV :: (('a×'b) ell2 ⇒⇩C⇩L _) set)›
proof -
have ‹(UNIV ⊗⇩v⇩N UNIV :: (('a×'b) ell2 ⇒⇩C⇩L _) set) =
commutant (commutant (range (λa. a ⊗⇩o id_cblinfun) ∪ range (λa. id_cblinfun ⊗⇩o a)))› (is ‹_ = ?rhs›)
by (simp add: tensor_vn_def commutant_cspan)
also have ‹… ⊇ commutant (commutant {a ⊗⇩o b |a b. True})› (is ‹_ ⊇ …›)
proof (rule double_commutant_in_vn_algI)
show vn: ‹von_neumann_algebra ?rhs›
by (metis calculation von_neumann_algebra_UNIV von_neumann_algebra_tensor_vn)
show ‹{a ⊗⇩o b |(a :: 'a ell2 ⇒⇩C⇩L _) (b :: 'b ell2 ⇒⇩C⇩L _). True} ⊆ ?rhs›
proof (rule subsetI)
fix x :: ‹('a × 'b) ell2 ⇒⇩C⇩L ('a × 'b) ell2›
assume ‹x ∈ {a ⊗⇩o b |a b. True}›
then obtain a b where ‹x = a ⊗⇩o b›
by auto
then have ‹x = (a ⊗⇩o id_cblinfun) o⇩C⇩L (id_cblinfun ⊗⇩o b)›
by (simp add: comp_tensor_op)
also have ‹… ∈ ?rhs›
proof -
have ‹a ⊗⇩o id_cblinfun ∈ ?rhs›
by (auto intro!: double_commutant_grows')
moreover have ‹id_cblinfun ⊗⇩o b ∈ ?rhs›
by (auto intro!: double_commutant_grows')
ultimately show ?thesis
using commutant_mult by blast
qed
finally show ‹x ∈ ?rhs›
by -
qed
qed
also have ‹… = cstrong_operator_topology closure_of (cspan {a ⊗⇩o b |a b. True})›
apply (rule double_commutant_theorem_span)
apply (auto simp: comp_tensor_op tensor_op_adjoint)
using tensor_id[symmetric] by blast+
also have ‹… = UNIV›
using tensor_op_dense by blast
finally show ?thesis
by auto
qed
unbundle no cblinfun_syntax
end