@[reducible, inline]

noncomputable abbrev PhiMap {A : Type u_1} {B : Type u_2} [starAlgebra B] [starAlgebra A] [QuantumSet A] [QuantumSet B] : (A →ₗ[ℂ] B) ≃ₗ[ℂ] ↥(LinearMap.IsBimoduleMaps ℂ A B)

Equations

• PhiMap = Upsilon.trans TensorProduct.toIsBimoduleMap

theorem PhiMap_apply {A : Type u_1} {B : Type u_2} [starAlgebra B] [starAlgebra A] [QuantumSet A] [QuantumSet B] (f : A →ₗ[ℂ] B) : PhiMap f = TensorProduct.toIsBimoduleMap (Upsilon f)

theorem oneInner_map_one_eq_oneInner_Psi_map {A : Type u_1} {B : Type u_2} [starAlgebra B] [starAlgebra A] [hA : QuantumSet A] [hB : QuantumSet B] (f : A →ₗ[ℂ] B) (r t : ℝ) : inner ℂ 1 (f 1) = inner ℂ 1 ((QuantumSet.Psi r t) f)

theorem oneInner_map_one_eq_oneInner_PhiMap_map_one {A : Type u_1} {B : Type u_2} [starAlgebra B] [starAlgebra A] [hA : QuantumSet A] [hB : QuantumSet B] (f : A →ₗ[ℂ] B) : inner ℂ 1 (f 1) = inner ℂ 1 (↑(PhiMap f) 1)