Type classifies bispaces

Open

QAlgorithms.Papers.Independent.Intakethird100.P93.proposition_2_6

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 two $(H,G)$ -bispaces $(X,\psi)$ and $(Y,\chi)$ , let $\operatorname{Type}(X)=[\psi(x)]$ and $\operatorname{Type}(Y)=[\chi(y)]$ in $H/t(G)$ ; equivariance makes the choices of points immaterial. Then

X\cong Y\iff\operatorname{Type}(X)=\operatorname{Type}(Y).

Here an isomorphism is a right equivariant homeomorphism $f:X\to Y$ satisfying $\chi\circ f=\psi$ . The result distinguishes all bispace isomorphism classes by their type.

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 2.6, PDF p.5. Isomorphisms are homeomorphisms preserving both
the right action and psi. The proof's mis-typed chi=psi∘f is read as chi∘f=psi,
as in its own converse; no change to the printed proposition is needed. -/
theorem proposition_2_6 {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y]
    (B : Bispace C X) (D : Bispace C Y) :
    Nonempty (BispaceIso C B D) ↔ bispaceType C B = bispaceType C D := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P93

Source

On the existence of bibundles, arXiv:1102.4388v2, PDF p. 5, Proposition 2.6

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,Y$ be topological spaces carrying data $B,D$ , respectively: each space is nonempty, each has a continuous right $G$ -action whose orbit map from every point is a homeomorphism from $G$ , and there are continuous maps $\psi_B:X\to H$ and $\psi_D:Y\to H$ satisfying $\psi_B(x\cdot_B g)=\psi_B(x)t(g)$ and $\psi_D(y\cdot_D g)=\psi_D(y)t(g)$ . Let $x_0\in X$ and $y_0\in Y$ be the points selected by classical choice from the nonemptiness data of $B,D$ . The theorem states that there exists a homeomorphism $e:X\to Y$ satisfying $e(x\cdot_B g)=e(x)\cdot_D g$ and $\psi_D(e(x))=\psi_B(x)$ for every $x\in X$ and $g\in G$ if and only if the quotient classes of $\psi_B(x_0)$ and $\psi_D(y_0)$ are equal in $H/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