The Reidemeister number is monotone under surjection (Remark 1)

Proved

RInf.reid_lift

by Lucas · Oct 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

reidemeister-numbertwisted-conjugacy

If a surjective homomorphism from G onto H intertwines the automorphism of G with the automorphism of H, and the Reidemeister number of the automorphism of H is infinite, then the Reidemeister number of the automorphism of G is infinite: twisted-conjugate elements of G map to twisted-conjugate elements of H, so an infinite sequence of pairwise non-twisted-conjugate elements of H lifts to a sequence of pairwise non-twisted-conjugate elements of G. This is the reduction of Remark 1 that carries infinitude from a quotient back to the group.

Preamble

import Mathlib
import Definitions.Def_RInf_alg
import Definitions.Def_RInf_braid

Formal statement

namespace RInf

/-!  Milestone 1 (Remark 1, after Lemma 2.2 of Dekimpe and Goncalves): the
Reidemeister number is monotone under surjection. If a surjective homomorphism
pi intertwines the automorphism α of G with the automorphism β of H, and the
Reidemeister number of β is infinite, then the Reidemeister number of α is
infinite: twisted-conjugate elements of G map to twisted-conjugate elements of
H, so infinitely many Reidemeister classes of H lift to pairwise distinct
classes of G. This is the reduction that carries infinitude from the
commutator layer quotient back to the braid group. -/
theorem reid_lift {G H : Type*} [Group G] [Group H]
    (pi : G →* H) (hsurj : ∀ y : H, ∃ x : G, pi x = y)
    (α : G ≃* G) (β : H ≃* H) (hcomm : ∀ x : G, pi (α x) = β (pi x))
    (hβ : ReidInf β.toMonoidHom) : ReidInf α.toMonoidHom := by sorry

end RInf

Source

K. Dekimpe, D. L. Goncalves, O. Ocampo, The R-infinity property for pure Artin braid groups, Monatshefte fur Mathematik 195 (2021) 15-33, Section 2 (Remark 1).

Read-back

What the Lean code literally says, in plain math · glm-5-latest-short

Restate: given a surjective homomorphism from G to H, an automorphism of G and an automorphism of H that commute with the homomorphism in the sense that the homomorphism composed with the first equals the second composed with the homomorphism, if the Reidemeister number of the automorphism of H is infinite then so is the Reidemeister number of the automorphism of G. Hypotheses: surjectivity and the intertwining equation.

View graph