The lexicographic cone is invariant under conjugation (Theorem 4 (iii))
ProvedPCB.lex_cone_conjalmost-direct-productsconjugationpositive-cones
The lexicographic cone is invariant under conjugation. Conjugation acts componentwise on the normal form through the cone-preserving action of the ambient group on each free factor, so the highest nontrivial component of a conjugate of a positive element is again positive. This is Theorem 4 (iii) of the paper, the ingredient that makes the lexicographic ordering bi-invariant.
Preamble
import Mathlib import Definitions.Def_PCB_alg import Definitions.Def_PCB_tor
Formal statement
namespace PCB
/-! Milestone 3 (Theorem 4 (iii)): the lexicographic cone is invariant
under conjugation. Conjugation acts componentwise through the
cone-preserving action on each free factor, and the almost-direct property
makes the action preserve the Magnus-type cone, so the highest nontrivial
component of a conjugate of a positive element is again positive. -/
theorem lex_cone_conj {k : ℕ} {G : Type*} [Group G] {F : Fin k → Type*} [∀ j, Group (F j)]
(W : AlmostDirectProductWorld k G F) :
∀ g ∈ lexCone W, ∀ x : G, x * g * x⁻¹ ∈ lexCone W := by sorry
end PCB
Source
O. Ocampo, J. R. T. Theodoro de Lima, Positive cones and bi-orderings on almost-direct products of free groups, arXiv:2209.04706 (2022), Section 2 (Theorem 4 (iii)).
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: in an almost-direct product world, every conjugate of an element of the lexicographic cone by any element of the group lies in the lexicographic cone. Hypotheses: the world is given; the conjugated element lies in the cone; no further hypotheses appear.