noncomputable def QuantumGraph.Grad {B : Type u_1} [starAlgebra B] [QuantumSet B] : (B →ₗ[ℂ] B) →+ B →ₗ[ℂ] TensorProduct ℂ B B

Equations

• QuantumGraph.Grad = { toFun := fun (f : B →ₗ[ℂ] B) => (LinearMap.rTensor B (LinearMap.adjoint f) - LinearMap.lTensor B f) ∘ₗ Coalgebra.comul, map_zero' := ⋯, map_add' := ⋯ }

theorem QuantumGraph.Grad_apply {B : Type u_1} [starAlgebra B] [QuantumSet B] (A : B →ₗ[ℂ] B) : QuantumGraph.Grad A = (LinearMap.rTensor B (LinearMap.adjoint A) - LinearMap.lTensor B A) ∘ₗ Coalgebra.comul

theorem QuantumGraph.Grad_eq {B : Type u_1} [starAlgebra B] [QuantumSet B] (gns : k B = 0) (A : B →ₗ[ℂ] B) : QuantumGraph.Grad A = ↑(PhiMap A.real) ∘ₗ LinearMap.rTensor B (Algebra.linearMap ℂ B) ∘ₗ ↑(TensorProduct.lid ℂ B).symm - ↑(PhiMap A) ∘ₗ LinearMap.lTensor B (Algebra.linearMap ℂ B) ∘ₗ ↑(TensorProduct.rid ℂ B).symm

theorem QuantumGraph.Grad_apply' {B : Type u_1} [starAlgebra B] [QuantumSet B] (gns : k B = 0) (A : B →ₗ[ℂ] B) (x : B) : (QuantumGraph.Grad A) x = ↑(PhiMap A.real) (1 ⊗ₜ[ℂ] x) - ↑(PhiMap A) (x ⊗ₜ[ℂ] 1)

theorem QuantumGraph.Real.range_grad_le_range_phiMap {B : Type u_1} [starAlgebra B] [QuantumSet B] (gns : k B = 0) {A : B →ₗ[ℂ] B} (hA : QuantumGraph.Real B A) : LinearMap.range (QuantumGraph.Grad A) ≤ LinearMap.range ↑(PhiMap A)

theorem Upsilon_symm_grad_apply_apply {B : Type u_1} [starAlgebra B] [QuantumSet B] (gns : k B = 0) (A : B →ₗ[ℂ] B) (x : B) : Upsilon.symm ((QuantumGraph.Grad A) x) = rmul x ∘ₗ A.real - A ∘ₗ rmul x

theorem QuantumGraph.grad_adjoint_comp_grad {B : Type u_1} [starAlgebra B] [QuantumSet B] (gns : k B = 0) (A : B →ₗ[ℂ] B) : LinearMap.adjoint (QuantumGraph.Grad A) ∘ₗ QuantumGraph.Grad A = QuantumGraph.outDegree (A •ₛ A.real) - A •ₛ A - LinearMap.adjoint (A •ₛ A) + QuantumGraph.inDegree (A.real •ₛ A)

theorem Bimodule.lsmul_sub {R : Type u_2} {H₁ : Type u_3} {H₂ : Type u_4} [CommSemiring R] [Ring H₁] [Ring H₂] [Algebra R H₁] [Algebra R H₂] (x : H₁) (a : TensorProduct R H₁ H₂) (b : TensorProduct R H₁ H₂) : Bimodule.lsmul x (a - b) = Bimodule.lsmul x a - Bimodule.lsmul x b

theorem Bimodule.sub_rsmul {R : Type u_2} {H₁ : Type u_3} {H₂ : Type u_4} [CommSemiring R] [Ring H₁] [Ring H₂] [Algebra R H₁] [Algebra R H₂] (x : H₂) (a : TensorProduct R H₁ H₂) (b : TensorProduct R H₁ H₂) : Bimodule.rsmul (a - b) x = Bimodule.rsmul a x - Bimodule.rsmul b x

theorem QuantumGraph.apply_mul_of_isReal {B : Type u_1} [starAlgebra B] [QuantumSet B] (gns : k B = 0) {A : B →ₗ[ℂ] B} (hA : LinearMap.IsReal A) (x : B) (y : B) : (QuantumGraph.Grad A) (x * y) = Bimodule.rsmul ((QuantumGraph.Grad A) x) y + Bimodule.lsmul x ((QuantumGraph.Grad A) y)