Type-preserving homotopies induce bibundle isomorphisms

Open

QAlgorithms.Papers.Independent.Intakethird100.P93.proposition_3_10

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 $M$ be paracompact Hausdorff, let $P\to N$ be an $(H,G)$ -bibundle with actual type map $\varphi:N\to H/t(G)$ , and let $f_0,f_1:M\to N$ be continuous. Suppose a continuous homotopy $h:I\times M\to N$ joins them and satisfies $\varphi(h(s,m))=\varphi(f_0(m))$ for every $s\in I=[0,1]$ and $m\in M$ . Then

f_0^*P\cong f_1^*P

as $(H,G)$ -bibundles, preserving the base, right action and structure map. This is the homotopy-invariance statement in the slice over $H/t(G)$ , with time-constant projected type imposed throughout the homotopy.

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)

/-- Proposition 3.10, PDF pp.15--17: only homotopies whose actual pulled-back
type is constant in time induce bibundle isomorphisms. Paracompactness and the
Hausdorff convention are retained. 
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 proposition_3_10 (htop : Topology.IsInducing (QuotientGroup.kerLift C.t))
    {M N P : Type u} [TopologicalSpace M] [ParacompactSpace M]
    [T2Space M] [TopologicalSpace N] [TopologicalSpace P] (B : Bibundle C N P)
    (f0 f1 : C(M, N)) (h : f0.Homotopy f1)
    (htype : ∀ (s : unitInterval) (m : M) (p q : P),
      B.bundle.proj p = h (s, m) → B.bundle.proj q = f0 m →
      typeProjection C (B.psi p) = typeProjection C (B.psi q)) :
    PullbacksIsomorphic C B f0 f1 := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P93

Source

On the existence of bibundles, arXiv:1102.4388v2, PDF p. 16, Proposition 3.10

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$ and let $\rho:H\to H/t(G)$ be the quotient map. Assume that each of $G\to G/K$ and $\rho$ has a continuous section on an open neighbourhood of every point of its codomain, with projection after section equal to the identity, and that the topology on $G/K$ is induced by $gK\mapsto t(g)$ into $H$ . Let $M$ be a paracompact Hausdorff topological space, let $N,P$ be topological spaces, all in the same universe, and let $B$ consist of a continuous right $G$ -action on $P$ , an invariant continuous projection $\pi:P\to N$ admitting, near every point of $N$ , a homeomorphism $\pi^{-1}(U)\cong U\times G$ preserving the base coordinate and taking the action to multiplication on the second coordinate, and a continuous map $\psi:P\to H$ satisfying $\psi(p\cdot g)=\psi(p)t(g)$ . Let $f_0,f_1:M\to N$ be continuous maps and $h:[0,1]\times M\to N$ a continuous homotopy with $h(0,m)=f_0(m)$ and $h(1,m)=f_1(m)$ . Suppose that for every $s\in[0,1]$ , $m\in M$ , and $p,q\in P$ ,

\pi(p)=h(s,m)\ \text{and}\ \pi(q)=f_0(m) \quad\Longrightarrow\quad \rho(\psi(p))=\rho(\psi(q)).

Then, for the subspaces $P_i=\{(m,p)\in M\times P:f_i(m)=\pi(p)\}$ , there is a homeomorphism $E:P_0\to P_1$ preserving the $M$ -coordinate and the value of $\psi$ on the $P$ -coordinate. Explicitly, if $E(m,p)=(m',p')$ , then $m'=m$ and $\psi(p')=\psi(p)$ ; moreover, for every $(m,p)\in P_0$ and $k\in G$ such that $f_0(m)=\pi(p\cdot k)$ , the $P$ -coordinate of $E(m,p\cdot k)$ is $p'\cdot k$ . The invariance of $\pi$ ensures this membership condition for every such $(m,p)$ and $k$ . Empty spaces are permitted, and the hypothesis quantified over $m$ is vacuous when $M$ is 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