Conjugation-equivalent homomorphisms satisfy the same diagram condition (Proposition 7(1))

Proved

BUP.homotopy_invariance

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

borsuk-ulamfundamental-groupshomotopy

If two homomorphisms of the fundamental group of the surface are equivalent in the sense of Section 2 - one is obtained from the other by conjugation with a loop - then one admits the commutative diagram of Proposition 6 with respect to the given involution extension and braid data if and only if the other does. The property of not having the Borsuk-Ulam property is thus invariant under the conjugation equivalence, and so is a property of the free homotopy class rather than of the pointed homotopy class.

Preamble

import Mathlib
import Definitions.Def_BUP_alg
import Definitions.Def_BUP_tor

Formal statement

namespace BUP

/-!  Milestone 1 (Proposition 7(1)): the Borsuk-Ulam diagram condition is
invariant under the conjugation equivalence of induced homomorphisms of
Section 2. If two homomorphisms of the fundamental group are equivalent - one
is obtained from the other by conjugation with a loop - then one admits the
commutative diagram of Proposition 6 if and only if the other does. The proof
lifts the conjugating loop to the pure braid group using the surjectivity of
the Fadell-Neuwirth projection and conjugates both legs of the diagram. -/
theorem homotopy_invariance {A B P Bg : Type*} [Group A] [Group B] [Group P] [Group Bg]
    (C : InvSES A B) (D : BraidData A P Bg) (h1 h2 : A →* A)
    (hequiv : homEquiv h1 h2) :
    NoBUP C D h1 ↔ NoBUP C D h2 := by sorry

end BUP

Source

D. L. Goncalves, J. Guaschi, V. C. Laass, The Borsuk-Ulam property for homotopy classes of selfmaps of surfaces of Euler characteristic zero, arXiv:1608.00397 (2016), Section 2 (Proposition 7(1)).

Read-back

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

Restate: given the involution extension C and the braid data D, and two homomorphisms h1 and h2 of the fundamental group that are conjugation equivalent in the sense of Section 2 - one is obtained from the other by conjugation with a loop - the homomorphism h1 admits the commutative diagram of Proposition 6 if and only if h2 does. Hypotheses: h1 and h2 are equivalent under the conjugation equivalence of the interface.

View graph