A crossed-module bispace induces a G-bispace

Open

QAlgorithms.Papers.Independent.Intakethird100.P93.lemma_2_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.

Let $(X,\psi)$ be an $(H,G)$ -bispace with right action denoted by $xg$ . Define

g\cdot x=x\,\alpha(\psi(x))^{-1}(g).

This is a continuous left action, its orbit maps are homeomorphisms $G\to X$ , and it commutes with the given right action. Together the two principal actions make $X$ a $G$ -bispace with structure map $\alpha\circ\psi$ , so $xg=\alpha(\psi(x))(g)\cdot x$ . This constructs the induced bispace rather than assuming its axioms.

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)

/-- Lemma 2.3, PDF p.4: formula (2.1) defines commuting principal left and right
actions, with G-bispace structure map alpha∘psi. -/
theorem lemma_2_3 {X : Type u} [TopologicalSpace X] (B : Bispace C X) :
    IsInducedGBispace C B := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P93

Source

On the existence of bibundles, arXiv:1102.4388v2, PDF p. 4, Lemma 2.3

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, satisfying $t(\alpha(h)(g))=h\,t(g)\,h^{-1}$ and $\alpha(t(g))(k)=gkg^{-1}$ . Assume that each quotient map $G\to G/\ker t$ and $H\to H/t(G)$ has a continuous right inverse on an open neighborhood of every quotient point. Let $X$ be a topological space and $B$ consist of a continuous right $G$ -action $x\cdot g$ , with $X\ne\varnothing$ and $g\mapsto x\cdot g$ a homeomorphism $G\to X$ for every $x$ , together with a continuous map $\psi:X\to H$ satisfying $\psi(x\cdot g)=\psi(x)t(g)$ . Define $g\star x=x\cdot\alpha(\psi(x))^{-1}(g)$ , where the inverse is the inverse automorphism of $G$ . The theorem asserts all of the following simultaneously: $X$ is nonempty and every right orbit map is a homeomorphism; the map $(g,x)\mapsto g\star x$ is continuous; $1_G\star x=x$ ; $(gk)\star x=g\star(k\star x)$ ; for every $x\in X$ there exists a homeomorphism $e:G\to X$ satisfying $e(g)=g\star x$ for every $g$ ; and, for all $g,k\in G$ and $x\in X$ ,

g\star(x\cdot k)=(g\star x)\cdot k, \qquad x\cdot g=\alpha(\psi(x))(g)\star x.

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