Implications among shrinkability notions

Open

QAlgorithms.Papers.Independent.Intakethird100.P32.shrinkability_implications

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. A shrinkable map has a continuous section $s:B\to X$ and a homotopy from $s\circ f$ to $\mathrm{id}_X$ that stays over $B$ . Then

f\text{ shrinkable}\ \Longrightarrow\ f\text{ is a homotopy equivalence},\\ f\text{ shrinkable}\ \Longrightarrow\ f\text{ locally shrinkable}\ \Longrightarrow\ f\text{ $\mathcal{CG}$-locally shrinkable}. \end{gathered}$$ Local shrinkability uses an open cover of $B$; $\mathcal{CG}$-local shrinkability uses a $\mathcal{CG}$-cover. All restrictions are formed in $\mathrm{CGH}$. The homotopy equivalence in the first assertion has $f$ itself as its forward map.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P32

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P32

universe u

open Set Topology

/-- Remark and Definition 4.3, PDF p.28: shrinkable maps are homotopy equivalences,
and shrinkable implies locally shrinkable implies CG-locally shrinkable.
The homotopy equivalence has f itself as its forward map. -/
theorem shrinkability_implications (X B : Type u) [TopologicalSpace X]
    [TopologicalSpace B] [T2Space X] [T2Space B]
    [CompactlyGeneratedSpace X] [CompactlyGeneratedSpace B] (f : C(X, B)) :
    (ShrinkableMap f → ∃ e : ContinuousMap.HomotopyEquiv X B, ∀ x, e x = f x) ∧
    (ShrinkableMap f → LocallyShrinkableMap f) ∧
    (LocallyShrinkableMap f → CGLocallyShrinkableMap 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, Remark §4.3: implications between shrinkability notions

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. To state the three conclusions explicitly, for any map $p:E\to D$ , write $S(p)$ for the following condition in the specified topologies: $p$ is continuous, and there exist continuous maps $s:D\to E$ and $H:[0,1]\times E\to E$ satisfying

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]$ . Write $S_k(p)$ for this same condition after replacing the topologies on both $E$ and $D$ by their compactly generated topologies. For a subset $W\subseteq B$ , let $p_W:f^{-1}(W)\to W$ send $x$ to $f(x)$ , initially using the subspace topologies. The theorem asserts the conjunction of three implications: (i) if $S(f)$ holds, there exists a homotopy equivalence $e:X\to B$ with $e(x)=f(x)$ for every $x\in X$ , meaning that $e$ is continuous and has a continuous map $q:B\to X$ with $q\circ e$ homotopic to $\mathrm{id}_X$ and $e\circ q$ homotopic to $\mathrm{id}_B$ ; (ii) if $S(f)$ holds, there exist an index type $A$ in the same universe and open subsets $(U_a)_{a\in A}$ covering $B$ such that $S_k(p_{U_a})$ holds for every $a$ ; and (iii) if such an indexed open cover with these section and homotopy conditions exists, then there exist an index type $A'$ in the same universe and subsets $(V_a)_{a\in A'}$ of $B$ such that $S_k(p_{V_a})$ holds for every $a$ , and for every compact subset $K\subseteq B$ there is a finite subset $J\subseteq A'$ with

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

The subsets in this last family need not be open. No spaces, indices, or family members are assumed nonempty; empty covers can cover an empty base, and the compact-set condition allows an empty finite selection when $K=\varnothing$ .

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