Noncommutative polynomials with the conjugate-linear star

MIPRE.NCPoly G is the free complex algebra on the letters G: finite complex combinations of words in G, multiplied by concatenation. It is a type synonym (a def, not an abbrev) for MonoidAlgebra ℂ (FreeMonoid G), and carries the involution of the free *-algebra on self-adjoint generators, (Σ_w c_w w)⋆ = Σ_w conj(c_w) reverse(w): conjugate the coefficients and reverse the words (MIPRE.NCPoly.coeff_star_apply, MIPRE.NCPoly.star_single). With it NCPoly G is a StarRing and a StarModule ℂ, and every letter NCPoly.gen g is self-adjoint.

This is the algebra of the Tsirelson route (planning/tsirelson-campaign.md, §3.1): the quadratic module of the measurement relations lives in it (MIPRE.Foundations.NCPoly.Cone), and strategies are evaluations of it on a Hilbert space.

Why a new star, and why a def

• Mathlib's FreeAlgebra ℂ G has a star (Mathlib.Algebra.Star.Free), but it reverses words ℂ-linearly: it fixes the scalars, star (algebraMap ℂ _ c) = algebraMap ℂ _ c. It is not a StarModule ℂ for the conjugation of ℂ, so star (i • 1) ≠ -i • 1, and hermitian squares s⋆ s would not be hermitian in the sense the route needs. It cannot be used.
• Mathlib has no Star instance on MonoidAlgebra. Declaring one on MonoidAlgebra ℂ (FreeMonoid G) itself (as an abbrev would) would make the conjugate-reverse star a global instance on a Mathlib type, so NCPoly G is a def. Its Ring and Algebra ℂ structures are those of the monoid algebra (inferInstanceAs), and its real structure is Module.complexToReal, so (r : ℝ) • z = (r : ℂ) • z holds by rfl and no diamond arises. (Mathlib.Algebra.Star.Free also puts a StarMul on FreeMonoid G, word reversal; this file does not import it and writes FreeMonoid.reverse throughout.)
• Since NCPoly G is not reducible to the monoid algebra, the lemmas about it are restated here, as a small transport API (coeff, ofCoeff, single, ext, induction_linear, single_mul_single, one_def, smul_single, basis, lift, …); downstream files use this API and never the MonoidAlgebra lemmas.

Main declarations

• MIPRE.NCPoly G, with its Ring and Algebra ℂ instances;
• the transport API: NCPoly.coeff, NCPoly.ofCoeff, NCPoly.single, NCPoly.ext, NCPoly.coeff_injective, NCPoly.induction_linear, NCPoly.single_mul_single, NCPoly.coeff_mul, NCPoly.one_def, NCPoly.smul_single, NCPoly.sum_single, the monomial basis NCPoly.basis, and the universal property NCPoly.lift (NCPoly.lift_single, NCPoly.algHom_ext);
• its Star, StarRing and StarModule ℂ instances, with NCPoly.coeff_star_apply and NCPoly.star_single;
• NCPoly.gen g, the degree-one monomial of a letter, with NCPoly.star_gen and NCPoly.isSelfAdjoint_gen;
• NCPoly.eval f : NCPoly G →ₐ[ℂ] A, evaluation at an assignment f : G → A of the letters, built from NCPoly.lift and FreeMonoid.lift (NCPoly.eval_single, NCPoly.eval_gen);
• NCPoly.eval_star: evaluation at self-adjoint letters commutes with the stars;
• NCPoly.evalStar f hf : NCPoly G →⋆ₐ[ℂ] A, the same evaluation as a ⋆-algebra hom.

At the pinned Mathlib MonoidAlgebra is a structure with constructor ofCoeff and field coeff, so the star is defined on coefficients and transported.

def MIPRE.NCPoly (G : Type u_1) : Type u_1

Noncommutative polynomials over ℂ in the letters G: the monoid algebra of the free monoid, with the conjugate-linear, word-reversing star declared below. A def, so that the star is not an instance on MonoidAlgebra.

Equations

• MIPRE.NCPoly G = MonoidAlgebra ℂ (FreeMonoid G)

@[instance_reducible]

noncomputable instance MIPRE.NCPoly.instRing {G : Type u_1} : Ring (NCPoly G)

The ring structure of the monoid algebra.

Equations

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

@[instance_reducible]

noncomputable instance MIPRE.NCPoly.instAlgebra {G : Type u_1} : Algebra ℂ (NCPoly G)

The complex algebra structure of the monoid algebra.

Equations

• MIPRE.NCPoly.instAlgebra = { smul := MIPRE.NCPoly.instAlgebra._aux_1, algebraMap := MIPRE.NCPoly.instAlgebra._aux_3, commutes' := ⋯, smul_def' := ⋯ }

@[instance_reducible]

noncomputable instance MIPRE.NCPoly.instInhabited {G : Type u_1} : Inhabited (NCPoly G)

NCPoly G is inhabited, by 0.

Equations

• MIPRE.NCPoly.instInhabited = { default := 0 }

instance MIPRE.NCPoly.instNontrivial {G : Type u_1} : Nontrivial (NCPoly G)

NCPoly G is nontrivial: 0 ≠ 1.

The transport API

def MIPRE.NCPoly.coeff {G : Type u_1} (x : NCPoly G) : FreeMonoid G →₀ ℂ

The coefficients of a polynomial, as a finitely supported function on words.

Equations

• x.coeff = x.coeff

def MIPRE.NCPoly.ofCoeff {G : Type u_1} (f : FreeMonoid G →₀ ℂ) : NCPoly G

The polynomial with prescribed coefficients.

Equations

• MIPRE.NCPoly.ofCoeff f = MonoidAlgebra.ofCoeff f

noncomputable def MIPRE.NCPoly.single {G : Type u_1} (w : FreeMonoid G) (c : ℂ) : NCPoly G

The monomial c w of a word w with coefficient c.

Equations

• MIPRE.NCPoly.single w c = MonoidAlgebra.single w c

@[simp]

theorem MIPRE.NCPoly.coeff_ofCoeff {G : Type u_1} (f : FreeMonoid G →₀ ℂ) : (ofCoeff f).coeff = f

The coefficients of ofCoeff f are f.

@[simp]

theorem MIPRE.NCPoly.ofCoeff_coeff {G : Type u_1} (x : NCPoly G) : ofCoeff x.coeff = x

A polynomial is recovered from its coefficients.

theorem MIPRE.NCPoly.coeff_injective {G : Type u_1} : Function.Injective coeff

A polynomial is determined by its coefficients.

@[simp]

theorem MIPRE.NCPoly.coeff_inj {G : Type u_1} {x y : NCPoly G} : x.coeff = y.coeff ↔ x = y

Equality of coefficient functions.

theorem MIPRE.NCPoly.ext {G : Type u_1} {x y : NCPoly G} (h : ∀ (w : FreeMonoid G), x.coeff w = y.coeff w) : x = y

Extensionality: two polynomials with the same coefficient on every word are equal.

theorem MIPRE.NCPoly.ext_iff {G : Type u_1} {x y : NCPoly G} : x = y ↔ ∀ (w : FreeMonoid G), x.coeff w = y.coeff w

@[simp]

theorem MIPRE.NCPoly.coeff_zero {G : Type u_1} : coeff 0 = 0

The coefficients of 0.

@[simp]

theorem MIPRE.NCPoly.coeff_add {G : Type u_1} (x y : NCPoly G) : (x + y).coeff = x.coeff + y.coeff

The coefficients of a sum.

@[simp]

theorem MIPRE.NCPoly.coeff_neg {G : Type u_1} (x : NCPoly G) : (-x).coeff = -x.coeff

The coefficients of a negation.

@[simp]

theorem MIPRE.NCPoly.coeff_sub {G : Type u_1} (x y : NCPoly G) : (x - y).coeff = x.coeff - y.coeff

The coefficients of a difference.

@[simp]

theorem MIPRE.NCPoly.coeff_smul {G : Type u_1} (c : ℂ) (x : NCPoly G) : (c • x).coeff = c • x.coeff

The coefficients of a complex multiple.

@[simp]

theorem MIPRE.NCPoly.coeff_real_smul {G : Type u_1} (r : ℝ) (x : NCPoly G) : (r • x).coeff = ↑r • x.coeff

The coefficients of a real multiple.

@[simp]

theorem MIPRE.NCPoly.coeff_sum {G : Type u_1} {ι : Type u_2} (s : Finset ι) (f : ι → NCPoly G) : (∑ i ∈ s, f i).coeff = ∑ i ∈ s, (f i).coeff

The coefficients of a finite sum.

@[simp]

theorem MIPRE.NCPoly.coeff_single {G : Type u_1} (w : FreeMonoid G) (c : ℂ) : (single w c).coeff = Finsupp.single w c

The coefficients of a monomial.

theorem MIPRE.NCPoly.coeff_single_apply {G : Type u_1} (w v : FreeMonoid G) (c : ℂ) [Decidable (w = v)] : (single w c).coeff v = if w = v then c else 0

The coefficient of a monomial at a word.

@[simp]

theorem MIPRE.NCPoly.single_zero {G : Type u_1} (w : FreeMonoid G) : single w 0 = 0

A monomial with coefficient 0 vanishes.

theorem MIPRE.NCPoly.single_neg {G : Type u_1} (w : FreeMonoid G) (c : ℂ) : single w (-c) = -single w c

single w commutes with negation.

@[simp]

theorem MIPRE.NCPoly.smul_single {G : Type u_1} (c' : ℂ) (w : FreeMonoid G) (c : ℂ) : c' • single w c = single w (c' * c)

A complex multiple of a monomial.

theorem MIPRE.NCPoly.single_eq_smul_single_one {G : Type u_1} (w : FreeMonoid G) (c : ℂ) : single w c = c • single w 1

A monomial is a multiple of the monomial with coefficient 1.

theorem MIPRE.NCPoly.one_def {G : Type u_1} : 1 = single 1 1

The unit is the empty word.

theorem MIPRE.NCPoly.coeff_one {G : Type u_1} : coeff 1 = Finsupp.single 1 1

The coefficients of the unit.

@[simp]

theorem MIPRE.NCPoly.single_mul_single {G : Type u_1} (w w' : FreeMonoid G) (c c' : ℂ) : single w c * single w' c' = single (w * w') (c * c')

The product of two monomials concatenates the words.

theorem MIPRE.NCPoly.coeff_mul {G : Type u_1} [DecidableEq (FreeMonoid G)] (x y : NCPoly G) (w : FreeMonoid G) : (x * y).coeff w = x.coeff.sum fun (u : FreeMonoid G) (a : ℂ) => y.coeff.sum fun (v : FreeMonoid G) (b : ℂ) => if u * v = w then a * b else 0

The coefficients of a product: the coefficient of w in x y is the sum of the x_u y_v over the factorizations w = u v.

@[simp]

theorem MIPRE.NCPoly.sum_single {G : Type u_1} (x : NCPoly G) : x.coeff.sum single = x

Every polynomial is the sum of its monomials.

theorem MIPRE.NCPoly.sum_support_single {G : Type u_1} (x : NCPoly G) : ∑ w ∈ x.coeff.support, single w (x.coeff w) = x

Every polynomial is the sum of its monomials, over the support of its coefficients.

theorem MIPRE.NCPoly.induction_linear {G : Type u_1} {motive : NCPoly G → Prop} (x : NCPoly G) (zero : motive 0) (add : ∀ (x y : NCPoly G), motive x → motive y → motive (x + y)) (single : ∀ (w : FreeMonoid G) (c : ℂ), motive (single w c)) : motive x

Induction on polynomials: a property that holds at 0, is closed under sums and holds on monomials holds everywhere.

noncomputable def MIPRE.NCPoly.basis {G : Type u_1} : Module.Basis (FreeMonoid G) ℂ (NCPoly G)

The monomial basis of NCPoly G, indexed by words.

Equations

• MIPRE.NCPoly.basis = MonoidAlgebra.basis (FreeMonoid G) ℂ

@[simp]

theorem MIPRE.NCPoly.basis_apply {G : Type u_1} (w : FreeMonoid G) : basis w = single w 1

The monomial basis vector of a word is the monomial with coefficient 1.

@[simp]

theorem MIPRE.NCPoly.basis_repr {G : Type u_1} (x : NCPoly G) : basis.repr x = x.coeff

The coordinates in the monomial basis are the coefficients.

noncomputable def MIPRE.NCPoly.lift {G : Type u_1} {A : Type u_2} [Semiring A] [Algebra ℂ A] : (FreeMonoid G →* A) ≃ (NCPoly G →ₐ[ℂ] A)

The universal property: a monoid hom from the words into a complex algebra A extends to a ℂ-algebra hom NCPoly G →ₐ[ℂ] A.

Equations

• MIPRE.NCPoly.lift = MonoidAlgebra.lift ℂ A (FreeMonoid G)

@[simp]

theorem MIPRE.NCPoly.lift_single {G : Type u_1} {A : Type u_2} [Semiring A] [Algebra ℂ A] (F : FreeMonoid G →* A) (w : FreeMonoid G) (c : ℂ) : (lift F) (single w c) = c • F w

The lift of a monoid hom on a monomial.

theorem MIPRE.NCPoly.algHom_ext {G : Type u_1} {A : Type u_2} [Semiring A] [Algebra ℂ A] {φ ψ : NCPoly G →ₐ[ℂ] A} (h : ∀ (w : FreeMonoid G), φ (single w 1) = ψ (single w 1)) : φ = ψ

Two algebra homs out of NCPoly G that agree on words are equal.

The star

def MIPRE.NCPoly.revEquiv {G : Type u_1} : FreeMonoid G ≃ FreeMonoid G

Word reversal, as an involutive permutation of FreeMonoid G.

Equations

• MIPRE.NCPoly.revEquiv = Function.Involutive.toPerm FreeMonoid.reverse ⋯

@[simp]

theorem MIPRE.NCPoly.revEquiv_apply {G : Type u_1} (w : FreeMonoid G) : revEquiv w = w.reverse

Word reversal, applied.

@[simp]

theorem MIPRE.NCPoly.revEquiv_symm_apply {G : Type u_1} (w : FreeMonoid G) : revEquiv.symm w = w.reverse

Word reversal is its own inverse.

@[simp]

theorem MIPRE.NCPoly.freeMonoid_reverse_one {G : Type u_1} : FreeMonoid.reverse 1 = 1

The empty word is its own reversal.

noncomputable def MIPRE.NCPoly.starCoeff {G : Type u_1} (f : FreeMonoid G →₀ ℂ) : FreeMonoid G →₀ ℂ

The star on coefficient functions: conjugate the coefficients, reverse the words.

Equations

• MIPRE.NCPoly.starCoeff f = Finsupp.equivMapDomain MIPRE.NCPoly.revEquiv (Finsupp.mapRange (⇑(starRingEnd ℂ)) MIPRE.NCPoly.starCoeff._proof_1 f)

@[instance_reducible]

noncomputable instance MIPRE.NCPoly.instStar {G : Type u_1} : Star (NCPoly G)

The star of NCPoly G: (Σ_w c_w w)⋆ = Σ_w conj(c_w) reverse(w).

Equations

• MIPRE.NCPoly.instStar = { star := fun (x : MIPRE.NCPoly G) => MIPRE.NCPoly.ofCoeff (MIPRE.NCPoly.starCoeff x.coeff) }

@[simp]

theorem MIPRE.NCPoly.coeff_star_apply {G : Type u_1} (x : NCPoly G) (w : FreeMonoid G) : (star x).coeff w = (starRingEnd ℂ) (x.coeff w.reverse)

The coefficient formula for the star: the coefficient of w in x⋆ is the conjugate of the coefficient of the reversed word in x.

theorem MIPRE.NCPoly.star_single {G : Type u_1} (w : FreeMonoid G) (c : ℂ) : star (single w c) = single w.reverse ((starRingEnd ℂ) c)

The star of a monomial.

theorem MIPRE.NCPoly.star_add' {G : Type u_1} (x y : NCPoly G) : star (x + y) = star x + star y

theorem MIPRE.NCPoly.star_zero' {G : Type u_1} : star 0 = 0

theorem MIPRE.NCPoly.star_star' {G : Type u_1} (x : NCPoly G) : star (star x) = x

theorem MIPRE.NCPoly.star_mul' {G : Type u_1} (x y : NCPoly G) : star (x * y) = star y * star x

@[instance_reducible]

noncomputable instance MIPRE.NCPoly.instStarRing {G : Type u_1} : StarRing (NCPoly G)

NCPoly G is a ⋆-ring: the star is additive, involutive and reverses products.

Equations

• MIPRE.NCPoly.instStarRing = { toStar := MIPRE.NCPoly.instStar, star_involutive := ⋯, star_mul := ⋯, star_add := ⋯ }

instance MIPRE.NCPoly.instStarModuleComplex {G : Type u_1} : StarModule ℂ (NCPoly G)

The star is conjugate-linear: (c • x)⋆ = conj c • x⋆.

@[simp]

theorem MIPRE.NCPoly.star_single_one {G : Type u_1} (w : FreeMonoid G) : star (single w 1) = single w.reverse 1

The star of a monomial with coefficient 1.

Generators

noncomputable def MIPRE.NCPoly.gen {G : Type u_1} (g : G) : NCPoly G

The generator of a letter: the degree-one monomial single (FreeMonoid.of g) 1.

Equations

• MIPRE.NCPoly.gen g = MIPRE.NCPoly.single (FreeMonoid.of g) 1

@[simp]

theorem MIPRE.NCPoly.star_gen {G : Type u_1} (g : G) : star (gen g) = gen g

Generators are fixed by the star.

theorem MIPRE.NCPoly.isSelfAdjoint_gen {G : Type u_1} (g : G) : IsSelfAdjoint (gen g)

Generators are self-adjoint.

theorem MIPRE.NCPoly.single_of_mul {G : Type u_1} (g : G) (w : FreeMonoid G) (c : ℂ) : single (FreeMonoid.of g * w) c = gen g * single w c

A word g w is the product of the generator g and the word w.

Evaluation

theorem MIPRE.NCPoly.star_lift_eq_lift_reverse {G : Type u_1} {M : Type u_2} [Monoid M] [StarMul M] (f : G → M) (hf : ∀ (g : G), IsSelfAdjoint (f g)) (w : FreeMonoid G) : star ((FreeMonoid.lift f) w) = (FreeMonoid.lift f) w.reverse

On a word, the star of the evaluation at self-adjoint letters is the evaluation of the reversed word.

noncomputable def MIPRE.NCPoly.eval {G : Type u_1} {A : Type u_2} [Semiring A] [Algebra ℂ A] (f : G → A) : NCPoly G →ₐ[ℂ] A

Evaluation of noncommutative polynomials at an assignment f : G → A of the letters, as a ℂ-algebra hom: a word goes to the product of the images of its letters.

Equations

• MIPRE.NCPoly.eval f = MIPRE.NCPoly.lift (FreeMonoid.lift f)

@[simp]

theorem MIPRE.NCPoly.eval_single {G : Type u_1} {A : Type u_2} [Semiring A] [Algebra ℂ A] (f : G → A) (w : FreeMonoid G) (c : ℂ) : (eval f) (single w c) = c • (FreeMonoid.lift f) w

Evaluation of a monomial.

@[simp]

theorem MIPRE.NCPoly.eval_gen {G : Type u_1} {A : Type u_2} [Semiring A] [Algebra ℂ A] (f : G → A) (g : G) : (eval f) (gen g) = f g

Evaluation of a generator.

theorem MIPRE.NCPoly.eval_star {G : Type u_1} {A : Type u_2} [Semiring A] [Algebra ℂ A] [StarRing A] [StarModule ℂ A] (f : G → A) (hf : ∀ (g : G), IsSelfAdjoint (f g)) (x : NCPoly G) : (eval f) (star x) = star ((eval f) x)

Evaluation at self-adjoint letters commutes with the stars.

noncomputable def MIPRE.NCPoly.evalStar {G : Type u_1} {A : Type u_2} [Semiring A] [Algebra ℂ A] [StarRing A] [StarModule ℂ A] (f : G → A) (hf : ∀ (g : G), IsSelfAdjoint (f g)) : NCPoly G →⋆ₐ[ℂ] A

Evaluation at self-adjoint letters, as a ⋆-algebra hom.

Equations

• MIPRE.NCPoly.evalStar f hf = { toAlgHom := MIPRE.NCPoly.eval f, map_star' := ⋯ }

@[simp]

theorem MIPRE.NCPoly.evalStar_apply {G : Type u_1} {A : Type u_2} [Semiring A] [Algebra ℂ A] [StarRing A] [StarModule ℂ A] (f : G → A) (hf : ∀ (g : G), IsSelfAdjoint (f g)) (x : NCPoly G) : (evalStar f hf) x = (eval f) x

The ⋆-algebra hom of an evaluation is the evaluation.