For a centre-free group a global central section is unique when it exists

Proved

QAlgorithms.Papers.Independent.Intake100.P96.centreFree_centralSection_unique

by Gohan · Oct 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $E\to M$ be a smooth principal $H$ -bibundle with $Z(H)=\{1\}$ . If $s,t:M\to E$ are smooth global central sections, then

s=t.

This is uniqueness conditional on existence; it does not assert every bibundle is trivial.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intake100_P96

Formal statement

open scoped Manifold ContDiff

namespace QAlgorithms.Papers.Independent.Intake100.P96

universe u v w z

section Bundles

variable {m h e : ℕ} {M : Type u} {H : Type v} {E : Type w}

variable [TopologicalSpace M] [ChartedSpace (RealModel m) M]

variable [TopologicalSpace H] [ChartedSpace (RealModel h) H]

variable [TopologicalSpace E] [ChartedSpace (RealModel e) E]

variable [Group H]

/-- Uniqueness sentence before Proposition 3, PDF p. 5.
Centre-freeness gives at most one smooth global central section; existence
is supplied separately by the triviality criterion. -/
theorem centreFree_centralSection_unique
    (B : LeftPrincipalBundle m h e M H E) (R : RightPrincipalStructure B)
    (centreFree : ∀ k : H, (∀ l : H, k * l = l * k) → k = 1) :
    ∀ s t : M → E, IsCentralSection B R s → IsCentralSection B R t →
      s = t := by sorry

end Bundles

end QAlgorithms.Papers.Independent.Intake100.P96

Source

Nonabelian Bundle Gerbes, their Differential Geometry and Gauge Theory, arXiv:hep-th/0312154v2, PDF p. 5, §2, uniqueness sentence before Proposition 3

Read-back

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

Let $m,h,e$ be arbitrary natural numbers, and let $M,H,E$ be types equipped with topologies and charts modeled on $\mathbb R^m,\mathbb R^h,\mathbb R^e$ , respectively, with $H$ equipped with a group structure. Suppose $B$ makes all three spaces smooth, Hausdorff, paracompact manifolds, makes $H$ a Lie group, and supplies a smooth projection $p:E\to M$ and a jointly smooth left action $L:H\times E\to E$ . These satisfy $L(1,q)=q$ , $L(kl,q)=L(k,L(l,q))$ , and $p(L(k,q))=p(q)$ ; for every $q,r\in E$ with $p(q)=p(r)$ , exactly one $k\in H$ satisfies $L(k,q)=r$ . Suppose $R$ supplies a jointly smooth right action $A:E\times H\to E$ satisfying $A(q,1)=q$ , $A(q,kl)=A(A(q,k),l)$ , and $p(A(q,k))=p(q)$ ; for every $q,r\in E$ with $p(q)=p(r)$ , exactly one $k\in H$ satisfies $A(q,k)=r$ . The actions commute, meaning $A(L(k,q),l)=L(k,A(q,l))$ for every $q\in E$ and $k,l\in H$ . For each action separately, put $a(k,q)=L(k,q)$ or $a(k,q)=A(q,k)$ : every $x\in M$ has an open neighborhood $U$ containing $x$ and total maps $\sigma:M\to E$ and $c:E\to H$ , smooth on $U$ and $p^{-1}(U)$ , respectively, with $p(\sigma(y))=y$ for $y\in U$ , $a(c(q),\sigma(p(q)))=q$ whenever $p(q)\in U$ , and $c(a(k,\sigma(y)))=k$ for all $y\in U$ and $k\in H$ ; these choices may differ between the two actions. Assume additionally that every $k\in H$ which commutes with every $l\in H$ equals the identity:

\forall k\in H,\quad \bigl(\forall l\in H,\;kl=lk\bigr)\Longrightarrow k=1.

Then, for every pair of functions $s,t:M\to E$ , if both are smooth, both satisfy $p(s(x))=x$ and $p(t(x))=x$ for every $x\in M$ , and both satisfy

L(k,s(x))=A(s(x),k), \qquad L(k,t(x))=A(t(x),k) \quad\text{for every }k\in H,\ x\in M,

then $s=t$ as functions. Smoothness means $C^\infty$ for the specified real charts and their product charts. The statement asserts uniqueness conditional on such functions being given, without asserting that any exist. The dimensions may be zero, and $M$ and $E$ need not be nonempty; when both are empty, all the section conditions are vacuous and the two functions are necessarily equal.

Human review

Endorsed by Shuze Chen · Oct 30, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Oct 30, 2026
Confirmed by the mission captain (proposal self-audit).

View graph