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.

@[reducible]

class starAlgebra (A : Type u_1) extends Ring A, Algebra ℂ A, StarRing A, StarModule ℂ A : Type u_1

• add : A → A → A
• add_assoc (a b c : A) : a + b + c = a + (b + c)
• zero : A
• zero_add (a : A) : 0 + a = a
• add_zero (a : A) : a + 0 = a
• nsmul : ℕ → A → A
• nsmul_zero (x : A) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : A) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• add_comm (a b : A) : a + b = b + a
• mul : A → A → A
• left_distrib (a b c : A) : a * (b + c) = a * b + a * c
• right_distrib (a b c : A) : (a + b) * c = a * c + b * c
• zero_mul (a : A) : 0 * a = 0
• mul_zero (a : A) : a * 0 = 0
• mul_assoc (a b c : A) : a * b * c = a * (b * c)
• one : A
• one_mul (a : A) : 1 * a = a
• mul_one (a : A) : a * 1 = a
• natCast : ℕ → A
• natCast_zero : NatCast.natCast 0 = 0
• natCast_succ (n : ℕ) : NatCast.natCast (n + 1) = NatCast.natCast n + 1
• npow : ℕ → A → A
• npow_zero (x : A) : Semiring.npow 0 x = 1
• npow_succ (n : ℕ) (x : A) : Semiring.npow (n + 1) x = Semiring.npow n x * x
• neg : A → A
• sub : A → A → A
• sub_eq_add_neg (a b : A) : a - b = a + -b
• zsmul : ℤ → A → A
• zsmul_zero' (a : A) : Ring.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : A) : Ring.zsmul (↑n.succ) a = Ring.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : A) : Ring.zsmul (Int.negSucc n) a = -Ring.zsmul (↑n.succ) a
• neg_add_cancel (a : A) : -a + a = 0
• intCast : ℤ → A
• intCast_ofNat (n : ℕ) : IntCast.intCast ↑n = ↑n
• intCast_negSucc (n : ℕ) : IntCast.intCast (Int.negSucc n) = -↑(n + 1)
• smul : ℂ → A → A
• algebraMap : ℂ →+* A
• commutes' (r : ℂ) (x : A) : Algebra.algebraMap r * x = x * Algebra.algebraMap r
• smul_def' (r : ℂ) (x : A) : r • x = Algebra.algebraMap r * x
• star : A → A
• star_involutive : Function.Involutive star
• star_mul (r s : A) : star (r * s) = star s * star r
• star_add (r s : A) : star (r + s) = star r + star s
• star_smul (r : ℂ) (a : A) : star (r • a) = star r • star a
• modAut : ℝ → A ≃ₐ[ℂ] A

  the modular automorphism σ _ as a linear isomorphism A ≃ₗ[ℂ] A

• modAut_trans (r s : ℝ) : (modAut r).trans (modAut s) = modAut (r + s)

  the modular automorphism is an additive homomorphism from ℝ to (A ≃ₐ[ℂ] A, add := · * ·, zero := 1)

• modAut_star (r : ℝ) (x : A) : star ((modAut r) x) = (modAut (-r)) (star x)

  applying star to modAut r x will give modAut (-r) (star x)

@[simp]

theorem starAlgebra.modAut_zero {A : Type u_1} [hA : starAlgebra A] : modAut 0 = 1

@[simp]

theorem starAlgebra.modAut_apply_modAut {A : Type u_1} [ha : starAlgebra A] (t r : ℝ) (a : A) : (modAut t) ((modAut r) a) = (modAut (t + r)) a

@[simp]

theorem starAlgebra.modAut_symm {A : Type u_1} [ha : starAlgebra A] (r : ℝ) : (modAut r).symm = modAut (-r)

class InnerProductAlgebra (A : Type u_1) [starAlgebra A] extends Norm A, MetricSpace A, Inner ℂ A, IsBoundedSMul ℂ A : Type u_1

• norm : A → ℝ
• dist : A → A → ℝ
• dist_self (x : A) : dist x x = 0
• dist_comm (x y : A) : dist x y = dist y x
• dist_triangle (x y z : A) : dist x z ≤ dist x y + dist y z
• edist : A → A → ENNReal
• edist_dist (x y : A) : edist x y = ENNReal.ofReal (dist x y)
• toUniformSpace : UniformSpace A
• uniformity_dist : uniformity A = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : A × A | dist p.1 p.2 < ε}
• toBornology : Bornology A
• cobounded_sets : (Bornology.cobounded A).sets = {s : Set A | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
• eq_of_dist_eq_zero {x y : A} : dist x y = 0 → x = y
• inner : A → A → ℂ
• dist_smul_pair' (x : ℂ) (y₁ y₂ : A) : dist (x • y₁) (x • y₂) ≤ dist x 0 * dist y₁ y₂
• dist_pair_smul' (x₁ x₂ : ℂ) (y : A) : dist (x₁ • y) (x₂ • y) ≤ dist x₁ x₂ * dist y 0
• norm_sq_eq_inner (x : A) : ‖x‖ ^ 2 = RCLike.re (inner x x)
• dist_eq (x y : A) : dist x y = ‖x - y‖
• conj_symm (x y : A) : (starRingEnd ℂ) (inner y x) = inner x y
• add_left (x y z : A) : inner (x + y) z = inner x z + inner y z
• smul_left (x y : A) (r : ℂ) : inner (r • x) y = (starRingEnd ℂ) r * inner x y

noncomputable instance InnerProductAlgebra.toNormedAddCommGroupOfRing {A : Type u_1} [starAlgebra A] [InnerProductAlgebra A] : NormedAddCommGroupOfRing A

Equations

• InnerProductAlgebra.toNormedAddCommGroupOfRing = NormedAddCommGroupOfRing.mk ⋯

noncomputable instance InnerProductAlgebra.toInnerProductSpace {A : Type u_1} [starAlgebra A] [InnerProductAlgebra A] : InnerProductSpace ℂ A

Equations

• InnerProductAlgebra.toInnerProductSpace = InnerProductSpace.mk ⋯ ⋯ ⋯ ⋯

class QuantumSet (A : Type u_2) [ha : starAlgebra A] extends InnerProductAlgebra A : Type (max (u_1 + 1) u_2)

• norm : A → ℝ
• dist : A → A → ℝ
• dist_self (x : A) : dist x x = 0
• dist_comm (x y : A) : dist x y = dist y x
• dist_triangle (x y z : A) : dist x z ≤ dist x y + dist y z
• edist : A → A → ENNReal
• edist_dist (x y : A) : edist x y = ENNReal.ofReal (dist x y)
• toUniformSpace : UniformSpace A
• uniformity_dist : uniformity A = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : A × A | dist p.1 p.2 < ε}
• toBornology : Bornology A
• cobounded_sets : (Bornology.cobounded A).sets = {s : Set A | ∃ (C : ℝ), ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
• eq_of_dist_eq_zero {x y : A} : dist x y = 0 → x = y
• inner : A → A → ℂ
• dist_smul_pair' (x : ℂ) (y₁ y₂ : A) : dist (x • y₁) (x • y₂) ≤ dist x 0 * dist y₁ y₂
• dist_pair_smul' (x₁ x₂ : ℂ) (y : A) : dist (x₁ • y) (x₂ • y) ≤ dist x₁ x₂ * dist y 0
• norm_sq_eq_inner (x : A) : ‖x‖ ^ 2 = RCLike.re (inner x x)
• dist_eq (x y : A) : dist x y = ‖x - y‖
• conj_symm (x y : A) : (starRingEnd ℂ) (inner y x) = inner x y
• add_left (x y z : A) : inner (x + y) z = inner x z + inner y z
• smul_left (x y : A) (r : ℂ) : inner (r • x) y = (starRingEnd ℂ) r * inner x y
• modAut_isSymmetric (r : ℝ) (x y : A) : inner ((modAut r) x) y = inner x ((modAut r) y)

  the modular automorphism is symmetric with respect to the inner product, in other words, it is self-adjoint

• k : ℝ
• inner_star_left (x y z : A) : inner (x * y) z = inner y ((modAut (-k A)) (star x) * z)
• inner_conj_left (x y z : A) : inner (x * y) z = inner x (z * (modAut (-k A - 1)) (star y))
• n : Type u_1
• n_isFintype : Fintype (n A)
• n_isDecidableEq : DecidableEq (n A)
• onb : OrthonormalBasis (n A) ℂ A

  fix an orthonormal basis on A

instance n_isFinite {A : Type u_1} [ha : starAlgebra A] [QuantumSet A] : Finite (n A)

instance QuantumSet.toFinite {A : Type u_1} [ha : starAlgebra A] [hA : QuantumSet A] : Module.Finite ℂ A

theorem QuantumSet.modAut_isSelfAdjoint {A : Type u_1} [ha : starAlgebra A] [hA : QuantumSet A] (r : ℝ) : IsSelfAdjoint (modAut r).toLinearMap

theorem QuantumSet.modAut_apply_modAut {A : Type u_1} [ha : starAlgebra A] (t r : ℝ) (a : A) : (modAut t) ((modAut r) a) = (modAut (t + r)) a

Alias of starAlgebra.modAut_apply_modAut.

noncomputable instance Complex.starAlgebra : _root_.starAlgebra ℂ

Equations

• Complex.starAlgebra = starAlgebra.mk (fun (x : ℝ) => 1) Complex.starAlgebra.proof_2 Complex.starAlgebra.proof_3

noncomputable instance instInnerProductAlgebraComplex : InnerProductAlgebra ℂ

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance Complex.quantumSet : QuantumSet ℂ

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem RCLike.inner_tmul {𝕜 : Type u_2} [RCLike 𝕜] (x y z w : 𝕜) : inner (x ⊗ₜ[𝕜] y) (z ⊗ₜ[𝕜] w) = inner (x * y) (z * w)

theorem TensorProduct.singleton_tmul {R : Type u_2} {E : Type u_3} {F : Type u_4} [CommSemiring R] [AddCommGroup E] [Module R E] [AddCommGroup F] [Module R F] (x : TensorProduct R E F) (b₁ : Basis (Fin 1) R E) (b₂ : Basis (Fin 1) R F) : ∃ (a : E) (b : F), x = a ⊗ₜ[R] b

theorem RCLike.inner_tensor_apply {𝕜 : Type u_2} [RCLike 𝕜] (x y : TensorProduct 𝕜 𝕜 𝕜) : inner x y = inner ((LinearMap.mul' 𝕜 𝕜) x) ((LinearMap.mul' 𝕜 𝕜) y)

@[simp]

theorem QuantumSet.complex_modAut : modAut = 1

theorem QuantumSet.complex_comul : CoalgebraStruct.comul = ↑(TensorProduct.lid ℂ ℂ).symm

def QuantumSet.modAut_isCoalgHom {A : Type u_2} [hA : starAlgebra A] [QuantumSet A] (r : ℝ) : (modAut r).toLinearMap.IsCoalgHom

Equations

• ⋯ = ⋯

theorem lmul_adjoint {B : Type u_2} [hb : starAlgebra B] [hB : QuantumSet B] (a : B) : LinearMap.adjoint (lmul a) = lmul ((modAut (-k B)) (star a))

theorem QuantumSet.inner_eq_counit' {B : Type u_2} [hb : starAlgebra B] [hB : QuantumSet B] : (fun (x : B) => inner 1 x) = ⇑CoalgebraStruct.counit

theorem QuantumSet.inner_conj {A : Type u_2} [ha : starAlgebra A] [hA : QuantumSet A] (a b : A) : inner a b = inner (star b) ((modAut (-(2 * k A) - 1)) (star a))

theorem QuantumSet.inner_conj' {A : Type u_2} [ha : starAlgebra A] [hA : QuantumSet A] (a b : A) : inner a b = inner ((modAut (-(2 * k A) - 1)) (star b)) (star a)

theorem QuantumSet.inner_modAut_right_conj {A : Type u_2} [ha : starAlgebra A] [hA : QuantumSet A] (a b : A) : inner a ((modAut (-k A)) (star b)) = inner b ((modAut (-k A - 1)) (star a))

theorem QuantumSet.inner_conj'' {A : Type u_2} [ha : starAlgebra A] [hA : QuantumSet A] (a b : A) : inner a b = inner ((modAut ((-(2 * k A) - 1) / 2)) (star b)) ((modAut ((-(2 * k A) - 1) / 2)) (star a))

theorem QuantumSet.inner_eq_counit {B : Type u_2} [hb : starAlgebra B] [hB : QuantumSet B] (x y : B) : inner x y = CoalgebraStruct.counit (star x * (modAut (k B)) y)

theorem counit_mul_modAut_symm' {A : Type u_2} [ha : starAlgebra A] [hA : QuantumSet A] (a b : A) (r : ℝ) : CoalgebraStruct.counit (a * (modAut r) b) = CoalgebraStruct.counit ((modAut (r + 1)) b * a)

theorem rmul_adjoint {B : Type u_2} [hb : starAlgebra B] [hB : QuantumSet B] (a : B) : LinearMap.adjoint (rmul a) = rmul ((modAut (-k B - 1)) (star a))

theorem counit_comp_mul_comp_rTensor_modAut {A : Type u_2} [ha : starAlgebra A] [hA : QuantumSet A] : CoalgebraStruct.counit ∘ₗ LinearMap.mul' ℂ A ∘ₗ LinearMap.rTensor A (modAut 1).toLinearMap = CoalgebraStruct.counit ∘ₗ LinearMap.mul' ℂ A ∘ₗ ↑(TensorProduct.comm ℂ A A)

theorem counit_comp_mul_comp_lTensor_modAut {A : Type u_2} [ha : starAlgebra A] [hA : QuantumSet A] : CoalgebraStruct.counit ∘ₗ LinearMap.mul' ℂ A ∘ₗ LinearMap.lTensor A (modAut (-1)).toLinearMap = CoalgebraStruct.counit ∘ₗ LinearMap.mul' ℂ A ∘ₗ ↑(TensorProduct.comm ℂ A A)

noncomputable def QuantumSet.Psi_toFun {A : Type u_2} {B : Type u_3} [hb : starAlgebra B] [ha : starAlgebra A] [hA : QuantumSet A] [hB : QuantumSet B] (t r : ℝ) : (A →ₗ[ℂ] B) →ₗ[ℂ] TensorProduct ℂ B Aᵐᵒᵖ

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumSet.Psi_toFun_apply {A : Type u_2} {B : Type u_3} [hb : starAlgebra B] [ha : starAlgebra A] [hA : QuantumSet A] [hB : QuantumSet B] (t r : ℝ) (b : A) (a : B) : (Psi_toFun t r) ↑(((rankOne ℂ) a) b) = (modAut t) a ⊗ₜ[ℂ] MulOpposite.op (star ((modAut r) b))

noncomputable def QuantumSet.Psi_invFun {A : Type u_2} {B : Type u_3} [hb : starAlgebra B] [ha : starAlgebra A] [hA : QuantumSet A] [hB : QuantumSet B] (t r : ℝ) : TensorProduct ℂ A Bᵐᵒᵖ →ₗ[ℂ] B →ₗ[ℂ] A

Equations

• One or more equations did not get rendered due to their size.

theorem QuantumSet.Psi_invFun_apply {A : Type u_3} {B : Type u_2} [hb : starAlgebra B] [ha : starAlgebra A] [hA : QuantumSet A] [hB : QuantumSet B] (t r : ℝ) (x : A) (y : Bᵐᵒᵖ) : (Psi_invFun t r) (x ⊗ₜ[ℂ] y) = ↑(((rankOne ℂ) ((modAut (-t)) x)) ((modAut (-r)) (star (MulOpposite.unop y))))

theorem QuantumSet.Psi_left_inv {A : Type u_2} {B : Type u_3} [hb : starAlgebra B] [ha : starAlgebra A] [hA : QuantumSet A] [hB : QuantumSet B] (t r : ℝ) (x : A) (y : B) : (Psi_invFun t r) ((Psi_toFun t r) ↑(((rankOne ℂ) x) y)) = ↑(((rankOne ℂ) x) y)

theorem QuantumSet.Psi_right_inv {A : Type u_3} {B : Type u_2} [hb : starAlgebra B] [ha : starAlgebra A] [hA : QuantumSet A] [hB : QuantumSet B] (t r : ℝ) (x : A) (y : Bᵐᵒᵖ) : (Psi_toFun t r) ((Psi_invFun t r) (x ⊗ₜ[ℂ] y)) = x ⊗ₜ[ℂ] y

noncomputable def QuantumSet.Psi {A : Type u_2} {B : Type u_3} [hb : starAlgebra B] [ha : starAlgebra A] [hA : QuantumSet A] [hB : QuantumSet B] (t r : ℝ) : (A →ₗ[ℂ] B) ≃ₗ[ℂ] TensorProduct ℂ B Aᵐᵒᵖ

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem QuantumSet.Psi_symm_apply {A : Type u_2} {B : Type u_3} [hb : starAlgebra B] [ha : starAlgebra A] [hA : QuantumSet A] [hB : QuantumSet B] (t r : ℝ) (x : TensorProduct ℂ B Aᵐᵒᵖ) : (Psi t r).symm x = (Psi_invFun t r) x

@[simp]

theorem QuantumSet.Psi_apply {A : Type u_2} {B : Type u_3} [hb : starAlgebra B] [ha : starAlgebra A] [hA : QuantumSet A] [hB : QuantumSet B] (t r : ℝ) (x : A →ₗ[ℂ] B) : (Psi t r) x = (Psi_toFun t r) x

theorem LinearMap.adjoint_real_eq {A : Type u_2} {B : Type u_3} [hb : starAlgebra B] [ha : starAlgebra A] [hA : QuantumSet A] [hB : QuantumSet B] (f : A →ₗ[ℂ] B) : (adjoint f).real = (modAut (2 * k A + 1)).toLinearMap ∘ₗ adjoint f.real ∘ₗ (modAut (-(2 * k B) - 1)).toLinearMap

theorem rankOne_real {A : Type u_2} {B : Type u_3} [hb : starAlgebra B] [ha : starAlgebra A] [hA : QuantumSet A] [hB : QuantumSet B] (a : A) (b : B) : (↑(((rankOne ℂ) a) b)).real = ↑(((rankOne ℂ) (star a)) ((modAut (-(2 * k B) - 1)) (star b)))

theorem QuantumSet.rTensor_mul_comp_lTensor_comul_eq_comul_comp_mul {A : Type u_2} [ha : starAlgebra A] [hA : QuantumSet A] : LinearMap.rTensor A (LinearMap.mul' ℂ A) ∘ₗ ↑(TensorProduct.assoc ℂ A A A).symm ∘ₗ LinearMap.lTensor A CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ LinearMap.mul' ℂ A

theorem QuantumSet.lTensor_mul_comp_rTensor_comul_eq_comul_comp_mul {A : Type u_2} [ha : starAlgebra A] [hA : QuantumSet A] : LinearMap.lTensor A (LinearMap.mul' ℂ A) ∘ₗ ↑(TensorProduct.assoc ℂ A A A) ∘ₗ LinearMap.rTensor A CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ LinearMap.mul' ℂ A

noncomputable def QuantumSet.isFrobeniusAlgebra {A : Type u_2} [ha : starAlgebra A] [hA : QuantumSet A] : FrobeniusAlgebra ℂ A

Equations

• QuantumSet.isFrobeniusAlgebra = FrobeniusAlgebra.mk ⋯

theorem QuantumSet.rTensor_counit_mul_comp_comm_comp_rTensor_comul_unit_eq_modAut_one {A : Type u_2} [ha : starAlgebra A] [hA : QuantumSet A] : ↑(TensorProduct.lid ℂ A) ∘ₗ LinearMap.rTensor A (CoalgebraStruct.counit ∘ₗ LinearMap.mul' ℂ A) ∘ₗ ↑(TensorProduct.assoc ℂ A A A).symm ∘ₗ LinearMap.lTensor A ↑(TensorProduct.comm ℂ A A) ∘ₗ ↑(TensorProduct.assoc ℂ A A A) ∘ₗ LinearMap.rTensor A (CoalgebraStruct.comul ∘ₗ Algebra.linearMap ℂ A) ∘ₗ ↑(TensorProduct.lid ℂ A).symm = (modAut 1).toLinearMap

theorem QuantumSet.lTensor_counit_mul_comp_comm_comp_lTensor_comul_unit_eq_modAut_neg_one {A : Type u_2} [ha : starAlgebra A] [hA : QuantumSet A] : ↑(TensorProduct.rid ℂ A) ∘ₗ LinearMap.lTensor A (CoalgebraStruct.counit ∘ₗ LinearMap.mul' ℂ A) ∘ₗ ↑(TensorProduct.assoc ℂ A A A) ∘ₗ LinearMap.rTensor A ↑(TensorProduct.comm ℂ A A) ∘ₗ ↑(TensorProduct.assoc ℂ A A A).symm ∘ₗ LinearMap.lTensor A (CoalgebraStruct.comul ∘ₗ Algebra.linearMap ℂ A) ∘ₗ ↑(TensorProduct.rid ℂ A).symm = (modAut (-1)).toLinearMap

theorem QuantumSet.counit_tensor_star_left_eq_bra {A : Type u_2} [ha : starAlgebra A] [hA : QuantumSet A] (x : A) : (⇑CoalgebraStruct.counit ∘ ⇑(LinearMap.mul' ℂ A) ∘ fun (x_1 : A) => (modAut (-k A)) (star x) ⊗ₜ[ℂ] x_1) = ⇑((bra ℂ) x)

theorem QuantumSet.mul_comp_tensor_left_unit_eq_ket {A : Type u_2} [ha : starAlgebra A] [hA : QuantumSet A] (x : A) : ⇑(LinearMap.mul' ℂ A) ∘ (fun (x_1 : A) => x ⊗ₜ[ℂ] x_1) ∘ ⇑(Algebra.linearMap ℂ A) = ⇑((ket ℂ) x)

theorem QuantumSet.rTensor_bra_comul_unit_eq_ket_star {A : Type u_2} [ha : starAlgebra A] [hA : QuantumSet A] (x : A) : ↑(TensorProduct.lid ℂ A) ∘ₗ LinearMap.rTensor A ↑((bra ℂ) x) ∘ₗ CoalgebraStruct.comul ∘ₗ Algebra.linearMap ℂ A = ↑((ket ℂ) ((modAut (-k A)) (star x)))

theorem QuantumSet.rTensor_bra_comul_unit_eq_ket_star' {A : Type u_2} [ha : starAlgebra A] [hA : QuantumSet A] (x : A) : ↑(TensorProduct.lid ℂ A) ∘ₗ LinearMap.rTensor A ↑((bra ℂ) ((modAut (-k A)) x)) ∘ₗ CoalgebraStruct.comul ∘ₗ Algebra.linearMap ℂ A = ↑((ket ℂ) (star x))

theorem QuantumSet.counit_mul_rTensor_ket_eq_bra_star {A : Type u_2} [ha : starAlgebra A] [hA : QuantumSet A] (x : A) : CoalgebraStruct.counit ∘ₗ LinearMap.mul' ℂ A ∘ₗ LinearMap.rTensor A ↑((ket ℂ) x) ∘ₗ ↑(TensorProduct.lid ℂ A).symm = ↑((bra ℂ) ((modAut (-k A)) (star x)))

theorem ket_real {𝕜 : Type u_2} {A : Type u_3} [RCLike 𝕜] [NormedAddCommGroup A] [InnerProductSpace 𝕜 A] [StarAddMonoid A] [StarModule 𝕜 A] (x : A) : (↑((ket 𝕜) x)).real = ↑((ket 𝕜) (star x))

theorem bra_real {A : Type u_2} [ha : starAlgebra A] [hA : QuantumSet A] (x : A) : (↑((bra ℂ) x)).real = ↑((bra ℂ) ((modAut (-(2 * k A) - 1)) (star x)))

theorem ket_toMatrix {𝕜 : Type u_2} {A : Type u_3} [RCLike 𝕜] [NormedAddCommGroup A] [InnerProductSpace 𝕜 A] {ι : Type u_4} [Fintype ι] (b : Basis ι 𝕜 A) (x : A) : (LinearMap.toMatrix (Basis.singleton Unit 𝕜) b) ↑((ket 𝕜) x) = Matrix.col Unit ⇑(b.repr x)

theorem bra_toMatrix {𝕜 : Type u_2} {A : Type u_3} [RCLike 𝕜] [NormedAddCommGroup A] [InnerProductSpace 𝕜 A] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (b : OrthonormalBasis ι 𝕜 A) (x : A) : (LinearMap.toMatrix b.toBasis (Basis.singleton Unit 𝕜)) ↑((bra 𝕜) x) = (Matrix.col Unit (b.repr x)).conjTranspose

theorem lmul_toMatrix_apply {n : Type u_2} [Fintype n] [DecidableEq n] (x : n → ℂ) (i j : n) : LinearMap.toMatrix' (LinearMap.mulLeft ℂ x) i j = if i = j then x i else 0

theorem rankOne_trace {𝕜 : Type u_2} {A : Type u_3} [RCLike 𝕜] [NormedAddCommGroup A] [InnerProductSpace 𝕜 A] [Module.Finite 𝕜 A] (x y : A) : (LinearMap.trace 𝕜 A) ↑(((rankOne 𝕜) x) y) = inner y x

theorem LinearMap.apply_eq_id {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {f : M →ₗ[R] M} : (∀ (x : M), f x = x) ↔ f = 1

theorem QuantumSet.starAlgEquiv_is_isometry_tfae {A : Type u_2} {B : Type u_3} [hb : starAlgebra B] [ha : starAlgebra A] [hA : QuantumSet A] [hB : QuantumSet B] (f : A ≃⋆ₐ[ℂ] B) : [LinearMap.adjoint f.toLinearMap = f.symm.toLinearMap, ∀ (x y : A), inner (f x) (f y) = inner x y, ∀ (x : A), ‖f x‖ = ‖x‖, Isometry ⇑f].TFAE

theorem QuantumSet.starAlgEquiv_isometry_iff_adjoint_eq_symm {A : Type u_2} {B : Type u_3} [hb : starAlgebra B] [ha : starAlgebra A] [hA : QuantumSet A] [hB : QuantumSet B] {f : A ≃⋆ₐ[ℂ] B} : Isometry ⇑f ↔ LinearMap.adjoint f.toLinearMap = f.symm.toLinearMap

theorem QuantumSet.starAlgEquiv_isometry_iff_coalgHom {A : Type u_3} {B : Type u_5} [hb : starAlgebra B] [ha : starAlgebra A] [hA : QuantumSet A] [hB : QuantumSet B] (gns₁ : k A = 0) (gns₂ : k B = 0) {f : A ≃⋆ₐ[ℂ] B} : Isometry ⇑f ↔ CoalgebraStruct.counit ∘ₗ f.toLinearMap = CoalgebraStruct.counit

theorem StarAlgEquiv.isReal {R : Type u_2} {A : Type u_3} {B : Type u_4} [Semiring R] [AddCommMonoid A] [AddCommMonoid B] [Mul A] [Mul B] [Module R A] [Module R B] [Star A] [Star B] (f : A ≃⋆ₐ[R] B) : LinearMap.IsReal f.toLinearMap

theorem QuantumSet.modAut_real {A : Type u_2} [ha : starAlgebra A] (r : ℝ) : (modAut r).toLinearMap.real = (modAut (-r)).toLinearMap

theorem AlgEquiv.linearMap_comp_eq_iff {R : Type u_2} {E₁ : Type u_3} {E₂ : Type u_4} {E₃ : Type u_5} [CommSemiring R] [Semiring E₁] [Semiring E₂] [AddCommMonoid E₃] [Algebra R E₁] [Algebra R E₂] [Module R E₃] (f : E₁ ≃ₐ[R] E₂) (x : E₂ →ₗ[R] E₃) (y : E₁ →ₗ[R] E₃) : x ∘ₗ f.toLinearMap = y ↔ x = y ∘ₗ f.symm.toLinearMap

theorem AlgEquiv.comp_linearMap_eq_iff {R : Type u_2} {E₁ : Type u_3} {E₂ : Type u_4} {E₃ : Type u_5} [CommSemiring R] [Semiring E₁] [Semiring E₂] [AddCommMonoid E₃] [Algebra R E₁] [Algebra R E₂] [Module R E₃] (f : E₁ ≃ₐ[R] E₂) (x : E₃ →ₗ[R] E₁) (y : E₃ →ₗ[R] E₂) : f.toLinearMap ∘ₗ x = y ↔ x = f.symm.toLinearMap ∘ₗ y

theorem QuantumSet.modAut_adjoint {A : Type u_2} [ha : starAlgebra A] [hA : QuantumSet A] (r : ℝ) : LinearMap.adjoint (modAut r).toLinearMap = (modAut r).toLinearMap

theorem QuantumSet.starAlgEquiv_commutes_with_modAut_of_isometry {A : Type u_2} {B : Type u_3} [hb : starAlgebra B] [ha : starAlgebra A] [hA : QuantumSet A] [hB : QuantumSet B] {f : A ≃⋆ₐ[ℂ] B} (hf : Isometry ⇑f) : (modAut (2 * k A + 1)).trans f.toAlgEquiv = f.toAlgEquiv.trans (modAut (2 * k B + 1))

theorem QuantumSet.starAlgEquiv_commutes_with_modAut_of_isometry' {A : Type u_2} {B : Type u_3} [hb : starAlgebra B] [ha : starAlgebra A] [hA : QuantumSet A] [hB : QuantumSet B] {f : A ≃⋆ₐ[ℂ] B} (hf : Isometry ⇑f) : f.toLinearMap ∘ₗ (modAut (2 * k A + 1)).toLinearMap = (modAut (2 * k B + 1)).toLinearMap ∘ₗ f.toLinearMap

theorem tenSwap_lTensor_comul_one_eq_Psi {A : Type u_2} {B : Type u_3} [hb : starAlgebra B] [ha : starAlgebra A] [hA : QuantumSet A] [hB : QuantumSet B] (f : A →ₗ[ℂ] B) : (tenSwap ℂ) ((LinearMap.lTensor A (↑(op ℂ) ∘ₗ f)) (CoalgebraStruct.comul 1)) = (QuantumSet.Psi 0 (k A + 1)) f

theorem map_op_comul_one_eq_Psi {A : Type u_2} {B : Type u_3} [hb : starAlgebra B] [ha : starAlgebra A] [hA : QuantumSet A] [hB : QuantumSet B] (f : A →ₗ[ℂ] B) : (TensorProduct.map f ↑(op ℂ)) (CoalgebraStruct.comul 1) = (QuantumSet.Psi 0 (k A)) f

theorem tenSwap_apply_lTensor {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [CommSemiring R] [AddCommMonoid A] [AddCommMonoid C] [Module R A] [AddCommMonoid B] [Module R B] [Module R C] (f : B →ₗ[R] C) (x : TensorProduct R A Bᵐᵒᵖ) : (tenSwap R) ((LinearMap.lTensor A f.op) x) = (LinearMap.rTensor Aᵐᵒᵖ f) ((tenSwap R) x)

theorem Psi_inv_comp_swap_lTensor_op_comp_comul_eq_rmul {A : Type u_2} [ha : starAlgebra A] [hA : QuantumSet A] : ↑(QuantumSet.Psi 0 (k A + 1)).symm ∘ₗ ↑(tenSwap ℂ) ∘ₗ LinearMap.lTensor A ↑(op ℂ) ∘ₗ CoalgebraStruct.comul = rmul

theorem QuantumSet.Psi_apply_one_one {A : Type u_2} {B : Type u_3} [hb : starAlgebra B] [ha : starAlgebra A] [hA : QuantumSet A] [hB : QuantumSet B] (t r : ℝ) : (Psi t r) ↑(((rankOne ℂ) 1) 1) = 1

theorem QuantumSet.Psi_symm_apply_one {A : Type u_2} {B : Type u_3} [hb : starAlgebra B] [ha : starAlgebra A] [hA : QuantumSet A] [hB : QuantumSet B] (t r : ℝ) : (Psi t r).symm 1 = ↑(((rankOne ℂ) 1) 1)

@[reducible, inline]

noncomputable abbrev Upsilon {A : Type u_2} {B : Type u_3} [hb : starAlgebra B] [ha : starAlgebra A] [hA : QuantumSet A] [hB : QuantumSet B] : (A →ₗ[ℂ] B) ≃ₗ[ℂ] TensorProduct ℂ A B

Equations

• Upsilon = (QuantumSet.Psi 0 (k A + 1)).trans ((tenSwap ℂ).trans (LinearEquiv.lTensor A (unop ℂ)))

@[simp]

theorem Upsilon_apply {A : Type u_2} {B : Type u_3} [hb : starAlgebra B] [ha : starAlgebra A] [hA : QuantumSet A] [hB : QuantumSet B] (a✝ : A →ₗ[ℂ] B) : Upsilon a✝ = (LinearEquiv.lTensor A (unop ℂ)) ((TensorProduct.map ↑(unop ℂ) ↑(op ℂ)) ((TensorProduct.comm ℂ B Aᵐᵒᵖ) ((QuantumSet.Psi_toFun 0 (k A + 1)) a✝)))

@[simp]

theorem Upsilon_symm_apply {A : Type u_2} {B : Type u_3} [hb : starAlgebra B] [ha : starAlgebra A] [hA : QuantumSet A] [hB : QuantumSet B] (a✝ : TensorProduct ℂ A B) : Upsilon.symm a✝ = (QuantumSet.Psi_invFun 0 (k A + 1)) ((TensorProduct.comm ℂ B Aᵐᵒᵖ).symm ((TensorProduct.map ↑(op ℂ) ↑(op ℂ).symm) ((LinearEquiv.lTensor A (unop ℂ)).symm a✝)))

theorem Upsilon_apply_one_one {A : Type u_2} {B : Type u_3} [hb : starAlgebra B] [ha : starAlgebra A] [hA : QuantumSet A] [hB : QuantumSet B] : Upsilon ↑(((rankOne ℂ) 1) 1) = 1

theorem Upsilon_symm_apply_one {A : Type u_2} {B : Type u_3} [hb : starAlgebra B] [ha : starAlgebra A] [hA : QuantumSet A] [hB : QuantumSet B] : Upsilon.symm 1 = ↑(((rankOne ℂ) 1) 1)

theorem Upsilon_rankOne {A : Type u_2} {B : Type u_3} [hb : starAlgebra B] [ha : starAlgebra A] [hA : QuantumSet A] [hB : QuantumSet B] (a : A) (b : B) : Upsilon ↑(((rankOne ℂ) a) b) = (modAut (-k B - 1)) (star b) ⊗ₜ[ℂ] a

theorem Upsilon_symm_tmul {A : Type u_2} {B : Type u_3} [hb : starAlgebra B] [ha : starAlgebra A] [hA : QuantumSet A] [hB : QuantumSet B] (a : A) (b : B) : Upsilon.symm (a ⊗ₜ[ℂ] b) = ↑(((rankOne ℂ) b) ((modAut (-k A - 1)) (star a)))

theorem rmulMapLmul_apply_Upsilon_eq {A : Type u_2} {B : Type u_3} [hb : starAlgebra B] [ha : starAlgebra A] [hA : QuantumSet A] [hB : QuantumSet B] (x : A →ₗ[ℂ] B) : rmulMapLmul (Upsilon x) = LinearMap.lTensor A (LinearMap.mul' ℂ B) ∘ₗ ↑(TensorProduct.assoc ℂ A B B) ∘ₗ LinearMap.rTensor B (LinearMap.lTensor A x) ∘ₗ LinearMap.rTensor B CoalgebraStruct.comul