A lifted type splits off a kernel bundle

Open

QAlgorithms.Papers.Independent.Intakethird100.P93.proposition_3_8

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 $P\to M$ be an $(H,G)$ -bibundle with type $\varphi$ , and suppose a continuous map $\widehat\varphi:M\to H$ satisfies $[\widehat\varphi(m)]=\varphi(m)$ . There exists a principal $G_1$ -bundle $R\to M$ such that

P\cong\iota(R)(\widehat\varphi)=\iota(R)\otimes T(\widehat\varphi).

In the underlying quotient $R\times_{G_1}G$ , the twisted right action is $[r,g]\cdot k=[r,g\alpha(\widehat\varphi(m))(k)]$ and the structure map is $t(g)\widehat\varphi(m)$ , where $m$ is the image of $r$ . The isomorphism preserves this action, structure map and projection. Existence of $R$ is part of the conclusion, so the result gives a decomposition from a lift of the actual 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.8, PDF p.13. R is an existential conclusion. The isomorphism
with ι(R)(lift) is pinned by its projection, twisted right action, and structure map.
The chosen lift projects to the actual type of P. 
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_8 (htop : Topology.IsInducing (QuotientGroup.kerLift C.t))
    {M P : Type u} [TopologicalSpace M] [TopologicalSpace P]
    (B : Bibundle C M P) (lift : C(M, H))
    (hlift : ∀ p, typeProjection C (lift (B.bundle.proj p)) =
      typeProjection C (B.psi p)) :
    ∃ Q : TopCat.{u},
      ∃ R : PrincipalBundle C.t.ker M Q,
        ∃ e : IotaSpace C R ≃ₜ P,
          (∀ q g, B.bundle.proj (e (iotaClass C R q g)) = R.proj q) ∧
          (∀ q g k, e (iotaClass C R q
            (g * C.alpha (lift (R.proj q)) k)) =
            B.bundle.right.act (e (iotaClass C R q g)) k) ∧
          ∀ q g, B.psi (e (iotaClass C R q g)) =
            C.t g * lift (R.proj q) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P93

Source

On the existence of bibundles, arXiv:1102.4388v2, PDF p. 13, Proposition 3.8

Read-back

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

Let $G,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, satisfying $t(\alpha_h(g))=h\,t(g)\,h^{-1}$ and $\alpha_{t(g)}(k)=gkg^{-1}$ for all $h,g,k$ . Set $K=\ker t$ and write $\rho:H\to H/t(G)$ . Assume that each of $G\to G/K$ and $\rho$ admits a continuous section on an open neighbourhood of every point of its codomain, with projection after section equal to the identity, and that the topology on $G/K$ is induced by $gK\mapsto t(g)$ into $H$ . Let $M,P$ be arbitrary topological spaces in the same universe, and let $B$ consist of a continuous right $G$ -action on $P$ , an invariant continuous projection $\pi:P\to M$ admitting, near each base point, a homeomorphism $\pi^{-1}(U)\cong U\times G$ preserving the base coordinate and intertwining the action with multiplication on the second coordinate, and a continuous $\psi:P\to H$ satisfying $\psi(p\cdot g)=\psi(p)t(g)$ . Given a continuous map $\ell:M\to H$ such that

\rho(\ell(\pi(p)))=\rho(\psi(p))\qquad\text{for every }p\in P,

there exist a topological space $Q$ in the same universe and a continuous right $K$ -action on $Q$ with an invariant continuous projection $r:Q\to M$ , locally equivariantly homeomorphic over neighbourhoods of every base point to $U\times K$ , together with a homeomorphism $E:I_R\to P$ . Here $I_R$ is the quotient of $Q\times G$ , with quotient topology, by $(q,g)\sim(q\cdot a,a^{-1}g)$ for $a\in K$ , and $[q,g]$ denotes the corresponding class. For all $q\in Q$ and $g,k\in G$ , this homeomorphism satisfies

\pi(E([q,g]))=r(q),\qquad E\bigl([q,g\,\alpha_{\ell(r(q))}(k)]\bigr)=E([q,g])\cdot k,\qquad \psi(E([q,g]))=t(g)\,\ell(r(q)).

No nonemptiness of the base is assumed; the hypothesis concerning every $p$ is vacuous when $P$ is 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