The unit-level set is precisely the unit-type reduction

Proved

QAlgorithms.Papers.Independent.Intakethird100.P93.lemma_2_10

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 an $(H,G)$ -bispace $(X,\psi)$ put $X_1=\{x\in X:\psi(x)=1\}$ . Then

X_1\ne\varnothing\iff\operatorname{Type}(X)=1.

If $X_1$ is nonempty, it is a reduction to $(1,G_1)$ : it is a single $G_1$ -orbit and its structure map has value $1$ . The assertion retains the possibility that $X_1$ is empty and supplies the reduction only when that condition is met.

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.10, PDF p.7, both clauses. No nonemptiness is imposed at nonunit type. -/
theorem lemma_2_10 {X : Type u} [TopologicalSpace X] (B : Bispace C X) :
    ((unitLevel C B).Nonempty ↔ bispaceType C B = unitType C) ∧
    ((unitLevel C B).Nonempty →
      IsReduction C B C.t.ker (⊥ : Subgroup H) (unitLevel C B)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P93

Source

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

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 both quotient maps $G\to G/\ker t$ and $H\to H/t(G)$ admit continuous right inverses on open neighborhoods of every target point. Let $X$ be a topological space with a continuous right action $x\cdot g$ satisfying $x\cdot1=x$ and $(x\cdot g)\cdot k=x\cdot(gk)$ , such that $X$ is nonempty and every orbit map $g\mapsto x\cdot g$ is a homeomorphism $G\to X$ . Let $\psi:X\to H$ be continuous with $\psi(x\cdot g)=\psi(x)t(g)$ . Write $q:H\to H/t(G)$ for the quotient map, let $x_0$ be the point selected from the nonemptiness of $X$ by classical choice in the definition of the bispace type, and put $U=\{x\in X:\psi(x)=1\}$ . Then

U\ne\varnothing\quad\Longleftrightarrow\quad q(\psi(x_0))=q(1).

Moreover, if $U\ne\varnothing$ , there is an $a\in X$ such that $U=\{a\cdot k:k\in\ker t\}$ , and every $x\in U$ satisfies $\psi(x)\in\{1\}$ .

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