Injective boundary determines every bibundle by its type

Open

QAlgorithms.Papers.Independent.Intakethird100.P93.corollary_3_4

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 $G_1=\{1\}$ . The canonical projection identifies $G$ topologically and as a group with $t(G)=G/G_1$ . For every $(H,G)$ -bibundle $\pi:P\to M$ with structure map $\psi$ and type map $\varphi$ , the canonical map gives

G\cong t(G),\qquad P\xrightarrow{\ \cong\ }\varphi^*H,\quad p\longmapsto(\pi(p),\psi(p)).

The second isomorphism preserves projection, right action and structure map. Both conclusions depend on the trivial-kernel assumption; no compactness or nonempty-base assumption is added.

Source correction: additionally require that the canonical map $\bar t:G/\ker(t)\to H$ is topologically inducing, so the quotient topology agrees with the subspace topology on $t(G)$ . The printed local-section assumptions alone do not imply this; see correction.printed/changed/why and MODERATION-r1.md.

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.4, PDF p.11, both conclusions. With trivial kernel the
canonical G→G/ker(t)=t(G) is a topological group isomorphism, and the actual
map p↦(pi(p),psi(p)) identifies every bibundle with the type pullback. 
Source correction (topology): Printed: the claim uses the p.4 local-section
assumptions and identifies t(G)=G/ker(t) on p.7. Changed: htop explicitly
identifies the quotient topology with the image subspace topology. Why: those
local-section assumptions alone allow the identity R_discrete -> R_usual;
its inverse is not continuous. No closed-image condition is added.
-/
theorem corollary_3_4 (htop : Topology.IsInducing (QuotientGroup.kerLift C.t))
    {M P : Type u} [TopologicalSpace M] [TopologicalSpace P]
    (hker : C.t.ker = ⊥) (B : Bibundle C M P) :
    (∃ e : G ≃ₜ (G ⧸ C.t.ker),
      (∀ g, e g = QuotientGroup.mk g) ∧ ∀ g k, e (g * k) = e g * e k) ∧
    (∃ phi : C(M, TypeGroup C),
      (∀ p, phi (B.bundle.proj p) = typeProjection C (B.psi p)) ∧
      ∃ e : P ≃ₜ TypePullback C phi,
        (∀ p, (e p).val = (B.bundle.proj p, B.psi p)) ∧
        (∀ p g, (e (B.bundle.right.act p g)).val =
          (B.bundle.proj p, B.psi p * C.t g))) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P93

Source

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

Read-back

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

Let $G,H$ be topological groups in a common universe, and let $C$ consist of a continuous homomorphism $t:G\to H$ and a homomorphism $\alpha:H\to\operatorname{Aut}(G)$ with continuous evaluation, satisfying $t(\alpha_h(g))=h\,t(g)\,h^{-1}$ and $\alpha_{t(g)}(k)=gkg^{-1}$ for all $h,g,k$ . Put $K=\ker t$ , $T=H/t(G)$ , and let $\rho:H\to T$ be the quotient map. Assume, as part of $C$ , that each of $G\to G/K$ and $\rho$ has, on an open neighbourhood of every point of its codomain, a continuous section whose composition with the quotient map is the identity. Assume also that the topology on $G/K$ is induced by $gK\mapsto t(g)$ into $H$ , and that $K=\{1_G\}$ . Let $M,P$ be arbitrary topological spaces in the same universe, and let $B$ supply a continuous right $G$ -action $p\cdot g$ , an invariant continuous projection $\pi:P\to M$ , equivariant local homeomorphisms $\pi^{-1}(U)\cong U\times G$ over an open neighbourhood $U$ of every base point, with $G$ acting by multiplication on the second coordinate, and a continuous map $\psi:P\to H$ with $\psi(p\cdot g)=\psi(p)t(g)$ . Then both of the following hold: there is a homeomorphism $a:G\to G/K$ such that $a(g)=gK$ for every $g$ and $a(gk)=a(g)a(k)$ for every $g,k\in G$ ; and there is a continuous map $\phi:M\to T$ with $\phi(\pi(p))=\rho(\psi(p))$ for every $p$ , together with a homeomorphism

e:P\;\longrightarrow\;\{(m,h)\in M\times H:\phi(m)=\rho(h)\}

to this subspace of $M\times H$ , satisfying $e(p)=(\pi(p),\psi(p))$ for every $p$ and $e(p\cdot g)=(\pi(p),\psi(p)t(g))$ for every $p\in P$ and $g\in G$ . The base $M$ is allowed 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