Quantum Sets on Finite Products

This file restores the finite-product quantum set instance from upstream Monlib.LinearAlgebra.QuantumSet.Pi.

@[reducible, inline]

abbrev PiQ {ι : Type u_1} (A : ι → Type u_3) : Type (max u_1 u_3)

The L² finite product of quantum sets.

Equations

• PiQ A = PiLp 2 A

@[reducible, defaultInstance 1000]

noncomputable instance instRingPiQ {ι : Type u_1} {A : ι → Type u_2} [hA : (i : ι) → starAlgebra (A i)] : Ring (PiQ A)

Equations

• instRingPiQ = (WithLp.equiv 2 ((i : ι) → A i)).ring

@[reducible, defaultInstance 1000]

noncomputable instance instAlgebraComplexPiQ {ι : Type u_1} {A : ι → Type u_2} [hA : (i : ι) → starAlgebra (A i)] : Algebra ℂ (PiQ A)

Equations

• instAlgebraComplexPiQ = Equiv.algebra ℂ (WithLp.equiv 2 ((i : ι) → A i))

@[implicit_reducible]

instance instStarPiQ {ι : Type u_1} {A : ι → Type u_2} [hA : (i : ι) → starAlgebra (A i)] : Star (PiQ A)

Equations

• instStarPiQ = { star := fun (x : PiQ A) => WithLp.toLp 2 (star x.ofLp) }

@[simp]

theorem PiLp.star_apply {ι : Type u_1} {A : ι → Type u_2} [hA : (i : ι) → starAlgebra (A i)] (x : PiQ A) (i : ι) : (star x).ofLp i = star (x.ofLp i)

@[simp]

theorem PiLp.mul_apply_quantum {ι : Type u_1} {A : ι → Type u_2} [hA : (i : ι) → starAlgebra (A i)] (x y : PiQ A) (i : ι) : (x * y).ofLp i = x.ofLp i * y.ofLp i

theorem PiLp.mul_apply {ι : Type u_1} {A : ι → Type u_2} [hA : (i : ι) → starAlgebra (A i)] (x y : PiQ A) (i : ι) : (x * y).ofLp i = x.ofLp i * y.ofLp i

@[implicit_reducible]

instance instStarRingPiQ {ι : Type u_1} {A : ι → Type u_2} [hA : (i : ι) → starAlgebra (A i)] : StarRing (PiQ A)

Equations

• instStarRingPiQ = { toStar := instStarPiQ, star_involutive := ⋯, star_mul := ⋯, star_add := ⋯ }

instance instStarModuleComplexPiQ {ι : Type u_1} {A : ι → Type u_2} [hA : (i : ι) → starAlgebra (A i)] : StarModule ℂ (PiQ A)

noncomputable def Pi.modAut {ι : Type u_1} {A : ι → Type u_2} [hA : (i : ι) → starAlgebra (A i)] (r : ℝ) : PiQ A ≃ₐ[ℂ] PiQ A

The pointwise modular automorphism on a finite product quantum set.

Equations

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

@[simp]

theorem Pi.modAut_apply {ι : Type u_1} {A : ι → Type u_2} [hA : (i : ι) → starAlgebra (A i)] (r : ℝ) (x : PiQ A) (i : ι) : ((modAut r) x).ofLp i = (starAlgebra.modAut r) (x.ofLp i)

@[reducible]

noncomputable instance piStarAlgebra {ι : Type u_1} {A : ι → Type u_2} [hA : (i : ι) → starAlgebra (A i)] : starAlgebra (PiQ A)

Equations

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

@[simp]

theorem piStarAlgebra_modAut_apply {ι : Type u_1} {A : ι → Type u_2} [hA : (i : ι) → starAlgebra (A i)] (r : ℝ) (x : PiQ A) (i : ι) : ((modAut r) x).ofLp i = (modAut r) (x.ofLp i)

@[implicit_reducible]

noncomputable instance piInnerProductAlgebra {ι : Type u_1} {A : ι → Type u_2} [hA : (i : ι) → starAlgebra (A i)] [hQ : (i : ι) → QuantumSet (A i)] [Fintype ι] : InnerProductAlgebra (PiQ A)

Equations

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

theorem piInnerProductAlgebra_inner_apply {ι : Type u_1} {A : ι → Type u_2} [hA : (i : ι) → starAlgebra (A i)] [hQ : (i : ι) → QuantumSet (A i)] [Fintype ι] (a b : PiQ A) : inner ℂ a b = ∑ i : ι, inner ℂ (a.ofLp i) (b.ofLp i)

theorem piInnerProductAlgebra.inner_apply {ι : Type u_1} {A : ι → Type u_2} [hA : (i : ι) → starAlgebra (A i)] [hQ : (i : ι) → QuantumSet (A i)] [Fintype ι] (a b : PiQ A) : inner ℂ a b = ∑ i : ι, inner ℂ (a.ofLp i) (b.ofLp i)

@[implicit_reducible]

noncomputable instance Pi.quantumSet {ι : Type u_1} {A : ι → Type u_2} [hA : (i : ι) → starAlgebra (A i)] [hQ : (i : ι) → QuantumSet (A i)] [Fintype ι] [Fact (∀ (i : ι), k (A i) = 0)] : QuantumSet (PiQ A)

Equations

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