CG-local shrinkability implies quasi-shrinkability

Open

QAlgorithms.Papers.Independent.Intakethird100.P32.cgLocallyShrinkable_isQuasiShrinkable

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $f:X\to B$ be a continuous map between compactly generated Hausdorff spaces. Suppose $f$ is shrinkable over every member of some $\mathcal{CG}$ -cover of $B$ . Then for every locally compact, paracompact Hausdorff space $T$ and every continuous map $g:T\to B$ , the pullback projection is shrinkable:

X\times_B T\longrightarrow T.

The pullback has its Kelley-corrected topology. This is quasi-shrinkability in Definition 4.4; all three conditions on the test space are retained.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P32

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P32

universe u

open Set Topology

/-- Lemma 4.10, PDF p.28: CG-local shrinkability implies quasi-shrinkability.
All locally compact, paracompact Hausdorff probes occur inside the conclusion;
no global shrinkability or numerable-cover conclusion is assumed. -/
theorem cgLocallyShrinkable_isQuasiShrinkable (X B : Type u)
    [TopologicalSpace X] [TopologicalSpace B] [T2Space X] [T2Space B]
    [CompactlyGeneratedSpace X] [CompactlyGeneratedSpace B] (f : C(X, B))
    (hf : CGLocallyShrinkableMap f) : QuasiShrinkableMap f := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P32

Source

Compactly Generated Stacks: A Cartesian Closed Theory of Topological Stacks, arXiv:0907.3925v3, PDF p. 28, Lemma 4.10

Read-back

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

Let $X$ and $B$ be Hausdorff, compactly generated topological spaces in the same universe, and let $f:X\to B$ be continuous. For any map $p:E\to D$ , let its compactly generated section and homotopy condition mean that, after replacing the topologies of $E$ and $D$ by their compactly generated topologies, $p$ is continuous and there exist continuous maps $s:D\to E$ and $H:[0,1]\times E\to E$ such that

p(s(d))=d,\qquad H(0,z)=s(p(z)),\qquad H(1,z)=z,\qquad p(H(r,z))=p(z)

for every $d\in D$ , $z\in E$ , and $r\in[0,1]$ . Suppose there exist an index type $A$ in the same universe and subsets $(V_a)_{a\in A}$ of $B$ such that, for every compact subset $K\subseteq B$ , some finite subset $J\subseteq A$ satisfies

K=\bigcup_{a\in J}\operatorname{int}_K(K\cap V_a),

and, for each $a$ , the restricted map $p_a:f^{-1}(V_a)\to V_a$ , $p_a(x)=f(x)$ , satisfies the stated section and homotopy condition, starting from the subspace topologies. Then, for every Hausdorff, locally compact, paracompact topological space $T$ in the same universe and every continuous map $g:T\to B$ , the projection

p:\{(x,t)\in X\times T:f(x)=g(t)\}\longrightarrow T,\qquad p(x,t)=t,

also satisfies that section and homotopy condition, starting from the pullback’s subspace topology and the given topology on $T$ . The conclusion also includes continuity of $f$ . The subsets $V_a$ need not be open, all spaces and family members may be empty, and the finite selection for an empty compact set may 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