Butcher Group Operations

This file exposes the convolution monoids on unit-constant B-series and labelled B-series through named UnitSeries aliases.

@[reducible, inline]

abbrev BSeries.Series.UnitSeries (R : Type u) [One R] : Type u

Unit-constant B-series, the coefficient families underlying the Butcher group.

Equations

• BSeries.Series.UnitSeries R = { a : BSeries.Series R // a.HasUnitConstant }

noncomputable def BSeries.Series.UnitSeries.ofCharacter {R : Type u} [CommSemiring R] (χ : HopfAlgebras.ForestAlgebra.Character R) : UnitSeries R

The unit-constant B-series determined by a forest-algebra character.

Equations

• BSeries.Series.UnitSeries.ofCharacter χ = BSeries.Series.characterEquiv.symm χ

noncomputable def BSeries.Series.UnitSeries.toCharacter {R : Type u} [CommSemiring R] (a : UnitSeries R) : HopfAlgebras.ForestAlgebra.Character R

The forest-algebra character determined by a unit-constant B-series.

Equations

• a.toCharacter = BSeries.Series.characterEquiv a

noncomputable def BSeries.Series.UnitSeries.one (R : Type u) [CommSemiring R] : UnitSeries R

The identity unit-constant B-series.

Equations

• BSeries.Series.UnitSeries.one R = 1

noncomputable def BSeries.Series.UnitSeries.mul {R : Type u} [CommSemiring R] (a b : UnitSeries R) : UnitSeries R

Convolution product of unit-constant B-series.

Equations

• a.mul b = a * b

noncomputable def BSeries.Series.UnitSeries.characterMulEquiv {R : Type u} [CommSemiring R] : UnitSeries R ≃* HopfAlgebras.ForestAlgebra.Character R

Unit-constant B-series are multiplicatively equivalent to characters.

Equations

• BSeries.Series.UnitSeries.characterMulEquiv = BSeries.Series.characterMulEquiv

@[simp]

theorem BSeries.Series.UnitSeries.val_ofCharacter {R : Type u} [CommSemiring R] (χ : HopfAlgebras.ForestAlgebra.Character R) : ↑(ofCharacter χ) = Series.ofCharacter χ

@[simp]

theorem BSeries.Series.UnitSeries.toCharacter_ofCharacter {R : Type u} [CommSemiring R] (χ : HopfAlgebras.ForestAlgebra.Character R) : (ofCharacter χ).toCharacter = χ

@[simp]

theorem BSeries.Series.UnitSeries.ofCharacter_toCharacter {R : Type u} [CommSemiring R] (a : UnitSeries R) : ofCharacter a.toCharacter = a

@[simp]

theorem BSeries.Series.UnitSeries.one_eq_one {R : Type u} [CommSemiring R] : one R = 1

@[simp]

theorem BSeries.Series.UnitSeries.mul_eq_mul {R : Type u} [CommSemiring R] (a b : UnitSeries R) : a.mul b = a * b

@[simp]

theorem BSeries.Series.UnitSeries.val_one {R : Type u} [CommSemiring R] : ↑1 = unit R

@[simp]

theorem BSeries.Series.UnitSeries.val_mul {R : Type u} [CommSemiring R] (a b : UnitSeries R) : ↑(a * b) = (↑a).convolution ↑b

@[simp]

theorem BSeries.Series.UnitSeries.toCharacter_one {R : Type u} [CommSemiring R] : toCharacter 1 = HopfAlgebras.ForestAlgebra.Character.unit R

@[simp]

theorem BSeries.Series.UnitSeries.toCharacter_mul {R : Type u} [CommSemiring R] (a b : UnitSeries R) : (a * b).toCharacter = a.toCharacter.convolution b.toCharacter

theorem BSeries.Series.UnitSeries.toCharacter_injective {R : Type u} [CommSemiring R] : Function.Injective toCharacter

theorem BSeries.Series.UnitSeries.ext_toCharacter {R : Type u} [CommSemiring R] {a b : UnitSeries R} (h : a.toCharacter = b.toCharacter) : a = b

noncomputable def BSeries.Series.UnitSeries.inverseLinearFunctional {R : Type u} [CommRing R] (a : UnitSeries R) : HopfAlgebras.ForestAlgebra.LinearFunctional R

The antipode-composed linear functional inverse associated to a unit-constant B-series.

Equations

• a.inverseLinearFunctional = a.toCharacter.inverseLinearFunctional

theorem BSeries.Series.UnitSeries.convolution_inverseLinearFunctional_left {R : Type u} [CommRing R] (a : UnitSeries R) : a.inverseLinearFunctional.convolution (HopfAlgebras.ForestAlgebra.LinearFunctional.ofCharacter a.toCharacter) = HopfAlgebras.ForestAlgebra.LinearFunctional.counit R

theorem BSeries.Series.UnitSeries.convolution_inverseLinearFunctional_right {R : Type u} [CommRing R] (a : UnitSeries R) : (HopfAlgebras.ForestAlgebra.LinearFunctional.ofCharacter a.toCharacter).convolution a.inverseLinearFunctional = HopfAlgebras.ForestAlgebra.LinearFunctional.counit R

theorem BSeries.Series.UnitSeries.mul_left_cancel {R : Type u} [CommRing R] {a b c : UnitSeries R} (h : a * b = a * c) : b = c

theorem BSeries.Series.UnitSeries.mul_right_cancel {R : Type u} [CommRing R] {a b c : UnitSeries R} (h : b * a = c * a) : b = c

theorem BSeries.Series.UnitSeries.mul_left_cancel_iff {R : Type u} [CommRing R] (a b c : UnitSeries R) : a * b = a * c ↔ b = c

theorem BSeries.Series.UnitSeries.mul_right_cancel_iff {R : Type u} [CommRing R] (a b c : UnitSeries R) : b * a = c * a ↔ b = c

@[reducible, inline]

abbrev BSeries.LSeries.UnitSeries (α : Type u) (R : Type v) [One R] : Type (max u v)

Unit-constant labelled B-series.

Equations

• BSeries.LSeries.UnitSeries α R = { a : BSeries.LSeries α R // a.HasUnitConstant }

noncomputable def BSeries.LSeries.UnitSeries.ofCharacter {α : Type u} {R : Type v} [CommSemiring R] (χ : HopfAlgebras.LForestAlgebra.Character α R) : UnitSeries α R

The unit-constant labelled B-series determined by a labelled forest character.

Equations

• BSeries.LSeries.UnitSeries.ofCharacter χ = BSeries.LSeries.characterEquiv.symm χ

noncomputable def BSeries.LSeries.UnitSeries.toCharacter {α : Type u} {R : Type v} [CommSemiring R] (a : UnitSeries α R) : HopfAlgebras.LForestAlgebra.Character α R

The labelled forest character determined by a unit-constant labelled B-series.

Equations

• a.toCharacter = BSeries.LSeries.characterEquiv a

noncomputable def BSeries.LSeries.UnitSeries.one (α : Type u) (R : Type v) [CommSemiring R] : UnitSeries α R

The identity unit-constant labelled B-series.

Equations

• BSeries.LSeries.UnitSeries.one α R = 1

noncomputable def BSeries.LSeries.UnitSeries.mul {α : Type u} {R : Type v} [CommSemiring R] (a b : UnitSeries α R) : UnitSeries α R

Convolution product of unit-constant labelled B-series.

Equations

• a.mul b = a * b

noncomputable def BSeries.LSeries.UnitSeries.characterMulEquiv {α : Type u} {R : Type v} [CommSemiring R] : UnitSeries α R ≃* HopfAlgebras.LForestAlgebra.Character α R

Unit-constant labelled B-series are multiplicatively equivalent to characters.

Equations

• BSeries.LSeries.UnitSeries.characterMulEquiv = BSeries.LSeries.characterMulEquiv

@[simp]

theorem BSeries.LSeries.UnitSeries.val_ofCharacter {α : Type u} {R : Type v} [CommSemiring R] (χ : HopfAlgebras.LForestAlgebra.Character α R) : ↑(ofCharacter χ) = LSeries.ofCharacter χ

@[simp]

theorem BSeries.LSeries.UnitSeries.toCharacter_ofCharacter {α : Type u} {R : Type v} [CommSemiring R] (χ : HopfAlgebras.LForestAlgebra.Character α R) : (ofCharacter χ).toCharacter = χ

@[simp]

theorem BSeries.LSeries.UnitSeries.ofCharacter_toCharacter {α : Type u} {R : Type v} [CommSemiring R] (a : UnitSeries α R) : ofCharacter a.toCharacter = a

@[simp]

theorem BSeries.LSeries.UnitSeries.one_eq_one {α : Type u} {R : Type v} [CommSemiring R] : one α R = 1

@[simp]

theorem BSeries.LSeries.UnitSeries.mul_eq_mul {α : Type u} {R : Type v} [CommSemiring R] (a b : UnitSeries α R) : a.mul b = a * b

@[simp]

theorem BSeries.LSeries.UnitSeries.val_one {α : Type u} {R : Type v} [CommSemiring R] : ↑1 = unit α R

@[simp]

theorem BSeries.LSeries.UnitSeries.val_mul {α : Type u} {R : Type v} [CommSemiring R] (a b : UnitSeries α R) : ↑(a * b) = (↑a).convolution ↑b

@[simp]

theorem BSeries.LSeries.UnitSeries.toCharacter_one {α : Type u} {R : Type v} [CommSemiring R] : toCharacter 1 = HopfAlgebras.LForestAlgebra.Character.unit α R

@[simp]

theorem BSeries.LSeries.UnitSeries.toCharacter_mul {α : Type u} {R : Type v} [CommSemiring R] (a b : UnitSeries α R) : (a * b).toCharacter = a.toCharacter.convolution b.toCharacter

theorem BSeries.LSeries.UnitSeries.toCharacter_injective {α : Type u} {R : Type v} [CommSemiring R] : Function.Injective toCharacter

theorem BSeries.LSeries.UnitSeries.ext_toCharacter {α : Type u} {R : Type v} [CommSemiring R] {a b : UnitSeries α R} (h : a.toCharacter = b.toCharacter) : a = b

noncomputable def BSeries.LSeries.UnitSeries.inverseLinearFunctional {α : Type u} {R : Type v} [CommRing R] (a : UnitSeries α R) : HopfAlgebras.LForestAlgebra.LinearFunctional α R

The antipode-composed linear functional inverse associated to a unit-constant labelled B-series.

Equations

• a.inverseLinearFunctional = a.toCharacter.inverseLinearFunctional

theorem BSeries.LSeries.UnitSeries.convolution_inverseLinearFunctional_left {α : Type u} {R : Type v} [CommRing R] (a : UnitSeries α R) : a.inverseLinearFunctional.convolution (HopfAlgebras.LForestAlgebra.LinearFunctional.ofCharacter a.toCharacter) = HopfAlgebras.LForestAlgebra.LinearFunctional.counit α R

theorem BSeries.LSeries.UnitSeries.convolution_inverseLinearFunctional_right {α : Type u} {R : Type v} [CommRing R] (a : UnitSeries α R) : (HopfAlgebras.LForestAlgebra.LinearFunctional.ofCharacter a.toCharacter).convolution a.inverseLinearFunctional = HopfAlgebras.LForestAlgebra.LinearFunctional.counit α R

theorem BSeries.LSeries.UnitSeries.mul_left_cancel {α : Type u} {R : Type v} [CommRing R] {a b c : UnitSeries α R} (h : a * b = a * c) : b = c

theorem BSeries.LSeries.UnitSeries.mul_right_cancel {α : Type u} {R : Type v} [CommRing R] {a b c : UnitSeries α R} (h : b * a = c * a) : b = c

theorem BSeries.LSeries.UnitSeries.mul_left_cancel_iff {α : Type u} {R : Type v} [CommRing R] (a b c : UnitSeries α R) : a * b = a * c ↔ b = c

theorem BSeries.LSeries.UnitSeries.mul_right_cancel_iff {α : Type u} {R : Type v} [CommRing R] (a b c : UnitSeries α R) : b * a = c * a ↔ b = c