Existence and reduction: exactness of (3.3)

Open

QAlgorithms.Papers.Independent.Intakethird100.P93.exact_3_3

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 base space $M$ , let $\iota(Q)=Q\times_{G_1}G$ , with $\psi([q,g])=t(g)$ , for a principal $G_1$ -bundle $Q$ . Let $\operatorname{Type}(P):M\to H/t(G)$ be the type of an $(H,G)$ -bibundle. Extension gives an injection on isomorphism classes, and its image consists precisely of the identically unit type classes:

\iota(Q)\cong\iota(R)\iff Q\cong R,\qquad \operatorname{Type}(P)\equiv1\iff \exists Q,\ P\cong\iota(Q).

This is the set-level exactness of (3.3), including injectivity of the first map. Equality of classes is expressed here by geometric isomorphisms of their representatives; the extension quotient and all its maps are the actual ones. The assertion does not require every continuous type map to be realized.

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)

/-- The main existence statement (3.3), PDF p.12, previewed pp.1--2.
Equality of isomorphism classes is presented by geometric isomorphisms: the first
clause says precisely that the actual extension induces an injection on classes;
the second says its essential image is precisely the identically unit type. The
extension is Q×ker(t)G with structure map [q,g]↦t(g), not a free map variable.
No surjectivity of Type onto all continuous type maps is asserted. 
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 exact_3_3 (htop : Topology.IsInducing (QuotientGroup.kerLift C.t))
    {M : Type u} [TopologicalSpace M] :
    (∀ (Q R : TopCat.{u}) (B : PrincipalBundle C.t.ker M Q)
      (D : PrincipalBundle C.t.ker M R),
      IotaIsomorphic C B D ↔ PrincipalIsomorphic B D) ∧
    (∀ (P : TopCat.{u}) (B : Bibundle C M P),
      HasUnitType C B ↔ ∃ (Q : TopCat.{u}) (R : PrincipalBundle C.t.ker M Q),
        IotaToBibundleIsomorphic C R B) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P93

Source

On the existence of bibundles, arXiv:1102.4388v2, PDF p. 12, §1 / §3, unnumbered main existence result: exactness of (3.3)

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$ . Set $K=\ker t$ , let $\rho:H\to H/t(G)$ be the quotient map, and assume that each of $G\to G/K$ and $\rho$ admits a continuous section on an open neighbourhood of every point of its codomain, meaning that projection after section is the identity there. Assume that the topology on $G/K$ is induced by $gK\mapsto t(g)$ into $H$ , and let $M$ be any topological space in the same universe. For a topological space $Q$ , a principal $K$ -bundle $B$ here means a continuous right $K$ -action on $Q$ and an invariant continuous projection $\pi_B:Q\to M$ that, near every point of $M$ , has a homeomorphism $\pi_B^{-1}(U)\cong U\times K$ preserving the base coordinate and taking the action to multiplication on the second coordinate. Define $I_B$ to be the quotient of $Q\times G$ by

(q,g)\sim(q\cdot k,k^{-1}g)\qquad(k\in K),

with quotient topology, and denote its elements by $[q,g]_B$ , regarding $k$ as an element of $G$ . The assertion is the conjunction of two statements. First, for every pair of topological spaces $Q,R$ in the given universe and every principal $K$ -bundle $B$ on $Q$ and $D$ on $R$ , there exists a homeomorphism $E:I_B\to I_D$ such that, for all $q\in Q$ , $r\in R$ , and $g,k\in G$ , the equality $E([q,g]_B)=[r,k]_D$ implies both $\pi_B(q)=\pi_D(r)$ and $t(g)=t(k)$ , and implies, for every $a\in G$ , the equality $E([q,ga]_B)=[r,ka]_D$ , if and only if there exists a homeomorphism $F:Q\to R$ with $\pi_D(F(q))=\pi_B(q)$ and $F(q\cdot k)=F(q)\cdot k$ for all $q\in Q$ and $k\in K$ . Second, for every topological space $P$ in the given universe and every $B$ consisting of a continuous right $G$ -action on $P$ , an invariant continuous projection $\pi:P\to M$ locally equivariantly homeomorphic over each base neighbourhood to $U\times G$ , and a continuous $\psi:P\to H$ satisfying $\psi(p\cdot g)=\psi(p)t(g)$ , the condition

\forall p\in P,\qquad \rho(\psi(p))=\rho(1_H)

holds if and only if there are a topological space $Q$ in the same universe, a principal $K$ -bundle $R$ on $Q$ with projection $\pi_R$ , and a homeomorphism $E:I_R\to P$ satisfying, for every $q\in Q$ and $g,k\in G$ ,

\pi(E([q,g]_R))=\pi_R(q),\qquad E([q,gk]_R)=E([q,g]_R)\cdot k,\qquad \psi(E([q,g]_R))=t(g).

The spaces quantified over may be empty; in particular, the displayed condition on all $p$ is vacuous when $P$ 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