LeanPool.Monlib4.LinearAlgebra.QuantumSet.Subset #

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

source

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

Type u_1

Type synonym for a quantum set with its modular exponent shifted to k.

Equations

QuantumSet.toSubset k A = A

Instances For

source

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

A ≃ toSubset k A

The tautological equivalence from a type to its shifted quantum-set synonym.

Equations

QuantumSet.toSubsetEquiv k = Equiv.refl A

Instances For

source

@[reducible, inline]

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

Type u_1

Abbreviation for the shifted quantum-set type synonym.

Equations

QuantumSet.subset k A = QuantumSet.toSubset k A

Instances For

source

@[implicit_reducible]

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

Inhabited (QuantumSet.subset new_k A)

Equations

instInhabitedSubset A = h

source

@[implicit_reducible]

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

Ring (QuantumSet.subset new_k A)

Equations

instRingSubset = h

source

@[implicit_reducible]

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

Algebra ℂ (QuantumSet.subset new_k A)

Equations

instAlgebraComplexSubset = h

source

@[implicit_reducible]

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

Star (QuantumSet.subset new_k A)

Equations

instStarSubset = h

source

@[implicit_reducible]

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

SMul ℂ (QuantumSet.subset new_k A)

Equations

instSMulComplexSubset = h

source

@[implicit_reducible]

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.toSubsetAlgEquiv (k : ℝ) {A : Type u_1} [Ring A] [Algebra ℂ A] :

A ≃ₐ[ℂ ] subset k A

The tautological algebra equivalence from a type to its shifted quantum-set synonym.

Equations

QuantumSet.toSubsetAlgEquiv k = AlgEquiv.refl

Instances For

source

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

(toSubsetAlgEquiv new_k) x = (toSubsetEquiv new_k) x

source

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

(toSubsetAlgEquiv new_k).symm x = (toSubsetEquiv new_k).symm x

source

@[implicit_reducible]

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

starAlgebra (subset k A)

Equations

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

source

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

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

source

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

(modAut r) ((toSubsetEquiv new_k) x) = (toSubsetEquiv 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) :

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

source

@[reducible]

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

NormedAddCommGroup (subset new_k A)

The normed additive group structure induced by shifting the quantum-set inner product.

Equations

QuantumSet.subsetNormedAddCommGroup new_k = InnerProductSpace.Core.toNormedAddCommGroup

Instances For

source

@[reducible]

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

InnerProductSpace ℂ (subset new_k A)

The inner product space structure induced by shifting the quantum-set inner product.

Equations

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

Instances For

source

@[reducible]

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

InnerProductAlgebra (subset new_k A)

The inner product algebra structure induced by shifting the quantum-set inner product.

Equations

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

Instances For

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 ℂ ((toSubsetEquiv new_k).symm x) ((modAut (new_k + -k A)) ((toSubsetEquiv 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 ℂ ((toSubsetEquiv new_k) x) ((toSubsetEquiv new_k) ((modAut (k A + -new_k)) y))

source

@[reducible]

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

QuantumSet (subset new_k A)

A shifted quantum-set synonym inherits a quantum-set structure with exponent new_k.

Equations

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

Instances For

source

@[reducible, inline]

noncomputable 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

Transport a linear map between quantum sets to shifted quantum-set synonyms.

Equations

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

Instances For

source

@[reducible, inline]

noncomputable 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

Transport a shifted linear map back to the original quantum sets.

Equations

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

Instances For

source

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

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

source

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

LinearMap.adjoint (toSubsetAlgEquiv sk₁).symm.toLinearMap = (toSubsetAlgEquiv 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.toSubsetEquiv sk₂) (f ((QuantumSet.toSubsetEquiv 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.toSubsetEquiv sk₂) a)) ((QuantumSet.toSubsetEquiv 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.toSubsetEquiv sk₂).symm a)) ((modAut (sk₁ + -k A)) ((QuantumSet.toSubsetEquiv 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.subsetTensorAlgEquiv {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)

The tautological algebra equivalence between tensor products of shifted synonyms.

Equations

QuantumSet.subsetTensorAlgEquiv r = (AlgEquiv.TensorProduct.map (QuantumSet.toSubsetAlgEquiv r).symm (QuantumSet.toSubsetAlgEquiv r).symm).trans (QuantumSet.toSubsetAlgEquiv r)

Instances For

source

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

(subsetTensorAlgEquiv r) (x ⊗ₜ[ℂ ] y) = (toSubsetAlgEquiv r) ((toSubsetAlgEquiv r).symm x ⊗ₜ[ℂ ] (toSubsetAlgEquiv r).symm y)

source

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

(subsetTensorAlgEquiv r).symm ((toSubsetAlgEquiv r) (a ⊗ₜ[ℂ ] b)) = (toSubsetAlgEquiv r) ((toSubsetAlgEquiv r) a ⊗ₜ[ℂ ] (toSubsetAlgEquiv r) b)

source

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

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

source

theorem QuantumSet.subsetTensorAlgEquiv_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 (subsetTensorAlgEquiv r).toLinearMap = (subsetTensorAlgEquiv r).symm.toLinearMap

source

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

CoalgebraStruct.comul = TensorProduct.map (toSubsetAlgEquiv r).toLinearMap (toSubsetAlgEquiv r).toLinearMap ∘ₗ CoalgebraStruct.comul ∘ₗ (toSubsetAlgEquiv 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.toSubsetEquiv_isReal {A : Type u_2} [Star A] (r : ℝ) :

LinearMap.IsReal (toSubsetEquiv r)

source

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

LinearMap.IsReal (toSubsetEquiv 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 = (toSubsetAlgEquiv 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 (toSubsetAlgEquiv r).symm.toLinearMap (toSubsetAlgEquiv r).symm.toLinearMap ∘ₗ CoalgebraStruct.comul ∘ₗ (toSubsetAlgEquiv r).toLinearMap

source

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

LinearMap.IsReal (toSubsetAlgEquiv 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

@[implicit_reducible]

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

PartialOrder (QuantumSet.subset r A)

Equations

instPartialOrderSubset r = hA

source

@[implicit_reducible]

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

NonUnitalNonAssocSemiring (QuantumSet.subset r A)

Equations

instNonUnitalNonAssocSemiringSubset r = hA

source

@[implicit_reducible]

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

NonUnitalSemiring (QuantumSet.subset r A)

Equations

instNonUnitalSemiringSubset r = hA

source

@[implicit_reducible]

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

@[implicit_reducible]

instance instAddCommMonoidSubset {A : Type u_3} [h : AddCommMonoid A] (r : ℝ) :

AddCommMonoid (QuantumSet.subset r A)

Equations

instAddCommMonoidSubset r = h

source

@[implicit_reducible]

instance instModuleComplexSubset {A : Type u_3} [AddCommMonoid A] [h : Module ℂ A] (r : ℝ) :

Module ℂ (QuantumSet.subset r A)

Equations

instModuleComplexSubset r = h

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