Degree-zero extraction is a bijection

Proved

QAlgorithms.Papers.Independent.Intake100.P87.zeroDescent_bijection

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

prove2quantum

Let $M,Y,G$ be ordinary finite-dimensional real smooth manifolds, let $\pi:Y\to M$ be a smooth surjective submersion, let $T$ be a set, and let $i:G\to T$ be injective. Neither a group structure on $G$ nor a smooth structure on $T$ is assumed. Let $\operatorname{Triv}^0_\pi(i)$ consist of pairs $(F,\mathrm{triv})$ with $F:M\to T$ , $\mathrm{triv}:Y\to G$ , and $F\circ\pi=i\circ\mathrm{triv}$ . Let $\operatorname{Des}^0_\pi(i)$ consist of functions $\mathrm{triv}:Y\to G$ such that $i(\mathrm{triv}(y))=i(\mathrm{triv}(z))$ whenever $\pi(y)=\pi(z)$ .

The specified extraction map is a bijection, and every descent function has a unique $G$ -valued factor:

\operatorname{Ex}_\pi:(F,\mathrm{triv})\longmapsto\mathrm{triv} \quad\text{is bijective},\qquad \forall\mathrm{triv}\in\operatorname{Des}^0_\pi(i),\quad \exists! f:M\to G\;\;f\circ\pi=\mathrm{triv}.

This is set-valued descent along the actual cover, with no smoothness requirement on the descent function.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intake100_P87

Formal statement

noncomputable section

open scoped ContDiff Manifold

namespace QAlgorithms.Papers.Independent.Intake100.P87

universe u v

/-- Degree-zero descent, Section 7.1, PDF pp. 48–49: Ex_pi is a bijection;
each descent function has a unique factor through pi with values in G. -/
theorem zeroDescent_bijection {Y M G : SmoothManifold.{u}} {T : Type v}
    (pi : SmoothSurjectiveSubmersion Y M) (i : G.carrier → T)
    (hi : Function.Injective i) :
    Function.Bijective (zeroExtract pi i) ∧
    ∀ data : ZeroDescent pi i, ∃! f : M.carrier → G.carrier,
      ∀ y, f (pi.toFun y) = data.val y := by sorry

end QAlgorithms.Papers.Independent.Intake100.P87

end

Source

Parallel Transport and Functors, arXiv:0705.0452v5, PDF p. 48, zero-descent

Read-back

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

Let $Y,M,G$ be finite-dimensional Hausdorff, second-countable smooth real manifolds with specified Euclidean models, allowing empty underlying spaces and zero dimensions. For every type $T$ , every smooth surjection $\pi:Y\to M$ with surjective differential everywhere, and every injective map $i:G\to T$ , the map sending a compatible pair $(F,g)$ , where $F:M\to T$ , $g:Y\to G$ , and $F(\pi(y))=i(g(y))$ for all $y$ , to its component $g$ is a bijection onto the type of maps $g:Y\to G$ satisfying $i(g(y))=i(g(z))$ whenever $\pi(y)=\pi(z)$ . In addition, for every such $g$ , there exists exactly one function $f:M\to G$ satisfying

\forall y\in Y,\qquad f(\pi(y))=g(y).

The functions $F$ , $g$ , and $f$ in this statement are not required to be smooth.

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