Categorical exactness: faithfulness and the unit-type image

Open

QAlgorithms.Papers.Independent.Intakethird100.P93.exact_3_2

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 any base $M$ , extend a principal $G_1$ -bundle by $\iota(Q)=Q\times_{G_1}G$ . A morphism $f:Q\to R$ is sent to $[q,g]\mapsto[f(q),g]$ . This extension is faithful, and its essential image consists exactly of unit-type bibundles:

\iota(f)=\iota(f')\Longrightarrow f=f',\qquad \operatorname{Type}(P)\equiv1\iff\exists R,\ P\cong\iota(R).

Morphisms are continuous right equivariant maps over $M$ , and bibundle isomorphisms also preserve the structure map. These are precisely the two clauses called exactness in the source; fullness and a stronger higher kernel property are not asserted.

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)

/-- Categorical exactness (3.2), PDF p.12, in exactly the two senses specified
by the source: faithfulness on Hom sets and the unit-type essential-image criterion.
Faithfulness is injectivity of the actual representativewise extension on maps;
full faithfulness is not asserted. 
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 exact_3_2 (htop : Topology.IsInducing (QuotientGroup.kerLift C.t))
    {M : Type u} [TopologicalSpace M] :
    (∀ (Q R : TopCat.{u}) (B : PrincipalBundle C.t.ker M Q)
      (D : PrincipalBundle C.t.ker M R), Function.Injective (iotaHom C B D)) ∧
    (∀ (P : TopCat.{u}) (B : Bibundle C M P),
      HasUnitType C B ↔ ∃ (Q : TopCat.{u}) (R : PrincipalBundle C.t.ker M Q),
        IotaToBibundleIsomorphic C R B) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P93

Source

On the existence of bibundles, arXiv:1102.4388v2, PDF p. 12, §3, categorical exactness (3.2)

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$ . Put $K=\ker t$ and write $\rho:H\to H/t(G)$ . Assume that each of $G\to G/K$ and $\rho$ has a continuous section on an open neighbourhood of every point of its codomain, with projection after section equal to the identity, and assume that the topology on $G/K$ is induced by $gK\mapsto t(g)$ into $H$ . Let $M$ be any topological space in the same universe. A principal $K$ -bundle $B$ on a topological space $Q$ means a continuous right $K$ -action and an invariant continuous projection $\pi_B:Q\to M$ with, near every point of $M$ , a homeomorphism $\pi_B^{-1}(U)\cong U\times K$ preserving the base coordinate and intertwining the action with multiplication on the second coordinate. Let $I_B$ be the quotient of $Q\times G$ , with quotient topology, by $(q,g)\sim(q\cdot k,k^{-1}g)$ for $k\in K$ , and write $[q,g]_B$ for its classes. Then the following two assertions hold. First, for every pair of topological spaces $Q,R$ in the given universe and principal $K$ -bundles $B,D$ on them, the assignment sending a continuous map $f:Q\to R$ satisfying $\pi_D(f(q))=\pi_B(q)$ and $f(q\cdot k)=f(q)\cdot k$ for every $q\in Q,k\in K$ to the function

I_B\longrightarrow I_D,\qquad [q,g]_B\longmapsto[f(q),g]_D

is injective: if two such bundle maps induce equal functions on these quotient spaces, the bundle maps are equal. Second, for every topological space $P$ in the given universe and every $B$ consisting of a continuous right $G$ -action on $P$ , an invariant continuous projection $\pi:P\to M$ locally equivariantly homeomorphic over each base neighbourhood to $U\times G$ , and a continuous $\psi:P\to H$ satisfying $\psi(p\cdot g)=\psi(p)t(g)$ , the condition $\rho(\psi(p))=\rho(1_H)$ for every $p\in P$ is equivalent to the existence of a topological space $Q$ in the same universe, a principal $K$ -bundle $R$ on $Q$ , and a homeomorphism $E:I_R\to P$ such that, for all $q\in Q$ and $g,k\in G$ ,

\pi(E([q,g]_R))=\pi_R(q),\qquad E([q,gk]_R)=E([q,g]_R)\cdot k,\qquad \psi(E([q,g]_R))=t(g).

Empty spaces are included in these quantifiers, and the condition on all $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