Transport of the diagram condition along equivalence of free involutions (Propositions 9 and 10)

Proved

BUP.world_transport

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

borsuk-ulamfree-involutionsshort-exact-sequences

If two involution extensions and two braid data are intertwined by isomorphisms - of the surface groups, the orbit groups, the pure braid groups, and the full braid groups - compatible with the covering injections, the deck projections, the braid inclusions, the braid projections, and the Fadell-Neuwirth projections, and the homomorphisms h and h' correspond under the isomorphism of the surface groups, then h admits the diagram of Proposition 6 in the first world if and only if h' does in the second. By Proposition 10 the equivalence classes of free involutions of a surface correspond to the equivalence classes of the induced short exact sequences, so this is the algebraic counterpart of the invariance of the Borsuk-Ulam property under equivalence of the free involutions.

Preamble

import Mathlib
import Definitions.Def_BUP_alg
import Definitions.Def_BUP_tor

Formal statement

namespace BUP

/-!  Milestone 2 (Propositions 9 and 10): the Borsuk-Ulam diagram condition is
invariant under transport along isomorphisms of the involution extension and
the braid data. If two involution extensions and two braid data are intertwined
by isomorphisms - of the surface groups, the orbit groups, the pure braid
groups, and the full braid groups - compatible with the injections, the deck
projections, the braid inclusions, the braid projections, and the
Fadell-Neuwirth projections, and the homomorphisms h and h' correspond under
the isomorphism of the surface groups, then h admits the diagram of
Proposition 6 if and only if h' does. This is the algebraic counterpart of the
invariance of the Borsuk-Ulam property under equivalence of the free
involutions. -/
theorem world_transport {A B P Bg A' B' P' Bg' : Type*} [Group A] [Group B] [Group P] [Group Bg]
    [Group A'] [Group B'] [Group P'] [Group Bg']
    (C : InvSES A B) (D : BraidData A P Bg) (C' : InvSES A' B') (D' : BraidData A' P' Bg')
    (eA : A ≃* A') (eB : B ≃* B') (eP : P ≃* P') (eBg : Bg ≃* Bg')
    (hc1 : ∀ a : A, eB (C.inj a) = C'.inj (eA a))
    (hc2 : ∀ b : B, C'.proj (eB b) = C.proj b)
    (hb1 : ∀ p : P, eBg (D.iota p) = D'.iota (eP p))
    (hb2 : ∀ g : Bg, D'.piBr (eBg g) = D.piBr g)
    (hb3 : ∀ p : P, eA (D.p1 p) = D'.p1 (eP p))
    (h : A →* A) (h' : A' →* A')
    (hcomm : ∀ a : A, eA (h a) = h' (eA a)) :
    NoBUP C D h ↔ NoBUP C' D' h' := 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 (Propositions 9 and 10).

Read-back

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

Restate: given two involution extensions C and C' and two braid data D and D', with isomorphisms of the surface groups, the orbit groups, the pure braid groups, and the full braid groups compatible with the injections, the deck projections, the braid inclusions, the braid projections, and the Fadell-Neuwirth projections, and homomorphisms h and h' that correspond under the isomorphism of the surface groups, the homomorphism h admits the diagram of Proposition 6 in the first world if and only if h' does in the second. Hypotheses: the five compatibility families and the correspondence of h and h'.

View graph