Hoffman algebra and its bases

DefinitionThe letter \(x\) as a word#✓fully proved

In the free monoid on the two letters \(x\) and \(y\), with \(x\) represented by the Boolean value false and \(y\) by true, this is the word of length one consisting of the letter \(x\).

def xWord : FreeMonoid Bool := FreeMonoid.ofList [false]

Used by 3

Used byHoffman monomial basis of \(\mathfrak{H}^0\) · Words of \(\mathfrak{H}^0\) · The monoid of \(\mathfrak{H}^0\)-words

DefinitionThe letter \(y\) as a word#✓fully proved

In the free monoid on the two letters \(x\) and \(y\), this is the word of length one consisting of the single letter \(y\).

The letters are encoded as booleans, with \(x\) as false and \(y\) as true.

def yWord : FreeMonoid Bool := FreeMonoid.ofList [true]

Used by 6

Used byHoffman basis of \(\mathfrak{H}^1\) · Hoffman monomial basis of \(\mathfrak{H}^0\) · Words of \(\mathfrak{H}^1\) · Words of \(\mathfrak{H}^0\) · The monoid of \(\mathfrak{H}^1\)-words · The monoid of \(\mathfrak{H}^0\)-words

DefinitionEntries of an index as positive integers#✓fully proved

For an index \((k_1, \dots, k_r)\), this is the list \((k_1, \dots, k_r)\) of its entries in order, each regarded as a positive integer.

def Index.pnatEntries : Index → List PNat
  | ⟨_, c⟩ => c.blocks.attach.map fun ⟨n, hm⟩ => ⟨n, c.blocks_pos hm⟩

Uses 1 · Used by 3

Statement usesMultiple-zeta index

Used byHoffman basis of \(\mathfrak{H}^1\) · Hoffman monomial basis of \(\mathfrak{H}^0\) · Hoffman word of an index

DefinitionHoffman word of a list of positive integers#✓fully proved

For a finite list \((k_1, \dots, k_r)\) of positive integers, this is the word \(z_{k_1} z_{k_2} \cdots z_{k_r}\) in the free monoid on the two letters \(x\) and \(y\), where \(z_k = x^{k-1} y\) is the Hoffman block of \(k\). The empty list gives the empty word.

def zWordPNat (l : List PNat) : FreeMonoid Bool :=
  (l.map hoffmanBlock).prod

Uses 1 · Used by 3

Statement usesHoffman block

Used byHoffman basis of \(\mathfrak{H}^1\) · Hoffman monomial basis of \(\mathfrak{H}^0\) · Hoffman word of an index

DefinitionHoffman word of an index#✓fully proved

For an index \(\mathbf{k} = (k_1, \dots, k_r)\) of positive integers, the Hoffman word of \(\mathbf{k}\) is \(z_{k_1} z_{k_2} \cdots z_{k_r}\) in the free monoid on the two letters \(x\) and \(y\), where \(z_k = x^{k-1} y\). The empty index gives the empty word.

def zWord (idx : Index) : FreeMonoid Bool :=
  zWordPNat idx.pnatEntries

Uses 3 · Used by 3

Statement usesMultiple-zeta index · Entries of an index as positive integers · Hoffman word of a list of positive integers

Used byHoffman basis of \(\mathfrak{H}^1\) · Hoffman monomial basis of \(\mathfrak{H}^0\) · Hoffman monomial of an index

DefinitionHoffman monomial of an index#✓fully proved

For an index \(\mathbf{k} = (k_1, \dots, k_r)\) of positive integers, this is the monomial \(z_{k_1} z_{k_2} \cdots z_{k_r}\) with coefficient \(1\) in the free associative algebra \(\mathbb{Q}\langle x, y \rangle\) over \(\mathbb{Q}\) on two noncommuting letters \(x\) and \(y\), where \(z_k = x^{k-1} y\). In other words, it is the Hoffman word of \(\mathbf{k}\) viewed as an element of \(\mathbb{Q}\langle x, y \rangle\). The empty index gives \(1\).

noncomputable def zMonomial (idx : Index) : FreeAlgebra ℚ Bool :=
  (FreeAlgebra.equivMonoidAlgebraFreeMonoid :
      FreeAlgebra ℚ Bool ≃ₐ[ℚ] MonoidAlgebra ℚ (FreeMonoid Bool)).symm
    (MonoidAlgebra.single (zWord idx) 1)

Uses 2 · Used by 2

Statement usesMultiple-zeta index · Hoffman word of an index

Used byHoffman basis of \(\mathfrak{H}^1\) · Hoffman monomial basis of \(\mathfrak{H}^0\)

DefinitionWords of \(\mathfrak{H}^1\)#✓fully proved

A word \(w\) in the two letters \(x\) and \(y\) is an \(\mathfrak{H}^1\)-word when \(w\) is empty or \(w = uy\) for some word \(u\), that is, when \(w\) is empty or ends in \(y\).

def IsHOneWord (w : FreeMonoid Bool) : Prop :=
  w = 1 ∨ ∃ u : FreeMonoid Bool, w = u * yWord

Uses 1 · Used by 3

Statement usesThe letter \(y\) as a word

Used byHoffman basis of \(\mathfrak{H}^1\) · Hoffman monomial basis of \(\mathfrak{H}^0\) · The monoid of \(\mathfrak{H}^1\)-words

DefinitionWords of \(\mathfrak{H}^0\)#✓fully proved

A word \(w\) in the two letters \(x\) and \(y\) is an \(\mathfrak{H}^0\)-word when \(w\) is empty or \(w = xuy\) for some word \(u\), that is, when \(w\) is empty or begins with \(x\) and ends in \(y\).

def IsHZeroWord (w : FreeMonoid Bool) : Prop :=
  w = 1 ∨ ∃ u : FreeMonoid Bool, w = xWord * u * yWord

Uses 2 · Used by 2

Statement usesThe letter \(x\) as a word · The letter \(y\) as a word

Used byHoffman monomial basis of \(\mathfrak{H}^0\) · The monoid of \(\mathfrak{H}^0\)-words

DefinitionThe monoid of \(\mathfrak{H}^1\)-words#✓fully proved

This is the submonoid of the free monoid on the two letters \(x\) and \(y\) consisting of the words that are empty or end in \(y\).

def wordSubmonoidHOne : Submonoid (FreeMonoid Bool) where
  carrier := { w | IsHOneWord w }
  mul_mem' := by
    intro a b ha hb
    simp only [Set.mem_ofPred_eq, IsHOneWord] at ha hb ⊢
    rcases ha with rfl | ⟨ua, rfl⟩
    · simp only [one_mul]
      exact hb
    · rcases hb with rfl | ⟨ub, rfl⟩
      · simp
      · exact Or.inr ⟨ua * yWord * ub, by simp [mul_assoc]⟩
  one_mem' := Or.inl rfl

Uses 2 · Used by 3

Statement usesWords of \(\mathfrak{H}^1\) · The letter \(y\) as a word

Used byThe subalgebra \(\mathfrak{H}^1\) · Hoffman basis of \(\mathfrak{H}^1\) · Hoffman monomial basis of \(\mathfrak{H}^0\)

DefinitionThe monoid of \(\mathfrak{H}^0\)-words#✓fully proved

This is the submonoid of the free monoid on the two letters \(x\) and \(y\) consisting of the words that are empty or begin with \(x\) and end in \(y\).

def wordSubmonoidHZero : Submonoid (FreeMonoid Bool) where
  carrier := { w | IsHZeroWord w }
  mul_mem' := by
    intro a b ha hb
    simp only [Set.mem_ofPred_eq, IsHZeroWord] at ha hb ⊢
    rcases ha with rfl | ⟨ua, rfl⟩
    · simp only [one_mul]
      exact hb
    · rcases hb with rfl | ⟨ub, rfl⟩
      · simp
      · exact Or.inr ⟨ua * yWord * xWord * ub, by simp [mul_assoc]⟩
  one_mem' := Or.inl rfl

Uses 3 · Used by 2

Statement usesWords of \(\mathfrak{H}^0\) · The letter \(x\) as a word · The letter \(y\) as a word

Used byThe subalgebra \(\mathfrak{H}^0\) · Hoffman monomial basis of \(\mathfrak{H}^0\)

DefinitionThe subalgebra \(\mathfrak{H}^1\)#✓fully proved

Let \(\mathbb{Q}\langle x, y\rangle\) be the free associative \(\mathbb{Q}\)-algebra on two letters \(x\) and \(y\), whose monomials are the words in \(x\) and \(y\). The subalgebra \(\mathfrak{H}^1\) of \(\mathbb{Q}\langle x, y\rangle\) is the \(\mathbb{Q}\)-linear span of the words that are empty or end in \(y\); equivalently, it consists of the polynomials in which every word with nonzero coefficient is empty or ends in \(y\).

noncomputable def hOne : Subalgebra ℚ (FreeAlgebra ℚ Bool) :=
  ((MonoidAlgebra.mapDomainAlgHom ℚ ℚ wordSubmonoidHOne.subtype).range).comap
    (FreeAlgebra.equivMonoidAlgebraFreeMonoid :
      FreeAlgebra ℚ Bool ≃ₐ[ℚ] MonoidAlgebra ℚ (FreeMonoid Bool)).toAlgHom

Uses 1 · Used by 1

Statement usesThe monoid of \(\mathfrak{H}^1\)-words

Used byHoffman basis of \(\mathfrak{H}^1\)

DefinitionThe subalgebra \(\mathfrak{H}^0\)#✓fully proved

Let \(\mathbb{Q}\langle x, y\rangle\) be the free associative \(\mathbb{Q}\)-algebra on two letters \(x\) and \(y\), whose monomials are the words in \(x\) and \(y\). The subalgebra \(\mathfrak{H}^0\) of \(\mathbb{Q}\langle x, y\rangle\) is the \(\mathbb{Q}\)-linear span of the words that are empty or begin with \(x\) and end in \(y\); equivalently, it consists of the polynomials in which every word with nonzero coefficient is empty or begins with \(x\) and ends in \(y\).

noncomputable def hZero : Subalgebra ℚ (FreeAlgebra ℚ Bool) :=
  ((MonoidAlgebra.mapDomainAlgHom ℚ ℚ wordSubmonoidHZero.subtype).range).comap
    (FreeAlgebra.equivMonoidAlgebraFreeMonoid :
      FreeAlgebra ℚ Bool ≃ₐ[ℚ] MonoidAlgebra ℚ (FreeMonoid Bool)).toAlgHom

Uses 1 · Used by 1

Statement usesThe monoid of \(\mathfrak{H}^0\)-words

Used byHoffman monomial basis of \(\mathfrak{H}^0\)

DefinitionEmpty or admissible indices#✓fully proved

An index is empty-or-admissible when it is admissible, that is, nonempty with first entry at least \(2\), or when it has no entries.

def IsHZeroIndex (idx : Index) : Prop :=
  idx.IsAdmissible ∨ idx.entries = []

Uses 3 · Used by 2

Statement usesMultiple-zeta index · Admissible index · Entries of an index

Used byHoffman monomial basis of \(\mathfrak{H}^0\) · The type of empty or admissible indices

DefinitionThe type of empty or admissible indices#✓fully proved

The type whose elements are the indices that are admissible, that is, nonempty with first entry at least \(2\), or that have no entries.

def HZeroIndex : Type := { idx : Index // IsHZeroIndex idx }

Uses 2 · Used by 1

Statement usesMultiple-zeta index · Empty or admissible indices

Used byHoffman monomial basis of \(\mathfrak{H}^0\)

TheoremHoffman basis of \(\mathfrak{H}^1\)#✓fully proved

Let \(\mathfrak{H} = \mathbb{Q}\langle x, y \rangle\) be the free associative \(\mathbb{Q}\)-algebra on two generators \(x\) and \(y\), let \(\mathfrak{H}^1\) be the \(\mathbb{Q}\)-linear span of the empty word and the words ending in \(y\) (a subalgebra), and for each positive integer \(k\) let \(z_k = x^{k-1} y\). The family of monomials \(z_{k_1} z_{k_2} \cdots z_{k_r}\), indexed by all indices \((k_1, \dots, k_r)\) of positive integers including the empty index (whose monomial is the empty word \(1\)), is a basis of \(\mathfrak{H}^1\) over \(\mathbb{Q}\).

theorem hOne_basis :
    ∃ b : Module.Basis Index ℚ ↥hOne,
      ∀ idx : Index, (↑(b idx) : FreeAlgebra ℚ Bool) = zMonomial idx

Sources

• M. E. Hoffman, The Algebra of Multiple Harmonic Series, J. Algebra 194 (1997), 477–495, DOI 10.1006/jabr.1997.7127.

Uses 12

Statement usesMultiple-zeta index · The subalgebra \(\mathfrak{H}^1\) · Hoffman monomial of an index

Proof usesEntries of an index · Entries of an index as positive integers · Words of \(\mathfrak{H}^1\) · Hoffman block · Hoffman block as a list · The monoid of \(\mathfrak{H}^1\)-words · The letter \(y\) as a word · Hoffman word of an index · Hoffman word of a list of positive integers

TheoremHoffman monomial basis of \(\mathfrak{H}^0\)#✓fully proved

Let \(\mathbb{Q}\langle x, y\rangle\) be the free associative \(\mathbb{Q}\)-algebra on two letters \(x\) and \(y\), and let \(\mathfrak{H}^0\) be its subalgebra consisting of the \(\mathbb{Q}\)-linear combinations of the empty word and of words that begin with \(x\) and end with \(y\). For \(k \ge 1\) put \(z_k = x^{k-1} y\), and for an index \(\mathbf{k} = (k_1, \dots, k_r)\) of positive integers (possibly empty) put \(z_{\mathbf{k}} = z_{k_1} \cdots z_{k_r}\), with \(z_{\mathbf{k}} = 1\) for the empty index. Call \(\mathbf{k}\) admissible if \(r \ge 1\) and \(k_1 \ge 2\). Then there is a \(\mathbb{Q}\)-basis of \(\mathfrak{H}^0\), indexed by the indices that are empty or admissible, whose element at each such index \(\mathbf{k}\) is \(z_{\mathbf{k}}\).

theorem hZero_basis :
    ∃ b : Module.Basis HZeroIndex ℚ ↥hZero,
      ∀ idx : HZeroIndex, (↑(b idx) : FreeAlgebra ℚ Bool) = zMonomial idx.val

Sources

• M. E. Hoffman, The Algebra of Multiple Harmonic Series, J. Algebra 194 (1997), 477–495, DOI 10.1006/jabr.1997.7127.

Uses 20

Statement usesThe type of empty or admissible indices · Multiple-zeta index · Empty or admissible indices · The subalgebra \(\mathfrak{H}^0\) · Hoffman monomial of an index

Proof usesAdmissible index · Entries of an index · Admissibility of an index via its entries · Entries of an index as positive integers · Admissible list · Words of \(\mathfrak{H}^1\) · Words of \(\mathfrak{H}^0\) · Hoffman block · Hoffman block as a list · The monoid of \(\mathfrak{H}^1\)-words · The monoid of \(\mathfrak{H}^0\)-words · The letter \(x\) as a word · The letter \(y\) as a word · Hoffman word of an index · Hoffman word of a list of positive integers

16 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.