Monlib.LinearAlgebra.QuantumSet.QIso

@[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₂) :

H →ₗ[ℂ ] TensorProduct ℂ H B₂

Equations

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

Instances For

source

@[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₂) :

TensorProduct ℂ B₁ (TensorProduct ℂ B₁ H) →ₗ[ℂ ] TensorProduct ℂ H B₂

Equations

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

Instances For

source

@[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₂) :

TensorProduct ℂ B₁ H →ₗ[ℂ ] TensorProduct ℂ H B₂

Equations

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

Instances For

source

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

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

Instances

source

theorem QFun.map_unit {B₁ : Type u_1} {B₂ : Type u_2} :

∀ {inst : starAlgebra B₁} {inst_1 : starAlgebra B₂} {inst_2 : QuantumSet B₁} {inst_3 : QuantumSet B₂} {H : Type u_3} {inst_4 : NormedAddCommGroup H} {inst_5 : InnerProductSpace ℂ H} {inst_6 : FiniteDimensional ℂ H} {P : TensorProduct ℂ B₁ H →ₗ[ℂ ] TensorProduct ℂ H B₂} [self : QFun H P], QFun.map_unit' P = LinearMap.lTensor H (Algebra.linearMap ℂ B₂) ∘ₗ ↑(TensorProduct.rid ℂ H).symm

source

theorem QFun.map_mul {B₁ : Type u_1} {B₂ : Type u_2} :

∀ {inst : starAlgebra B₁} {inst_1 : starAlgebra B₂} {inst_2 : QuantumSet B₁} {inst_3 : QuantumSet B₂} {H : Type u_3} {inst_4 : NormedAddCommGroup H} {inst_5 : InnerProductSpace ℂ H} {inst_6 : FiniteDimensional ℂ H} {P : TensorProduct ℂ B₁ H →ₗ[ℂ ] TensorProduct ℂ H B₂} [self : QFun H P], QFun.map_mul' P = P ∘ₗ LinearMap.rTensor H (LinearMap.mul' ℂ B₁) ∘ₗ ↑(TensorProduct.assoc ℂ B₁ B₁ H).symm

source

theorem QFun.map_real {B₁ : Type u_1} {B₂ : Type u_2} :

source

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)

source

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) (Coalgebra.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 (Coalgebra.comul ∘ₗ Algebra.linearMap ℂ B₁) ∘ₗ ↑(TensorProduct.lid ℂ H).symm)

source

@[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₂) :

TensorProduct ℂ B₁ H →ₗ[ℂ ] H

Equations

QFun.map_counit' P = ↑(TensorProduct.rid ℂ H) ∘ₗ LinearMap.lTensor H Coalgebra.counit ∘ₗ P

Instances For

source

@[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₂) :

TensorProduct ℂ B₁ H →ₗ[ℂ ] TensorProduct ℂ (TensorProduct ℂ H B₂) B₂

Equations

QFun.map_comul' P = LinearMap.rTensor B₂ P ∘ₗ ↑(TensorProduct.assoc ℂ B₁ H B₂).symm ∘ₗ LinearMap.lTensor B₁ P ∘ₗ ↑(TensorProduct.assoc ℂ B₁ B₁ H) ∘ₗ LinearMap.rTensor H Coalgebra.comul

Instances For

source

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

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

Instances

source

theorem QFun.qBijective.map_counit {B₁ : Type u_1} {B₂ : Type u_2} :

∀ {inst : starAlgebra B₁} {inst_1 : starAlgebra B₂} {inst_2 : QuantumSet B₁} {inst_3 : QuantumSet B₂} {H : Type u_3} {inst_4 : NormedAddCommGroup H} {inst_5 : InnerProductSpace ℂ H} {inst_6 : FiniteDimensional ℂ H} {P : TensorProduct ℂ B₁ H →ₗ[ℂ ] TensorProduct ℂ H B₂} (hp : QFun H P) [self : hp.qBijective], QFun.map_counit' P = ↑(TensorProduct.lid ℂ H) ∘ₗ LinearMap.rTensor H Coalgebra.counit

source

theorem QFun.qBijective.map_comul {B₁ : Type u_1} {B₂ : Type u_2} :

∀ {inst : starAlgebra B₁} {inst_1 : starAlgebra B₂} {inst_2 : QuantumSet B₁} {inst_3 : QuantumSet B₂} {H : Type u_3} {inst_4 : NormedAddCommGroup H} {inst_5 : InnerProductSpace ℂ H} {inst_6 : FiniteDimensional ℂ H} {P : TensorProduct ℂ B₁ H →ₗ[ℂ ] TensorProduct ℂ H B₂} (hp : QFun H P) [self : hp.qBijective], QFun.map_comul' P = ↑(TensorProduct.assoc ℂ H B₂ B₂).symm ∘ₗ LinearMap.lTensor H Coalgebra.comul ∘ₗ P

source

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₂) ∘ₗ LinearMap.rTensor R f

source

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

LinearMap.rTensor M₄ ↑(TensorProduct.lid R M₃).symm ∘ₗ f = ↑(TensorProduct.assoc R R M₃ M₄).symm ∘ₗ LinearMap.lTensor R f ∘ₗ ↑(TensorProduct.lid R (TensorProduct R M₁ M₂)).symm

source

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

LinearMap.rTensor (TensorProduct R B C) x = ↑(TensorProduct.assoc R D B C) ∘ₗ LinearMap.rTensor C (LinearMap.rTensor B x) ∘ₗ ↑(TensorProduct.assoc R A B C).symm

source

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

LinearMap.rTensor C (LinearMap.rTensor B x) = ↑(TensorProduct.assoc R D B C).symm ∘ₗ LinearMap.rTensor (TensorProduct R B C) x ∘ₗ ↑(TensorProduct.assoc R A B C)

source

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

source

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] :

LinearMap.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 ∘ₗ LinearMap.lTensor A ↑(TensorProduct.assoc R B C D)

source

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)

source

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 (Coalgebra.counit ∘ₗ LinearMap.mul' R A) ∘ₗ ↑(TensorProduct.assoc R A A A) ∘ₗ LinearMap.rTensor A (Coalgebra.comul ∘ₗ Algebra.linearMap R A) ∘ₗ ↑(TensorProduct.lid R A).symm = 1

source

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

P ∘ₗ LinearMap.adjoint P = 1

source

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

LinearMap.adjoint P ∘ₗ P = 1

source

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

QFun.map_counit' P = ↑(TensorProduct.lid ℂ H) ∘ₗ LinearMap.rTensor H Coalgebra.counit

source

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₂] :

LinearMap.lTensor M₁ 1 = 1

source

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₂] :

LinearMap.rTensor M₁ 1 = 1

source

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

QFun.map_comul' P = ↑(TensorProduct.assoc ℂ H B₂ B₂).symm ∘ₗ LinearMap.lTensor H Coalgebra.comul ∘ₗ P

source

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

source

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₂

Equations

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

Instances For

source

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

source

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

source

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

source

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₁ ∘ₗ Coalgebra.counit

source

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)

source

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 Coalgebra.counit ∘ₗ LinearMap.adjoint P = ↑(TensorProduct.comm ℂ ℂ H).symm ∘ₗ LinearMap.lTensor H Coalgebra.counit

source

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