Right principal bundles over a paracompact cylinder are pulled back

Open

QAlgorithms.Papers.Independent.Intakethird100.P59.torsor_cylinder_pullback

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $G$ be a compactly generated topological group and $T$ a compactly generated paracompact space. All principal bundles below are locally trivial right $G$ -bundles in compactly generated spaces. For every such bundle $P\to[0,1]\times T$ , there are a right principal $G$ -bundle $Q\to T$ and a $G$ -equivariant homeomorphism over $[0,1]\times T$ :

P\cong\operatorname{pr}_T^*Q.

The bundle $Q$ need not be trivial. This identifies cylinder families with pullbacks from the parameter space, without requiring connectedness or discreteness of $G$ .

Formalization Note Products, subspaces, and the pullback carry compactly generated topologies. The isomorphism preserves the projection and the right action. The Milnor classifying space mentioned in the source is used in the proof and is not additional input to the statement.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P59

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P59

universe u v

/-- Lemma 7.1, PDF p.12. Every right G-torsor over the cylinder on a
paracompact CGTop space is isomorphic over the cylinder to a pulled-back torsor.
The homeomorphism preserves both the base projection and the right action.
The Milnor space mentioned in the source is a proof tool, not input data. -/
theorem torsor_cylinder_pullback
    (G T E : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactlyGeneratedSpace G] [TopologicalSpace T] [CompactlyGeneratedSpace T]
    [ParacompactSpace T] [TopologicalSpace E] [CompactlyGeneratedSpace E]
    (p : C(E, (Set.Icc (0 : ℝ) 1) × T)) (a : RightAction G E)
    (hp : IsRightPrincipal p a) :
    ∃ (Q : Type u) (tQ : TopologicalSpace Q),
      letI := tQ
      ∃ (_ : CompactlyGeneratedSpace Q) (q : C(Q, T)) (b : RightAction G Q),
        IsRightPrincipal q b ∧
        ∃ h : E ≃ₜ CylinderPullback q,
          (∀ e, (h e).1.1 = p e) ∧
          (∀ e g, (h (a.act e g)).1.2 = b.act (h e).1.2 g) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P59

Source

Mapping stacks of topological stacks, arXiv:0809.2373v2, PDF p. 12, Lemma 7.1

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

Let $G,T,E$ have underlying types in a common universe. Assume that $G$ is a group with a topology for which multiplication and inversion are continuous, that $G,T,E$ are compactly generated topological spaces, and that $T$ is paracompact. Put $I=[0,1]\subseteq\mathbb R$ with its usual topology, and let $p:E\to I\times T$ be continuous, where $I\times T$ has the ordinary product topology. Let $a:E\times G\to E$ satisfy $a(e,1)=e$ and $a(a(e,g),h)=a(e,gh)$ . For this statement, say that a continuous map $f:X\to Y$ and a right action $c$ satisfy the following condition: the map $(x,g)\mapsto c(x,g)$ is continuous from the compactly generated modification of $X\times G$ ; $f(c(x,g))=f(x)$ for every $x,g$ ; and every $y\in Y$ lies in an open subset $U\subseteq Y$ admitting a homeomorphism $\phi:f^{-1}(U)\to U\times G$ such that the underlying first coordinate of $\phi(z)$ equals $f(z)$ , and, for every $z\in f^{-1}(U)$ and $g\in G$ , the point $c(z,g)$ belongs to $f^{-1}(U)$ and

\phi(c(z,g))=\bigl(\phi(z)_1,\phi(z)_2g\bigr).

In this condition, both subspaces $f^{-1}(U)$ and $U$ receive the compactly generated modifications of their subspace topologies, and their displayed product with $G$ receives the compactly generated modification of the resulting product topology. If $p,a$ satisfy this condition, then there exist a type $Q$ in the same universe, a topology on $Q$ making it compactly generated, a continuous map $q:Q\to T$ , and a right action $b:Q\times G\to Q$ satisfying $b(x,1)=x$ and $b(b(x,g),h)=b(x,gh)$ , such that $q,b$ also satisfy the stated condition. Furthermore, there is a homeomorphism

h:E\longrightarrow \left\{((s,t),x)\in(I\times T)\times Q:\ t=q(x)\right\}.

The target topology is obtained by first taking the compactly generated modification of $(I\times T)\times Q$ , with $I\times T$ carrying its ordinary product topology, and then taking the compactly generated modification of the indicated subspace topology. Writing $h(e)=((s_e,t_e),x_e)$ , the homeomorphism satisfies

(s_e,t_e)=p(e),\qquad x_{a(e,g)}=b(x_e,g)

for every $e\in E$ and $g\in G$ . No nonemptiness assumption is imposed on $T$ or $E$ .

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph