Bibundle triviality is unit type plus trivial kernel reduction

Open

QAlgorithms.Papers.Independent.Intakethird100.P93.corollary_3_6

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.

Let $P\to M$ be an $(H,G)$ -bibundle with structure map $\psi$ , and put $P_1=\psi^{-1}(1)$ . Then

P\text{ is trivial as an }(H,G)\text{-bibundle} \iff \operatorname{Type}(P)\equiv1\ \text{and }P_1\text{ is trivial as a }G_1\text{-bundle}.

Triviality on the left means an equivariant homeomorphism over $M$ with $M\times G$ preserving the structure map $t$ on the second coordinate. Triviality of $P_1$ means an equivariant homeomorphism over $M$ with $M\times G_1$ ; it is not assumed to be a principal bundle before unit type is known. This tests bibundle triviality with its structure map retained.

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)

/-- Corollary 3.6, PDF p.11. 'Trivial' preserves the bibundle structure.
The preceding text's (1,t(G)) is corrected to (1,ker(t)), as required by
Lemma 2.10 and the reconstruction on the same page. The empty base is allowed. -/
theorem corollary_3_6 {M P : Type u} [TopologicalSpace M] [TopologicalSpace P]
    (B : Bibundle C M P) :
    IsTrivialBibundle C B ↔ HasUnitType C B ∧ IsTrivialUnitLevel C B := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P93

Source

On the existence of bibundles, arXiv:1102.4388v2, PDF p. 11, Corollary 3.6

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)$ with continuous evaluation $(h,g)\mapsto\alpha(h)(g)$ , satisfying $t(\alpha(h)(g))=ht(g)h^{-1}$ and $\alpha(t(g))(k)=gkg^{-1}$ for all $h,g,k$ . Assume that $G\to G/\ker t$ and $H\to H/t(G)$ each have a continuous section on an open neighbourhood of every target point. Let $M,P$ be topological spaces, and let $B$ consist of a continuous right $G$ -action on $P$ , a continuous action-invariant map $\pi:P\to M$ , and a continuous map $\psi:P\to H$ satisfying $\psi(p\cdot g)=\psi(p)t(g)$ . Assume that each $m\in M$ has an open neighbourhood $U$ and a homeomorphism $\pi^{-1}(U)\to U\times G$ preserving the base coordinate and carrying the action to right multiplication on the $G$ -coordinate. Write $K=\ker t$ and $P_1=\{p\in P:\psi(p)=1\}$ , with their subspace topologies. There exists a homeomorphism $e:P\to M\times G$ such that, for every $p\in P$ and $g\in G$ , its coordinates satisfy $e_1(p)=\pi(p)$ , $e(p\cdot g)=(e_1(p),e_2(p)g)$ , and $t(e_2(p))=\psi(p)$ , if and only if both $[\psi(p)]=[1]$ in $H/t(G)$ for every $p\in P$ , and there exists a homeomorphism $d:P_1\to M\times K$ with $d_1(p)=\pi(p)$ and $d(p\cdot k)=(d_1(p),d_2(p)k)$ for every $p\in P_1$ and $k\in K$ for which $p\cdot k\in P_1$ . In this last formula the action uses the underlying element of $G$ ; the equivariance of $\psi$ ensures that $p\cdot k\in P_1$ always holds. No nonemptiness of $M$ is assumed; an empty base forces $P$ to be 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