Quantum Sets

This file ports the structural core of upstream Monlib.LinearAlgebra.QuantumSet.Basic: star algebras with modular automorphisms, inner-product algebras, quantum sets, the base quantum set on ℂ, modular inner-product identities, the coalgebra comultiplication on ℂ, and the Psi/Upsilon equivalences used by downstream quantum-graph files.

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

A star algebra over ℂ equipped with a real-parameter modular automorphism group.

• 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
• 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
• npow : ℕ → A → A
• npow_zero (x : A) : Monoid.npow 0 x = 1
• npow_succ (n : ℕ) (x : A) : Monoid.npow (n + 1) x = Monoid.npow n x * x
• zero_mul (a : A) : 0 * a = 0
• mul_zero (a : A) : a * 0 = 0
• 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
• natCast : ℕ → A
• natCast_zero : ↑0 = 0
• natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1
• 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) : (algebraMap ℂ A) r * x = x * (algebraMap ℂ A) r
• smul_def' (r : ℂ) (x : A) : r • x = (algebraMap ℂ A) 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 σ_r as an algebra equivalence.

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

  The modular automorphisms compose additively in the real parameter.

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

  Star changes the sign of the modular parameter.

@[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 : Type u_1

A star algebra whose ring additive group carries a compatible complex inner product.

• 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 → ℂ
• norm_smul_le (c : ℂ) (x : A) : ‖c • x‖ ≤ ‖c‖ * ‖x‖
• 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

@[implicit_reducible]

noncomputable instance InnerProductAlgebra.toNormedAddCommGroup {A : Type u_1} [starAlgebra A] [InnerProductAlgebra A] : NormedAddCommGroup A

Equations

• InnerProductAlgebra.toNormedAddCommGroup = { toNorm := inst✝.toNorm, toAddCommGroup := inst✝¹.toAddCommGroup, toMetricSpace := inst✝.toMetricSpace, dist_eq := ⋯ }

@[implicit_reducible]

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

Equations

• InnerProductAlgebra.toNormedAddCommGroupOfRing = { toRing := inst✝¹.toRing, toNorm := inst✝.toNorm, toMetricSpace := inst✝.toMetricSpace, dist_eq := ⋯ }

@[implicit_reducible]

noncomputable instance InnerProductAlgebra.toNormedSpace {A : Type u_1} [starAlgebra A] [InnerProductAlgebra A] : NormedSpace ℂ A

Equations

• InnerProductAlgebra.toNormedSpace = { toModule := inferInstance, norm_smul_le := ⋯ }

instance InnerProductAlgebra.toNormSMulClass {A : Type u_1} [starAlgebra A] [InnerProductAlgebra A] : NormSMulClass ℂ A

@[implicit_reducible]

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

Equations

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

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

A finite-dimensional quantum set with a modular automorphism and fixed orthonormal basis.

• 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 → ℂ
• norm_smul_le (c : ℂ) (x : A) : ‖c • x‖ ≤ ‖c‖ * ‖x‖
• 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 for the quantum-set inner product.

• k : ℝ

  The modular exponent used in the KMS identities.

• 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

  The index type of the fixed orthonormal basis.

• nIsFintype : Fintype (n A)

  The fixed basis index type is finite.

• nIsDecidableEq : DecidableEq (n A)

  The fixed basis index type has decidable equality.

• onb : OrthonormalBasis (n A) ℂ A

  A fixed orthonormal basis of the quantum set.

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

The fixed basis index type of a quantum set is finite.

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

A quantum set is finite-dimensional over ℂ via its fixed orthonormal basis.

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.

theorem QuantumSet.inner_conj {A : Type u_1} [ha : starAlgebra A] [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_1} [ha : starAlgebra A] [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_1} [ha : starAlgebra A] [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_1} [ha : starAlgebra A] [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))

@[implicit_reducible]

noncomputable instance Complex.starAlgebra : _root_.starAlgebra ℂ

Equations

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

@[implicit_reducible]

noncomputable instance instInnerProductAlgebraComplex : InnerProductAlgebra ℂ

Equations

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

@[implicit_reducible]

noncomputable instance Complex.quantumSet : QuantumSet ℂ

Equations

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

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₁ : Module.Basis (Fin 1) R E) (b₂ : Module.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

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

Modular automorphisms preserve the coalgebra structure of a quantum set.

@[reducible]

noncomputable instance QuantumSet.isFrobeniusAlgebra {A : Type u_1} [ha : starAlgebra A] [QuantumSet A] : FrobeniusAlgebra ℂ A

A quantum set carries the Frobenius algebra structure induced by its coalgebra.

Equations

• QuantumSet.isFrobeniusAlgebra = FiniteDimensionalCoAlgebraIsFrobeniusAlgebraOf ⋯

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] [QuantumSet B] : (fun (x : B) => inner ℂ 1 x) = ⇑CoalgebraStruct.counit

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

theorem counit_mul_modAut_symm' {A : Type u_1} [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_1} [ha : starAlgebra A] [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_1} [ha : starAlgebra A] [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.PsiToFun {A : Type u_1} [ha : starAlgebra A] {B : Type u_2} [hb : starAlgebra B] [hA : QuantumSet A] [hB : QuantumSet B] (t r : ℝ) : (A →ₗ[ℂ] B) →ₗ[ℂ] TensorProduct ℂ B Aᵐᵒᵖ

The matrix-coordinate map used to identify linear maps with a tensor product.

Equations

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

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

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

The inverse coordinate map to QuantumSet.PsiToFun.

Equations

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

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

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

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

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

The linear equivalence between maps and tensors used in the quantum-set formalism.

Equations

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

@[simp]

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

@[simp]

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

theorem LinearMap.adjoint_real_eq {A : Type u_1} [ha : starAlgebra A] {B : Type u_2} [hb : starAlgebra B] [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 QuantumSet.modAut_adjoint {A : Type u_1} [ha : starAlgebra A] [QuantumSet A] (r : ℝ) : LinearMap.adjoint (modAut r).toLinearMap = (modAut r).toLinearMap

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

theorem rankOne_real {A : Type u_1} [ha : starAlgebra A] {B : Type u_2} [hb : starAlgebra B] [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_1} [ha : starAlgebra A] [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_1} [ha : starAlgebra A] [QuantumSet A] : LinearMap.lTensor A (LinearMap.mul' ℂ A) ∘ₗ ↑(TensorProduct.assoc ℂ A A A) ∘ₗ LinearMap.rTensor A CoalgebraStruct.comul = CoalgebraStruct.comul ∘ₗ LinearMap.mul' ℂ A

theorem QuantumSet.rTensor_counit_mul_comp_comm_comp_rTensor_comul_unit_eq_modAut_one {A : Type u_1} [ha : starAlgebra A] [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_1} [ha : starAlgebra A] [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_1} [ha : starAlgebra A] [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_1} [ha : starAlgebra A] [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_1} [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_1} [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_1} [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_3} {A : Type u_4} [RCLike 𝕜] [NormedAddCommGroup A] [InnerProductSpace 𝕜 A] [StarAddMonoid A] [StarModule 𝕜 A] (x : A) : (↑((ket 𝕜) x)).real = ↑((ket 𝕜) (star x))

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

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

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

theorem lmul_toMatrix_apply {n : Type u_3} [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_3} {A : Type u_4} [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_3} {M : Type u_4} [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_1} [ha : starAlgebra A] {B : Type u_2} [hb : starAlgebra B] [QuantumSet A] [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_1} [ha : starAlgebra A] {B : Type u_2} [hb : starAlgebra B] [QuantumSet A] [QuantumSet B] {f : A ≃⋆ₐ[ℂ] B} : Isometry ⇑f ↔ LinearMap.adjoint f.toLinearMap = f.symm.toLinearMap

theorem QuantumSet.starAlgEquiv_isometry_iff_coalgHom {A : Type u_1} [ha : starAlgebra A] {B : Type u_2} [hb : starAlgebra B] [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_3} {A : Type u_4} {B : Type u_5} [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 AlgEquiv.linearMap_comp_eq_iff {R : Type u_3} {E₁ : Type u_4} {E₂ : Type u_5} {E₃ : Type u_6} [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_3} {E₁ : Type u_4} {E₂ : Type u_5} {E₃ : Type u_6} [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.starAlgEquiv_commutes_with_modAut_of_isometry {A : Type u_1} [ha : starAlgebra A] {B : Type u_2} [hb : starAlgebra B] [QuantumSet A] [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_1} [ha : starAlgebra A] {B : Type u_2} [hb : starAlgebra B] [QuantumSet A] [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 QuantumSet.Psi_apply_one_one {A : Type u_1} [ha : starAlgebra A] {B : Type u_2} [hb : starAlgebra B] [QuantumSet A] [QuantumSet B] (t r : ℝ) : (Psi t r) ↑(((rankOne ℂ) 1) 1) = 1

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

@[reducible, inline]

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

The Psi equivalence with tensor factors swapped back from the opposite space.

Equations

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

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

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

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

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

theorem tenSwap_lTensor_comul_one_eq_Psi {A : Type u_1} [ha : starAlgebra A] {B : Type u_2} [hb : starAlgebra B] [QuantumSet A] [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_1} [ha : starAlgebra A] {B : Type u_2} [hb : starAlgebra B] [QuantumSet A] [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_3} {A : Type u_4} {B : Type u_5} {C : Type u_6} [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_1} [ha : starAlgebra A] [QuantumSet A] : ↑(QuantumSet.Psi 0 (k A + 1)).symm ∘ₗ ↑(tenSwap ℂ) ∘ₗ LinearMap.lTensor A ↑(op ℂ) ∘ₗ CoalgebraStruct.comul = rmul

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

theorem Upsilon_symm_tmul {A : Type u_1} [ha : starAlgebra A] {B : Type u_2} [hb : starAlgebra B] [QuantumSet A] [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_1} [ha : starAlgebra A] {B : Type u_2} [hb : starAlgebra B] [QuantumSet A] [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