Rota–Baxter operators on groups

DefinitionRota–Baxter operators on groups#✓fully proved

A Rota–Baxter operator (of weight \(1\)) on a group \(G\) is a map \(B \colon G \to G\) such that \(B(g)\,B(h) = B\bigl(g\,B(g)\,h\,B(g)^{-1}\bigr)\) for all \(g, h \in G\).

def IsRotaBaxterOperator {G : Type} [Group G] (B : G → G) : Prop :=
  ∀ g h : G, B g * B h = B (g * B g * h * (B g)⁻¹)
Used by 1

DefinitionKourovka Problem 20.125 (surjective non-injective Rota–Baxter operators)#✓fully proved

The statement, asked by V. G. Bardakov, that there exist a non-abelian group \(G\) and a Rota–Baxter operator \(B\) on \(G\) such that \(B\) is surjective but not injective.

def surjectiveNonInjectiveRotaBaxterOperatorExists : Prop :=
  ∃ (G : Type) (_ : Group G), (∃ x y : G, x * y ≠ y * x) ∧
    ∃ B : G → G, IsRotaBaxterOperator B ∧ Function.Surjective B ∧ ¬ Function.Injective B
Uses 1 · Used by 1

TheoremA surjective, non-injective Rota–Baxter operator on a non-abelian group#●ready to prove

There exist a non-abelian group \(G\) and a Rota–Baxter operator \(B\) on \(G\) that is surjective but not injective.

For example, van Doorn, Judin, Monticone and Morrison take \(G = S_3 \times \mathbb{Z}^{\mathbb{N}}\) and \(B(\sigma, f) = (\sigma^{-1}, s(f))\), where \(s\) is the left shift.

public theorem_wanted surjectiveNonInjectiveRotaBaxterOperatorExists_holds :
    surjectiveNonInjectiveRotaBaxterOperatorExists
Sources
  • E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Problem 20.125 (V. G. Bardakov); resolution: P. Monticone, Kourovka Notebook Problem 20.125, solution note, 23 March 2026; W. van Doorn, E. Judin, P. Monticone and D. Morrison, On some problems from the Kourovka Notebook, preprint, arXiv:2607.17477 (2026), van Doorn-Judin-Monticone-Morrison, Theorem 5.1: G = S3 × Z^N with B(σ, f) = (σ⁻¹, s(f)), s the left shift; the Kourovka Notebook (21st issue) marks 20.125 solved (AI solution confirmed by V. G. Bardakov), https://arxiv.org/abs/2607.17477.
Uses 1
2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.