Schur Product Operator

This file ports the definition of the upstream Monlib.LinearAlgebra.QuantumSet.SchurMul operator. The deeper upstream Schur-product theorem stack depends on the finite-dimensional Hilbert-algebra coalgebra instance and tensor-product infrastructure that are not yet recovered in the current monlib4 slice.

noncomputable def schurMul {B : Type u_1} {C : Type u_2} [AddCommMonoid B] [NonUnitalNonAssocSemiring C] [Module ℂ B] [Module ℂ C] [CoalgebraStruct ℂ B] [SMulCommClass ℂ C C] [IsScalarTower ℂ C C] : (B →ₗ[ℂ] C) →ₗ[ℂ] (B →ₗ[ℂ] C) →ₗ[ℂ] B →ₗ[ℂ] C

Schur product x •ₛ y := m ∘ (x ⊗ y) ∘ comul.

Equations

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

@[simp]

theorem schurMul_apply_apply {B : Type u_1} {C : Type u_2} [AddCommMonoid B] [NonUnitalNonAssocSemiring C] [Module ℂ B] [Module ℂ C] [CoalgebraStruct ℂ B] [SMulCommClass ℂ C C] [IsScalarTower ℂ C C] (x y : B →ₗ[ℂ] C) : x •ₛ y = LinearMap.mul' ℂ C ∘ₗ TensorProduct.map x y ∘ₗ CoalgebraStruct.comul

def schurMulNotation : Lean.TrailingParserDescr

Schur product x •ₛ y := m ∘ (x ⊗ y) ∘ comul.

Equations

• schurMulNotation = Lean.ParserDescr.trailingNode `schurMulNotation 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " •ₛ ") (Lean.ParserDescr.cat `term 80))

theorem nonUnitalAlgHom_comp_mul {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₙₐ[R] B) : LinearMapClass.linearMap f ∘ₗ LinearMap.mul' R A = LinearMap.mul' R B ∘ₗ TensorProduct.map (LinearMapClass.linearMap f) (LinearMapClass.linearMap f)

theorem algHom_comp_mul {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) : f.toLinearMap ∘ₗ LinearMap.mul' R A = LinearMap.mul' R B ∘ₗ TensorProduct.map f.toLinearMap f.toLinearMap

theorem schurMul.apply_rankOne {A : Type u_1} {B : Type u_2} [NormedAddCommGroupOfRing A] [NormedAddCommGroupOfRing B] [InnerProductSpace ℂ A] [InnerProductSpace ℂ B] [SMulCommClass ℂ A A] [SMulCommClass ℂ B B] [IsScalarTower ℂ A A] [IsScalarTower ℂ B B] [FiniteDimensional ℂ A] (a c : B) (b d : A) : ↑(((rankOne ℂ) a) b) •ₛ ↑(((rankOne ℂ) c) d) = ↑(((rankOne ℂ) (a * c)) (b * d))

theorem schurMul.apply_ket {B : Type u_2} [NormedAddCommGroupOfRing B] [InnerProductSpace ℂ B] [SMulCommClass ℂ B B] [IsScalarTower ℂ B B] (a b : B) : ↑((ket ℂ) a) •ₛ ↑((ket ℂ) b) = ↑((ket ℂ) (a * b))

theorem bra_tmul {𝕜 : Type u_3} {B : Type u_4} {C : Type u_5} [RCLike 𝕜] [NormedAddCommGroup B] [NormedAddCommGroup C] [InnerProductSpace 𝕜 B] [InnerProductSpace 𝕜 C] (a : B) (b : C) : ↑((bra 𝕜) (a ⊗ₜ[𝕜] b)) = ↑(TensorProduct.lid 𝕜 𝕜) ∘ₗ TensorProduct.map ↑((bra 𝕜) a) ↑((bra 𝕜) b)

theorem bra_map_bra {𝕜 : Type u_3} {B : Type u_4} {C : Type u_5} [RCLike 𝕜] [NormedAddCommGroup B] [NormedAddCommGroup C] [InnerProductSpace 𝕜 B] [InnerProductSpace 𝕜 C] (a : B) (b : C) : TensorProduct.map ↑((bra 𝕜) a) ↑((bra 𝕜) b) = ↑(TensorProduct.lid 𝕜 𝕜).symm ∘ₗ ↑((bra 𝕜) (a ⊗ₜ[𝕜] b))

theorem ket_tmul {𝕜 : Type u_3} {B : Type u_4} {C : Type u_5} [RCLike 𝕜] [NormedAddCommGroup B] [NormedAddCommGroup C] [InnerProductSpace 𝕜 B] [InnerProductSpace 𝕜 C] (a : B) (b : C) : ↑((ket 𝕜) (a ⊗ₜ[𝕜] b)) = TensorProduct.map ↑((ket 𝕜) a) ↑((ket 𝕜) b) ∘ₗ ↑(TensorProduct.lid 𝕜 𝕜).symm

theorem ket_map_ket {𝕜 : Type u_3} {B : Type u_4} {C : Type u_5} [RCLike 𝕜] [NormedAddCommGroup B] [NormedAddCommGroup C] [InnerProductSpace 𝕜 B] [InnerProductSpace 𝕜 C] (a : B) (b : C) : TensorProduct.map ↑((ket 𝕜) a) ↑((ket 𝕜) b) = ↑((ket 𝕜) (a ⊗ₜ[𝕜] b)) ∘ₗ ↑(TensorProduct.lid 𝕜 𝕜)

theorem bra_comp_linearMap {𝕜 : Type u_3} {E₁ : Type u_4} {E₂ : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [NormedAddCommGroup E₂] [InnerProductSpace 𝕜 E₂] [FiniteDimensional 𝕜 E₁] [FiniteDimensional 𝕜 E₂] (x : E₂) (f : E₁ →ₗ[𝕜] E₂) : ↑((bra 𝕜) x) ∘ₗ f = ↑((bra 𝕜) ((LinearMap.adjoint f) x))

theorem linearMap_comp_ket {𝕜 : Type u_3} {E₁ : Type u_4} {E₂ : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [NormedAddCommGroup E₂] [InnerProductSpace 𝕜 E₂] (x : E₁) (f : E₁ →ₗ[𝕜] E₂) : f ∘ₗ ↑((ket 𝕜) x) = ↑((ket 𝕜) (f x))

theorem mul_comp_lid_symm {R : Type u_3} [CommSemiring R] : LinearMap.mul' R R ∘ₗ ↑(TensorProduct.lid R R).symm = LinearMap.id

theorem schurMul.apply_bra {B : Type u_2} [NormedAddCommGroupOfRing B] [InnerProductSpace ℂ B] [SMulCommClass ℂ B B] [IsScalarTower ℂ B B] [FiniteDimensional ℂ B] (a b : B) : ↑((bra ℂ) a) •ₛ ↑((bra ℂ) b) = ↑((bra ℂ) (a * b))

theorem schurMul.comp_apply_of {A : Type u_1} {B : Type u_2} [NormedAddCommGroupOfRing A] [NormedAddCommGroupOfRing B] [InnerProductSpace ℂ A] [InnerProductSpace ℂ B] [SMulCommClass ℂ A A] [SMulCommClass ℂ B B] [IsScalarTower ℂ A A] [IsScalarTower ℂ B B] [FiniteDimensional ℂ A] {C : Type u_3} [NormedAddCommGroupOfRing C] [InnerProductSpace ℂ C] [SMulCommClass ℂ C C] [IsScalarTower ℂ C C] [FiniteDimensional ℂ C] (δ : ℂ) (hAδ : CoalgebraStruct.comul ∘ₗ LinearMap.mul' ℂ A = δ • LinearMap.id) (a b : A →ₗ[ℂ] B) (c d : C →ₗ[ℂ] A) : (a •ₛ b) ∘ₗ c •ₛ d = δ • (a ∘ₗ c) •ₛ b ∘ₗ d

theorem schurMul_one_one_right {A : Type u_1} {B : Type u_2} [NormedAddCommGroupOfRing A] [NormedAddCommGroupOfRing B] [InnerProductSpace ℂ A] [InnerProductSpace ℂ B] [SMulCommClass ℂ A A] [SMulCommClass ℂ B B] [IsScalarTower ℂ A A] [IsScalarTower ℂ B B] [FiniteDimensional ℂ A] [FiniteDimensional ℂ B] (x : A →ₗ[ℂ] B) : x •ₛ ↑(((rankOne ℂ) 1) 1) = x

theorem schurMul_one_one_left {A : Type u_1} {B : Type u_2} [NormedAddCommGroupOfRing A] [NormedAddCommGroupOfRing B] [InnerProductSpace ℂ A] [InnerProductSpace ℂ B] [SMulCommClass ℂ A A] [SMulCommClass ℂ B B] [IsScalarTower ℂ A A] [IsScalarTower ℂ B B] [FiniteDimensional ℂ A] [FiniteDimensional ℂ B] (x : A →ₗ[ℂ] B) : ↑(((rankOne ℂ) 1) 1) •ₛ x = x

theorem schurMul_one_right_rankOne {A : Type u_1} [NormedAddCommGroupOfRing A] [InnerProductSpace ℂ A] [SMulCommClass ℂ A A] [IsScalarTower ℂ A A] [FiniteDimensional ℂ A] (a b : A) : ↑(((rankOne ℂ) a) b) •ₛ 1 = lmul a ∘ₗ LinearMap.adjoint (lmul b)

theorem schurMul_one_left_rankOne {A : Type u_1} [NormedAddCommGroupOfRing A] [InnerProductSpace ℂ A] [SMulCommClass ℂ A A] [IsScalarTower ℂ A A] [FiniteDimensional ℂ A] (a b : A) : 1 •ₛ ↑(((rankOne ℂ) a) b) = rmul a ∘ₗ LinearMap.adjoint (rmul b)

theorem schurMul_adjoint {A : Type u_1} {B : Type u_2} [NormedAddCommGroupOfRing A] [NormedAddCommGroupOfRing B] [InnerProductSpace ℂ A] [InnerProductSpace ℂ B] [SMulCommClass ℂ A A] [SMulCommClass ℂ B B] [IsScalarTower ℂ A A] [IsScalarTower ℂ B B] [FiniteDimensional ℂ A] [FiniteDimensional ℂ B] (x y : A →ₗ[ℂ] B) : LinearMap.adjoint (x •ₛ y) = LinearMap.adjoint x •ₛ LinearMap.adjoint y

theorem schurMul_real {A : Type u_3} {B : Type u_4} [starAlgebra A] [starAlgebra B] [QuantumSet A] [QuantumSet B] (x y : A →ₗ[ℂ] B) : (x •ₛ y).real = y.real •ₛ x.real

theorem Psi.schurMul {A : Type u_3} {B : Type u_4} [starAlgebra A] [starAlgebra B] [hA : QuantumSet A] [QuantumSet B] (r₁ r₂ : ℝ) (f g : A →ₗ[ℂ] B) : (QuantumSet.Psi r₁ r₂) (f •ₛ g) = (QuantumSet.Psi r₁ r₂) f * (QuantumSet.Psi r₁ r₂) g

theorem schurMul_assoc {A : Type u_3} {B : Type u_4} [starAlgebra A] [starAlgebra B] [hA : QuantumSet A] [QuantumSet B] (f g h : A →ₗ[ℂ] B) : (f •ₛ g) •ₛ h = f •ₛ g •ₛ h

theorem comul_comp_nonUnitalAlgHom_adjoint {A : Type u_1} {B : Type u_2} [NormedAddCommGroupOfRing A] [NormedAddCommGroupOfRing B] [InnerProductSpace ℂ A] [InnerProductSpace ℂ B] [SMulCommClass ℂ A A] [SMulCommClass ℂ B B] [IsScalarTower ℂ A A] [IsScalarTower ℂ B B] [FiniteDimensional ℂ A] [FiniteDimensional ℂ B] (f : A →ₙₐ[ℂ] B) : CoalgebraStruct.comul ∘ₗ LinearMap.adjoint (LinearMapClass.linearMap f) = TensorProduct.map (LinearMap.adjoint (LinearMapClass.linearMap f)) (LinearMap.adjoint (LinearMapClass.linearMap f)) ∘ₗ CoalgebraStruct.comul

theorem comul_comp_algHom_adjoint {A : Type u_1} {B : Type u_2} [NormedAddCommGroupOfRing A] [NormedAddCommGroupOfRing B] [InnerProductSpace ℂ A] [InnerProductSpace ℂ B] [SMulCommClass ℂ A A] [SMulCommClass ℂ B B] [IsScalarTower ℂ A A] [IsScalarTower ℂ B B] [FiniteDimensional ℂ A] [FiniteDimensional ℂ B] (f : A →ₐ[ℂ] B) : CoalgebraStruct.comul ∘ₗ LinearMap.adjoint f.toLinearMap = TensorProduct.map (LinearMap.adjoint f.toLinearMap) (LinearMap.adjoint f.toLinearMap) ∘ₗ CoalgebraStruct.comul

theorem schurMul_nonUnitalAlgHom_comp_coalgHom {A : Type u_1} {B : Type u_2} [NormedAddCommGroupOfRing A] [NormedAddCommGroupOfRing B] [InnerProductSpace ℂ A] [InnerProductSpace ℂ B] [SMulCommClass ℂ A A] [SMulCommClass ℂ B B] [IsScalarTower ℂ A A] [IsScalarTower ℂ B B] [FiniteDimensional ℂ A] [FiniteDimensional ℂ B] {C : Type u_3} {D : Type u_4} [Semiring C] [Semiring D] [Module ℂ C] [Module ℂ D] [SMulCommClass ℂ C C] [SMulCommClass ℂ D D] [IsScalarTower ℂ C C] [IsScalarTower ℂ D D] (g : C →ₙₐ[ℂ] D) (f : A →ₗc[ℂ] B) (x y : B →ₗ[ℂ] C) : (LinearMapClass.linearMap g ∘ₗ x ∘ₗ f.toLinearMap) •ₛ LinearMapClass.linearMap g ∘ₗ y ∘ₗ f.toLinearMap = LinearMapClass.linearMap g ∘ₗ (x •ₛ y) ∘ₗ f.toLinearMap

theorem schurMul_algHom_comp_coalgHom {A : Type u_1} {B : Type u_2} [NormedAddCommGroupOfRing A] [NormedAddCommGroupOfRing B] [InnerProductSpace ℂ A] [InnerProductSpace ℂ B] [SMulCommClass ℂ A A] [SMulCommClass ℂ B B] [IsScalarTower ℂ A A] [IsScalarTower ℂ B B] [FiniteDimensional ℂ A] [FiniteDimensional ℂ B] {C : Type u_3} {D : Type u_4} [Semiring C] [Semiring D] [Module ℂ C] [Module ℂ D] [SMulCommClass ℂ C C] [SMulCommClass ℂ D D] [IsScalarTower ℂ C C] [IsScalarTower ℂ D D] (g : C →ₐ[ℂ] D) (f : A →ₗc[ℂ] B) (x y : B →ₗ[ℂ] C) : (g.toLinearMap ∘ₗ x ∘ₗ f.toLinearMap) •ₛ g.toLinearMap ∘ₗ y ∘ₗ f.toLinearMap = g.toLinearMap ∘ₗ (x •ₛ y) ∘ₗ f.toLinearMap

theorem schurMul_nonUnitalAlgHom_comp_nonUnitalAlgHom_adjoint {A : Type u_1} {B : Type u_2} [NormedAddCommGroupOfRing A] [NormedAddCommGroupOfRing B] [InnerProductSpace ℂ A] [InnerProductSpace ℂ B] [SMulCommClass ℂ A A] [SMulCommClass ℂ B B] [IsScalarTower ℂ A A] [IsScalarTower ℂ B B] [FiniteDimensional ℂ A] [FiniteDimensional ℂ B] {C : Type u_3} {D : Type u_4} [Semiring C] [Semiring D] [Module ℂ C] [Module ℂ D] [SMulCommClass ℂ C C] [SMulCommClass ℂ D D] [IsScalarTower ℂ C C] [IsScalarTower ℂ D D] (g : C →ₙₐ[ℂ] D) (f : B →ₙₐ[ℂ] A) (x y : B →ₗ[ℂ] C) : (LinearMapClass.linearMap g ∘ₗ x ∘ₗ LinearMap.adjoint (LinearMapClass.linearMap f)) •ₛ LinearMapClass.linearMap g ∘ₗ y ∘ₗ LinearMap.adjoint (LinearMapClass.linearMap f) = LinearMapClass.linearMap g ∘ₗ (x •ₛ y) ∘ₗ LinearMap.adjoint (LinearMapClass.linearMap f)

theorem schurMul_algHom_comp_algHom_adjoint {A : Type u_1} {B : Type u_2} [NormedAddCommGroupOfRing A] [NormedAddCommGroupOfRing B] [InnerProductSpace ℂ A] [InnerProductSpace ℂ B] [SMulCommClass ℂ A A] [SMulCommClass ℂ B B] [IsScalarTower ℂ A A] [IsScalarTower ℂ B B] [FiniteDimensional ℂ A] [FiniteDimensional ℂ B] {C : Type u_3} {D : Type u_4} [Semiring C] [Semiring D] [Module ℂ C] [Module ℂ D] [SMulCommClass ℂ C C] [SMulCommClass ℂ D D] [IsScalarTower ℂ C C] [IsScalarTower ℂ D D] (g : C →ₐ[ℂ] D) (f : B →ₐ[ℂ] A) (x y : B →ₗ[ℂ] C) : (g.toLinearMap ∘ₗ x ∘ₗ LinearMap.adjoint f.toLinearMap) •ₛ g.toLinearMap ∘ₗ y ∘ₗ LinearMap.adjoint f.toLinearMap = g.toLinearMap ∘ₗ (x •ₛ y) ∘ₗ LinearMap.adjoint f.toLinearMap

theorem QuantumSet.schurMul_algHom_comp_algHom_adjoint {A : Type u_3} {B : Type u_4} {C : Type u_5} {D : Type u_6} [starAlgebra A] [starAlgebra B] [QuantumSet A] [QuantumSet B] [starAlgebra C] [starAlgebra D] [QuantumSet C] [QuantumSet D] (g : C →ₐ[ℂ] D) (f : B →ₐ[ℂ] A) (x y : B →ₗ[ℂ] C) : (g.toLinearMap ∘ₗ x ∘ₗ LinearMap.adjoint f.toLinearMap) •ₛ g.toLinearMap ∘ₗ y ∘ₗ LinearMap.adjoint f.toLinearMap = g.toLinearMap ∘ₗ (x •ₛ y) ∘ₗ LinearMap.adjoint f.toLinearMap

theorem schurMul_one_iff_one_schurMul_of_isReal {A : Type u_3} {B : Type u_4} [starAlgebra A] [starAlgebra B] [QuantumSet A] [QuantumSet B] {x y z : A →ₗ[ℂ] B} (hx : LinearMap.IsReal x) (hy : LinearMap.IsReal y) (hz : LinearMap.IsReal z) : x •ₛ y = z ↔ y •ₛ x = z

theorem schurMul_reflexive_of_isReal {A : Type u_3} [starAlgebra A] [QuantumSet A] {x : A →ₗ[ℂ] A} (hx : LinearMap.IsReal x) : x •ₛ 1 = 1 ↔ 1 •ₛ x = 1

theorem schurMul_irreflexive_of_isReal {A : Type u_3} [starAlgebra A] [QuantumSet A] {x : A →ₗ[ℂ] A} (hx : LinearMap.IsReal x) : x •ₛ 1 = 0 ↔ 1 •ₛ x = 0

theorem schurIdempotent_iff_Psi_isIdempotentElem {A : Type u_3} {B : Type u_4} [starAlgebra A] [starAlgebra B] [hA : QuantumSet A] [QuantumSet B] (f : A →ₗ[ℂ] B) (t r : ℝ) : f •ₛ f = f ↔ IsIdempotentElem ((QuantumSet.Psi t r) f)