Rota–Baxter operators [UPSTREAM]

A Rota–Baxter operator of weight λ on a k-algebra A is a k-linear endomorphism R satisfying R a * R b = R (R a * b + a * R b + λ • (a * b)). For λ = -1 this is the operator of [MCB25]'s Definition 3.1.1, written there as R(a) R(b) = R(a R(b)) + R(R(a) b) − R(a b); the prototype is the algebra of Laurent series with R the projection onto the polar (divergent) part.

Rota–Baxter operators of weight -1 are the algebraic substrate of Connes–Kreimer renormalization: on a connected graded Hopf algebra they drive the Birkhoff factorization of a character (the Bogolyubov recursion), which [MCB25] use to package semantic-consistency checking "into a single map, which recursively modifies an initially chosen assignment of semantic values so as to incorporate the consistency checking over all substructures."

Main definitions

• RotaBaxter k A lam: a k-linear R : A → A with the weight-lam identity.
• RotaBaxter.rangeMulClosed: R a * R b ∈ range R — the range is closed under multiplication.
• RotaBaxter.complement: for weight -1, 1 - R is again a weight--1 Rota–Baxter operator (the complementary projection that gives the splitting A = range R ⊕ range (1 - R)).
• RotaBaxterSemiring ℛ: the weight +1 operator on a commutative semiring ([MCB25] Def. 3.1.2), for settings where addition is not invertible (tropical, Viterbi, Boolean parsing) — here the divergence term op (a * b) cannot be moved across the identity, so weight +1 and weight -1 are genuinely distinct.

References

[MCB25] (Def. 3.1.1, Def. 3.1.2, Prop. 3.1.7)

structure RotaBaxter (k : Type u_1) (A : Type u_2) [CommRing k] [CommRing A] [Algebra k A] (lam : k) : Type u_2

A Rota–Baxter operator of weight lam on the k-algebra A: a k-linear endomorphism op satisfying op a * op b = op (op a * b + a * op b + lam • (a * b)) ([MCB25] Def. 3.1.1 is the lam = -1 case).

• op : A →ₗ[k] A

  The underlying k-linear operator.

• rotaBaxter (a b : A) : self.op a * self.op b = self.op (self.op a * b + a * self.op b + lam • (a * b))

  The Rota–Baxter identity of weight lam.

theorem RotaBaxter.op_mul_op {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] {lam : k} (R : RotaBaxter k A lam) (a b : A) : R.op a * R.op b = R.op (R.op a * b + a * R.op b + lam • (a * b))

theorem RotaBaxter.rangeMulClosed {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] {lam : k} (R : RotaBaxter k A lam) {a b : A} (ha : a ∈ R.op.range) (hb : b ∈ R.op.range) : a * b ∈ R.op.range

The range of a Rota–Baxter operator is closed under multiplication: R a * R b ∈ range R. This is the algebraic heart of the splitting ([MCB25] Prop. 3.1.7, "these are subalgebras ... because of the Rota–Baxter identity satisfied by R").

def RotaBaxter.id {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] : RotaBaxter k A (-1)

Identity is Rota–Baxter of weight -1 ([MCB25] Rem. 3.2.2: the scheme R = id used in the tropical/min-plus toy model).

Equations

• RotaBaxter.id = { op := LinearMap.id, rotaBaxter := ⋯ }

def RotaBaxter.zero {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] {lam : k} : RotaBaxter k A lam

The zero operator is Rota–Baxter of every weight.

Equations

• RotaBaxter.zero = { op := 0, rotaBaxter := ⋯ }

def RotaBaxter.complement {k : Type u_1} {A : Type u_2} [CommRing k] [CommRing A] [Algebra k A] (R : RotaBaxter k A (-1)) : RotaBaxter k A (-1)

The complementary operator. For a weight--1 Rota–Baxter operator R, the operator 1 - R is again Rota–Baxter of weight -1. When R is idempotent this is the complementary projection, giving the splitting A = range R ⊕ range (1 - R) into the two subalgebras of the Birkhoff factorization ([MCB25] Prop. 3.1.7).

Equations

• R.complement = { op := LinearMap.id - R.op, rotaBaxter := ⋯ }

Rota–Baxter operators on semirings

structure RotaBaxterSemiring (ℛ : Type u_3) [CommSemiring ℛ] : Type u_3

A Rota–Baxter operator of weight +1 on a commutative semiring ([MCB25] Def. 3.1.2): an additive op : ℛ → ℛ satisfying op a * op b = op (a * op b) + op (op a * b) + op (a * b). The semiring analogue of RotaBaxter (weight -1) for settings where addition is not invertible — tropical (ℝ ∪ {−∞}, max, +), Viterbi, and Boolean parsing semirings. Because there is no subtraction, the divergence term op (a * b) cannot be moved across the identity, so the weight +1 and weight -1 semiring operators are genuinely different operators.

• op : ℛ →+ ℛ

  The underlying additive operator.

• rotaBaxter (a b : ℛ) : self.op a * self.op b = self.op (a * self.op b) + self.op (self.op a * b) + self.op (a * b)

  The weight-+1 Rota–Baxter identity.

theorem RotaBaxterSemiring.op_mul_op {ℛ : Type u_3} [CommSemiring ℛ] (R : RotaBaxterSemiring ℛ) (a b : ℛ) : R.op a * R.op b = R.op (a * R.op b) + R.op (R.op a * b) + R.op (a * b)

theorem RotaBaxterSemiring.rangeMulClosed {ℛ : Type u_3} [CommSemiring ℛ] (R : RotaBaxterSemiring ℛ) {a b : ℛ} (ha : a ∈ Set.range ⇑R.op) (hb : b ∈ Set.range ⇑R.op) : a * b ∈ Set.range ⇑R.op

The range of a weight-+1 Rota–Baxter semiring operator is closed under multiplication: R a * R b ∈ range R, since R a * R b = R (a * R b + R a * b + a * b). The semiring analogue of RotaBaxter.rangeMulClosed — the algebraic heart of the splitting into "meaningful" and "meaningless" subsemirings.