Extension reconstructs a reduced bispace

Open

QAlgorithms.Papers.Independent.Intakethird100.P93.lemma_2_11

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 $G_0\le G$ and $H_0\le H$ be a crossed submodule: $t(G_0)\subseteq H_0$ and $\alpha(H_0)$ preserves $G_0$ setwise. Let $X_0\subseteq X$ be a reduction of an $(H,G)$ -bispace, meaning a single nonempty $G_0$ -orbit with $\psi(X_0)\subseteq H_0$ . Form $X_0(G)=X_0\times_{G_0}G$ using $(x,g)k=(xk,k^{-1}g)$ . Then

X_0(G)\longrightarrow X,\qquad [x,g]\longmapsto xg

is a right equivariant homeomorphism preserving $\psi([x,g])=\psi(x)t(g)$ . This identifies extension of the given reduction with the original bispace by the canonical map.

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.11, PDF p.7: the canonical map [x,g]↦xg is a homeomorphism,
right equivariant and structure preserving. The equations on representatives also
specify the descended action and structure map without assuming their existence. -/
theorem lemma_2_11 {X : Type u} [TopologicalSpace X] (B : Bispace C X)
    (K : Subgroup G) (L : Subgroup H) (S : Set X)
    (hsub : IsCrossedSubmodule C K L) (hred : IsReduction C B K L S) :
    ∃ e : ExtensionSpace B.right K S ≃ₜ X,
      (∀ x g, e (extensionClass B.right K S x g) = B.right.act x.val g) ∧
      (∀ x g k, e (extensionClass B.right K S x (g * k)) =
        B.right.act (e (extensionClass B.right K S x g)) k) ∧
      (∀ x g, B.psi (e (extensionClass B.right K S x g)) =
        B.psi x.val * C.t g) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P93

Source

On the existence of bibundles, arXiv:1102.4388v2, PDF p. 7, Lemma 2.11

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)$ whose evaluation is continuous, satisfying $t(\alpha_h(g))=h\,t(g)\,h^{-1}$ and $\alpha_{t(g)}(k)=gkg^{-1}$ for all $h\in H$ and $g,k\in G$ . Assume the quotient maps $G\to G/\ker t$ and $H\to H/t(G)$ have 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 every 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 $K\le G$ , $L\le H$ , and $S\subseteq X$ . Assume $t(k)\in L$ for every $k\in K$ , and $\alpha_h(k)\in K$ for every $h\in L$ and $k\in K$ . Assume also that there exists $a\in X$ with $S=\{a\cdot k:k\in K\}$ , and that $\psi(x)\in L$ for every $x\in S$ ; in particular, these hypotheses require $S$ to be nonempty. Let $E$ be the quotient of $S\times G$ , with $S$ carrying its subspace topology, obtained by identifying $(x,g)$ with $(x\cdot k,k^{-1}g)$ whenever $k\in K$ , where the first coordinates are regarded as points of $S$ . Then there exists a homeomorphism $e:E\to X$ such that, for every $x\in S$ 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]))=\psi(x)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