The Reidemeister number is monotone under extension by a normal invariant subgroup (Lemma 2.2)

Disproved

RInf.reid_extend

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

normal-subgroupsreidemeister-number

If the group H embeds into G with normal image, the automorphism of H is the restriction of the automorphism of G, and the Reidemeister number of the automorphism of H is infinite, then the Reidemeister number of the automorphism of G is infinite. Together with the surjection monotonicity this is the abstract justification of the transfer design that carries infinitude from the commutator layer to the braid group.

Preamble

import Mathlib
import Definitions.Def_RInf_alg
import Definitions.Def_RInf_braid

Formal statement

namespace RInf

/-!  Milestone 7 (Lemma 2.2 of Dekimpe and Goncalves): the Reidemeister
number is monotone under extension by a normal invariant subgroup. If H embeds
into G with normal image, the automorphism β of H is the restriction of the
automorphism α of G, and the Reidemeister number of β is infinite, then the
Reidemeister number of α is infinite. Together with milestone 1 this is the
abstract justification of the transfer design of the world, which carries the
infinitude from the commutator layer to the braid group. -/
theorem reid_extend {H G : Type*} [Group H] [Group G]
    (inj : H →* G) (hinj : ∀ x y : H, inj x = inj y → x = y)
    (hnorm : ∀ (g : G) (x : H), ∃ y : H, inj y = g * inj x * g⁻¹)
    (α : G ≃* G) (β : H ≃* H) (hcomm : ∀ x : H, inj (β x) = α (inj 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 (Lemma 2.2 of Dekimpe and Goncalves).

Read-back

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

Restate: if H embeds into G with injective image normalized by every element of G, and the automorphism of G restricts, through the embedding, to the automorphism of H, and the Reidemeister number of the latter is infinite, then the Reidemeister number of the former is infinite. Hypotheses: injectivity of the embedding, normality of the image, and the restriction equation.

View graph