LeanPool.Monlib4.QuantumGraph.Basic

Imported Lean Pool material for LeanPool.Monlib4.QuantumGraph.Basic.

instance FiniteDimensional.innerProductSpace.complete {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] : CompleteSpace E

theorem symmMap_apply_schurMul {A : Type u_1} {B : Type u_2} [starAlgebra A] [starAlgebra B] [hA : QuantumSet A] [QuantumSet B] (f g : A →ₗ[ℂ] B) : (symmMap ℂ A B) (f •ₛ g) = (symmMap ℂ A B) g •ₛ (symmMap ℂ A B) f

theorem QuantumSet.modAut_star {A : Type u_1} [self : starAlgebra A] (r : ℝ) (x : A) : star ((modAut r) x) = (modAut (-r)) (star x)

Alias of starAlgebra.modAut_star.

---

Star changes the sign of the modular parameter.

theorem QuantumSet.modAut_zero {A : Type u_1} [hA : starAlgebra A] : modAut 0 = 1

Alias of starAlgebra.modAut_zero.

theorem Psi_apply_linearMap_comp_linearMap_of_commute_modAut {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [ha : starAlgebra A] [hb : starAlgebra B] [hc : starAlgebra C] [hd : starAlgebra D] [hA : QuantumSet A] [hB : QuantumSet B] [hC : QuantumSet C] [hD : QuantumSet D] {f : A →ₗ[ℂ] B} {g : D →ₗ[ℂ] C} (t r : ℝ) (hf : (modAut t).toLinearMap ∘ₗ f = f ∘ₗ (modAut t).toLinearMap) (hg : (modAut r).toLinearMap ∘ₗ g = g ∘ₗ (modAut r).toLinearMap) (x : C →ₗ[ℂ] A) : (QuantumSet.Psi t r) (f ∘ₗ x ∘ₗ g) = (TensorProduct.map f ((symmMap ℂ C D).symm g).op) ((QuantumSet.Psi t r) x)

theorem symmMap_symm_comp {A : Type u_1} {B : Type u_2} {C : Type u_3} [starAlgebra A] [starAlgebra B] [hA : QuantumSet A] [hB : QuantumSet B] [starAlgebra C] [QuantumSet C] (x : A →ₗ[ℂ] B) (y : C →ₗ[ℂ] A) : (symmMap ℂ B C).symm (x ∘ₗ y) = (symmMap ℂ A C).symm y ∘ₗ (symmMap ℂ B A).symm x

theorem linearMap_map_Psi_of_commute_modAut {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [ha : starAlgebra A] [hb : starAlgebra B] [hc : starAlgebra C] [hd : starAlgebra D] [hA : QuantumSet A] [hB : QuantumSet B] [hC : QuantumSet C] [hD : QuantumSet D] {f : A →ₗ[ℂ] B} {g : Cᵐᵒᵖ →ₗ[ℂ] Dᵐᵒᵖ} (t r : ℝ) (hf : (modAut t).toLinearMap ∘ₗ f = f ∘ₗ (modAut t).toLinearMap) (hg : (modAut r).toLinearMap ∘ₗ g.unop = g.unop ∘ₗ (modAut r).toLinearMap) (x : C →ₗ[ℂ] A) : (TensorProduct.map f g) ((QuantumSet.Psi t r) x) = (QuantumSet.Psi t r) (f ∘ₗ x ∘ₗ (symmMap ℂ C D) g.unop)

@[simp]

theorem LinearMap.op_real {K : Type u_1} {E : Type u_2} {F : Type u_3} [AddCommMonoid E] [StarAddMonoid E] [AddCommMonoid F] [StarAddMonoid F] [Semiring K] [Module K E] [Module K F] [InvolutiveStar K] [StarModule K E] [StarModule K F] (φ : E →ₗ[K] F) : φ.op.real = φ.real.op

theorem modAut_map_comp_Psi {A : Type u_1} {B : Type u_2} [ha : starAlgebra A] [hb : starAlgebra B] [hA : QuantumSet A] [hB : QuantumSet B] (t₁ r₁ t₂ r₂ : ℝ) : TensorProduct.map (modAut t₁).toLinearMap (AlgEquiv.op (modAut r₁)).toLinearMap ∘ₗ ↑(QuantumSet.Psi t₂ r₂) = ↑(QuantumSet.Psi (t₁ + t₂) (-r₁ + r₂))

theorem lTensor_modAut_comp_Psi {A : Type u_1} {B : Type u_2} [ha : starAlgebra A] [hb : starAlgebra B] [hA : QuantumSet A] [hB : QuantumSet B] (t₂ r₁ r₂ : ℝ) : LinearMap.lTensor B (AlgEquiv.op (modAut r₁)).toLinearMap ∘ₗ ↑(QuantumSet.Psi t₂ r₂) = ↑(QuantumSet.Psi t₂ (-r₁ + r₂))

theorem rTensor_modAut_comp_Psi {A : Type u_1} {B : Type u_2} [ha : starAlgebra A] [hb : starAlgebra B] [hA : QuantumSet A] [hB : QuantumSet B] (t₁ t₂ r₂ : ℝ) : LinearMap.rTensor Aᵐᵒᵖ (modAut t₁).toLinearMap ∘ₗ ↑(QuantumSet.Psi t₂ r₂) = ↑(QuantumSet.Psi (t₁ + t₂) r₂)

theorem rmulMapLmul_apply_Upsilon_apply {A : Type u_1} {B : Type u_2} [ha : starAlgebra A] [hb : starAlgebra B] [hA : QuantumSet A] [hB : QuantumSet B] (x : A →ₗ[ℂ] B) (y : TensorProduct ℂ A B) : (rmulMapLmul (Upsilon x)) y = Upsilon (x •ₛ Upsilon.symm y)

theorem QuantumSet.comm_op_modAut_map_comul_one_eq_Psi {A : Type u_1} {B : Type u_2} [ha : starAlgebra A] [hb : starAlgebra B] [hA : QuantumSet A] [hB : QuantumSet B] (r : ℝ) (f : A →ₗ[ℂ] B) : (TensorProduct.comm ℂ Aᵐᵒᵖ B) ((TensorProduct.map (↑(op ℂ) ∘ₗ (modAut r).toLinearMap) f) (CoalgebraStruct.comul 1)) = (Psi 0 (k A + 1 - r)) f

@[simp]

theorem AlgEquiv.symm_one {R : Type u_3} {A : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] : symm 1 = 1

theorem LinearMap.lTensor_eq {R : Type u_3} {M : Type u_4} {N : Type u_5} {P : Type u_6} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (f : N →ₗ[R] P) : lTensor M f = TensorProduct.map id f

theorem AlgEquiv.symm_op {R : Type u_3} {A : Type u_4} {B : Type u_5} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A ≃ₐ[R] B) : (op f).symm = op f.symm

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

Alias of starAlgebra.modAut_trans.

---

The modular automorphisms compose additively in the real parameter.

theorem isReal_iff_Psi {A : Type u_3} {B : Type u_4} [ha : starAlgebra A] [hb : starAlgebra B] [hA : QuantumSet A] [hB : QuantumSet B] (f : A →ₗ[ℂ] B) (t r : ℝ) : LinearMap.IsReal f ↔ star ((QuantumSet.Psi t r) f) = (QuantumSet.Psi (-t) (2 * k A + 1 - r)) f

theorem isReal_iff_Psi_isSelfAdjoint {A : Type u_3} {B : Type u_4} [ha : starAlgebra A] [hb : starAlgebra B] [hA : QuantumSet A] [hB : QuantumSet B] (f : A →ₗ[ℂ] B) : LinearMap.IsReal f ↔ IsSelfAdjoint ((QuantumSet.Psi 0 (k A + 1 / 2)) f)

theorem real_Upsilon_toBimodule {A : Type u_3} {B : Type u_4} [ha : starAlgebra A] [hb : starAlgebra B] [hA : QuantumSet A] [hB : QuantumSet B] {f : A →ₗ[ℂ] B} (gns₁ : k A = 0) (gns₂ : k B = 0) : ↑(TensorProduct.toIsBimoduleMap (Upsilon f.real)) = LinearMap.adjoint ↑(TensorProduct.toIsBimoduleMap (Upsilon f))

class schurProjection {A : Type u_3} {B : Type u_4} [ha : starAlgebra A] [hb : starAlgebra B] [hA : QuantumSet A] [hB : QuantumSet B] (f : A →ₗ[ℂ] B) : Prop

A Schur projection is an idempotent real map for the Schur product.

• isIdempotentElem : f •ₛ f = f

  Schur idempotence.

• isReal : LinearMap.IsReal f

  Realness of the underlying linear map.

theorem Coalgebra.comul_mul_of_gns {A : Type u_3} [ha : starAlgebra A] [hA : QuantumSet A] (gns : k A = 0) (a b : A) : comul (a * b) = ∑ i : n A, (a * onb i) ⊗ₜ[ℂ] (star (onb i) * b)

theorem QuantumSet.counit_isReal {A : Type u_5} [starAlgebra A] [QuantumSet A] : LinearMap.IsReal CoalgebraStruct.counit

theorem QuantumSet.innerOne_map_one_isReal_ofReal {A : Type u_5} {B : Type u_6} [starAlgebra A] [starAlgebra B] [QuantumSet A] [QuantumSet B] {f : A →ₗ[ℂ] B} (hf : LinearMap.IsReal f) : inner ℂ 1 (f 1) = ↑(inner ℂ 1 (f 1)).re

@[reducible]

noncomputable def starAlgebra.mulOpposite {A : Type u_5} [starAlgebra A] : starAlgebra Aᵐᵒᵖ

The star-algebra structure transported to the opposite algebra.

Equations

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

@[reducible]

noncomputable def InnerProductAlgebra.mulOpposite {A : Type u_5} [starAlgebra A] [InnerProductAlgebra A] : InnerProductAlgebra Aᵐᵒᵖ

The inner-product algebra structure transported to the opposite algebra.

Equations

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

@[implicit_reducible]

noncomputable instance QuantumSet.mulOpposite {A : Type u_5} [starAlgebra A] [QuantumSet A] [kms : Fact (k A = -(1 / 2))] : QuantumSet Aᵐᵒᵖ

Equations

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

@[implicit_reducible]

noncomputable instance CoalgebraStruct.mulOpposite {A : Type u_5} [Semiring A] [Algebra ℂ A] [CoalgebraStruct ℂ A] : CoalgebraStruct ℂ Aᵐᵒᵖ

Equations

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

theorem Coalgebra.counit_mulOpposite_eq {A : Type u_5} [Semiring A] [Algebra ℂ A] [CoalgebraStruct ℂ A] (a : Aᵐᵒᵖ) : counit a = counit (MulOpposite.unop a)

theorem QuantumSet.counit_isFaithful {A : Type u_5} [starAlgebra A] [QuantumSet A] : Module.Dual.IsFaithful CoalgebraStruct.counit

def Module.Dual.op {R : Type u_5} {A : Type u_6} [CommSemiring R] [AddCommMonoid A] [Module R A] (f : Dual R A) : Dual R Aᵐᵒᵖ

Opposite-algebra version of a module dual functional.

Equations

• f.op = ↑(unop R) ∘ₗ LinearMap.op f

theorem Module.Dual.op_apply {R : Type u_5} {A : Type u_6} [CommSemiring R] [AddCommMonoid A] [Module R A] (f : Dual R A) (x : Aᵐᵒᵖ) : f.op x = f (MulOpposite.unop x)

theorem Coalgebra.counit_moduleDualOp_eq {A : Type u_5} [Semiring A] [Algebra ℂ A] [CoalgebraStruct ℂ A] : Module.Dual.op counit = counit

@[reducible]

def MulOpposite.starRing {A : Type u_5} [NonUnitalNonAssocSemiring A] [hA : StarRing A] : StarRing Aᵐᵒᵖ

Star-ring structure on the opposite of a star ring.

Equations

• MulOpposite.starRing = { toStarMul := MulOpposite.instStarMul, star_add := ⋯ }

theorem Module.Dual.op_isFaithful_iff {𝕜 : Type u_5} {A : Type u_6} [RCLike 𝕜] [NonUnitalSemiring A] [StarRing A] [Module 𝕜 A] (φ : Dual 𝕜 A) : φ.IsFaithful ↔ φ.op.IsFaithful

theorem QuantumSet.counit_op_isFaithful {A : Type u_5} [starAlgebra A] [QuantumSet A] : Module.Dual.IsFaithful CoalgebraStruct.counit

@[implicit_reducible]

noncomputable instance QuantumSet.tensorOpSelf {A : Type u_5} [starAlgebra A] [QuantumSet A] [kms : Fact (k A = -(1 / 2))] : QuantumSet (TensorProduct ℂ A Aᵐᵒᵖ)

Equations

• QuantumSet.tensorOpSelf = QuantumSet.tensorProduct

theorem MulOpposite.norm_eq {𝕜 : Type u_5} {H : Type u_6} [RCLike 𝕜] [NormedAddCommGroup H] (x : Hᵐᵒᵖ) : ‖x‖ = ‖unop x‖

theorem Coalgebra.comul_mul {A : Type u_3} [ha : starAlgebra A] [hA : QuantumSet A] (a b : A) : comul (a * b) = ∑ i : n A, (a * (modAut (k A / 2)) (onb i)) ⊗ₜ[ℂ] (star ((modAut (k A / 2)) (onb i)) * b)

theorem schurProjection.isPosMap {A : Type u_3} {B : Type u_4} [ha : starAlgebra A] [hb : starAlgebra B] [hA : QuantumSet A] [hB : QuantumSet B] [PartialOrder A] [PartialOrder B] [StarOrderedRing B] (h₁ : ∀ ⦃a : A⦄, 0 ≤ a ↔ ∃ (b : A), a = star b * b) {f : A →ₗ[ℂ] B} (hf : schurProjection f) : LinearMap.IsPosMap f

theorem schurIdempotent.isSchurProjection_iff_isPosMap {A : Type u_3} {B : Type u_4} [ha : starAlgebra A] [hb : starAlgebra B] [hA : QuantumSet A] [hB : QuantumSet B] [PartialOrder A] [PartialOrder B] [StarOrderedRing A] [StarOrderedRing B] (h₁ : ∀ ⦃a : A⦄, 0 ≤ a ↔ ∃ (b : A), a = star b * b) (hh : isEquivToPiMat A) {f : A →ₗ[ℂ] B} (hf : f •ₛ f = f) : schurProjection f ↔ LinearMap.IsPosMap f

class QuantumGraph (A : Type u_5) [starAlgebra A] [hA : QuantumSet A] [CoalgebraStruct ℂ A] (f : A →ₗ[ℂ] A) : Prop

A quantum graph is a Schur-idempotent endomorphism of a quantum set.

• isIdempotentElem : f •ₛ f = f

  Schur idempotence of the adjacency map.

theorem quantumGraph_iff {A : Type u_5} [starAlgebra A] [QuantumSet A] [CoalgebraStruct ℂ A] {f : A →ₗ[ℂ] A} : QuantumGraph A f ↔ f •ₛ f = f

class QuantumGraph.IsReal {A : Type u_5} [starAlgebra A] [hA : QuantumSet A] [CoalgebraStruct ℂ A] {f : A →ₗ[ℂ] A} (h : QuantumGraph A f) : Prop

Predicate asserting that a quantum graph is real.

• isReal : LinearMap.IsReal f

  Realness of the adjacency map.

class QuantumGraph.Real (A : Type u_5) [starAlgebra A] [hA : QuantumSet A] [CoalgebraStruct ℂ A] (f : A →ₗ[ℂ] A) : Prop

A real quantum graph bundles Schur idempotence and realness.

• isIdempotentElem : f •ₛ f = f

  Schur idempotence of the adjacency map.

• isReal : LinearMap.IsReal f

  Realness of the adjacency map.

theorem QuantumGraph.real_iff {A : Type u_5} [starAlgebra A] [QuantumSet A] [CoalgebraStruct ℂ A] {f : A →ₗ[ℂ] A} : Real A f ↔ f •ₛ f = f ∧ LinearMap.IsReal f

theorem quantumGraphReal_iff_schurProjection {A : Type u_3} [ha : starAlgebra A] [hA : QuantumSet A] {f : A →ₗ[ℂ] A} : QuantumGraph.Real A f ↔ schurProjection f

theorem QuantumGraph.Real.toQuantumGraph {A : Type u_3} [ha : starAlgebra A] [hA : QuantumSet A] {f : A →ₗ[ℂ] A} (h : Real A f) : QuantumGraph A f

theorem quantumGraphReal_iff_Psi_isIdempotentElem_and_isSelfAdjoint {A : Type u_3} [ha : starAlgebra A] [hA : QuantumSet A] {f : A →ₗ[ℂ] A} : QuantumGraph.Real A f ↔ IsIdempotentElem ((QuantumSet.Psi 0 (k A + 1 / 2)) f) ∧ IsSelfAdjoint ((QuantumSet.Psi 0 (k A + 1 / 2)) f)

theorem schurMul_Upsilon_toBimodule {A : Type u_3} {B : Type u_4} [ha : starAlgebra A] [hb : starAlgebra B] [hA : QuantumSet A] [hB : QuantumSet B] {f g : A →ₗ[ℂ] B} : ↑(TensorProduct.toIsBimoduleMap (Upsilon (f •ₛ g))) = ↑(TensorProduct.toIsBimoduleMap (Upsilon f)) * ↑(TensorProduct.toIsBimoduleMap (Upsilon g))

theorem quantumGraphReal_iff_Upsilon_toBimodule_orthogonalProjection {A : Type u_3} [ha : starAlgebra A] [hA : QuantumSet A] {f : A →ₗ[ℂ] A} (gns : k A = 0) : QuantumGraph.Real A f ↔ (LinearMap.toContinuousLinearMap ↑(TensorProduct.toIsBimoduleMap (Upsilon f))).IsOrthogonalProjection

theorem StarAlgEquiv.toAlgEquiv_toAlgHom_toLinearMap {R : Type u_5} {A : Type u_6} {B : Type u_7} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] [Star A] [Star B] (f : A ≃⋆ₐ[R] B) : (↑f.toAlgEquiv).toLinearMap = f.toLinearMap

theorem QuantumGraph.Real_conj_starAlgEquiv {A : Type u_5} {B : Type u_6} [starAlgebra A] [starAlgebra B] [QuantumSet A] [QuantumSet B] {x : A →ₗ[ℂ] A} (hx : Real A x) {f : A ≃⋆ₐ[ℂ] B} (hf : Isometry ⇑f) : Real B (f.toLinearMap ∘ₗ x ∘ₗ LinearMap.adjoint f.toLinearMap)

Real quantum graphs are preserved by isometric star-algebra equivalence conjugation.

theorem Submodule.eq_iff_orthogonalProjection_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {U V : Submodule ℂ E} [CompleteSpace E] [CompleteSpace ↥U] [CompleteSpace ↥V] : U = V ↔ orthogonalProjection' U = orthogonalProjection' V

theorem Submodule.adjoint_subtype {E : Type u_5} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] {U : Submodule ℂ E} : LinearMap.adjoint U.subtype = ↑U.orthogonalProjectionOnto

theorem Submodule.map_orthogonalProjection_self {E : Type u_5} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [FiniteDimensional ℂ E] {U : Submodule ℂ E} : map (↑U.orthogonalProjectionOnto) U = ⊤

theorem orthogonalProjection_submoduleMap {E : Type u_5} {E' : Type u_6} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [NormedAddCommGroup E'] [InnerProductSpace ℂ E'] {U : Submodule ℂ E} [FiniteDimensional ℂ E] [FiniteDimensional ℂ E'] (f : E ≃ₗᵢ[ℂ] E') : ↑(orthogonalProjection' (Submodule.map (↑f.toLinearEquiv) U)) = ↑f.toLinearEquiv ∘ₗ ↑(orthogonalProjection' U) ∘ₗ ↑f.symm.toLinearEquiv

theorem orthogonalProjection_submoduleMap_isometry {E : Type u_5} {E' : Type u_6} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [NormedAddCommGroup E'] [InnerProductSpace ℂ E'] {U : Submodule ℂ E} [FiniteDimensional ℂ E] [FiniteDimensional ℂ E'] {f : E ≃ₗ[ℂ] E'} (hf : Isometry ⇑f) : ↑(orthogonalProjection' (Submodule.map (↑f) U)) = ↑f ∘ₗ ↑(orthogonalProjection' U) ∘ₗ ↑f.symm

instance StarAlgEquivClass.instLinearMapClass {R : Type u_5} {A : Type u_6} {B : Type u_7} [Semiring R] [AddCommMonoid A] [AddCommMonoid B] [Mul A] [Mul B] [Module R A] [Module R B] [Star A] [Star B] {F : Type u_8} [EquivLike F A B] [NonUnitalAlgEquivClass F R A B] [StarHomClass F A B] : LinearMapClass F R A B

theorem orthogonalProjection_submoduleMap_isometry_starAlgEquiv {E : Type u_5} {E' : Type u_6} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [NormedAddCommGroup E'] [InnerProductSpace ℂ E'] {U : Submodule ℂ E} [Mul E] [Mul E'] [Star E] [Star E'] [FiniteDimensional ℂ E] [FiniteDimensional ℂ E'] {f : E ≃⋆ₐ[ℂ] E'} (hf : Isometry ⇑f) : ↑(orthogonalProjection' (Submodule.map f.toLinearMap U)) = f.toLinearMap ∘ₗ ↑(orthogonalProjection' U) ∘ₗ f.symm.toLinearMap

theorem orthogonalProjection_submoduleMap' {E : Type u_5} {E' : Type u_6} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [NormedAddCommGroup E'] [InnerProductSpace ℂ E'] {U : Submodule ℂ E} [FiniteDimensional ℂ E] [FiniteDimensional ℂ E'] (f : E' ≃ₗᵢ[ℂ] E) : ↑(orthogonalProjection' (Submodule.map (↑f.symm.toLinearEquiv) U)) = ↑f.symm.toLinearEquiv ∘ₗ ↑(orthogonalProjection' U) ∘ₗ ↑f.toLinearEquiv

noncomputable def QuantumGraph.Real.upsilonSubmodule {A : Type u_3} [ha : starAlgebra A] [hA : QuantumSet A] {f : A →ₗ[ℂ] A} (gns : k A = 0) (hf : Real A f) : Submodule ℂ (TensorProduct ℂ A A)

The submodule whose orthogonal projection corresponds to Upsilon f.

Equations

• QuantumGraph.Real.upsilonSubmodule gns hf = Classical.choose ⋯

instance QuantumGraph.Real.upsilonSubmodule.hasOrthogonalProjection {A : Type u_3} [ha : starAlgebra A] [hA : QuantumSet A] {f : A →ₗ[ℂ] A} (gns : k A = 0) (hf : Real A f) : (upsilonSubmodule gns hf).HasOrthogonalProjection

theorem QuantumGraph.Real.upsilonOrthogonalProjection {A : Type u_3} [ha : starAlgebra A] [hA : QuantumSet A] {f : A →ₗ[ℂ] A} (gns : k A = 0) (hf : Real A f) : orthogonalProjection' (upsilonSubmodule gns hf) = LinearMap.toContinuousLinearMap ↑(TensorProduct.toIsBimoduleMap (Upsilon f))

theorem QuantumGraph.Real.upsilonOrthogonalProjection' {A : Type u_3} [ha : starAlgebra A] [hA : QuantumSet A] {f : A →ₗ[ℂ] A} (gns : k A = 0) (hf : Real A f) : ↑(orthogonalProjection' (upsilonSubmodule gns hf)) = rmulMapLmul (↑(orthogonalProjection' (upsilonSubmodule gns hf)) 1)

noncomputable def QuantumGraph.Real.upsilonOrthonormalBasis {A : Type u_3} [ha : starAlgebra A] [hA : QuantumSet A] {f : A →ₗ[ℂ] A} (gns : k A = 0) (hf : Real A f) : OrthonormalBasis (Fin (Module.finrank ℂ ↥(upsilonSubmodule gns hf))) ℂ ↥(upsilonSubmodule gns hf)

A canonical orthonormal basis of upsilonSubmodule.

Equations

• QuantumGraph.Real.upsilonOrthonormalBasis gns hf = stdOrthonormalBasis ℂ ↥(QuantumGraph.Real.upsilonSubmodule gns hf)

theorem OrthonormalBasis.tensorProduct_toBasis {𝕜 : Type u_5} {E : Type u_6} {F : Type u_7} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {ι₁ : Type u_8} {ι₂ : Type u_9} [Fintype ι₁] [Fintype ι₂] (b₁ : OrthonormalBasis ι₁ 𝕜 E) (b₂ : OrthonormalBasis ι₂ 𝕜 F) : (b₁.tensorProduct b₂).toBasis = b₁.toBasis.tensorProduct b₂.toBasis

theorem TensorProduct.of_orthonormalBasis_eq_span {𝕜 : Type u_5} {E : Type u_6} {F : Type u_7} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (x : TensorProduct 𝕜 E F) {ι₁ : Type u_8} {ι₂ : Type u_9} [Fintype ι₁] [Fintype ι₂] (b₁ : OrthonormalBasis ι₁ 𝕜 E) (b₂ : OrthonormalBasis ι₂ 𝕜 F) : x = ∑ i : ι₁, ∑ j : ι₂, ((b₁.tensorProduct b₂).repr x).ofLp (i, j) • b₁ i ⊗ₜ[𝕜] b₂ j

noncomputable def TensorProduct.ofOrthonormalBasisProd {𝕜 : Type u_5} {E : Type u_6} {F : Type u_7} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (x : TensorProduct 𝕜 E F) {ι₁ : Type u_8} {ι₂ : Type u_9} [Fintype ι₁] [Fintype ι₂] (b₁ : OrthonormalBasis ι₁ 𝕜 E) (b₂ : OrthonormalBasis ι₂ 𝕜 F) : ι₁ × ι₂ → E × F

Coordinates of a tensor as a product-indexed family of scalar-weighted basis pairs.

Equations

• x.ofOrthonormalBasisProd b₁ b₂ (i, j) = (((b₁.tensorProduct b₂).repr x).ofLp (i, j) • b₁ i, b₂ j)

@[simp]

theorem TensorProduct.of_othonormalBasis_prod_eq {𝕜 : Type u_5} {E : Type u_6} {F : Type u_7} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (x : TensorProduct 𝕜 E F) {ι₁ : Type u_8} {ι₂ : Type u_9} [Fintype ι₁] [Fintype ι₂] (b₁ : OrthonormalBasis ι₁ 𝕜 E) (b₂ : OrthonormalBasis ι₂ 𝕜 F) : ∑ i : ι₁ × ι₂, (x.ofOrthonormalBasisProd b₁ b₂ i).1 ⊗ₜ[𝕜] (x.ofOrthonormalBasisProd b₁ b₂ i).2 = x

@[simp]

theorem TensorProduct.of_othonormalBasis_prod_eq' {𝕜 : Type u_5} {E : Type u_6} {F : Type u_7} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (x : TensorProduct 𝕜 E F) {ι₁ : Type u_8} {ι₂ : Type u_9} [Fintype ι₁] [Fintype ι₂] (b₁ : OrthonormalBasis ι₁ 𝕜 E) (b₂ : OrthonormalBasis ι₂ 𝕜 F) : ∑ i : ι₁ × ι₂, (x.ofOrthonormalBasisProd b₁ b₂ i).1 ⊗ₜ[𝕜] b₂ i.2 = x

theorem QuantumGraph.Real.upsilon_eq {A : Type u_3} [ha : starAlgebra A] [hA : QuantumSet A] {f : A →ₗ[ℂ] A} (hf : Real A f) (gns : k A = 0) : have u := upsilonOrthonormalBasis gns hf; have b := onb; have a := fun (x : TensorProduct ℂ A A) (i : n A × n A) => (x.ofOrthonormalBasisProd b b i).1; f = ↑(∑ i : Fin (Module.finrank ℂ ↥(upsilonSubmodule gns hf)), ∑ j : n A × n A, inner ℂ (↑(u i)) 1 • ((rankOne ℂ) (b j.2)) ((modAut (-1)) (star (a (↑(u i)) j))))

theorem QuantumGraph.Real.upsilon_eq' {A : Type u_3} [ha : starAlgebra A] [hA : QuantumSet A] {f : A →ₗ[ℂ] A} (hf : Real A f) (gns : k A = 0) : have u := upsilonOrthonormalBasis gns hf; have b := onb; have a := fun (x : TensorProduct ℂ A A) (i : n A × n A) => (x.ofOrthonormalBasisProd b b i).1; f = ↑(∑ i : Fin (Module.finrank ℂ ↥(upsilonSubmodule gns hf)), ∑ j : n A × n A, inner ℂ 1 ↑(u i) • ((rankOne ℂ) (star (b j.2))) (a (↑(u i)) j))

noncomputable def TensorProduct.ofOrthonormalBasisProd₁Lm {𝕜 : Type u_5} {E : Type u_6} {F : Type u_7} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι₁ : Type u_8} {ι₂ : Type u_9} [Fintype ι₁] [Fintype ι₂] (b₁ : OrthonormalBasis ι₁ 𝕜 E) (b₂ : OrthonormalBasis ι₂ 𝕜 F) : TensorProduct 𝕜 E F →ₗ[𝕜] ι₁ × ι₂ → E

Linear map sending a tensor to its first-coordinate orthonormal-basis expansion data.

Equations

• TensorProduct.ofOrthonormalBasisProd₁Lm b₁ b₂ = { toFun := fun (x : TensorProduct 𝕜 E F) (i : ι₁ × ι₂) => (x.ofOrthonormalBasisProd b₁ b₂ i).1, map_add' := ⋯, map_smul' := ⋯ }

theorem TensorProduct.ofOrthonormalBasisProd₁Lm_eq {𝕜 : Type u_5} {E : Type u_6} {F : Type u_7} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {ι₁ : Type u_8} {ι₂ : Type u_9} [Fintype ι₁] [Fintype ι₂] (b₁ : OrthonormalBasis ι₁ 𝕜 E) (b₂ : OrthonormalBasis ι₂ 𝕜 F) (x : TensorProduct 𝕜 E F) (i : ι₁ × ι₂) : (ofOrthonormalBasisProd₁Lm b₁ b₂) x i = (x.ofOrthonormalBasisProd b₁ b₂ i).1

theorem QuantumGraph.Real.upsilon_eq'' {A : Type u_3} [ha : starAlgebra A] [hA : QuantumSet A] {f : A →ₗ[ℂ] A} (hf : Real A f) (gns : k A = 0) : have P := orthogonalProjection' (upsilonSubmodule gns hf); have a := fun (x : TensorProduct ℂ A A) (i : n A × n A) => (x.ofOrthonormalBasisProd onb onb i).1; f = ↑(∑ j : n A × n A, ((rankOne ℂ) (star (onb j.2))) (a (P 1) j))

theorem QuantumSet.starAlgEquiv_commutes_with_modAut_of_isometry'' {A : Type u_5} {B : Type u_6} [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 LinearMap.tensorProduct_map_isometry_of {𝕜 : Type u_5} {A : Type u_6} {B : Type u_7} {C : Type u_8} {D : Type u_9} [RCLike 𝕜] [NormedAddCommGroup A] [NormedAddCommGroup B] [NormedAddCommGroup C] [NormedAddCommGroup D] [InnerProductSpace 𝕜 A] [InnerProductSpace 𝕜 B] [InnerProductSpace 𝕜 C] [InnerProductSpace 𝕜 D] [FiniteDimensional 𝕜 A] [FiniteDimensional 𝕜 B] [FiniteDimensional 𝕜 C] [FiniteDimensional 𝕜 D] {f : A →ₗ[𝕜] B} (hf : Isometry ⇑f) {g : C →ₗ[𝕜] D} (hg : Isometry ⇑g) : Isometry ⇑(TensorProduct.map f g)

theorem StarAlgEquiv.tensorProduct_map_isometry_of {A : Type u_5} {B : Type u_6} {C : Type u_7} {D : Type u_8} [starAlgebra A] [starAlgebra B] [starAlgebra C] [starAlgebra D] [QuantumSet A] [QuantumSet B] [QuantumSet C] [QuantumSet D] {f : A ≃⋆ₐ[ℂ] B} (hf : Isometry ⇑f) {g : C ≃⋆ₐ[ℂ] D} (hg : Isometry ⇑g) : Isometry ⇑(TensorProduct.map f g)

noncomputable def LinearIsometryEquiv.TensorProduct.map {𝕜 : Type u_5} {A : Type u_6} {B : Type u_7} {C : Type u_8} {D : Type u_9} [RCLike 𝕜] [NormedAddCommGroup A] [NormedAddCommGroup B] [NormedAddCommGroup C] [NormedAddCommGroup D] [InnerProductSpace 𝕜 A] [InnerProductSpace 𝕜 B] [InnerProductSpace 𝕜 C] [InnerProductSpace 𝕜 D] [FiniteDimensional 𝕜 A] [FiniteDimensional 𝕜 B] [FiniteDimensional 𝕜 C] [FiniteDimensional 𝕜 D] (f : A ≃ₗᵢ[𝕜] B) (g : C ≃ₗᵢ[𝕜] D) : TensorProduct 𝕜 A C ≃ₗᵢ[𝕜] TensorProduct 𝕜 B D

Tensor product of two linear isometry equivalences.

Equations

• LinearIsometryEquiv.TensorProduct.map f g = { toLinearEquiv := LinearEquiv.TensorProduct.map f.toLinearEquiv g.toLinearEquiv, norm_map' := ⋯ }

@[simp]

theorem LinearIsometryEquiv.TensorProduct.map_symm_apply {𝕜 : Type u_5} {A : Type u_6} {B : Type u_7} {C : Type u_8} {D : Type u_9} [RCLike 𝕜] [NormedAddCommGroup A] [NormedAddCommGroup B] [NormedAddCommGroup C] [NormedAddCommGroup D] [InnerProductSpace 𝕜 A] [InnerProductSpace 𝕜 B] [InnerProductSpace 𝕜 C] [InnerProductSpace 𝕜 D] [FiniteDimensional 𝕜 A] [FiniteDimensional 𝕜 B] [FiniteDimensional 𝕜 C] [FiniteDimensional 𝕜 D] (f : A ≃ₗᵢ[𝕜] B) (g : C ≃ₗᵢ[𝕜] D) (x : TensorProduct 𝕜 B D) : (map f g).symm x = (_root_.TensorProduct.map ↑f.symm ↑g.symm) x

@[simp]

theorem LinearIsometryEquiv.TensorProduct.map_apply {𝕜 : Type u_5} {A : Type u_6} {B : Type u_7} {C : Type u_8} {D : Type u_9} [RCLike 𝕜] [NormedAddCommGroup A] [NormedAddCommGroup B] [NormedAddCommGroup C] [NormedAddCommGroup D] [InnerProductSpace 𝕜 A] [InnerProductSpace 𝕜 B] [InnerProductSpace 𝕜 C] [InnerProductSpace 𝕜 D] [FiniteDimensional 𝕜 A] [FiniteDimensional 𝕜 B] [FiniteDimensional 𝕜 C] [FiniteDimensional 𝕜 D] (f : A ≃ₗᵢ[𝕜] B) (g : C ≃ₗᵢ[𝕜] D) (x : TensorProduct 𝕜 A C) : (map f g) x = (_root_.TensorProduct.map ↑f.toLinearEquiv ↑g.toLinearEquiv) x

theorem LinearIsometryEquiv.TensorProduct.map_tmul {𝕜 : Type u_5} {A : Type u_6} {B : Type u_7} {C : Type u_8} {D : Type u_9} [RCLike 𝕜] [NormedAddCommGroup A] [NormedAddCommGroup B] [NormedAddCommGroup C] [NormedAddCommGroup D] [InnerProductSpace 𝕜 A] [InnerProductSpace 𝕜 B] [InnerProductSpace 𝕜 C] [InnerProductSpace 𝕜 D] [FiniteDimensional 𝕜 A] [FiniteDimensional 𝕜 B] [FiniteDimensional 𝕜 C] [FiniteDimensional 𝕜 D] (f : A ≃ₗᵢ[𝕜] B) (g : C ≃ₗᵢ[𝕜] D) (x : A) (y : C) : (map f g) (x ⊗ₜ[𝕜] y) = f x ⊗ₜ[𝕜] g y

theorem oneHom_isometry_inner_one_right {𝕜 : Type u_5} {A : Type u_6} {B : Type u_7} [RCLike 𝕜] [NormedAddCommGroup A] [NormedAddCommGroup B] [InnerProductSpace 𝕜 A] [InnerProductSpace 𝕜 B] [One A] [One B] {F : Type u_8} [FunLike F A B] [LinearMapClass F 𝕜 A B] [OneHomClass F A B] {f : F} (hf : Isometry ⇑f) (x : A) : inner 𝕜 (f x) 1 = inner 𝕜 x 1

theorem QuantumGraph.Real.upsilon_starAlgEquiv_conj_eq {A : Type u_3} {B : Type u_4} [ha : starAlgebra A] [hb : starAlgebra B] [hA : QuantumSet A] [hB : QuantumSet B] {f : A →ₗ[ℂ] A} (gns : k A = 0) (gns₂ : k B = 0) (hf : Real A f) {φ : A ≃⋆ₐ[ℂ] B} (hφ : Isometry ⇑φ) : have u := upsilonOrthonormalBasis gns hf; have b := onb; have a := fun (x : TensorProduct ℂ A A) (i : n A × n A) => (x.ofOrthonormalBasisProd b b i).1; φ.toLinearMap ∘ₗ f ∘ₗ LinearMap.adjoint φ.toLinearMap = ↑(∑ i : Fin (Module.finrank ℂ ↥(upsilonSubmodule gns hf)), ∑ j : n A × n A, ∑ p : n A × n A, (inner ℂ (φ (a (↑(u i)) p)) 1 * inner ℂ (φ (b p.2)) 1) • ((rankOne ℂ) (φ (b j.2))) ((modAut (-1)) (star (φ (a (↑(u i)) j)))))

theorem LinearMapClass.apply_rankOne_apply {E₁ : Type u_5} {E₂ : Type u_6} {E₃ : Type u_7} {𝕜 : Type u_8} [RCLike 𝕜] [NormedAddCommGroup E₁] [NormedAddCommGroup E₂] [NormedAddCommGroup E₃] [InnerProductSpace 𝕜 E₁] [InnerProductSpace 𝕜 E₂] [InnerProductSpace 𝕜 E₃] {F : Type u_9} [FunLike F E₁ E₃] [LinearMapClass F 𝕜 E₁ E₃] (x : E₁) (y z : E₂) (u : F) : u ((((rankOne 𝕜) x) y) z) = (((rankOne 𝕜) (u x)) y) z

theorem Upsilon_apply_comp {A : Type u_3} {B : Type u_4} [ha : starAlgebra A] [hb : starAlgebra B] [hA : QuantumSet A] [hB : QuantumSet B] {C : Type u_5} {D : Type u_6} [starAlgebra C] [QuantumSet C] [starAlgebra D] [QuantumSet D] {f : A →ₗ[ℂ] B} {g : D →ₗ[ℂ] C} (x : C →ₗ[ℂ] A) (hcd : k C = k D) (h : (modAut (k C + 1)).toLinearMap ∘ₗ g = g ∘ₗ (modAut (k D + 1)).toLinearMap) : Upsilon (f ∘ₗ x ∘ₗ g) = (TensorProduct.map ((symmMap ℂ C D).symm g) f) (Upsilon x)

theorem TensorProduct.toIsBimoduleMap_comp {R : Type u_5} {H₁ : Type u_6} {H₂ : Type u_7} {H₃ : Type u_8} {H₄ : Type u_9} [CommSemiring R] [Semiring H₁] [Semiring H₂] [Semiring H₃] [Semiring H₄] [Algebra R H₁] [Algebra R H₂] [Algebra R H₃] [Algebra R H₄] {f : H₁ ≃ₐ[R] H₃} {g : H₂ ≃ₐ[R] H₄} {x : TensorProduct R H₁ H₂} : ↑(toIsBimoduleMap ((AlgEquiv.TensorProduct.map f g) x)) = (AlgEquiv.TensorProduct.map f g).toLinearMap ∘ₗ ↑(toIsBimoduleMap x) ∘ₗ (AlgEquiv.TensorProduct.map f.symm g.symm).toLinearMap

theorem QuantumGraph.Real.upsilon_starAlgEquiv_conj_submodule {A : Type u_3} {B : Type u_4} [ha : starAlgebra A] [hb : starAlgebra B] [hA : QuantumSet A] [hB : QuantumSet B] {f : A →ₗ[ℂ] A} (gns : k A = 0) (gns₂ : k B = 0) (hf : Real A f) {φ : A ≃⋆ₐ[ℂ] B} (hφ : Isometry ⇑φ) : upsilonSubmodule gns₂ ⋯ = Submodule.map (StarAlgEquiv.TensorProduct.map φ φ).toLinearMap (upsilonSubmodule gns hf)

theorem PhiMap.apply_real {B : Type u_4} [hb : starAlgebra B] [hB : QuantumSet B] (gns : k B = 0) (A : B →ₗ[ℂ] B) : ↑(PhiMap A.real) = LinearMap.adjoint ↑(PhiMap A)

theorem PhiMap_rankOne {B : Type u_4} [hb : starAlgebra B] [hB : QuantumSet B] (x y : B) : ↑(PhiMap ↑(((rankOne ℂ) x) y)) = TensorProduct.map (LinearMap.adjoint (rmul y)) (lmul x)

theorem LinearMap.real_zero {B : Type u_4} [hb : starAlgebra B] [hB : QuantumSet B] : real 0 = 0

theorem lTensor_counit_PhiMap_rTensor_algebraLinearMap {B : Type u_4} [hb : starAlgebra B] [hB : QuantumSet B] (x : B →ₗ[ℂ] B) : (modAut (-k B)).toLinearMap ∘ₗ ↑(TensorProduct.rid ℂ B) ∘ₗ LinearMap.lTensor B CoalgebraStruct.counit ∘ₗ ↑(PhiMap x) ∘ₗ LinearMap.rTensor B (Algebra.linearMap ℂ B) ∘ₗ ↑(TensorProduct.lid ℂ B).symm ∘ₗ (modAut (k B)).toLinearMap = (symmMap ℂ B B) x

noncomputable def QuantumGraph.NumOfEdges {A : Type u_5} [starAlgebra A] [QuantumSet A] : (A →ₗ[ℂ] A) →ₗ[ℂ] ℂ

Linear functional computing the weighted number of edges of a quantum graph.

Equations

• QuantumGraph.NumOfEdges = { toFun := fun (f : A →ₗ[ℂ] A) => inner ℂ 1 (f 1), map_add' := ⋯, map_smul' := ⋯ }