def QuantumSet.toSubset (_k : ℝ) (A : Type u_1) : Type u_1

Equations

• QuantumSet.toSubset _k A = A

def QuantumSet.toSubset_equiv (k : ℝ) {A : Type u_1} : A ≃ QuantumSet.toSubset k A

Equations

• QuantumSet.toSubset_equiv k = Equiv.refl A

@[reducible, inline]

abbrev QuantumSet.subset (k : ℝ) (A : Type u_1) : Type u_1

Equations

• QuantumSet.subset k A = QuantumSet.toSubset k A

instance instCoeFunSubset (k : ℝ) (A : Type u_1) : CoeFun (QuantumSet.subset k A) fun (x : QuantumSet.subset k A) => A

Equations

• instCoeFunSubset k A = { coe := ⇑(QuantumSet.toSubset_equiv k) }

instance instInhabitedSubset {new_k : ℝ} (A : Type u_1) [h : Inhabited A] : Inhabited (QuantumSet.subset new_k A)

Equations

• instInhabitedSubset A = h

instance instRingSubset {new_k : ℝ} {A : Type u_1} [h : Ring A] : Ring (QuantumSet.subset new_k A)

Equations

• instRingSubset = h

instance instAlgebraComplexSubset {new_k : ℝ} {A : Type u_1} [Ring A] [h : Algebra ℂ A] : Algebra ℂ (QuantumSet.subset new_k A)

Equations

• instAlgebraComplexSubset = h

instance instStarSubset {new_k : ℝ} {A : Type u_1} [h : Star A] : Star (QuantumSet.subset new_k A)

Equations

• instStarSubset = h

instance instSMulComplexSubset {new_k : ℝ} {A : Type u_1} [h : SMul ℂ A] : SMul ℂ (QuantumSet.subset new_k A)

Equations

• instSMulComplexSubset = h

instance instStarRingSubset {new_k : ℝ} {A : Type u_1} [Ring A] [h : StarRing A] : StarRing (QuantumSet.subset new_k A)

Equations

• instStarRingSubset = h

instance instStarModuleComplexSubset {new_k : ℝ} {A : Type u_1} [Star A] [SMul ℂ A] [h : StarModule ℂ A] : StarModule ℂ (QuantumSet.subset new_k A)

Equations

• ⋯ = h

def QuantumSet.toSubset_algEquiv (k : ℝ) {A : Type u_1} [Ring A] [Algebra ℂ A] : A ≃ₐ[ℂ] QuantumSet.subset k A

Equations

• QuantumSet.toSubset_algEquiv k = AlgEquiv.refl

theorem QuantumSet.toSubset_algEquiv_eq_toSubset_equiv {new_k : ℝ} {A : Type u_1} [Ring A] [Algebra ℂ A] (x : A) : (QuantumSet.toSubset_algEquiv new_k) x = (QuantumSet.toSubset_equiv new_k) x

theorem QuantumSet.toSubset_algEquiv_symm_eq_toSubset_equiv {new_k : ℝ} {A : Type u_1} [Ring A] [Algebra ℂ A] (x : QuantumSet.subset new_k A) : (QuantumSet.toSubset_algEquiv new_k).symm x = (QuantumSet.toSubset_equiv new_k).symm x

instance QuantumSet.subsetStarAlgebra {A : Type u_1} [ha : starAlgebra A] (k : ℝ) : starAlgebra (QuantumSet.subset k A)

Equations

• QuantumSet.subsetStarAlgebra k = starAlgebra.mk (fun (r : ℝ) => (QuantumSet.toSubset_algEquiv k).symm.trans ((modAut r).trans (QuantumSet.toSubset_algEquiv k))) ⋯ ⋯

theorem QuantumSet.subsetStarAlgebra_modAut_apply {new_k : ℝ} {A : Type u_1} [ha : starAlgebra A] (r : ℝ) (x : QuantumSet.subset new_k A) : (modAut r) x = (QuantumSet.toSubset_equiv new_k) ((modAut r) ((QuantumSet.toSubset_equiv new_k).symm x))

theorem QuantumSet.subsetStarAlgebra_modAut_apply' {new_k : ℝ} {A : Type u_1} [ha : starAlgebra A] (r : ℝ) (x : A) : (modAut r) ((QuantumSet.toSubset_equiv new_k) x) = (QuantumSet.toSubset_equiv new_k) ((modAut r) x)

theorem QuantumSet.subsetStarAlgebra_modAut_apply'' {new_k : ℝ} {A : Type u_1} [ha : starAlgebra A] (r : ℝ) (x : QuantumSet.subset new_k A) : (QuantumSet.toSubset_equiv new_k).symm ((modAut r) x) = (modAut r) ((QuantumSet.toSubset_equiv new_k).symm x)

noncomputable def QuantumSet.subset_normedAddCommGroup {A : Type u_1} [ha : starAlgebra A] [hA : QuantumSet A] (new_k : ℝ) : NormedAddCommGroup (QuantumSet.subset new_k A)

Equations

• QuantumSet.subset_normedAddCommGroup new_k = InnerProductSpace.Core.toNormedAddCommGroup

noncomputable def QuantumSet.subset_innerProductSpace {A : Type u_1} [ha : starAlgebra A] (hA : QuantumSet A) (new_k : ℝ) : InnerProductSpace ℂ (QuantumSet.subset new_k A)

Equations

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

noncomputable instance QuantumSet.subset_innerProductAlgebra {A : Type u_1} [ha : starAlgebra A] (hA : QuantumSet A) (new_k : ℝ) : InnerProductAlgebra (QuantumSet.subset new_k A)

Equations

• hA.subset_innerProductAlgebra new_k = InnerProductAlgebra.mk ⋯ ⋯ ⋯ ⋯ ⋯

theorem QuantumSet.subset_inner_eq {A : Type u_1} [ha : starAlgebra A] [hA : QuantumSet A] (new_k : ℝ) (x : QuantumSet.subset new_k A) (y : QuantumSet.subset new_k A) : inner x y = inner ((QuantumSet.toSubset_equiv new_k).symm x) ((modAut (new_k + -k A)) ((QuantumSet.toSubset_equiv new_k).symm y))

theorem QuantumSet.inner_eq_subset_inner {A : Type u_1} [ha : starAlgebra A] [hA : QuantumSet A] (new_k : ℝ) (x : A) (y : A) : inner x y = inner ((QuantumSet.toSubset_equiv new_k) x) ((QuantumSet.toSubset_equiv new_k) ((modAut (k A + -new_k)) y))

noncomputable instance QuantumSet.instSubset {A : Type u_1} [ha : starAlgebra A] (hA : QuantumSet A) (new_k : ℝ) : QuantumSet (QuantumSet.subset new_k A)

Equations

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

@[reducible, inline]

abbrev LinearMap.toSubsetQuantumSet {A : Type u_1} [ha : starAlgebra A] {B : Type u_2} [starAlgebra B] [QuantumSet A] [QuantumSet B] (f : A →ₗ[ℂ] B) (sk₁ : ℝ) (sk₂ : ℝ) : QuantumSet.subset sk₁ A →ₗ[ℂ] QuantumSet.subset sk₂ B

Equations

• f.toSubsetQuantumSet sk₁ sk₂ = (QuantumSet.toSubset_algEquiv sk₂).toLinearMap ∘ₗ f ∘ₗ (QuantumSet.toSubset_algEquiv sk₁).symm.toLinearMap

@[reducible, inline]

abbrev LinearMap.ofSubsetQuantumSet {A : Type u_1} [ha : starAlgebra A] {B : Type u_2} [starAlgebra B] [QuantumSet A] [QuantumSet B] (sk₁ : ℝ) (sk₂ : ℝ) (f : QuantumSet.subset sk₁ A →ₗ[ℂ] QuantumSet.subset sk₂ B) : A →ₗ[ℂ] B

Equations

• LinearMap.ofSubsetQuantumSet sk₁ sk₂ f = (QuantumSet.toSubset_algEquiv sk₂).symm.toLinearMap ∘ₗ f ∘ₗ (QuantumSet.toSubset_algEquiv sk₁).toLinearMap

theorem QuantumSet.toSubset_algEquiv_adjoint {A : Type u_1} [ha : starAlgebra A] [hA : QuantumSet A] (sk₁ : ℝ) : LinearMap.adjoint (QuantumSet.toSubset_algEquiv sk₁).toLinearMap = (modAut (sk₁ + -k A)).toLinearMap ∘ₗ (QuantumSet.toSubset_algEquiv sk₁).symm.toLinearMap

theorem QuantumSet.toSubset_algEquiv_symm_adjoint {A : Type u_1} [ha : starAlgebra A] [hA : QuantumSet A] (sk₁ : ℝ) : LinearMap.adjoint (QuantumSet.toSubset_algEquiv sk₁).symm.toLinearMap = (QuantumSet.toSubset_algEquiv sk₁).toLinearMap ∘ₗ (modAut (-sk₁ + k A)).toLinearMap

theorem LinearMap.toSubsetQuantumSet_apply {A : Type u_1} [ha : starAlgebra A] {B : Type u_2} [starAlgebra B] [QuantumSet A] [QuantumSet B] (f : A →ₗ[ℂ] B) (sk₁ : ℝ) (sk₂ : ℝ) (x : QuantumSet.subset sk₁ A) : (f.toSubsetQuantumSet sk₁ sk₂) x = (QuantumSet.toSubset_equiv sk₂) (f ((QuantumSet.toSubset_equiv sk₁).symm x))

theorem LinearMap.toSubsetQuantumSet_adjoint_apply {A : Type u_1} [ha : starAlgebra A] {B : Type u_2} [hb : starAlgebra B] [hA : QuantumSet A] [hB : QuantumSet B] (f : A →ₗ[ℂ] B) (sk₁ : ℝ) (sk₂ : ℝ) : LinearMap.adjoint (f.toSubsetQuantumSet sk₁ sk₂) = ((modAut (-sk₁ + k A)).toLinearMap ∘ₗ LinearMap.adjoint f ∘ₗ (modAut (sk₂ + -k B)).toLinearMap).toSubsetQuantumSet sk₂ sk₁

theorem LinearMap.ofSubsetQuantumSet_adjoint_apply {A : Type u_1} [ha : starAlgebra A] {B : Type u_2} [hb : starAlgebra B] [hA : QuantumSet A] [hB : QuantumSet B] (sk₁ : ℝ) (sk₂ : ℝ) (f : QuantumSet.subset sk₁ A →ₗ[ℂ] QuantumSet.subset sk₂ B) : LinearMap.adjoint (LinearMap.ofSubsetQuantumSet sk₁ sk₂ f) = (modAut (sk₁ + -k A)).toLinearMap ∘ₗ LinearMap.ofSubsetQuantumSet sk₂ sk₁ (LinearMap.adjoint f) ∘ₗ (modAut (-sk₂ + k B)).toLinearMap

theorem rankOne_toSubsetQuantumSet {A : Type u_1} [ha : starAlgebra A] {B : Type u_2} [hb : starAlgebra B] [hA : QuantumSet A] [hB : QuantumSet B] (sk₁ : ℝ) (sk₂ : ℝ) (a : B) (b : A) : (↑(((rankOne ℂ) a) b)).toSubsetQuantumSet sk₁ sk₂ = ↑(((rankOne ℂ) ((QuantumSet.toSubset_equiv sk₂) a)) ((QuantumSet.toSubset_equiv sk₁) ((modAut (-sk₁ + k A)) b)))

theorem rankOne_ofSubsetQuantumSet {A : Type u_1} [ha : starAlgebra A] {B : Type u_2} [starAlgebra B] [hA : QuantumSet A] [hB : QuantumSet B] (sk₁ : ℝ) (sk₂ : ℝ) (a : QuantumSet.subset sk₂ B) (b : QuantumSet.subset sk₁ A) : LinearMap.ofSubsetQuantumSet sk₁ sk₂ ↑(((rankOne ℂ) a) b) = ↑(((rankOne ℂ) ((QuantumSet.toSubset_equiv sk₂).symm a)) ((modAut (sk₁ + -k A)) ((QuantumSet.toSubset_equiv sk₁).symm b)))

@[simp]

theorem QuantumSet.subset_k {A : Type u_2} [starAlgebra A] [h : QuantumSet A] (r : ℝ) : k (QuantumSet.subset r A) = r

@[simp]

theorem QuantumSet.subset_n {A : Type u_2} [starAlgebra A] [h : QuantumSet A] (r : ℝ) : n (QuantumSet.subset r A) = n A

noncomputable def QuantumSet.subset_tensor_algEquiv {A : Type u_2} {B : Type u_3} [starAlgebra A] [starAlgebra B] (r : ℝ) : TensorProduct ℂ (QuantumSet.subset r A) (QuantumSet.subset r B) ≃ₐ[ℂ] QuantumSet.subset r (TensorProduct ℂ A B)

Equations

• QuantumSet.subset_tensor_algEquiv r = (AlgEquiv.TensorProduct.map (QuantumSet.toSubset_algEquiv r).symm (QuantumSet.toSubset_algEquiv r).symm).trans (QuantumSet.toSubset_algEquiv r)

theorem QuantumSet.subset_tensor_algEquiv_tmul {A : Type u_2} {B : Type u_3} [starAlgebra A] [starAlgebra B] (r : ℝ) (x : QuantumSet.subset r A) (y : QuantumSet.subset r B) : (QuantumSet.subset_tensor_algEquiv r) (x ⊗ₜ[ℂ] y) = (QuantumSet.toSubset_algEquiv r) ((QuantumSet.toSubset_algEquiv r).symm x ⊗ₜ[ℂ] (QuantumSet.toSubset_algEquiv r).symm y)

theorem QuantumSet.subset_tensor_algEquiv_symm_tmul {A : Type u_2} {B : Type u_3} [starAlgebra A] [starAlgebra B] (r : ℝ) (a : A) (b : B) : (QuantumSet.subset_tensor_algEquiv r).symm ((QuantumSet.toSubset_algEquiv r) (a ⊗ₜ[ℂ] b)) = (QuantumSet.toSubset_algEquiv r) ((QuantumSet.toSubset_algEquiv r) a ⊗ₜ[ℂ] (QuantumSet.toSubset_algEquiv r) b)

theorem LinearMap.mul'_quantumSet_subset_eq {A : Type u_2} [starAlgebra A] [QuantumSet A] (r : ℝ) : LinearMap.mul' ℂ (QuantumSet.subset r A) = (QuantumSet.toSubset_algEquiv r).toLinearMap ∘ₗ LinearMap.mul' ℂ A ∘ₗ TensorProduct.map (QuantumSet.toSubset_algEquiv r).symm.toLinearMap (QuantumSet.toSubset_algEquiv r).symm.toLinearMap

theorem QuantumSet.subset_tensor_algEquiv_adjoint {A : Type u_2} {B : Type u_3} [starAlgebra A] [starAlgebra B] [QuantumSet A] [QuantumSet B] [h : Fact (k A = k B)] (r : ℝ) : LinearMap.adjoint (QuantumSet.subset_tensor_algEquiv r).toLinearMap = (QuantumSet.subset_tensor_algEquiv r).symm.toLinearMap

theorem QuantumSet.comul_subset_eq {A : Type u_2} [starAlgebra A] [QuantumSet A] (r : ℝ) : Coalgebra.comul = TensorProduct.map (QuantumSet.toSubset_algEquiv r).toLinearMap (QuantumSet.toSubset_algEquiv r).toLinearMap ∘ₗ Coalgebra.comul ∘ₗ (QuantumSet.toSubset_algEquiv r).symm.toLinearMap

theorem schurMul_toSubsetQuantumSet {A : Type u_2} {B : Type u_3} [starAlgebra A] [starAlgebra B] [QuantumSet A] [QuantumSet B] {f : A →ₗ[ℂ] B} (r₁ : ℝ) (r₂ : ℝ) : f.toSubsetQuantumSet r₁ r₂ •ₛ f.toSubsetQuantumSet r₁ r₂ = (f •ₛ f).toSubsetQuantumSet r₁ r₂

theorem LinearMap.toSubsetQuantumSet_inj {A : Type u_2} {B : Type u_3} [starAlgebra A] [starAlgebra B] [QuantumSet A] [QuantumSet B] {f : A →ₗ[ℂ] B} {g : A →ₗ[ℂ] B} (r₁ : ℝ) (r₂ : ℝ) : f.toSubsetQuantumSet r₁ r₂ = g.toSubsetQuantumSet r₁ r₂ ↔ f = g

theorem QuantumSet.toSubset_equiv_isReal {A : Type u_2} [Star A] (r : ℝ) : LinearMap.IsReal (QuantumSet.toSubset_equiv r)

theorem QuantumSet.toSubset_equiv_symm_isReal {A : Type u_2} [Star A] (r : ℝ) : LinearMap.IsReal (QuantumSet.toSubset_equiv r).symm

theorem LinearMap.toSubsetQuantumSet_isReal_iff {A : Type u_2} {B : Type u_3} [starAlgebra A] [starAlgebra B] [QuantumSet A] [QuantumSet B] {f : A →ₗ[ℂ] B} (r₁ : ℝ) (r₂ : ℝ) : LinearMap.IsReal (f.toSubsetQuantumSet r₁ r₂) ↔ LinearMap.IsReal f

theorem QuantumSet.toSubset_onb {A : Type u_2} [starAlgebra A] [hA : QuantumSet A] (r : ℝ) (i : n A) : onb i = (QuantumSet.toSubset_algEquiv r) ((modAut (k A / 2 + -(r / 2))) (onb i))

theorem QuantumSet.comul_of_subset {A : Type u_2} [starAlgebra A] [hA : QuantumSet A] (r : ℝ) : Coalgebra.comul = TensorProduct.map (QuantumSet.toSubset_algEquiv r).symm.toLinearMap (QuantumSet.toSubset_algEquiv r).symm.toLinearMap ∘ₗ Coalgebra.comul ∘ₗ (QuantumSet.toSubset_algEquiv r).toLinearMap

theorem QuantumSet.toSubset_algEquiv_isReal {A : Type u_3} [Ring A] [Algebra ℂ A] [Star A] (r : ℝ) : LinearMap.IsReal (QuantumSet.toSubset_algEquiv r)

theorem QuantumSet.innerOne_map_one_toSubset_eq {A : Type u_3} {B : Type u_4} [starAlgebra A] [starAlgebra B] [QuantumSet A] [QuantumSet B] (r₁ : ℝ) (r₂ : ℝ) {f : A →ₗ[ℂ] B} : inner 1 (f 1) = inner 1 ((f.toSubsetQuantumSet r₁ r₂) 1)

instance instPartialOrderSubset {A : Type u_3} [hA : PartialOrder A] (r : ℝ) : PartialOrder (QuantumSet.subset r A)

Equations

• instPartialOrderSubset r = hA

instance instNonUnitalNonAssocSemiringSubset {A : Type u_3} [hA : NonUnitalNonAssocSemiring A] (r : ℝ) : NonUnitalNonAssocSemiring (QuantumSet.subset r A)

Equations

• instNonUnitalNonAssocSemiringSubset r = hA

instance instNonUnitalSemiringSubset {A : Type u_3} [hA : NonUnitalSemiring A] (r : ℝ) : NonUnitalSemiring (QuantumSet.subset r A)

Equations

• instNonUnitalSemiringSubset r = hA

instance instStarRingSubset_1 {A : Type u_3} [NonUnitalNonAssocSemiring A] [hA : StarRing A] (r : ℝ) : StarRing (QuantumSet.subset r A)

Equations

• instStarRingSubset_1 r = hA

instance instStarOrderedRingSubset {A : Type u_3} [NonUnitalSemiring A] [PartialOrder A] [StarRing A] [hA : StarOrderedRing A] (r : ℝ) : StarOrderedRing (QuantumSet.subset r A)

Equations

• ⋯ = hA

instance instNontrivialSubset {A : Type u_3} [hA : Nontrivial A] (r : ℝ) : Nontrivial (QuantumSet.subset r A)

Equations

• ⋯ = hA

theorem QuantumSet.normOne_toSubset {A : Type u_3} [starAlgebra A] [QuantumSet A] (r : ℝ) : ‖1‖ = ‖1‖

theorem LinearMap.toSubsetQuantumSet_eq_iff {A : Type u_3} {B : Type u_4} [ha : starAlgebra A] [starAlgebra B] [hA : QuantumSet A] [hB : QuantumSet B] (sk₁ : ℝ) (sk₂ : ℝ) (f : A →ₗ[ℂ] B) (g : QuantumSet.subset sk₁ A →ₗ[ℂ] QuantumSet.subset sk₂ B) : f.toSubsetQuantumSet sk₁ sk₂ = g ↔ f = LinearMap.ofSubsetQuantumSet sk₁ sk₂ g