The Klein bottle classes with the Borsuk-Ulam property are exactly the classes that lift to the torus (Theorem 3)

Disproved

BUP.thm3_lifts

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

borsuk-ulamcovering-spacesklein-bottle

In the idealized Klein bottle world with its double covering by the torus, the homotopy class with induced homomorphism h does not have the Borsuk-Ulam property if and only if h lifts through the covering: every value of h lies in the image of the covering injection of the torus. A class of the Klein bottle has the Borsuk-Ulam property with respect to the free involution exactly when it lifts to the torus. The proof separates the homomorphisms of the Klein bottle group according to the type analysis of Proposition 35: the non-liftable ones admit the explicit witnesses of Proposition 38, while the liftable ones inherit the Borsuk-Ulam property from the triple of the Klein bottle, the involution, and the torus as in Proposition 39.

Preamble

import Mathlib
import Definitions.Def_BUP_alg
import Definitions.Def_BUP_tor

Formal statement

namespace BUP

/-!  The goal (Theorem 3, from Propositions 38 and 39): the classification of
the homotopy classes of selfmaps of the Klein bottle that have the
Borsuk-Ulam property with respect to a free involution. In the idealized Klein
bottle world, the homotopy class with induced homomorphism h does not have the
Borsuk-Ulam property if and only if h does not lift through the double
covering of the Klein bottle by the torus: a class has the Borsuk-Ulam
property exactly when every value of its induced homomorphism lies in the
image of the covering injection. The proof separates the homomorphisms of the
Klein bottle group according to the type analysis of Proposition 35: the
non-liftable ones admit the explicit witnesses of Proposition 38, while the
liftable ones inherit the Borsuk-Ulam property from the triple of the Klein
bottle, the involution, and the torus as in Proposition 39. -/
theorem thm3_lifts {A B P Bg T : Type*} [Group A] [Group B] [Group P] [Group Bg] [Group T]
    (W : KleinWorld A B P Bg T) (h : A →* A) :
    NoBUP W.C W.D h ↔ ¬ W.LiftsTor 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 6 (Theorem 3, from Propositions 35, 38, and 39).

Read-back

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

Restate: in a Klein bottle world with its double covering by the torus, the homotopy class with induced homomorphism h does not have the Borsuk-Ulam property if and only if h lifts through the covering: every value of h lies in the image of the covering injection of the torus. Hypotheses: the Klein bottle world is given; no further hypotheses appear.

View graph