noncomputable def symmMap (R : Type u_1) [RCLike R] (M₁ : Type u_2) (M₂ : Type u_3) [NormedAddCommGroup M₁] [NormedAddCommGroup M₂] [InnerProductSpace R M₁] [InnerProductSpace R M₂] [StarAddMonoid M₁] [StarAddMonoid M₂] [StarModule R M₁] [StarModule R M₂] [FiniteDimensional R M₁] [FiniteDimensional R M₂] : (M₁ →ₗ[R] M₂) ≃ₗ[R] M₂ →ₗ[R] M₁

Equations

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

@[simp]

theorem symmMap_apply (R : Type u_1) [RCLike R] (M₁ : Type u_2) (M₂ : Type u_3) [NormedAddCommGroup M₁] [NormedAddCommGroup M₂] [InnerProductSpace R M₁] [InnerProductSpace R M₂] [StarAddMonoid M₁] [StarAddMonoid M₂] [StarModule R M₁] [StarModule R M₂] [FiniteDimensional R M₁] [FiniteDimensional R M₂] (f : M₁ →ₗ[R] M₂) : (symmMap R M₁ M₂) f = LinearMap.adjoint f.real

@[simp]

theorem symmMap_symm_apply (R : Type u_1) [RCLike R] (M₁ : Type u_2) (M₂ : Type u_3) [NormedAddCommGroup M₁] [NormedAddCommGroup M₂] [InnerProductSpace R M₁] [InnerProductSpace R M₂] [StarAddMonoid M₁] [StarAddMonoid M₂] [StarModule R M₁] [StarModule R M₂] [FiniteDimensional R M₁] [FiniteDimensional R M₂] (f : M₂ →ₗ[R] M₁) : (symmMap R M₁ M₂).symm f = (LinearMap.adjoint f).real

theorem symmMap_real {R : Type u_1} [RCLike R] {M : Type u_2} [NormedAddCommGroup M] [InnerProductSpace R M] [StarAddMonoid M] [StarModule R M] [FiniteDimensional R M] : (↑(symmMap R M M)).real = ↑(symmMap R M M).symm

theorem symmMap_rankOne_apply {A : Type u_1} {B : Type u_2} [ha : starAlgebra A] [hb : starAlgebra B] [hA : QuantumSet A] [hB : QuantumSet B] (a : A) (b : B) : (symmMap ℂ B A) ↑(((rankOne ℂ) a) b) = ↑(((rankOne ℂ) ((modAut (-(2 * k B) - 1)) (star b))) (star a))

theorem symmMap_symm_rankOne_apply {A : Type u_1} {B : Type u_2} [ha : starAlgebra A] [hb : starAlgebra B] [hA : QuantumSet A] [hB : QuantumSet B] (a : A) (b : B) : (symmMap ℂ A B).symm ↑(((rankOne ℂ) a) b) = ↑(((rankOne ℂ) (star b)) ((modAut (-(2 * k A) - 1)) (star a)))

theorem symmMap_eq {A : Type u_1} {B : Type u_2} [ha : starAlgebra A] [hb : starAlgebra B] [hA : QuantumSet A] [hB : QuantumSet B] (f : A →ₗ[ℂ] B) : (symmMap ℂ A B) f = (modAut (-k A)).toLinearMap ∘ₗ ↑(TensorProduct.rid ℂ A) ∘ₗ LinearMap.lTensor A (Coalgebra.counit ∘ₗ LinearMap.mul' ℂ B) ∘ₗ ↑(TensorProduct.assoc ℂ A B B) ∘ₗ LinearMap.rTensor B (LinearMap.lTensor A f) ∘ₗ LinearMap.rTensor B (Coalgebra.comul ∘ₗ Algebra.linearMap ℂ A) ∘ₗ ↑(TensorProduct.lid ℂ B).symm ∘ₗ (modAut (k B)).toLinearMap

theorem symmMap_symm_eq {A : Type u_1} {B : Type u_2} [ha : starAlgebra A] [hb : starAlgebra B] [hA : QuantumSet A] [hB : QuantumSet B] (f : A →ₗ[ℂ] B) : (symmMap ℂ B A).symm f = (modAut (k A)).toLinearMap ∘ₗ ↑(TensorProduct.lid ℂ A) ∘ₗ LinearMap.rTensor A (Coalgebra.counit ∘ₗ LinearMap.mul' ℂ B) ∘ₗ LinearMap.rTensor A (LinearMap.lTensor B f) ∘ₗ ↑(TensorProduct.assoc ℂ B A A).symm ∘ₗ LinearMap.lTensor B (Coalgebra.comul ∘ₗ Algebra.linearMap ℂ A) ∘ₗ ↑(TensorProduct.rid ℂ B).symm ∘ₗ (modAut (-k B)).toLinearMap

theorem counit_map_mul_eq_counit_mul_modAut_conj_symmMap {A : Type u_1} {B : Type u_2} [ha : starAlgebra A] [hb : starAlgebra B] [hA : QuantumSet A] [hB : QuantumSet B] (f : A →ₗ[ℂ] B) (x : A) (y : B) : Coalgebra.counit (f x * y) = Coalgebra.counit (x * (modAut (k A)) (((symmMap ℂ A B) f) ((modAut (-k B)) y)))

theorem LinearMap.adjoint_eq_iff {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F) (B : F →ₗ[𝕜] E) : LinearMap.adjoint A = B ↔ A = LinearMap.adjoint B

theorem symmMap_eq_conj_modAut_tfae {B : Type u_2} [hb : starAlgebra B] [hB : QuantumSet B] (f : B →ₗ[ℂ] B) : [(symmMap ℂ B B) f = (modAut (-k B)).toLinearMap ∘ₗ f ∘ₗ (modAut (k B)).toLinearMap, f.real = (modAut (k B)).toLinearMap ∘ₗ LinearMap.adjoint f ∘ₗ (modAut (-k B)).toLinearMap, ∀ (x y : B), Coalgebra.counit (f x * y) = Coalgebra.counit (x * f y)].TFAE

theorem symmMap_eq_self_tfae {B : Type u_2} [hb : starAlgebra B] [hB : QuantumSet B] (f : B →ₗ[ℂ] B) (gns : k B = 0) : [(symmMap ℂ B B) f = f, (symmMap ℂ B B).symm f = f, f.real = LinearMap.adjoint f, ∀ (x y : B), Coalgebra.counit (f x * y) = Coalgebra.counit (x * f y)].TFAE

theorem commute_real_real {R : Type u_3} {A : Type u_4} [Semiring R] [StarRing R] [AddCommMonoid A] [Module R A] [StarAddMonoid A] [StarModule R A] (f : A →ₗ[R] A) (g : A →ₗ[R] A) : Commute f.real g.real ↔ Commute f g

theorem linearMap_commute_modAut_pos_neg {B : Type u_2} [hb : starAlgebra B] [hB : QuantumSet B] (r : ℝ) (x : B →ₗ[ℂ] B) : Commute x (modAut r).toLinearMap ↔ Commute x (modAut (-r)).toLinearMap

theorem symmMap_apply_eq_symmMap_symm_apply_iff {A : Type u_1} {B : Type u_2} [ha : starAlgebra A] [hb : starAlgebra B] [hA : QuantumSet A] [hB : QuantumSet B] (f : A →ₗ[ℂ] B) : (symmMap ℂ A B) f = (symmMap ℂ B A).symm f ↔ f ∘ₗ (modAut (2 * k A + 1)).toLinearMap = (modAut (2 * k B + 1)).toLinearMap ∘ₗ f

theorem Psi.real_apply {A : Type u_1} {B : Type u_2} [ha : starAlgebra A] [hb : starAlgebra B] [hA : QuantumSet A] [hB : QuantumSet B] (r₁ : ℝ) (r₂ : ℝ) (f : A →ₗ[ℂ] B) : (QuantumSet.Psi r₁ r₂) f.real = (TensorProduct.map (modAut (2 * r₁)).toLinearMap (AlgEquiv.op (modAut (1 - 2 * (r₂ - k A)))).toLinearMap) (star ((QuantumSet.Psi r₁ r₂) f))

theorem Psi.adjoint_apply {A : Type u_1} {B : Type u_2} [ha : starAlgebra A] [hb : starAlgebra B] [hA : QuantumSet A] [hB : QuantumSet B] (r₁ : ℝ) (r₂ : ℝ) (f : A →ₗ[ℂ] B) : (QuantumSet.Psi r₁ r₂) (LinearMap.adjoint f) = (TensorProduct.map (modAut (r₁ - r₂)).toLinearMap (AlgEquiv.op (modAut (r₁ - r₂))).toLinearMap) ((tenSwap ℂ) (star ((QuantumSet.Psi r₁ r₂) f)))

theorem Psi.symmMap_apply {A : Type u_1} {B : Type u_2} [ha : starAlgebra A] [hb : starAlgebra B] [hA : QuantumSet A] [hB : QuantumSet B] (r₁ : ℝ) (r₂ : ℝ) (f : A →ₗ[ℂ] B) : (QuantumSet.Psi r₁ r₂) ((symmMap ℂ A B) f) = (TensorProduct.map (modAut (r₁ + r₂ - 1 - 2 * k A)).toLinearMap (AlgEquiv.op (modAut (-r₁ - r₂))).toLinearMap) ((tenSwap ℂ) ((QuantumSet.Psi r₁ r₂) f))

theorem Psi.symmMap_symm_apply {A : Type u_1} {B : Type u_2} [ha : starAlgebra A] [hb : starAlgebra B] [hA : QuantumSet A] [hB : QuantumSet B] (r₁ : ℝ) (r₂ : ℝ) (f : A →ₗ[ℂ] B) : (QuantumSet.Psi r₁ r₂) ((symmMap ℂ B A).symm f) = (TensorProduct.map (modAut (r₁ + r₂)).toLinearMap (AlgEquiv.op (modAut (1 - r₁ - r₂ + 2 * k B))).toLinearMap) ((tenSwap ℂ) ((QuantumSet.Psi r₁ r₂) f))

theorem symmMap_apply_adjoint {A : Type u_1} {B : Type u_2} [ha : starAlgebra A] [hb : starAlgebra B] [hA : QuantumSet A] [hB : QuantumSet B] (x : A →ₗ[ℂ] B) : LinearMap.adjoint ((symmMap ℂ A B) x) = (symmMap ℂ A B).symm (LinearMap.adjoint x)

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