A unit-type bispace is reconstructed from its unit level

Open

QAlgorithms.Papers.Independent.Intakethird100.P93.lemma_2_12

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 $\operatorname{Type}(X)=1$ , and put $X_1=\psi^{-1}(1)$ . Then the actual extension from $G_1$ reconstructs $X$ :

X_1\times_{G_1}G\xrightarrow{\ \cong\ } X,\qquad [x,g]\longmapsto xg.

This is a right equivariant homeomorphism with structure map $\psi([x,g])=t(g)$ . Neither the existence of the reduction nor a reconstruction isomorphism is an input; both are consequences of the unit-type condition.

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.12, PDF p.8: reconstruct from the actual unit-level set, by [x,g]↦xg.
No reduction or reconstruction is assumed as a hypothesis. -/
theorem lemma_2_12 {X : Type u} [TopologicalSpace X] (B : Bispace C X)
    (htype : bispaceType C B = unitType C) :
    ∃ e : ExtensionSpace B.right C.t.ker (unitLevel C B) ≃ₜ X,
      (∀ x g, e (extensionClass B.right C.t.ker (unitLevel C B) x g) =
        B.right.act x.val g) ∧
      (∀ x g k, e (extensionClass B.right C.t.ker (unitLevel C B) x (g * k)) =
        B.right.act (e (extensionClass B.right C.t.ker (unitLevel C B) x g)) k) ∧
      (∀ x g, B.psi (e (extensionClass B.right C.t.ker (unitLevel C B) x g)) =
        C.t g) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P93

Source

On the existence of bibundles, arXiv:1102.4388v2, PDF p. 8, Lemma 2.12

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}$ for every $h\in H$ and $g,k\in G$ . Assume the quotient maps $G\to G/\ker t$ and $H\to H/t(G)$ each admit continuous right inverses on open neighborhoods of every target point. Let $X$ be a topological space with a continuous right $G$ -action $x\cdot g$ satisfying the identity and action laws, such that $X$ is nonempty and each orbit map $g\mapsto x\cdot g$ is a homeomorphism $G\to X$ , and let $\psi:X\to H$ be continuous with $\psi(x\cdot g)=\psi(x)t(g)$ . Let $x_0$ be the point selected by classical choice from this nonemptiness, and assume $\psi(x_0)t(G)=t(G)$ in $H/t(G)$ . Put $U=\{x\in X:\psi(x)=1\}$ , with its subspace topology, and let $E$ be the quotient of $U\times G$ obtained by imposing $(x,g)\sim(x\cdot a,a^{-1}g)$ for $a\in\ker t$ . Then there exists a homeomorphism $e:E\to X$ such that, for every $x\in U$ and $g,k\in G$ ,

e([x,g])=x\cdot g,\qquad e([x,gk])=e([x,g])\cdot k,\qquad \psi(e([x,g]))=t(g).

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