The kernel quotient is the type pullback of H

Open

QAlgorithms.Papers.Independent.Intakethird100.P93.proposition_3_3

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 $\pi:P\to M$ be an $(H,G)$ -bibundle with structure map $\psi$ . Its descended continuous type map $\varphi:M\to H/t(G)$ satisfies $\varphi(\pi(p))=[\psi(p)]$ . There is a canonical $(H,t(G))$ -bibundle isomorphism

P/G_1\xrightarrow{\ \cong\ }\varphi^*H =\{(m,h):\varphi(m)=[h]\},\qquad [p]\longmapsto(\pi(p),\psi(p)).

The quotient and pullback have their quotient and subspace topologies, respectively. The map preserves the base, structure map and the induced right image-group action. This describes the actual kernel quotient rather than an unrelated bundle of the same type.

Source correction: additionally require that the canonical map $\bar t:G/\ker(t)\to H$ is topologically inducing, so the quotient topology agrees with the subspace topology on $t(G)$ . The printed local-section assumptions alone do not imply this; see correction.printed/changed/why and MODERATION-r1.md.

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 3.3, PDF p.11. The quotient-to-pullback isomorphism is
[p]↦(pi(p),psi(p)). Its right structure group is t(G)=G/ker(t), correcting the
surrounding text's transposed (t(G),H). The actual descended type is constructed. 
Source correction (topology): Printed: the claim uses the p.4 local-section
assumptions and identifies t(G)=G/ker(t) on p.7. Changed: htop explicitly
identifies the quotient topology with the image subspace topology. Why: those
local-section assumptions alone allow the identity R_discrete -> R_usual;
its inverse is not continuous. No closed-image condition is added.
-/
theorem proposition_3_3 (htop : Topology.IsInducing (QuotientGroup.kerLift C.t))
    {M P : Type u} [TopologicalSpace M] [TopologicalSpace P]
    (B : Bibundle C M P) :
    ∃ phi : C(M, TypeGroup C),
      (∀ p, phi (B.bundle.proj p) = typeProjection C (B.psi p)) ∧
      ∃ e : OrbitSpace B.bundle.right C.t.ker ≃ₜ TypePullback C phi,
        (∀ p, (e (orbitClass B.bundle.right C.t.ker p)).val =
          (B.bundle.proj p, B.psi p)) ∧
        (∀ p g, (e (orbitClass B.bundle.right C.t.ker
          (B.bundle.right.act p g))).val =
          (B.bundle.proj p, B.psi p * C.t g)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P93

Source

On the existence of bibundles, arXiv:1102.4388v2, PDF p. 11, Proposition 3.3

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

Let $G$ and $H$ be topological groups in a common universe, 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$ . Put $K=\ker t$ , $T=H/t(G)$ , and write $\rho:H\to T$ for the quotient map. As part of $C$ , each of the quotient maps $G\to G/K$ and $\rho$ has a continuous section on some open neighbourhood of every point of its codomain, with the quotient map composed with that section equal to the identity on the neighbourhood. Assume that the topology on $G/K$ is exactly the topology induced by the map $G/K\to H$ , $gK\mapsto t(g)$ . Let $M,P$ be arbitrary topological spaces in the same universe, and let $B$ consist of a continuous right $G$ -action $p\cdot g$ on $P$ , a continuous map $\pi:P\to M$ invariant under the action, and a continuous map $\psi:P\to H$ satisfying $\psi(p\cdot g)=\psi(p)t(g)$ . Require that every $m\in M$ have an open neighbourhood $U$ and a homeomorphism $\pi^{-1}(U)\cong U\times G$ preserving the projection to $U$ and taking the right action to $(x,a)\cdot g=(x,ag)$ . Then there exists a continuous map $\phi:M\to T$ such that $\phi(\pi(p))=\rho(\psi(p))$ for every $p\in P$ , and there exists a homeomorphism

e:P/K\;\longrightarrow\;\{(m,h)\in M\times H:\phi(m)=\rho(h)\},

where $P/K$ is the quotient by the relation $p'\sim p$ when $p'=p\cdot k$ for some $k\in K$ , and the space on the right has the subspace topology. Writing $[p]$ for the orbit class, this homeomorphism satisfies $e([p])=(\pi(p),\psi(p))$ for every $p$ , and $e([p\cdot g])=(\pi(p),\psi(p)t(g))$ for every $p\in P$ and $g\in G$ . The base $M$ is allowed to be empty.

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