LeanPool.Monlib4.LinearAlgebra.QuantumSet.QIso

Imported Lean Pool material for LeanPool.Monlib4.LinearAlgebra.QuantumSet.QIso.

@[reducible, inline]

noncomputable abbrev QFun.mapUnit' {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₂) : H →ₗ[ℂ] TensorProduct ℂ H B₂

The unit-preservation expression for a quantum function.

Equations

• QFun.mapUnit' P = P ∘ₗ LinearMap.rTensor H (Algebra.linearMap ℂ B₁) ∘ₗ ↑(TensorProduct.lid ℂ H).symm

@[reducible, inline]

noncomputable abbrev QFun.mapMul' {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₂) : TensorProduct ℂ B₁ (TensorProduct ℂ B₁ H) →ₗ[ℂ] TensorProduct ℂ H B₂

The multiplication-preservation expression for a quantum function.

Equations

• QFun.mapMul' P = LinearMap.lTensor H (LinearMap.mul' ℂ B₂) ∘ₗ ↑(TensorProduct.assoc ℂ H B₂ B₂) ∘ₗ LinearMap.rTensor B₂ P ∘ₗ ↑(TensorProduct.assoc ℂ B₁ H B₂).symm ∘ₗ LinearMap.lTensor B₁ P

@[reducible, inline]

noncomputable abbrev QFun.mapReal' {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₂) : TensorProduct ℂ B₁ H →ₗ[ℂ] TensorProduct ℂ H B₂

The reality condition expression for a quantum function.

Equations

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

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₂) : Prop

A quantum function between quantum sets, encoded as a linear map with unit, multiplication, and reality compatibility.

• map_unit : mapUnit' P = LinearMap.lTensor H (Algebra.linearMap ℂ B₂) ∘ₗ ↑(TensorProduct.rid ℂ H).symm
• map_mul : mapMul' P = P ∘ₗ LinearMap.rTensor H (LinearMap.mul' ℂ B₁) ∘ₗ ↑(TensorProduct.assoc ℂ B₁ B₁ H).symm
• map_real : mapReal' P = P

theorem TensorProduct.rid_symm_adjoint {𝕜 : Type u_3} {E : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] : LinearMap.adjoint ↑(TensorProduct.rid 𝕜 E).symm = ↑(TensorProduct.rid 𝕜 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.mapCounit' {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₂) : TensorProduct ℂ B₁ H →ₗ[ℂ] H

The counit-preservation expression for a quantum function.

Equations

• QFun.mapCounit' P = ↑(TensorProduct.rid ℂ H) ∘ₗ LinearMap.lTensor H CoalgebraStruct.counit ∘ₗ P

@[reducible, inline]

noncomputable abbrev QFun.mapComul' {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₂) : TensorProduct ℂ B₁ H →ₗ[ℂ] TensorProduct ℂ (TensorProduct ℂ H B₂) B₂

The comultiplication-preservation expression for a quantum function.

Equations

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

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) : Prop

A quantum function is quantum-bijective when it also preserves counit and comultiplication.

• map_counit : mapCounit' P = ↑(TensorProduct.lid ℂ H) ∘ₗ LinearMap.rTensor H CoalgebraStruct.counit
• map_comul : mapComul' P = ↑(TensorProduct.assoc ℂ H B₂ B₂).symm ∘ₗ LinearMap.lTensor H CoalgebraStruct.comul ∘ₗ P

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₂) : f ∘ₗ ↑(TensorProduct.rid R M) = ↑(TensorProduct.rid R M₂) ∘ₗ rTensor R f

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 : mapComul' P = ↑(TensorProduct.assoc ℂ H B₂ B₂).symm ∘ₗ LinearMap.lTensor H CoalgebraStruct.comul ∘ₗ P) : P ∘ₗ LinearMap.adjoint P = 1

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 : mapCounit' P = ↑(TensorProduct.lid ℂ H) ∘ₗ LinearMap.rTensor H CoalgebraStruct.counit) : LinearMap.adjoint P ∘ₗ P = 1

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) : mapCounit' P = ↑(TensorProduct.lid ℂ H) ∘ₗ LinearMap.rTensor H CoalgebraStruct.counit

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₂] : lTensor M₁ 1 = 1

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₂] : rTensor M₁ 1 = 1

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) : mapComul' 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) : hp.qBijective ↔ P ∘ₗ LinearMap.adjoint P = 1 ∧ LinearMap.adjoint P ∘ₗ P = 1

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) : TensorProduct ℂ B₁ H ≃ₗ[ℂ] TensorProduct ℂ H B₂

The linear equivalence induced by a quantum-bijective quantum function.

Equations

• h.toLinearEquiv = { toLinearMap := P, invFun := ⇑(LinearMap.adjoint P), left_inv := ⋯, right_inv := ⋯ }

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) : ↑h.toLinearEquiv = P

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) : ↑h.toLinearEquiv.symm = LinearMap.adjoint P

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) : ↑h.toLinearEquiv ∘ₗ LinearMap.rTensor H 1 ∘ₗ ↑h.toLinearEquiv.symm = LinearMap.lTensor H 1

theorem rankOne_one_one_eq {B₁ : Type u_1} {B₂ : Type u_2} [starAlgebra B₁] [starAlgebra B₂] [QuantumSet B₁] [QuantumSet B₂] : ↑(((rankOne ℂ) 1) 1) = Algebra.linearMap ℂ B₁ ∘ₗ CoalgebraStruct.counit

theorem QFun.mapUnit'' {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) : LinearMap.rTensor H CoalgebraStruct.counit ∘ₗ LinearMap.adjoint P = ↑(TensorProduct.comm ℂ ℂ H).symm ∘ₗ LinearMap.lTensor H CoalgebraStruct.counit

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|).