The Phi Map

This file packages the upstream Upsilon equivalence as a bimodule-map equivalence and records the one-vector inner-product identities used by downstream quantum graph files.

@[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)

The Upsilon equivalence viewed through the tensor-product bimodule map API.

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)

Applying PhiMap is applying Upsilon and then coercing to a bimodule map.

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)

Mapping the unit and then pairing with the unit agrees with applying Psi first.

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)

Mapping the unit and pairing with the unit agrees after applying PhiMap.