Quotient by the kernel is an image-group bispace

Open

QAlgorithms.Papers.Independent.Intakethird100.P93.lemma_2_9

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. Give $X/G_1$ its orbit quotient topology, and identify the image structure group $t(G)$ with $G/G_1$ with its quotient topology. The action and structure map descend to make $X/G_1$ an $(H,t(G))$ -bispace:

[x]\,[g]=[xg],\qquad \bar\psi([x])=\psi(x),\qquad \bar\psi([x]\,[g])=\bar\psi([x])t(g).

In particular, the descended continuous right action is principal for $G/G_1$ . This records the correct structure group after killing the kernel; a free action of the original group is not asserted.

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.9, PDF p.7. The induced principal right action has structure group
G/ker(t), the image group with its quotient topology, rather than G itself.
Both descended maps are pinned on representatives. -/
theorem lemma_2_9 {X : Type u} [TopologicalSpace X] (B : Bispace C X) :
    ∃ R : RightAction (G ⧸ C.t.ker) (OrbitSpace B.right C.t.ker),
      IsRightTorsor R ∧
      ∃ psi : C(OrbitSpace B.right C.t.ker, H),
        (∀ x g, R.act (orbitClass B.right C.t.ker x)
          (QuotientGroup.mk g) = orbitClass B.right C.t.ker (B.right.act x g)) ∧
        (∀ x, psi (orbitClass B.right C.t.ker x) = B.psi x) ∧
        (∀ q k, psi (R.act q k) = psi q * QuotientGroup.kerLift C.t k) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P93

Source

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

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 $(h,g)\mapsto\alpha_h(g)$ , 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)$ each have a continuous right inverse on an open neighborhood 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 map $g\mapsto x\cdot g$ is a homeomorphism $G\to X$ ; let $\psi_B:X\to H$ be continuous with $\psi_B(x\cdot g)=\psi_B(x)t(g)$ . Put $K=\ker t$ , and let $Q$ be the quotient of $X$ obtained by identifying $x$ with $x\cdot a$ for every $a\in K$ , writing $[x]$ for its classes. Then there exist a jointly continuous right action $R:Q\times(G/K)\to Q$ , satisfying $R(q,1)=q$ and $R(R(q,a),b)=R(q,ab)$ , and a continuous map $\psi:Q\to H$ , such that $Q$ is nonempty, for every $q\in Q$ the map $a\mapsto R(q,a)$ is a homeomorphism $G/K\to Q$ , and

R([x],gK)=[x\cdot g],\qquad \psi([x])=\psi_B(x),\qquad \psi(R(q,a))=\psi(q)\,\overline t(a)

for all $x\in X$ , $g\in G$ , $q\in Q$ , and $a\in G/K$ , where $\overline t:G/K\to H$ is the induced homomorphism defined by $\overline t(gK)=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