Extension detects trivial kernel bundles

Open

QAlgorithms.Papers.Independent.Intakethird100.P93.proposition_3_7

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.

For any principal $G_1$ -bundle $Q\to M$ , form the actual quotient extension $\iota(Q)=Q\times_{G_1}G$ with structure map $\psi([q,g])=t(g)$ . Then

Q\text{ is trivial as a }G_1\text{-bundle} \iff\iota(Q)\text{ is trivial as an }(H,G)\text{-bibundle}.

On the right the trivialization must preserve the structure map as well as the base and right action. The conclusion therefore detects the original kernel-bundle triviality, rather than the weaker triviality of an underlying $G$ -bundle.

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.7, PDF p.11: ordinary G1-bundle triviality is equivalent to
bibundle triviality of the actual quotient extension, including its structure map. -/
theorem proposition_3_7 {M Q : Type u} [TopologicalSpace M] [TopologicalSpace Q]
    (R : PrincipalBundle C.t.ker M Q) :
    IsTrivialPrincipal R ↔ IsTrivialIota C R := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P93

Source

On the existence of bibundles, arXiv:1102.4388v2, PDF p. 11, Proposition 3.7

Read-back

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

Let $G,H$ be topological groups, with 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 both quotient maps $G\to G/\ker t$ and $H\to H/t(G)$ admit continuous sections on open neighborhoods of every target point, meaning that the quotient of each section is the inclusion of its neighborhood. Put $K=\ker t$ . For arbitrary topological spaces $M,Q$ , let $R$ consist of a continuous right $K$ -action on $Q$ , satisfying the identity and multiplication laws, and a continuous invariant projection $\pi:Q\to M$ , with, around every $m\in M$ , an open neighborhood $U$ and a homeomorphism $\pi^{-1}(U)\cong U\times K$ preserving the projection and carrying the action to right multiplication on $K$ . Let $E=(Q\times G)/{\sim}$ , where $(q,g)\sim(q\cdot k,k^{-1}g)$ for $k\in K$ , and write $[q,g]$ for a class. Then the following two existence statements are equivalent: there is a homeomorphism $a:Q\to M\times K$ satisfying $\operatorname{pr}_M a(q)=\pi(q)$ and $a(q\cdot k)=(\operatorname{pr}_M a(q),\operatorname{pr}_K a(q)\,k)$ for every $q,k$ ; and there is a homeomorphism $e:E\to M\times G$ satisfying, for all $q\in Q$ and $g,b\in G$ ,

\operatorname{pr}_M e([q,g])=\pi(q),\qquad e([q,gb])=\bigl(\operatorname{pr}_M e([q,g]),\operatorname{pr}_G e([q,g])\,b\bigr),\qquad t\bigl(\operatorname{pr}_G e([q,g])\bigr)=t(g).

The equivalence includes the empty-base case, when $Q$ and $E$ are necessarily empty.

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