Quantum Set #

This file defines the structure of a quantum set.

A quantum set is defined as a star-algebra A over ℂ with a positive element Q such that Q is invertible and a sum of rank-one operators (in other words, positive definite). The quantum set is also equipped with a faithful positive linear functional φ on A, which is used to define the inner product on A, i.e., ⟪x, y⟫_ℂ = φ (star x * y). The quantum set is also equipped with a trace functional on A such that φ x = trace (Q * x).

Main definitions #

quantum_set A is a structure that defines a quantum set.
quantum_set.mod_aut A t defines the modular automorphism of a quantum set, which is a family of automorphisms of A parameterized by t : ℝ, given by x ↦ Q^(-t) * x * Q^t, where Q is the unique positive definite element in A given by the quantum set structure.

source

@[class]

structure quantum_set (A : Type u_1) :

Type (u_1+1)

to_normed_add_comm_group_of_ring : normed_add_comm_group_of_ring A
to_inner_product_space : inner_product_space ℂ A
to_partial_order : partial_order A
to_star_ordered_ring : star_ordered_ring A
to_has_smul_comm_class : smul_comm_class ℂ A A
to_is_scalar_tower : is_scalar_tower ℂ A A
to_finite_dimensional : finite_dimensional ℂ A
to_has_inv : has_inv A
φ : module.dual ℂ A
hφ : quantum_set.φ.is_faithful_pos_map
inner_eq : ∀ (x y : A), has_inner.inner x y = ⇑quantum_set.φ (has_star.star x * y)
functional_adjoint_eq : let _inst : algebra ℂ A := algebra.of_is_scalar_tower_smul_comm_class in ⇑linear_map.adjoint quantum_set.φ = ↑(algebra.linear_map ℂ A)
A_pos : Type ?
A_pos_has_pow : has_pow {x // 0 < x} ℝ
A_pos_has_inv : has_inv {x // 0 < x}
A_pos_pow_mul : ∀ (x : {x // 0 < x}) (t s : ℝ), ↑(x ^ t) * ↑(x ^ s) = ↑(x ^ (t + s))
A_pos_pow_zero : ∀ (x : {x // 0 < x}), ↑(x ^ 0) = 1
A_pos_pow_one : ∀ (x : {x // 0 < x}), x ^ 1 = x
A_pos_pow_neg : ∀ (x : {x // 0 < x}) (t : ℝ), x ^ -t = (x ^ t)⁻¹
A_pos_inv_coe : ∀ (x : {x // 0 < x}), (↑x)⁻¹ = ↑x⁻¹
Q : {x // 0 < x}
trace : module.dual ℂ A
trace_is_tracial : quantum_set.trace.is_tracial
functional_eq : ∀ (x : A), ⇑quantum_set.φ x = ⇑quantum_set.trace (↑quantum_set.Q * x)

Instances for quantum_set

quantum_set.has_sizeof_inst

source

@[simp]

theorem quantum_set.mod_aut_apply (A : Type u_1) [quantum_set A] (t : ℝ) (x : A) :

⇑(quantum_set.mod_aut A t) x = ↑(quantum_set.Q ^ -t) * x * ↑(quantum_set.Q ^ t)

source

@[simp]

theorem quantum_set.mod_aut_symm_apply (A : Type u_1) [quantum_set A] (t : ℝ) (x : A) :

⇑((quantum_set.mod_aut A t).symm) x = ↑(quantum_set.Q ^ t) * x * ↑(quantum_set.Q ^ -t)

source

def quantum_set.mod_aut (A : Type u_1) [quantum_set A] (t : ℝ) :

A ≃ₐ[ℂ ] A

Equations

quantum_set.mod_aut A t = let A_pos : Type u_1 := {x // 0 < x}, Q : A_pos := quantum_set.Q in {to_fun := λ (x : A), ↑(Q ^ -t) * x * ↑(Q ^ t), inv_fun := λ (x : A), ↑(Q ^ t) * x * ↑(Q ^ -t), left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}

source

theorem quantum_set.mod_aut_trans {A : Type u_1} [quantum_set A] (t s : ℝ) :

(quantum_set.mod_aut A t).trans (quantum_set.mod_aut A s) = quantum_set.mod_aut A (t + s)

source

theorem quantum_set.mod_aut_neg {A : Type u_1} [quantum_set A] (t : ℝ) :

quantum_set.mod_aut A (-t) = (quantum_set.mod_aut A t).symm