Theory Cstar_Algebra_On
section ‹$C^*$-algebras›
theory Cstar_Algebra_On
imports
Lie_Groups.Algebra_On
Types_To_Sets_Extension.SML_Topological_Space
Complex_Bounded_Operators.Complex_Vector_Spaces
"HOL-Analysis.Abstract_Metric_Spaces"
begin
bundle scaleC_syntax begin
notation Complex_Vector_Spaces0.scaleC_class.scaleC (infixr ‹*⇩C› 75)
end
unbundle no scaleC_syntax
subsection ‹Additional lemmas for \<^theory>‹Lie_Groups.Algebra_On››
lemma (in algebra_on)
shows distR': "⟦x∈S; y∈S; z∈S⟧ ⟹ (x-y) ⦁ z = x ⦁ z - y ⦁ z"
and distL': "⟦x∈S; y∈S; z∈S⟧ ⟹ z ⦁ (x-y) = z ⦁ x - z ⦁ y"
using distR m1.mem_uminus apply fastforce
using distL m1.mem_uminus by fastforce
subsection ‹Involutive rings and algebras›
locale involutive_semigroup = semigroup_add_on_with +
fixes involution :: "'a⇒'a" (‹_⇧†› [99] 100)
assumes involution[simp]: "x∈S ⟹ (x⇧†)⇧† = x"
and antiautomorphism: "⟦x∈S; y∈S⟧ ⟹ (pls x y)⇧† = pls (y⇧†) (x⇧†)"
and involution_mem[simp]: "x∈S ⟹ x⇧† ∈ S"
bundle class_ring_notation begin
notation plus (infixl "+" 65)
notation minus (infixl ‹-› 65)
notation uminus (‹(‹open_block notation=‹prefix -››- _)› [81] 80)
end
unbundle no class_ring_notation
locale involutive_ring =
Ring_Theory.ring R addition multiplication zero unit +
involutive_semigroup R multiplication involution
for R :: "'a set" and addition :: "'a⇒'a⇒'a" (infixl "+" 65)
and multiplication (infixl "⋅" 70) and zero ("𝟬") and unit ("𝟭")
and involution :: "'a⇒'a" (‹_⇧†› [99] 100) +
assumes ivl_ring: "⟦x∈R; y∈R⟧ ⟹ (x+y)⇧† = x⇧† + y⇧†"
begin
lemma unit_self_adjoint: "𝟭⇧† = 𝟭"
using antiautomorphism[of _ 𝟭] involution involution_mem
by (metis multiplicative.right_unit multiplicative.unit_closed)
lemma ivl_uminus: "x∈R ⟹ involution (-x) = - involution x"
by (metis (no_types, lifting) additive.inverse_equality additive.invertible additive.invertibleE
additive.invertible_left_inverse2 additive.unit_closed involution_mem ivl_ring)
lemma ivl_minus: "⟦x∈R; y∈R⟧ ⟹ involution (x-y) = involution x - involution y"
by (simp add: ivl_ring ivl_uminus)
end
unbundle class_ring_notation
text ‹A general definition of $^*$-algebra might look as follows.
\begin{definition}[$^*$-algebra]
Let $A$ be a ring with involution $^*$, and $R$ any commutative ring with involution $'$.
$A$ is a $^*$-algebra if it is an associative algebra over $R$, such that:
\[
\forall r \in R. \forall a \in A. (r a)^* = r' a^*
\]
A \emph{$^*$-homomorphism} $f\colon A \to B$ is an algebra homomorphism that respects involution:
\[ \forall a \in A. f(a)^{*_B} = f(a^{*_A}) \]
\end{definition}
Since nearly all formalisation seems to use classes for the vector addition and base field,
and some texts (e.g. \cite{fewster2019}) define $^*$-algebras using the complex numbers as
a base ring directly, we do so as well, without worrying about the involution of the base ring
being specified only implicitly, on a type-level. Even category theory is, most of the time,
only interested in categories of spaces over a shared base field/ring.
Note also our involutive complex algebras are unital (and associative).›
locale involutive_complex_algebra =
assoc_algebra_1_on S scale multiplication unit +
involutive_ring S "(+)" multiplication 0 unit involution
for S :: "'a::ab_group_add set"
and scale :: "complex ⇒ 'a ⇒ 'a" (infixr ‹*⇩C› 75)
and multiplication :: "'a ⇒ 'a ⇒ 'a" (infixr ‹⦁› 74)
and unit :: "'a" (‹𝟭›)
and involution :: "'a⇒'a" (‹_⇧†› [99] 100) +
assumes ivl_scale: "s∈S ⟹ (c *⇩C s)⇧† = cnj c *⇩C s⇧†"
lemma involutive_complex_algebraI:
fixes S :: "'a::ab_group_add set"
and scl :: "complex ⇒ 'a ⇒ 'a"
and mlt :: "'a ⇒ 'a ⇒ 'a"
and e :: "'a"
and involution :: "'a⇒'a"
assumes "assoc_algebra_1_on S scl mlt e"
and involution: "∀x. x∈S ⟶ involution (involution x) = x"
and antiautomorphism: "∀x y. x∈S ⟶ y∈S ⟶ involution (mlt x y) = mlt (involution y) (involution x)"
and ivl_mem: "∀x. x∈S ⟶ involution x ∈ S"
and ivl_ring: "∀x y. x∈S⟶ y∈S ⟶ involution (x+y) = (involution x) + (involution y)"
and ivl_scale: "∀x c. x∈S ⟶ involution (scl c x) = scl (cnj c) (involution x)"
shows "involutive_complex_algebra S scl mlt e involution"
proof -
interpret alg: assoc_algebra_1_on S scl mlt e using assms(1).
interpret mon: Group_Theory.monoid S "(+)" 0
by (unfold_locales, simp_all add: group_cancel.add1 alg.m1.mem_add alg.m1.mem_zero)
have "mon.invertible u" if "u ∈ S" for u
by (meson ab_left_minus alg.m1.mem_uminus mon.invertibleI neg_eq_iff_add_eq_0 that)
then show "involutive_complex_algebra S scl mlt e involution"
by (unfold_locales, simp_all add: alg.m1.subspace_UNIV alg.m1.subspace_add add.commute
add.left_commute alg.amult_assoc alg.distL alg.distR assms(2-))
qed
lemma (in module_on) sub_module:
assumes "subspace A" "A⊆S"
shows "module_on A scale"
using assms module_on.intro module_on.subspace_def module_on_axioms scale_left_distrib_on
scale_one_on scale_right_distrib_on scale_scale_on subset_eq by (smt (verit, ccfv_threshold))
locale involutive_subalgebra =
subalg: involutive_complex_algebra A + involutive_complex_algebra B for A B +
assumes "A ⊆ B"
lemma (in involutive_complex_algebra) subalgebraI:
fixes A
assumes unital_subspace: "m1.subspace A" "A ⊆ S" "𝟭 ∈ A"
and mult_closed: "∀x y. x ∈ A ⟶ y ∈ A ⟶ x ⦁ y ∈ A"
and involution_closed: "∀x. x ∈ A ⟶ involution x ∈ A"
shows "involutive_subalgebra (*⇩C) (⦁) 𝟭 involution A S"
proof -
interpret vector_space_on A
using m1.sub_module unital_subspace(1,2) vector_space_on.intro by blast
interpret subalg: assoc_algebra_1_on A "(*⇩C)" "(⦁)" 𝟭
apply unfold_locales
apply (meson in_mono linearL'(2) unital_subspace(2))
apply (meson unital_subspace(2) in_mono linearL'(1))
apply (meson distributive(1) in_mono unital_subspace(2))
apply (meson unital_subspace(2) linearR'(1) subsetD)
using assms(4) apply blast
using unital_subspace(2) apply blast
apply (simp add: unital_subspace(3))
using unital_subspace(2) apply blast
using unital_subspace(2) apply blast
by simp
interpret ivl_subalg: involutive_complex_algebra A
apply (intro involutive_complex_algebraI)
subgoal by unfold_locales
using involution unital_subspace(2) apply blast
apply (meson antiautomorphism in_mono unital_subspace(2))
using involution_closed apply blast
apply (meson ivl_ring subset_eq unital_subspace(2))
using assms(2) ivl_scale by blast
show ?thesis
by (unfold_locales, simp add: assms(2))
qed
subsection ‹Preliminaries and experiments›
context Metric_space begin