Theory Gelfand_Naimark_Segal
section ‹The Gelfand--Naimark--Segal Construction›
theory Gelfand_Naimark_Segal
imports
Inner_Completion
Cstar_Algebra_On
Complex_Bounded_Operators.Complex_Bounded_Linear_Function
Smooth_Manifolds.Analysis_More
begin
unbundle lifting_syntax
subsection ‹Strengthen lifting lemmas›
subsubsection ‹Lifting to the metric completion›
lemma inj_to_metric_completion: "inj to_metric_completion"
using isometry_on_injective to_metric_completion_isometry by blast
definition "from_metric_completion ≡ the_inv to_metric_completion"
lemma lift_to_metric_completion2:
fixes f::"('a::metric_space) ⇒ ('b::complete_space)"
assumes "uniformly_continuous_on UNIV f"
shows "∃g. (uniformly_continuous_on UNIV g)
∧ (f = g o to_metric_completion)
∧ (∀x ∈ range to_metric_completion. g x = f (from_metric_completion x))"
unfolding from_metric_completion_def
using lift_to_metric_completion[OF assms]
by (simp add: inj_to_metric_completion the_inv_f_f)
lemma lift_to_metric_completion_isometry2:
fixes f::"('a::metric_space) ⇒ ('b::complete_space)"
assumes "isometry_on UNIV f"
shows "∃g. isometry_on UNIV g
∧ range g = closure(range f)
∧ f = g o to_metric_completion
∧ (∀x ∈ range to_metric_completion. g x = f (from_metric_completion x))"
unfolding from_metric_completion_def
using lift_to_metric_completion_isometry[OF assms]
by (simp add: inj_to_metric_completion the_inv_f_f)
lemma dense_imp_conv_seq:
assumes "closure S = U" "x∈U"
shows "∃s. (s n) ∈ S ∧ s ⇢ x"
using LIMSEQ_if_less
by (metis (full_types, lifting) ext all_not_in_conv
assms closed_empty closure_closed order.strict_iff_order)
lemma to_metric_completion_sequence_ex:
shows "∃s. (to_metric_completion o s) ⇢ x"
using dense_imp_conv_seq[of "range to_metric_completion" UNIV]
by (smt (verit, best) UNIV_I closure_sequential function_factors_right image_iff
to_metric_completion_dense')
lemma cinner_extensionality_dense:
assumes dense_S: "closure S = UNIV"
and inner_on_S: "∀z∈S. cinner z x = cinner z y"
shows "x = y"
proof (rule cinner_extensionality)
fix z :: "'a::complex_inner"
obtain s where s: "s ⇢ z" "⋀n::nat. (s n) ∙⇩C x = (s n) ∙⇩C y"
by (metis UNIV_I closure_sequential dense_S inner_on_S)
have "(λn. s n ∙⇩C x) ⇢ z ∙⇩C x"
and"(λn. s n ∙⇩C x) ⇢ z ∙⇩C y"
apply (simp add: s(1) tendsto_cinner)
unfolding s(2) by (simp add: s(1) tendsto_cinner)
thus "z ∙⇩C x = z ∙⇩C y"
using LIMSEQ_unique by blast
qed
lemma cinner_extensionality_metric_completion:
assumes "∀z. cinner (to_metric_completion z) x = cinner (to_metric_completion z) y"
shows "x = y"
using cinner_extensionality_dense[OF to_metric_completion_dense'] assms
by blast
lemma completion_ext_simp1:
fixes f::"('m::metric_space) ⇒ ('c::complete_space)" and g
defines "D ≡ range to_metric_completion"
shows "(f = g o to_metric_completion) ⟷
(∀x ∈ D. g x = f (from_metric_completion x))"
unfolding assms o_def from_metric_completion_def
using f_the_inv_into_f the_inv_f_f inj_to_metric_completion
by (metis rangeI)
lemma lift_to_metric_completion4:
fixes f::"('m::metric_space) ⇒ ('c::complete_space)"
assumes "uniformly_continuous_on UNIV f"
shows "∃!g. (uniformly_continuous_on UNIV g)
∧ (f = g ∘ to_metric_completion)"
proof -
{ fix x y and v :: "'m metric_completion"
assume x: "isUCont x" "f = x ∘ to_metric_completion"
and y: "isUCont y" "f = y ∘ to_metric_completion"
have x3: "∀b∈range to_metric_completion. x b = f (from_metric_completion b)"
and y3: "∀b∈range to_metric_completion. y b = f (from_metric_completion b)"
using completion_ext_simp1 x(2) y(2) by blast+
have "∃s. (to_metric_completion o s) ⇢ v"
using to_metric_completion_sequence_ex .
then obtain s :: "nat⇒'m" where s: "(to_metric_completion ∘ s) ⇢ v"
by blast
let ?s = "to_metric_completion o s"
have x_to_x: "(x ∘ ?s) ⇢ x v"
and y_to_y: "(y ∘ ?s) ⇢ y v"
using continuous_at_sequentially isUCont_isCont s x(1) y(1) by blast+
moreover have "∀b∈range to_metric_completion. x b = y b"
using x3 y3 by presburger
ultimately have x_to_y: "(x ∘ ?s) ⇢ y v"
by (metis fun.map_comp x(2) y(2))
have "x v = y v"
using LIMSEQ_unique x_to_x x_to_y by blast
} note 1 = this
have "∃!x. isUCont x ∧
f = x ∘ to_metric_completion ∧
(∀xa∈range to_metric_completion.
x xa = f (from_metric_completion xa))"
by (metis (no_types, lifting) ext "1" assms lift_to_metric_completion2)
thus ?thesis
using completion_ext_simp1
by (metis (no_types, lifting))
qed
lemma lift_to_metric_completion3:
fixes f::"('m::metric_space) ⇒ ('c::complete_space)"
assumes "uniformly_continuous_on UNIV f"
shows "∃!g. (uniformly_continuous_on UNIV g)
∧ (f = g o to_metric_completion)
∧ (∀x ∈ range to_metric_completion. g x = f (from_metric_completion x))"
by (metis assms lift_to_metric_completion2 lift_to_metric_completion4)
subsubsection ‹Lifting a bounded operator from an inner product space to a Hilbert space›
lemma to_metric_completion_cblinfun_exists:
fixes f :: ‹'a::complex_normed_vector ⇒ 'b::cbanach›
assumes f_add: ‹⋀x y. f (x + y) = f x + f y›
assumes f_scale: ‹⋀c x y. f (c *⇩C x) = c *⇩C f x›
assumes bounded: ‹⋀x. norm (f x) ≤ B * norm x›
shows "cblinfun_extension_exists (range to_metric_completion)
(map_fun (from_metric_completion) id f)"
(is ‹cblinfun_extension_exists ?D ?f›)
proof -
interpret f: bounded_clinear f
by unfold_locales (use f_add f_scale bounded in ‹auto simp: mult.commute›)
obtain K where K: "⋀x. norm (f x) ≤ norm x * K"
using f.real.bounded by blast
interpret m: bounded_clinear to_metric_completion
using to_metric_completion_bounded_clinear .
show ?thesis
proof (rule cblinfun_extension_exists_bounded_dense)
fix c x y
assume x: "x ∈ ?D"
show "?f (c *⇩C x) = c *⇩C ?f x"
unfolding map_fun_def from_metric_completion_def apply simp
using the_inv_f_f[OF inj_to_metric_completion]
by (metis x assms(2) m.scale rangeE)
show "norm (?f x) ≤ K * norm x"
unfolding map_fun_def from_metric_completion_def apply simp
using the_inv_f_f[OF inj_to_metric_completion]
using to_metric_completion_norm
by (metis Extra_Ordered_Fields.sign_simps(5) K rangeE x)
assume y: "y ∈ ?D"
show "?f (x + y) = ?f x + ?f y"
unfolding map_fun_def from_metric_completion_def apply simp
using the_inv_f_f[OF inj_to_metric_completion] f_the_inv_into_f[OF inj_to_metric_completion]
using m.add f.add
by (metis (no_types, lifting) x y)
qed (use range_is_csubspace to_metric_completion_clinear in blast,
use to_metric_completion_dense' in blast)
qed
lemma to_metric_completion_cblinfun_exists':
fixes f :: ‹('a::complex_normed_vector, 'b::cbanach) cblinfun›
shows "cblinfun_extension_exists (range to_metric_completion)
(map_fun (from_metric_completion) id f)"
using to_metric_completion_cblinfun_exists
cblinfun.add_right cblinfun.scaleC_right norm_cblinfun
by meson
subsection ‹The $C^*$-algebra of bounded operators on a Hilbert space›
text ‹The assumption on the next lemma is a nondegeneracy condition found as the defining
assumption of \<^locale>‹assoc_algebra_1_on›. It's similar also to the class \<^class>‹zero_neq_one›,
which enters for example into \<^class>‹ring_1›, \<^class>‹field›, and \<^class>‹one_dim›.›
lemma Cstar_cblinfun:
includes cblinfun_syntax
assumes "(id_cblinfun :: ('b ⇒⇩C⇩L ('b::chilbert_space))) ≠ 0"
shows "Cstar_algebra UNIV (UNIV :: ('b ⇒⇩C⇩L ('b::chilbert_space)) set) (*⇩C) (o⇩C⇩L) norm id_cblinfun adj"
(is "Cstar_algebra ?C ?B _ _ _ _ _")
proof -
interpret normed_vector_space_on ?C cmod ?B "(*⇩C)" norm
by (unfold_locales,
auto simp: norm_triangle_ineq norm_mult_ineq norm_mult complex_vector.vector_space_assms(1,2))
interpret Group_Theory.monoid ?B "(+)" 0
by unfold_locales auto
interpret involutive_complex_algebra ?B "(*⇩C)" "(o⇩C⇩L)" id_cblinfun adj
by (unfold_locales,
auto simp: assms cblinfun_compose_add_left cblinfun_compose_add_right lift_cblinfun_comp(2)
add_eq_0_iff adj_plus)
have "complete ?B"
by (simp add: complete_UNIV)
then have "mcomplete"
unfolding mcomplete_iff_complete[symmetric] dist_cblinfun_def totalized_induced_metric_def
by (simp add: norm_minus_commute)
show ?thesis
apply unfold_locales
using ‹mcomplete› by (auto simp:
norm_is_Proj_nonzero norm_cblinfun_compose power2_eq_square)
qed
text ‹The above can be used e.g. as
@{thm Cstar_cblinfun[OF id_cblinfun_not_0]}, or using \<^class>‹zero_neq_one›.›
subsection ‹Type class of $C^*$-algebras›
text ‹Make a bundle to (de)activate dagger notation for adjoints of functions
between types in the class of complex inner product spaces.›
bundle cadjoint_syntax begin
notation Complex_Inner_Product.cadjoint ("_⇧†" [99] 100)
end
unbundle no cadjoint_syntax
class cstar = complex_normed_algebra_1 + cbanach +
fixes involution::"'a⇒'a" ("_⇧†" [99] 100)
assumes ivl_scaleC: "(c *⇩C s)⇧† = cnj c *⇩C s⇧†"
and ivl_plus [simp]: "(x+y)⇧† = x⇧† + y⇧†"
and involution[simp]: "(x⇧†)⇧† = x"
and ivl_times [simp]: "(x * y)⇧† = y⇧† * x⇧†"
and ivl_isometric: "norm (A⇧†) = norm A"
and Cstar: "norm (A⇧† * A) = (norm (A⇧†)) * (norm A)"
begin
text ‹
A class analogue of \<^locale>‹Cstar_algebra›,
reproducing the axioms @{thm Cstar_algebra_axioms_def} one-by-one.
Some assumptions of \<^locale>‹Cstar_algebra› are in \<^class>‹real_normed_algebra›, compare:
\begin{itemize}
\item @{thm Cstar_algebra.normed_algebra} with @{thm norm_mult_ineq},
\item @{thm Cstar_algebra.normed_unital} with @{thm norm_one}.
\end{itemize}
›
end
bundle cstar_syntax begin
notation involution ("_⇧†" [99] 100)
end
unbundle cstar_syntax
lemma cstar_locale: "Cstar_algebra UNIV (UNIV::'a::cstar set)
scaleC times norm 1 involution"
proof -
have 0: "Metric_space.mcomplete (UNIV::'a set)
(normed_vector_space_on.totalized_induced_metric UNIV norm)"
by (simp add: complete_UNIV totalized_induced_metric_eq_dist)
have 1: "monoid.invertible UNIV (+) 0 u"
for u :: 'a
proof -
interpret Group_Theory.monoid UNIV "(+)" "0::'a"
by unfold_locales simp_all
show ?thesis
unfolding invertible_def[simplified]
by (intro exI[of _ "-u"]) simp
qed
have 2: "involution u * involution (of_complex c) =
of_complex (cnj c) * involution u"
for u :: 'a and c::complex
using ivl_scaleC by auto
have 3: "norm (of_complex c * u) = cmod c * norm u"
for u :: 'a and c::complex
by (metis norm_scaleC scaleC_conv_of_complex)
have 4: "v * (of_complex c * u) = of_complex c * (v * u)"
for u v :: 'a and c::complex
by (metis mult_scaleC_right scaleC_conv_of_complex)
show ?thesis
apply unfold_locales
apply (simp_all add: ivl_isometric Cstar
norm_triangle_ineq norm_mult Groups.mult_ac(1)
nat_distrib(2) cross3_simps(23) norm_mult_ineq)
using 0 1 2 3 4 by simp_all
qed
text ‹We \emph{have to} interpret \<^class>‹cstar› as a \<^locale>‹Cstar_algebra›
in stages, and name the interpretation of the \<^locale>‹involutive_complex_algebra›,
otherwise there is a naming conflict between
@{thm algebra_on.lie_algebraI} and @{thm vector_space_on.lie_algebraI}.›