Rota–Baxter operators

A map P : A → A is a Rota–Baxter operator of weight θ if P a * P b = P (P a * b + a * P b + θ • (a * b)) for all a b. The projection of Laurent series onto their polar part has weight -1. Over a semiring, whose addition is not invertible, the operators of interest have weight +1; over a ring the two are exchanged by P ↦ -P.

The identity makes the ranges of P and of θ • id + P closed under multiplication. For an idempotent operator of weight -1 these are the two subalgebras of the splitting of A on which the algebraic Birkhoff factorization of renormalization rests.

Main definitions

• IsRotaBaxter θ P: P satisfies the Rota–Baxter identity of weight θ.

Main results

• IsRotaBaxter.mul_mem_range, IsRotaBaxter.mul_mem_range_smul_add: the ranges of P and of θ • id + P are closed under multiplication.
• IsRotaBaxter.neg: if the additive map P has weight θ, then -P has weight -θ.

Implementation notes

IsRotaBaxter is a predicate on functions, so it applies to additive and linear maps alike, and a construction that never uses the identity, such as the Bogolyubov recursion ConnesKreimer.birkhoffMinus, takes the bare operator. The weight ±1 forms isRotaBaxter_one_iff and isRotaBaxter_neg_one_iff do not mention the scalars, which lets a weight move between scalar rings.

References

• [EFGK04]
• [MT15]

def IsRotaBaxter {k : Type u_1} {A : Type u_2} [Add A] [Mul A] [SMul k A] (θ : k) (P : A → A) : Prop

P is a Rota–Baxter operator of weight θ if P a * P b = P (P a * b + a * P b + θ • (a * b)) for all a b.

Equations

• IsRotaBaxter θ P = ∀ (a b : A), P a * P b = P (P a * b + a * P b + θ • (a * b))

theorem IsRotaBaxter.mul_mem_range {k : Type u_1} {A : Type u_2} [Add A] [Mul A] [SMul k A] {θ : k} {P : A → A} {a b : A} (h : IsRotaBaxter θ P) (ha : a ∈ Set.range P) (hb : b ∈ Set.range P) : a * b ∈ Set.range P

The range of a Rota–Baxter operator is closed under multiplication.

theorem isRotaBaxter_one_iff {k : Type u_1} {A : Type u_2} [Add A] [Mul A] [Monoid k] [MulAction k A] {P : A → A} : IsRotaBaxter 1 P ↔ ∀ (a b : A), P a * P b = P (P a * b + a * P b + a * b)

theorem IsRotaBaxter.mul_mem_range_smul_add {k : Type u_1} {A : Type u_2} [Monoid k] [NonUnitalNonAssocSemiring A] [DistribMulAction k A] [IsScalarTower k A A] [SMulCommClass k A A] {θ : k} {P : A → A} {a b : A} (h : IsRotaBaxter θ P) (ha : a ∈ Set.range fun (x : A) => θ • x + P x) (hb : b ∈ Set.range fun (x : A) => θ • x + P x) : a * b ∈ Set.range fun (x : A) => θ • x + P x

The range of θ • id + P is closed under multiplication when P has weight θ: the product of the values at x and y is the value at P x * y + x * P y + θ • (x * y).

theorem isRotaBaxter_neg_one_iff {k : Type u_1} {A : Type u_2} [Ring k] [NonUnitalNonAssocRing A] [Module k A] {P : A → A} : IsRotaBaxter (-1) P ↔ ∀ (a b : A), P a * P b = P (P a * b + a * P b - a * b)

theorem IsRotaBaxter.neg {k : Type u_1} {A : Type u_2} [Ring k] [NonUnitalNonAssocRing A] [Module k A] {θ : k} {P : A →+ A} (h : IsRotaBaxter θ ⇑P) : IsRotaBaxter (-θ) ⇑(-P)

If P is an additive Rota–Baxter operator of weight θ, then -P has weight -θ.