Contractible H supplies bibundle structures

Open

QAlgorithms.Papers.Independent.Intakethird100.P93.proposition_3_16

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

prove2quantum

Let $t:G\to H$ be a topological crossed module, with continuous action $\alpha:H\to\operatorname{Aut}(G)$ . Thus $t(\alpha(h)g)=ht(g)h^{-1}$ and $\alpha(t(g))k=gkg^{-1}$ . Put $G_1=\ker t$ and give both $G/G_1$ and $H/t(G)$ their quotient topologies. Assume their quotient projections admit continuous local sections. All actions, structure maps and isomorphisms below are continuous, all principal bundles are locally trivial, and a bispace has a nonempty principal homogeneous underlying right space.

Assume that $H$ is contractible as an ordinary topological space. Let $M$ be paracompact Hausdorff and let $P\to M$ be any locally trivial principal $G$ -bundle. Then there exists a continuous structure map

\psi:P\to H,\qquad \psi(pg)=\psi(p)t(g),

so that the given principal bundle admits an $(H,G)$ -bibundle structure. The classifying context ensures numerability, and neither a prior structure map nor a classifying-map lift is assumed. Contractibility of $H$ , not of $G$ , is the required hypothesis.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P93

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P93

universe u

variable {G H : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
  [Group H] [TopologicalSpace H] [IsTopologicalGroup H]

variable (C : CrossedModule G H)

/-- Proposition 3.16, PDF p.23. Contractibility is ordinary contractibility of H.
The conclusion supplies a continuous structure map on the given principal bundle;
no preassigned lift, section, or bibundle structure is assumed. -/
theorem proposition_3_16 {M P : Type u} [TopologicalSpace M] [ParacompactSpace M]
    [T2Space M] [TopologicalSpace P] [ContractibleSpace H]
    (R : PrincipalBundle G M P) :
    ∃ psi : C(P, H), ∀ p g, psi (R.right.act p g) = psi p * C.t g := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P93

Source

On the existence of bibundles, arXiv:1102.4388v2, PDF p. 23, Proposition 3.16

Read-back

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

Let $G,H$ be topological groups, and let $C$ consist of a continuous homomorphism $t:G\to H$ and a homomorphism $\alpha:H\to\operatorname{Aut}(G)$ whose evaluation is continuous, satisfying $t(\alpha_h(g))=h\,t(g)\,h^{-1}$ and $\alpha_{t(g)}(k)=gkg^{-1}$ for all $h\in H$ and $g,k\in G$ . Assume that each quotient map $G\to G/\ker t$ and $H\to H/t(G)$ admits continuous sections on open neighborhoods of every target point, with quotient equal to inclusion, and assume that the topological space $H$ is contractible. Let $M$ be any paracompact Hausdorff topological space, let $P$ be any topological space, and let $R$ be a principal $G$ -bundle over $M$ : it has a continuous right action $p\cdot g$ satisfying $p\cdot1=p$ and $(p\cdot g)\cdot k=p\cdot(gk)$ , a continuous projection $\pi:P\to M$ satisfying $\pi(p\cdot g)=\pi(p)$ , and, around every $m\in M$ , an open neighborhood $U$ with a homeomorphism $\pi^{-1}(U)\cong U\times G$ preserving the projection and carrying the action to right multiplication on the second factor. Then there exists a continuous map $\psi:P\to H$ such that

\psi(p\cdot g)=\psi(p)\,t(g) \qquad\text{for every }p\in P,\ g\in G.

No uniqueness is asserted. The empty base is permitted; then $P$ is necessarily empty and the equivariance condition is vacuous.

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