@[reducible, inline]
noncomputable abbrev
QFun.map_unit'
{B₁ : Type u_1}
{B₂ : Type u_2}
[starAlgebra B₁]
[starAlgebra B₂]
[QuantumSet B₁]
[QuantumSet B₂]
{H : Type u_3}
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
[FiniteDimensional ℂ H]
(P : TensorProduct ℂ B₁ H →ₗ[ℂ] TensorProduct ℂ H B₂)
:
Equations
- QFun.map_unit' P = P ∘ₗ LinearMap.rTensor H (Algebra.linearMap ℂ B₁) ∘ₗ ↑(TensorProduct.lid ℂ H).symm
Instances For
@[reducible, inline]
noncomputable abbrev
QFun.map_mul'
{B₁ : Type u_1}
{B₂ : Type u_2}
[starAlgebra B₁]
[starAlgebra B₂]
[QuantumSet B₁]
[QuantumSet B₂]
{H : Type u_3}
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
[FiniteDimensional ℂ H]
(P : TensorProduct ℂ B₁ H →ₗ[ℂ] TensorProduct ℂ H B₂)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
noncomputable abbrev
QFun.map_real'
{B₁ : Type u_1}
{B₂ : Type u_2}
[starAlgebra B₁]
[starAlgebra B₂]
[QuantumSet B₁]
[QuantumSet B₂]
{H : Type u_3}
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
[FiniteDimensional ℂ H]
(P : TensorProduct ℂ B₁ H →ₗ[ℂ] TensorProduct ℂ H B₂)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
class
QFun
{B₁ : Type u_1}
{B₂ : Type u_2}
[starAlgebra B₁]
[starAlgebra B₂]
[QuantumSet B₁]
[QuantumSet B₂]
(H : Type u_3)
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
[FiniteDimensional ℂ H]
(P : TensorProduct ℂ B₁ H →ₗ[ℂ] TensorProduct ℂ H B₂)
:
- map_unit : map_unit' P = LinearMap.lTensor H (Algebra.linearMap ℂ B₂) ∘ₗ ↑(TensorProduct.rid ℂ H).symm
- map_mul : map_mul' P = P ∘ₗ LinearMap.rTensor H (LinearMap.mul' ℂ B₁) ∘ₗ ↑(TensorProduct.assoc ℂ B₁ B₁ H).symm
Instances
theorem
TensorProduct.rid_symm_adjoint
{𝕜 : Type u_3}
{E : Type u_4}
[RCLike 𝕜]
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
[FiniteDimensional 𝕜 E]
:
theorem
QFun.adjoint_eq
{B₁ : Type u_1}
{B₂ : Type u_2}
[starAlgebra B₁]
[starAlgebra B₂]
[QuantumSet B₁]
[QuantumSet B₂]
{H : Type u_3}
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
[FiniteDimensional ℂ H]
{P : TensorProduct ℂ B₁ H →ₗ[ℂ] TensorProduct ℂ H B₂}
(hp : QFun H P)
:
LinearMap.adjoint P = ↑(TensorProduct.rid ℂ (TensorProduct ℂ B₁ H)) ∘ₗ LinearMap.lTensor (TensorProduct ℂ B₁ H) (CoalgebraStruct.counit ∘ₗ LinearMap.mul' ℂ B₂) ∘ₗ ↑(TensorProduct.assoc ℂ B₁ H (TensorProduct ℂ B₂ B₂)).symm ∘ₗ LinearMap.lTensor B₁ (↑(TensorProduct.assoc ℂ H B₂ B₂) ∘ₗ LinearMap.rTensor B₂ P) ∘ₗ ↑(TensorProduct.assoc ℂ B₁ (TensorProduct ℂ B₁ H) B₂) ∘ₗ LinearMap.rTensor B₂
(↑(TensorProduct.assoc ℂ B₁ B₁ H) ∘ₗ LinearMap.rTensor H (CoalgebraStruct.comul ∘ₗ Algebra.linearMap ℂ B₁) ∘ₗ ↑(TensorProduct.lid ℂ H).symm)
@[reducible, inline]
noncomputable abbrev
QFun.map_counit'
{B₁ : Type u_1}
{B₂ : Type u_2}
[starAlgebra B₁]
[starAlgebra B₂]
[QuantumSet B₁]
[QuantumSet B₂]
{H : Type u_3}
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
(P : TensorProduct ℂ B₁ H →ₗ[ℂ] TensorProduct ℂ H B₂)
:
Equations
Instances For
@[reducible, inline]
noncomputable abbrev
QFun.map_comul'
{B₁ : Type u_1}
{B₂ : Type u_2}
[starAlgebra B₁]
[starAlgebra B₂]
[QuantumSet B₁]
[QuantumSet B₂]
{H : Type u_3}
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
(P : TensorProduct ℂ B₁ H →ₗ[ℂ] TensorProduct ℂ H B₂)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
class
QFun.qBijective
{B₁ : Type u_1}
{B₂ : Type u_2}
[starAlgebra B₁]
[starAlgebra B₂]
[QuantumSet B₁]
[QuantumSet B₂]
{H : Type u_3}
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
[FiniteDimensional ℂ H]
{P : TensorProduct ℂ B₁ H →ₗ[ℂ] TensorProduct ℂ H B₂}
(hp : QFun H P)
:
- map_comul : map_comul' P = ↑(TensorProduct.assoc ℂ H B₂ B₂).symm ∘ₗ LinearMap.lTensor H CoalgebraStruct.comul ∘ₗ P
Instances
theorem
LinearMap.comp_rid_eq_rid_comp_rTensor
{R : Type u_4}
[CommSemiring R]
{M : Type u_5}
{M₂ : Type u_6}
[AddCommMonoid M]
[Module R M]
[AddCommMonoid M₂]
[Module R M₂]
(f : M →ₗ[R] M₂)
:
theorem
LinearMap.rTensor_lid_symm_comp_eq_assoc_symm_comp_lTensor_comp_lid_symm
{R : Type u_4}
[CommSemiring R]
{M₁ : Type u_5}
{M₂ : Type u_6}
{M₃ : Type u_7}
{M₄ : Type u_8}
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[AddCommMonoid M₃]
[AddCommMonoid M₄]
[Module R M₁]
[Module R M₂]
[Module R M₃]
[Module R M₄]
(f : TensorProduct R M₁ M₂ →ₗ[R] TensorProduct R M₃ M₄)
:
rTensor M₄ ↑(TensorProduct.lid R M₃).symm ∘ₗ f = ↑(TensorProduct.assoc R R M₃ M₄).symm ∘ₗ lTensor R f ∘ₗ ↑(TensorProduct.lid R (TensorProduct R M₁ M₂)).symm
theorem
LinearMap.rTensor_tensor_eq_assoc_comp_rTensor_rTensor_comp_assoc_symm
{R : Type u_4}
[CommSemiring R]
{A : Type u_5}
{B : Type u_6}
{C : Type u_7}
{D : Type u_8}
[AddCommMonoid A]
[AddCommMonoid B]
[AddCommMonoid C]
[AddCommMonoid D]
[Module R A]
[Module R B]
[Module R C]
[Module R D]
(x : A →ₗ[R] D)
:
rTensor (TensorProduct R B C) x = ↑(TensorProduct.assoc R D B C) ∘ₗ rTensor C (rTensor B x) ∘ₗ ↑(TensorProduct.assoc R A B C).symm
theorem
LinearMap.rTensor_rTensor_eq_assoc_symm_comp_rTensor_comp_assoc
{R : Type u_4}
[CommSemiring R]
{A : Type u_5}
{B : Type u_6}
{C : Type u_7}
{D : Type u_8}
[AddCommMonoid A]
[AddCommMonoid B]
[AddCommMonoid C]
[AddCommMonoid D]
[Module R A]
[Module R B]
[Module R C]
[Module R D]
(x : A →ₗ[R] D)
:
rTensor C (rTensor B x) = ↑(TensorProduct.assoc R D B C).symm ∘ₗ rTensor (TensorProduct R B C) x ∘ₗ ↑(TensorProduct.assoc R A B C)
theorem
TensorProduct.lTensor_lTensor_comp_assoc
{R : Type u_4}
[CommSemiring R]
{A : Type u_5}
{B : Type u_6}
{C : Type u_7}
{D : Type u_8}
[AddCommMonoid A]
[AddCommMonoid B]
[AddCommMonoid C]
[AddCommMonoid D]
[Module R A]
[Module R B]
[Module R C]
[Module R D]
(x : A →ₗ[R] D)
:
LinearMap.lTensor B (LinearMap.lTensor C x) ∘ₗ ↑(TensorProduct.assoc R B C A) = ↑(TensorProduct.assoc R B C D) ∘ₗ LinearMap.lTensor (TensorProduct R B C) x
theorem
LinearMap.rTensor_assoc_symm_comp_assoc_symm
{R : Type u_4}
[CommSemiring R]
{A : Type u_5}
{B : Type u_6}
{C : Type u_7}
{D : Type u_8}
[AddCommMonoid A]
[AddCommMonoid B]
[AddCommMonoid C]
[AddCommMonoid D]
[Module R A]
[Module R B]
[Module R C]
[Module R D]
:
rTensor D ↑(TensorProduct.assoc R A B C).symm ∘ₗ ↑(TensorProduct.assoc R A (TensorProduct R B C) D).symm = ↑(TensorProduct.assoc R (TensorProduct R A B) C D).symm ∘ₗ ↑(TensorProduct.assoc R A B (TensorProduct R C D)).symm ∘ₗ lTensor A ↑(TensorProduct.assoc R B C D)
theorem
rid_tensor
{R : Type u_4}
[CommSemiring R]
{A : Type u_5}
{B : Type u_6}
[AddCommMonoid A]
[Module R A]
[AddCommMonoid B]
[Module R B]
:
↑(TensorProduct.rid R (TensorProduct R A B)) = LinearMap.lTensor A ↑(TensorProduct.rid R B) ∘ₗ ↑(TensorProduct.assoc R A B R)
theorem
FrobeniusAlgebra.snake_equation_2
{R : Type u_4}
[CommSemiring R]
{A : Type u_5}
[Semiring A]
[FrobeniusAlgebra R A]
:
↑(TensorProduct.rid R A) ∘ₗ LinearMap.lTensor A (CoalgebraStruct.counit ∘ₗ LinearMap.mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A) ∘ₗ LinearMap.rTensor A (CoalgebraStruct.comul ∘ₗ Algebra.linearMap R A) ∘ₗ ↑(TensorProduct.lid R A).symm = 1
theorem
QFun.self_comp_adjoint_eq_id_of_map_comul
{B₁ : Type u_1}
{B₂ : Type u_2}
[starAlgebra B₁]
[starAlgebra B₂]
[QuantumSet B₁]
[QuantumSet B₂]
{H : Type u_3}
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
[FiniteDimensional ℂ H]
{P : TensorProduct ℂ B₁ H →ₗ[ℂ] TensorProduct ℂ H B₂}
(hp : QFun H P)
(h : map_comul' P = ↑(TensorProduct.assoc ℂ H B₂ B₂).symm ∘ₗ LinearMap.lTensor H CoalgebraStruct.comul ∘ₗ P)
:
theorem
QFun.adjoint_comp_self_eq_id_of_map_counit
{B₁ : Type u_1}
{B₂ : Type u_2}
[starAlgebra B₁]
[starAlgebra B₂]
[QuantumSet B₁]
[QuantumSet B₂]
{H : Type u_3}
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
[FiniteDimensional ℂ H]
{P : TensorProduct ℂ B₁ H →ₗ[ℂ] TensorProduct ℂ H B₂}
(hp : QFun H P)
(h : map_counit' P = ↑(TensorProduct.lid ℂ H) ∘ₗ LinearMap.rTensor H CoalgebraStruct.counit)
:
theorem
QFun.map_counit_of_adjoint_comp_self_eq_id
{B₁ : Type u_1}
{B₂ : Type u_2}
[starAlgebra B₁]
[starAlgebra B₂]
[QuantumSet B₁]
[QuantumSet B₂]
{H : Type u_3}
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
[FiniteDimensional ℂ H]
{P : TensorProduct ℂ B₁ H →ₗ[ℂ] TensorProduct ℂ H B₂}
(hp : QFun H P)
(h : LinearMap.adjoint P ∘ₗ P = 1)
:
theorem
LinearMap.lTensor_one
{R : Type u_4}
{M₁ : Type u_5}
{M₂ : Type u_6}
[CommSemiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[Module R M₁]
[Module R M₂]
:
theorem
LinearMap.rTensor_one
{R : Type u_4}
{M₁ : Type u_5}
{M₂ : Type u_6}
[CommSemiring R]
[AddCommMonoid M₁]
[AddCommMonoid M₂]
[Module R M₁]
[Module R M₂]
:
theorem
QFun.map_comul_of_inv_eq_adjoint
{B₁ : Type u_1}
{B₂ : Type u_2}
[starAlgebra B₁]
[starAlgebra B₂]
[QuantumSet B₁]
[QuantumSet B₂]
{H : Type u_3}
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
[FiniteDimensional ℂ H]
{P : TensorProduct ℂ B₁ H →ₗ[ℂ] TensorProduct ℂ H B₂}
(hp : QFun H P)
(h₁ : P ∘ₗ LinearMap.adjoint P = 1)
(h₂ : LinearMap.adjoint P ∘ₗ P = 1)
:
map_comul' P = ↑(TensorProduct.assoc ℂ H B₂ B₂).symm ∘ₗ LinearMap.lTensor H CoalgebraStruct.comul ∘ₗ P
theorem
QFun.qBijective_iff_inv_eq_adjoint
{B₁ : Type u_1}
{B₂ : Type u_2}
[starAlgebra B₁]
[starAlgebra B₂]
[QuantumSet B₁]
[QuantumSet B₂]
{H : Type u_3}
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
[FiniteDimensional ℂ H]
{P : TensorProduct ℂ B₁ H →ₗ[ℂ] TensorProduct ℂ H B₂}
(hp : QFun H P)
:
noncomputable def
QFun.qBijective.toLinearEquiv
{B₁ : Type u_1}
{B₂ : Type u_2}
[starAlgebra B₁]
[starAlgebra B₂]
[QuantumSet B₁]
[QuantumSet B₂]
{H : Type u_3}
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
[FiniteDimensional ℂ H]
{P : TensorProduct ℂ B₁ H →ₗ[ℂ] TensorProduct ℂ H B₂}
[hp : QFun H P]
(h : hp.qBijective)
:
Equations
- h.toLinearEquiv = { toLinearMap := P, invFun := ⇑(LinearMap.adjoint P), left_inv := ⋯, right_inv := ⋯ }
Instances For
theorem
QFun.qBijective.toLinearEquiv_toLinearMap
{B₁ : Type u_1}
{B₂ : Type u_2}
[starAlgebra B₁]
[starAlgebra B₂]
[QuantumSet B₁]
[QuantumSet B₂]
{H : Type u_3}
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
[FiniteDimensional ℂ H]
{P : TensorProduct ℂ B₁ H →ₗ[ℂ] TensorProduct ℂ H B₂}
[hp : QFun H P]
(h : hp.qBijective)
:
theorem
QFun.qBijective.toLinearEquiv_symm_toLinearMap
{B₁ : Type u_1}
{B₂ : Type u_2}
[starAlgebra B₁]
[starAlgebra B₂]
[QuantumSet B₁]
[QuantumSet B₂]
{H : Type u_3}
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
[FiniteDimensional ℂ H]
{P : TensorProduct ℂ B₁ H →ₗ[ℂ] TensorProduct ℂ H B₂}
[hp : QFun H P]
(h : hp.qBijective)
:
theorem
QFun.qBijective_iso_id
{B₁ : Type u_1}
{B₂ : Type u_2}
[starAlgebra B₁]
[starAlgebra B₂]
[QuantumSet B₁]
[QuantumSet B₂]
{H : Type u_3}
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
[FiniteDimensional ℂ H]
{P : TensorProduct ℂ B₁ H →ₗ[ℂ] TensorProduct ℂ H B₂}
[hp : QFun H P]
(h : hp.qBijective)
:
theorem
rankOne_one_one_eq
{B₁ : Type u_1}
{B₂ : Type u_2}
[starAlgebra B₁]
[starAlgebra B₂]
[QuantumSet B₁]
[QuantumSet B₂]
:
theorem
QFun.map_unit''
{B₁ : Type u_1}
{B₂ : Type u_2}
[starAlgebra B₁]
[starAlgebra B₂]
[QuantumSet B₁]
[QuantumSet B₂]
{H : Type u_3}
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
[FiniteDimensional ℂ H]
{P : TensorProduct ℂ B₁ H →ₗ[ℂ] TensorProduct ℂ H B₂}
(hp : QFun H P)
:
P ∘ₗ LinearMap.rTensor H (Algebra.linearMap ℂ B₁) = LinearMap.lTensor H (Algebra.linearMap ℂ B₂) ∘ₗ ↑(TensorProduct.comm ℂ ℂ H)
theorem
QFun.counit_map_adjoint
{B₁ : Type u_1}
{B₂ : Type u_2}
[starAlgebra B₁]
[starAlgebra B₂]
[QuantumSet B₁]
[QuantumSet B₂]
{H : Type u_3}
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
[FiniteDimensional ℂ H]
{P : TensorProduct ℂ B₁ H →ₗ[ℂ] TensorProduct ℂ H B₂}
(hp : QFun H P)
:
theorem
QFun.qBijective_iso_rankOne_one_one
{B₁ : Type u_1}
{B₂ : Type u_2}
[starAlgebra B₁]
[starAlgebra B₂]
[QuantumSet B₁]
[QuantumSet B₂]
{H : Type u_3}
[NormedAddCommGroup H]
[InnerProductSpace ℂ H]
[FiniteDimensional ℂ H]
{P : TensorProduct ℂ B₁ H →ₗ[ℂ] TensorProduct ℂ H B₂}
[hp : QFun H P]
(h : hp.qBijective)
:
↑h.toLinearEquiv ∘ₗ LinearMap.rTensor H ↑(((rankOne ℂ) 1) 1) ∘ₗ ↑h.toLinearEquiv.symm = LinearMap.lTensor H ↑(((rankOne ℂ) 1) 1)
for any qBijective function P,
we get P ∘ (|1⟩⟨1| ⊗ id) ∘ adjoint P = (id ⊗ |1⟩⟨1|).