Continuous local cocycles extracted from a bibundle

Open

QAlgorithms.Papers.Independent.Intakethird100.P93.local_data

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 $\pi:P\to M$ be an $(H,G)$ -bibundle with structure map $\psi$ . There exist an open cover $\{U_i\}$ , continuous local sections $s_i:U_i\to P$ , continuous transition maps $g_{ij}:U_i\cap U_j\to G$ , and continuous maps $h_i:U_i\to H$ , such that $s_j=s_i g_{ij}$ and $h_i=\psi\circ s_i$ . On every appropriate overlap,

g_{ij}g_{jk}=g_{ik},\qquad h_j=h_i\,t(g_{ij}).

The cover and all local data are conclusions, with maps defined on their actual subspaces. This describes the local geometric data without adding a cohomology-classification assertion for an unspecified equivalence relation.

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)

/-- Note 3.2, PDF pp.13--14: the actual bundle admits continuous local cocycle
data with sj=si gij and hi=psi∘si, satisfying both printed cocycle identities.
This makes no claim about an unspecified quotient cohomology classification. -/
theorem local_data {M P : Type u} [TopologicalSpace M] [TopologicalSpace P]
    (B : Bibundle C M P) : Nonempty (LocalCocycleData C B) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P93

Source

On the existence of bibundles, arXiv:1102.4388v2, PDF p. 13, Note 3.2, local cocycle description

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,g,k$ . Assume that each quotient map $G\to G/\ker t$ and $H\to H/t(G)$ has continuous sections on open neighborhoods of every target point, each composing with its quotient map to the inclusion. For arbitrary topological spaces $M,P$ , suppose $B$ has a continuous right $G$ -action on $P$ satisfying the identity and multiplication laws, a continuous invariant projection $\pi:P\to M$ locally admitting projection-preserving, equivariant homeomorphisms $\pi^{-1}(U)\cong U\times G$ around every point of $M$ , with right multiplication on the second factor, and a continuous $\psi:P\to H$ satisfying $\psi(p\cdot g)=\psi(p)t(g)$ . Then there exist an index type $I$ in the same universe, an open cover $(U_i)_{i\in I}$ of $M$ , continuous sections $s_i:U_i\to P$ with $\pi(s_i(m))=m$ , continuous maps $g_{ij}:U_i\cap U_j\to G$ , and continuous maps $h_i:U_i\to H$ , satisfying, for all indicated indices and points,

h_i(m)=\psi(s_i(m)),\qquad s_j(m)=s_i(m)\cdot g_{ij}(m),\qquad h_j(m)=h_i(m)\,t(g_{ij}(m)),\qquad g_{ij}(m)g_{jk}(m)=g_{ik}(m),

where the first equality holds on $U_i$ , the middle two on $U_i\cap U_j$ , and the last on $U_i\cap U_j\cap U_k$ . This asserts existence of such data without uniqueness. Empty open sets and overlaps are permitted; if $M$ is empty, an empty index type is permitted and all pointwise conditions are vacuous.

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