Monlib.LinearAlgebra.QuantumSet.Subset

source

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

Type u_1

Equations

QuantumSet.toSubset _k A = A

Instances For

source

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

A ≃ toSubset k A

Equations

QuantumSet.toSubset_equiv k = Equiv.refl A

Instances For

source

@[reducible, inline]

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

Type u_1

Equations

QuantumSet.subset k A = QuantumSet.toSubset k A

Instances For

source

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

source

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

Inhabited (QuantumSet.subset new_k A)

Equations

instInhabitedSubset A = h

source

instance instRingSubset {new_k : ℝ} {A : Type u_1} [h : Ring A] :

Ring (QuantumSet.subset new_k A)

Equations

instRingSubset = h

source

instance instAlgebraComplexSubset {new_k : ℝ} {A : Type u_1} [Ring A] [h : Algebra ℂ A] :

Algebra ℂ (QuantumSet.subset new_k A)

Equations

instAlgebraComplexSubset = h

source

instance instStarSubset {new_k : ℝ} {A : Type u_1} [h : Star A] :

Star (QuantumSet.subset new_k A)

Equations

instStarSubset = h

source

instance instSMulComplexSubset {new_k : ℝ} {A : Type u_1} [h : SMul ℂ A] :

SMul ℂ (QuantumSet.subset new_k A)

Equations

instSMulComplexSubset = h

source

instance instStarRingSubset {new_k : ℝ} {A : Type u_1} [Ring A] [h : StarRing A] :

StarRing (QuantumSet.subset new_k A)

Equations

instStarRingSubset = h

source

instance instStarModuleComplexSubset {new_k : ℝ} {A : Type u_1} [Star A] [SMul ℂ A] [h : StarModule ℂ A] :

StarModule ℂ (QuantumSet.subset new_k A)

source

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

A ≃ₐ[ℂ ] subset k A

Equations

QuantumSet.toSubset_algEquiv k = AlgEquiv.refl

Instances For

source

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

(toSubset_algEquiv new_k) x = (toSubset_equiv new_k) x

source

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

(toSubset_algEquiv new_k).symm x = (toSubset_equiv new_k).symm x

source

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

starAlgebra (subset k A)

Equations

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

source

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

(modAut r) x = (toSubset_equiv new_k) ((modAut r) ((toSubset_equiv new_k).symm x))

source

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

(modAut r) ((toSubset_equiv new_k) x) = (toSubset_equiv new_k) ((modAut r) x)

source

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

(toSubset_equiv new_k).symm ((modAut r) x) = (modAut r) ((toSubset_equiv new_k).symm x)

source

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

NormedAddCommGroup (subset new_k A)

Equations

QuantumSet.subset_normedAddCommGroup new_k = InnerProductSpace.Core.toNormedAddCommGroup

Instances For

source

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

InnerProductSpace ℂ (subset new_k A)

Equations

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

Instances For

source

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

InnerProductAlgebra (subset new_k A)

Equations

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

source

theorem QuantumSet.subset_inner_eq {A : Type u_1} [ha : starAlgebra A] [hA : QuantumSet A] (new_k : ℝ) (x y : subset new_k A) :

inner x y = inner ((toSubset_equiv new_k).symm x) ((modAut (new_k + -k A)) ((toSubset_equiv new_k).symm y))

source

theorem QuantumSet.inner_eq_subset_inner {A : Type u_1} [ha : starAlgebra A] [hA : QuantumSet A] (new_k : ℝ) (x y : A) :

inner x y = inner ((toSubset_equiv new_k) x) ((toSubset_equiv new_k) ((modAut (k A + -new_k)) y))

source

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

QuantumSet (subset new_k A)

Equations

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

source

@[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

Instances For

source

@[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

Instances For

source

theorem QuantumSet.toSubset_algEquiv_adjoint {A : Type u_1} [ha : starAlgebra A] [hA : QuantumSet A] (sk₁ : ℝ) :

LinearMap.adjoint (toSubset_algEquiv sk₁).toLinearMap = (modAut (sk₁ + -k A)).toLinearMap ∘ₗ (toSubset_algEquiv sk₁).symm.toLinearMap

source

theorem QuantumSet.toSubset_algEquiv_symm_adjoint {A : Type u_1} [ha : starAlgebra A] [hA : QuantumSet A] (sk₁ : ℝ) :

LinearMap.adjoint (toSubset_algEquiv sk₁).symm.toLinearMap = (toSubset_algEquiv sk₁).toLinearMap ∘ₗ (modAut (-sk₁ + k A)).toLinearMap

source

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

source

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

adjoint (f.toSubsetQuantumSet sk₁ sk₂) = ((modAut (-sk₁ + k A)).toLinearMap ∘ₗ adjoint f ∘ₗ (modAut (sk₂ + -k B)).toLinearMap).toSubsetQuantumSet sk₂ sk₁

source

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

adjoint (ofSubsetQuantumSet sk₁ sk₂ f) = (modAut (sk₁ + -k A)).toLinearMap ∘ₗ ofSubsetQuantumSet sk₂ sk₁ (adjoint f) ∘ₗ (modAut (-sk₂ + k B)).toLinearMap

source

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

source

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

source

@[simp]

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

k (subset r A) = r

source

@[simp]

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

n (subset r A) = n A

source

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

TensorProduct ℂ (subset r A) (subset r B) ≃ₐ[ℂ ] 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)

Instances For

source

theorem QuantumSet.subset_tensor_algEquiv_tmul {A : Type u_2} {B : Type u_3} [starAlgebra A] [starAlgebra B] (r : ℝ) (x : subset r A) (y : subset r B) :

(subset_tensor_algEquiv r) (x ⊗ₜ[ℂ ] y) = (toSubset_algEquiv r) ((toSubset_algEquiv r).symm x ⊗ₜ[ℂ ] (toSubset_algEquiv r).symm y)

source

theorem QuantumSet.subset_tensor_algEquiv_symm_tmul {A : Type u_2} {B : Type u_3} [starAlgebra A] [starAlgebra B] (r : ℝ) (a : A) (b : B) :

(subset_tensor_algEquiv r).symm ((toSubset_algEquiv r) (a ⊗ₜ[ℂ ] b)) = (toSubset_algEquiv r) ((toSubset_algEquiv r) a ⊗ₜ[ℂ ] (toSubset_algEquiv r) b)

source

theorem LinearMap.mul'_quantumSet_subset_eq {A : Type u_2} [starAlgebra A] [QuantumSet A] (r : ℝ) :

mul' ℂ (QuantumSet.subset r A) = (QuantumSet.toSubset_algEquiv r).toLinearMap ∘ₗ mul' ℂ A ∘ₗ TensorProduct.map (QuantumSet.toSubset_algEquiv r).symm.toLinearMap (QuantumSet.toSubset_algEquiv r).symm.toLinearMap

source

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 (subset_tensor_algEquiv r).toLinearMap = (subset_tensor_algEquiv r).symm.toLinearMap

source

theorem QuantumSet.comul_subset_eq {A : Type u_2} [starAlgebra A] [QuantumSet A] (r : ℝ) :

CoalgebraStruct.comul = TensorProduct.map (toSubset_algEquiv r).toLinearMap (toSubset_algEquiv r).toLinearMap ∘ₗ CoalgebraStruct.comul ∘ₗ (toSubset_algEquiv r).symm.toLinearMap

source

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₂

source

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

f.toSubsetQuantumSet r₁ r₂ = g.toSubsetQuantumSet r₁ r₂ ↔ f = g

source

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

LinearMap.IsReal (toSubset_equiv r)

source

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

LinearMap.IsReal (toSubset_equiv r).symm

source

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

IsReal (f.toSubsetQuantumSet r₁ r₂) ↔ IsReal f

source

theorem QuantumSet.toSubset_onb {A : Type u_2} [starAlgebra A] [hA : QuantumSet A] (r : ℝ) (i : n A) :

onb i = (toSubset_algEquiv r) ((modAut (k A / 2 + -(r / 2))) (onb i))

source

theorem QuantumSet.comul_of_subset {A : Type u_2} [starAlgebra A] [hA : QuantumSet A] (r : ℝ) :

CoalgebraStruct.comul = TensorProduct.map (toSubset_algEquiv r).symm.toLinearMap (toSubset_algEquiv r).symm.toLinearMap ∘ₗ CoalgebraStruct.comul ∘ₗ (toSubset_algEquiv r).toLinearMap

source

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

LinearMap.IsReal (toSubset_algEquiv r)

source

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)

source

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

PartialOrder (QuantumSet.subset r A)

Equations

instPartialOrderSubset r = hA

source

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

NonUnitalNonAssocSemiring (QuantumSet.subset r A)

Equations

instNonUnitalNonAssocSemiringSubset r = hA

source

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

NonUnitalSemiring (QuantumSet.subset r A)

Equations

instNonUnitalSemiringSubset r = hA

source

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

StarRing (QuantumSet.subset r A)

Equations

instStarRingSubset_1 r = hA

source

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

StarOrderedRing (QuantumSet.subset r A)

source

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

Nontrivial (QuantumSet.subset r A)

source

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

‖1‖ = ‖1‖

source

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 = ofSubsetQuantumSet sk₁ sk₂ g