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 , Algebra , StarRing , StarModule , Semiring , AddCommGroup , AddGroupWithOne , NonUnitalSemiring , NonAssocSemiring , MonoidWithZero , NonUnitalNonAssocSemiring , Monoid , MulZeroOneClass , SemigroupWithZero , AddCommMonoidWithOne , MulOneClass , IntCast , AddMonoidWithOne , AddGroup , AddCommMonoid , Distrib , Semigroup , MulZeroClass , NatCast , SubNegMonoid , AddMonoid , One , Neg , Sub , AddCommSemigroup , AddSemigroup , AddZeroClass , Mul , Zero , AddCommMagma , Add , SMul , RingHom , MonoidHom , OneHom , AddMonoidHom , NonUnitalRingHom , MonoidWithZeroHom , MulHom , ZeroHom , AddHom , StarMul , InvolutiveStar , Star : Type u_1

@[simp]

theorem starAlgebra.modAut_trans {A : Type u_1} [self : starAlgebra A] (r : ℝ) (s : ℝ) : (modAut r).trans (modAut s) = modAut (r + s)

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

@[simp]

theorem starAlgebra.modAut_star {A : Type u_1} [self : starAlgebra A] (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 , MetricSpace , Inner , BoundedSMul , PseudoMetricSpace , Dist : 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), PseudoMetricSpace.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

theorem InnerProductAlgebra.norm_sq_eq_inner {A : Type u_1} : ∀ {inst : starAlgebra A} [self : InnerProductAlgebra A] (x : A), ‖x‖ ^ 2 = RCLike.re (inner x x)

theorem InnerProductAlgebra.dist_eq {A : Type u_1} : ∀ {inst : starAlgebra A} [self : InnerProductAlgebra A] (x y : A), dist x y = ‖x - y‖

theorem InnerProductAlgebra.conj_symm {A : Type u_1} : ∀ {inst : starAlgebra A} [self : InnerProductAlgebra A] (x y : A), (starRingEnd ℂ) (inner y x) = inner x y

theorem InnerProductAlgebra.add_left {A : Type u_1} : ∀ {inst : starAlgebra A} [self : InnerProductAlgebra A] (x y z : A), inner (x + y) z = inner x z + inner y z

theorem InnerProductAlgebra.smul_left {A : Type u_1} : ∀ {inst : starAlgebra A} [self : InnerProductAlgebra A] (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 , Norm , MetricSpace , Inner , BoundedSMul , PseudoMetricSpace , Dist : 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), PseudoMetricSpace.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

@[simp]

theorem QuantumSet.modAut_isSymmetric {A : Type u_2} {ha : starAlgebra A} [self : QuantumSet A] (r : ℝ) (x : A) (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

@[simp]

theorem QuantumSet.inner_star_left {A : Type u_2} {ha : starAlgebra A} [self : QuantumSet A] (x : A) (y : A) (z : A) : inner (x * y) z = inner y ((modAut (-k A)) (star x) * z)

@[simp]

theorem QuantumSet.inner_conj_left {A : Type u_2} {ha : starAlgebra A} [self : QuantumSet A] (x : A) (y : A) (z : A) : inner (x * y) z = inner x (z * (modAut (-k A - 1)) (star y))

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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 : 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 : TensorProduct 𝕜 𝕜 𝕜) (y : TensorProduct 𝕜 𝕜 𝕜) : inner x y = inner ((LinearMap.mul' 𝕜 𝕜) x) ((LinearMap.mul' 𝕜 𝕜) y)

@[simp]

theorem QuantumSet.complex_modAut : modAut = 1

theorem QuantumSet.complex_comul : Coalgebra.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) = ⇑Coalgebra.counit

theorem QuantumSet.inner_conj {A : Type u_2} [ha : starAlgebra A] [hA : QuantumSet A] (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 : 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 : 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 : 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 : B) (y : B) : inner x y = Coalgebra.counit (star x * (modAut (k B)) y)

theorem counit_mul_modAut_symm' {A : Type u_2} [ha : starAlgebra A] [hA : QuantumSet A] (a : A) (b : A) (r : ℝ) : Coalgebra.counit (a * (modAut r) b) = Coalgebra.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] : Coalgebra.counit ∘ₗ LinearMap.mul' ℂ A ∘ₗ LinearMap.rTensor A (modAut 1).toLinearMap = Coalgebra.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] : Coalgebra.counit ∘ₗ LinearMap.mul' ℂ A ∘ₗ LinearMap.lTensor A (modAut (-1)).toLinearMap = Coalgebra.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) : (QuantumSet.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ᵐᵒᵖ) : (QuantumSet.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) : (QuantumSet.Psi_invFun t r) ((QuantumSet.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ᵐᵒᵖ) : (QuantumSet.Psi_toFun t r) ((QuantumSet.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_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) : (QuantumSet.Psi t r) x = (QuantumSet.Psi_toFun t r) x

@[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ᵐᵒᵖ) : (QuantumSet.Psi t r).symm x = (QuantumSet.Psi_invFun 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) : (LinearMap.adjoint f).real = (modAut (2 * k A + 1)).toLinearMap ∘ₗ LinearMap.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 Coalgebra.comul = Coalgebra.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 Coalgebra.comul = Coalgebra.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 (Coalgebra.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 (Coalgebra.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 (Coalgebra.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 (Coalgebra.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) : (⇑Coalgebra.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) ∘ₗ Coalgebra.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)) ∘ₗ Coalgebra.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) : Coalgebra.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 : n) (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 : A) (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 ↔ Coalgebra.counit ∘ₗ f.toLinearMap = Coalgebra.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)) (Coalgebra.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 ℂ)) (Coalgebra.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 ℂ) ∘ₗ Coalgebra.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 : ℝ) : (QuantumSet.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 : ℝ) : (QuantumSet.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 Coalgebra.comul