Definitions for Compactly Generated Stacks: A Cartesian Closed Theory of Topological Stacks

Definition

QAlgorithms_Papers_Independent_Intakethird100_P32

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

prove2quantum

The objects the formalized statements of Compactly Generated Stacks: A Cartesian Closed Theory of Topological Stacks (arXiv:0907.3925) are stated in. Each was checked against the paper by a blind read-back and a moderator.

IsOpenCover: An ordinary open cover, allowing an empty index type over the empty space (Definition 2.7, PDF p.12; Definition 3.1, PDF p.16).
IsShrinking: A shrinking has the SAME index type, remains an open cover, and has each closure contained in the corresponding original member (Definition 2.7, PDF p.12).
ShrinkingSpace: Every universe-small open cover has a shrinking (Definition 2.7, PDF p.12).
CGCover: The concrete CG-cover condition (Definition 3.1, PDF p.16). The interior is taken INSIDE each compact subspace K. A finite collection has an open-cover refinement precisely when these relative interiors cover K.
HasOpenRefinement: An open refinement can canonically be taken to be the interiors of the members of V, indexed by the same set (Proposition 3.3, PDF p.18).
allCompactSubsets: The actual family of ALL compact subsets, with no chosen exhaustion (Corollary 3.1, PDF p.18).
ShrinkableMap: A continuous section and a homotopy from s composed with f to the identity, with every homotopy stage over the base (Definition 4.2, PDF p.28).
KelleyShrinkable: Apply the Kelley correction to both spaces before asserting shrinkability. The source topologies are captured before the local instances are replaced; compact test spaces have universe u (pp.4,10,28).
restrictedProjection: Restriction of f over a subset V of its base, prior to Kelley correction (Definition 4.3, PDF p.28).
LocallyShrinkableMap: Shrinkability over an ordinary open cover, with CGH restrictions formed by Kelley correction (Definition 4.3, PDF p.28).
CGLocallyShrinkableMap: Shrinkability over a CG-cover, with the same restriction construction (Definition 4.3, PDF p.28).
pullbackProjection: Projection of the actual topological fiber product, prior to Kelley correction (Definition 4.4, PDF p.28).
QuasiShrinkableMap: All pullbacks to locally compact, PARACOMPACT, Hausdorff test spaces are shrinkable (Definition 4.4, PDF p.28). Printed X ×_Y T is corrected to X ×_B T: Y is undefined, while f and the test map both have target B.

Definition code

import Mathlib

/-!
Statements from Carchedi, arXiv:0907.3925v3. Local definitions have complete bodies;
only the six source-result declarations use `sorry`. Other planned nodes are explicitly
deferred in this unit's HARD.md and GAPS.json. Compilation is pending the batch handoff.
-/

namespace QAlgorithms.Papers.Independent.Intakethird100.P32

universe u

open Set Topology

/-- An ordinary open cover, allowing an empty index type over the empty space
(Definition 2.7, PDF p.12; Definition 3.1, PDF p.16). -/
def IsOpenCover {X : Type u} [TopologicalSpace X] {A : Type u}
    (U : A → Set X) : Prop :=
  (∀ a, IsOpen (U a)) ∧ ∀ x, ∃ a, x ∈ U a

/-- A shrinking has the SAME index type, remains an open cover, and has each
closure contained in the corresponding original member (Definition 2.7, PDF p.12). -/
def IsShrinking {X : Type u} [TopologicalSpace X] {A : Type u}
    (U V : A → Set X) : Prop :=
  IsOpenCover V ∧ ∀ a, closure (V a) ⊆ U a

/-- Every universe-small open cover has a shrinking (Definition 2.7, PDF p.12). -/
def ShrinkingSpace (X : Type u) [TopologicalSpace X] : Prop :=
  ∀ (A : Type u) (U : A → Set X), IsOpenCover U → ∃ V, IsShrinking U V

/-- The concrete CG-cover condition (Definition 3.1, PDF p.16).
The interior is taken INSIDE each compact subspace K. A finite collection has an
open-cover refinement precisely when these relative interiors cover K. -/
def CGCover {X : Type u} [TopologicalSpace X] {A : Type u}
    (V : A → Set X) : Prop :=
  ∀ K : Set X, IsCompact K → ∃ J : Finset A,
    ∀ x : K, ∃ a, a ∈ J ∧ x ∈ interior ((Subtype.val : K → X) ⁻¹' V a)

/-- An open refinement can canonically be taken to be the interiors of the members
of V, indexed by the same set (Proposition 3.3, PDF p.18). -/
def HasOpenRefinement {X : Type u} [TopologicalSpace X] {A : Type u}
    (V : A → Set X) : Prop :=
  ∀ x, ∃ a, x ∈ interior (V a)

/-- The actual family of ALL compact subsets, with no chosen exhaustion
(Corollary 3.1, PDF p.18). -/
def allCompactSubsets (X : Type u) [TopologicalSpace X] :
    {K : Set X // IsCompact K} → Set X := fun K => K.val

/-- A continuous section and a homotopy from s composed with f to the identity,
with every homotopy stage over the base (Definition 4.2, PDF p.28). -/
def ShrinkableMap {X B : Type u} [TopologicalSpace X] [TopologicalSpace B]
    (f : X → B) : Prop :=
  Continuous f ∧ ∃ s : C(B, X),
    (∀ b, f (s b) = b) ∧ ∃ H : C(unitInterval × X, X),
      (∀ x, H (0, x) = s (f x)) ∧
      (∀ x, H (1, x) = x) ∧
      ∀ t x, f (H (t, x)) = f x

/-- Apply the Kelley correction to both spaces before asserting shrinkability.
The source topologies are captured before the local instances are replaced;
compact test spaces have universe u (pp.4,10,28). -/
def KelleyShrinkable {X B : Type u} [TopologicalSpace X] [TopologicalSpace B]
    (f : X → B) : Prop :=
  let tx := TopologicalSpace.compactlyGenerated.{u} X
  let tb := TopologicalSpace.compactlyGenerated.{u} B
  letI : TopologicalSpace X := tx
  letI : TopologicalSpace B := tb
  ShrinkableMap f

/-- Restriction of f over a subset V of its base, prior to Kelley correction
(Definition 4.3, PDF p.28). -/
def restrictedProjection {X B : Type u} (f : X → B) (V : Set B) :
    {x : X // f x ∈ V} → V := fun x => ⟨f x.val, x.property⟩

/-- Shrinkability over an ordinary open cover, with CGH restrictions formed by
Kelley correction (Definition 4.3, PDF p.28). -/
def LocallyShrinkableMap {X B : Type u} [TopologicalSpace X] [TopologicalSpace B]
    (f : X → B) : Prop :=
  Continuous f ∧ ∃ (A : Type u) (U : A → Set B),
    IsOpenCover U ∧ ∀ a, KelleyShrinkable (restrictedProjection f (U a))

/-- Shrinkability over a CG-cover, with the same restriction construction
(Definition 4.3, PDF p.28). -/
def CGLocallyShrinkableMap {X B : Type u} [TopologicalSpace X] [TopologicalSpace B]
    (f : X → B) : Prop :=
  Continuous f ∧ ∃ (A : Type u) (V : A → Set B),
    CGCover V ∧ ∀ a, KelleyShrinkable (restrictedProjection f (V a))

/-- Projection of the actual topological fiber product, prior to Kelley correction
(Definition 4.4, PDF p.28). -/
def pullbackProjection {X B T : Type u} (f : X → B) (g : T → B) :
    {p : X × T // f p.1 = g p.2} → T := fun p => p.val.2

/-- All pullbacks to locally compact, PARACOMPACT, Hausdorff test spaces are
shrinkable (Definition 4.4, PDF p.28). Printed X ×_Y T is corrected to X ×_B T:
Y is undefined, while f and the test map both have target B. -/
def QuasiShrinkableMap {X B : Type u} [TopologicalSpace X] [TopologicalSpace B]
    (f : X → B) : Prop :=
  Continuous f ∧ ∀ (T : Type u) [TopologicalSpace T]
    [T2Space T] [LocallyCompactSpace T] [ParacompactSpace T]
    (g : C(T, B)), KelleyShrinkable (pullbackProjection f g)

/-- Sanity: a one-member universal open cover is its own shrinking. -/
example (X : Type u) [TopologicalSpace X] :
    IsShrinking (fun _ : PUnit => (Set.univ : Set X))
      (fun _ : PUnit => (Set.univ : Set X)) := by
  constructor
  · constructor
    · intro a
      exact isOpen_univ
    · intro x
      exact ⟨PUnit.unit, Set.mem_univ x⟩
  · intro a
    exact Set.subset_univ _

/-- Sanity: the empty family is a CG-cover of the empty space. -/
example : CGCover (fun _ : Empty => (∅ : Set Empty)) := by
  intro K hK
  refine ⟨∅, ?_⟩
  intro x
  exact isEmptyElim x.val

/-- Sanity: a universal singleton family satisfies the finite relative-interior test. -/
example (X : Type u) [TopologicalSpace X] :
    CGCover (fun _ : PUnit => (Set.univ : Set X)) := by
  intro K hK
  refine ⟨{PUnit.unit}, ?_⟩
  intro x
  refine ⟨PUnit.unit, by simp, ?_⟩
  simp

/-- Sanity: a point belongs to the member selected by its own compact singleton. -/
example (X : Type u) [TopologicalSpace X] (x : X) :
    x ∈ allCompactSubsets X ⟨{x}, isCompact_singleton⟩ := by
  exact Set.mem_singleton x

/-- Sanity: identity maps have the identity section and constant fiber homotopy. -/
example (X : Type u) [TopologicalSpace X] : ShrinkableMap (id : X → X) := by
  refine ⟨continuous_id, ContinuousMap.id X, ?_, ⟨Prod.snd, continuous_snd⟩,
    ?_, ?_, ?_⟩
  · intro x
    rfl
  · intro x
    rfl
  · intro x
    rfl
  · intro t x
    rfl

/-- Sanity: Kelley correction also permits the identity section and homotopy. -/
example (X : Type u) [TopologicalSpace X] : KelleyShrinkable (id : X → X) := by
  letI : TopologicalSpace X := TopologicalSpace.compactlyGenerated.{u} X
  change ShrinkableMap (id : X → X)
  refine ⟨continuous_id, ContinuousMap.id X, ?_, ⟨Prod.snd, continuous_snd⟩,
    ?_, ?_, ?_⟩
  · intro x
    rfl
  · intro x
    rfl
  · intro x
    rfl
  · intro t x
    rfl

/-- Sanity: identity restrictions and fiber products use the actual coordinates. -/
example {X : Type u} (V : Set X) (x : V) :
    restrictedProjection (id : X → X) V x = x := rfl

/-- Sanity: pullback projection retains the test-space coordinate. -/
example {X : Type u} (x : X) :
    pullbackProjection (id : X → X) (id : X → X) ⟨(x, x), rfl⟩ = x := rfl

/-- Sanity: a one-member family with full interior is an open refinement. -/
example (X : Type u) [TopologicalSpace X] :
    HasOpenRefinement (fun _ : PUnit => (Set.univ : Set X)) := by
  intro x
  exact ⟨PUnit.unit, by simp⟩

/-- Sanity: the identity is locally shrinkable over the universal cover. -/
example (X : Type u) [TopologicalSpace X] : LocallyShrinkableMap (id : X → X) := by
  refine ⟨continuous_id, PUnit, fun _ => Set.univ, ?_, ?_⟩
  · exact ⟨fun _ => isOpen_univ, fun x => ⟨PUnit.unit, Set.mem_univ x⟩⟩
  · intro a
    letI univTopology : TopologicalSpace (Set.univ : Set X) :=
      TopologicalSpace.compactlyGenerated.{u} (Set.univ : Set X)
    change ShrinkableMap (id : ↥(Set.univ : Set X) → ↥(Set.univ : Set X))
    refine ⟨continuous_id, ContinuousMap.id _, ?_, ⟨Prod.snd, continuous_snd⟩,
      ?_, ?_, ?_⟩
    · intro x
      rfl
    · intro x
      rfl
    · intro x
      rfl
    · intro t x
      rfl

/-- Sanity: CG-local shrinkability permits the universal singleton CG-cover. -/
example (X : Type u) [TopologicalSpace X] : CGLocallyShrinkableMap (id : X → X) := by
  refine ⟨continuous_id, PUnit, fun _ => Set.univ, ?_, ?_⟩
  · intro K hK
    refine ⟨{PUnit.unit}, ?_⟩
    intro x
    exact ⟨PUnit.unit, by simp, by simp⟩
  · intro a
    letI univTopology : TopologicalSpace (Set.univ : Set X) :=
      TopologicalSpace.compactlyGenerated.{u} (Set.univ : Set X)
    change ShrinkableMap (id : ↥(Set.univ : Set X) → ↥(Set.univ : Set X))
    refine ⟨continuous_id, ContinuousMap.id _, ?_, ⟨Prod.snd, continuous_snd⟩,
      ?_, ?_, ?_⟩
    · intro x
      rfl
    · intro x
      rfl
    · intro x
      rfl
    · intro t x
      rfl

/-- Sanity: the quasi-shrinkable test includes each point of the base. -/
example {X B : Type u} [TopologicalSpace X] [TopologicalSpace B]
    (f : X → B) (hf : QuasiShrinkableMap f) (b : B) :
    KelleyShrinkable (pullbackProjection f (ContinuousMap.const PUnit b)) := by
  exact hf.2 PUnit (ContinuousMap.const PUnit b)

end QAlgorithms.Papers.Independent.Intakethird100.P32

Source

Compactly Generated Stacks: A Cartesian Closed Theory of Topological Stacks, arXiv:0907.3925v3, https://arxiv.org/abs/0907.3925v3

Read-back

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

`QAlgorithms.Papers.Independent.Intakethird100.P32.CGCover`

For a topological space $X$ , an index type $A$ in the same universe $u$ , and a family $(V_a)_{a\in A}$ of subsets of $X$ , this property means that for every compact subset $K\subseteq X$ , there exists a finite subset $J\subseteq A$ such that every point of $K$ belongs to $\operatorname{int}_K(K\cap V_a)$ for some $a\in J$ . Here $K$ carries its subspace topology, and the interior is taken in that space $K$ . The finite set $J$ may depend on $K$ ; the sets $V_a$ need not be open. The empty compact subset is included and can use $J=\varnothing$ . An empty index type satisfies the property exactly when $X$ is empty.

`QAlgorithms.Papers.Independent.Intakethird100.P32.CGLocallyShrinkableMap`

For topological spaces $X$ and $B$ with underlying types in the same universe $u$ , and a function $f:X\to B$ , this property means that $f$ is continuous in the given topologies and there exist an index type $A$ in universe $u$ 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)$ , with interiors taken in the subspace $K$ . For each $a$ , put $E_a=f^{-1}(V_a)$ and let $p_a:E_a\to V_a$ send $x$ to $f(x)$ ; give both spaces their subspace topologies and then their compactly generated topologies, denoted $kE_a$ and $kV_a$ . The map $p_a:kE_a\to kV_a$ must be continuous, and there must exist continuous maps $s_a:kV_a\to kE_a$ and $H_a:[0,1]\times kE_a\to kE_a$ , using the product topology, satisfying $p_a(s_a(b))=b$ , $H_a(0,x)=s_a(p_a(x))$ , $H_a(1,x)=x$ , and $p_a(H_a(t,x))=p_a(x)$ for every $b\in V_a$ , $x\in E_a$ , and $t\in[0,1]$ . The sets $V_a$ need not be open. Empty members and the empty compact subset are included; the latter may use $J=\varnothing$ , and an empty index type is possible only when $B$ is empty.

`QAlgorithms.Papers.Independent.Intakethird100.P32.HasOpenRefinement`

For a topological space $X$ , an index type $A$ in the same universe $u$ , and a family $(V_a)_{a\in A}$ of subsets of $X$ , this property means that every point $x\in X$ belongs to the interior in $X$ of some $V_a$ ; equivalently, the family $(\operatorname{int}_X V_a)_{a\in A}$ covers $X$ . The sets $V_a$ themselves are not required to be open. For empty $X$ the condition is vacuous, and an empty index type is permitted exactly in that case.

`QAlgorithms.Papers.Independent.Intakethird100.P32.IsOpenCover`

For a topological space $X$ , an index type $A$ in the same universe $u$ as $X$ , and a family of subsets $(U_a)_{a\in A}$ of $X$ , this property means that every $U_a$ is open and every point of $X$ belongs to at least one $U_a$ . Empty members are allowed. The index type may be empty, in which case the property holds exactly when $X$ is empty.

`QAlgorithms.Papers.Independent.Intakethird100.P32.IsShrinking`

For a topological space $X$ , an index type $A$ in the same universe $u$ , and two families $(U_a)_{a\in A}$ and $(V_a)_{a\in A}$ of subsets of $X$ , this property means that every $V_a$ is open, every point of $X$ lies in some $V_a$ , and $\overline{V_a}\subseteq U_a$ for every $a\in A$ , where closure is taken in $X$ . There is no separate requirement that the sets $U_a$ be open. Empty members are allowed; if $A$ is empty, the property holds exactly when $X$ is empty.

`QAlgorithms.Papers.Independent.Intakethird100.P32.KelleyShrinkable`

For topological spaces $X$ and $B$ with underlying types in the same universe $u$ , and a function $f:X\to B$ , let $kX$ and $kB$ denote those same underlying sets equipped with the compactly generated topologies obtained from their given topologies, using universe $u$ . This property means that $f:kX\to kB$ is continuous and there exist a continuous section $s:kB\to kX$ and a continuous map $H:[0,1]\times kX\to kX$ , with the product topology on its domain, such that $f(s(b))=b$ , $H(0,x)=s(f(x))$ , $H(1,x)=x$ , and $f(H(t,x))=f(x)$ for all $b\in B$ , $x\in X$ , and $t\in[0,1]$ . These continuity requirements use the replaced topologies. Empty spaces are included; an empty $X$ and nonempty $B$ cannot admit the required section.

`QAlgorithms.Papers.Independent.Intakethird100.P32.LocallyShrinkableMap`

For topological spaces $X$ and $B$ with underlying types in the same universe $u$ , and a function $f:X\to B$ , this property means that $f$ is continuous in the given topologies and there exist an index type $A$ in universe $u$ and open subsets $(U_a)_{a\in A}$ covering $B$ with the following property. For each $a$ , put $E_a=f^{-1}(U_a)$ and let $p_a:E_a\to U_a$ send $x$ to $f(x)$ ; give $E_a$ and $U_a$ their subspace topologies and then replace each by its compactly generated topology, denoted $kE_a$ and $kU_a$ . The map $p_a:kE_a\to kU_a$ is continuous, and there exist continuous maps $s_a:kU_a\to kE_a$ and $H_a:[0,1]\times kE_a\to kE_a$ , using the product topology, such that $p_a(s_a(b))=b$ , $H_a(0,x)=s_a(p_a(x))$ , $H_a(1,x)=x$ , and $p_a(H_a(t,x))=p_a(x)$ for all $b\in U_a$ , $x\in E_a$ , and $t\in[0,1]$ . Empty cover members are allowed, and the index type may be empty when $B$ is empty.

`QAlgorithms.Papers.Independent.Intakethird100.P32.QuasiShrinkableMap`

For topological spaces $X$ and $B$ in the same universe and a function $f:X\to B$ , the property defined here means that $f$ is continuous and satisfies the following condition: for every Hausdorff, locally compact, paracompact topological space $T$ in that universe and every continuous map $g:T\to B$ , form the subspace

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

and its projection $p:P\to T$ , $p(x,t)=t$ . After replacing the topologies of both $P$ and $T$ by their compactly generated topologies, $p$ is continuous and there exist a continuous section $s:T\to P$ and a continuous map $H:[0,1]\times P\to P$ such that

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

for every $t\in T$ , $z\in P$ , and $r\in[0,1]$ . The product used for $H$ uses the replaced topology on $P$ . No nonemptiness assumption is imposed on these spaces; the requirement includes empty test spaces, and whenever a test space is nonempty, the required section must exist on all of it.

`QAlgorithms.Papers.Independent.Intakethird100.P32.ShrinkableMap`

For topological spaces $X$ and $B$ with underlying types in the same universe $u$ , and a function $f:X\to B$ , this property means that $f$ is continuous and there exists a continuous map $s:B\to X$ satisfying $f(s(b))=b$ for every $b\in B$ , together with a continuous map $H:[0,1]\times X\to X$ , using the product topology, such that $H(0,x)=s(f(x))$ , $H(1,x)=x$ , and $f(H(t,x))=f(x)$ for every $x\in X$ and every $t\in[0,1]$ . No nonemptiness is assumed: if $X$ is empty and $B$ is nonempty, the required section cannot exist; if both are empty, the conditions hold.

`QAlgorithms.Papers.Independent.Intakethird100.P32.ShrinkingSpace`

For a topological space $X$ with underlying type in universe $u$ , this property means that for every index type $A$ in universe $u$ and every family $(U_a)_{a\in A}$ of open subsets covering $X$ , there exists a family $(V_a)_{a\in A}$ of open subsets covering $X$ , with the same index type, such that $\overline{V_a}\subseteq U_a$ for every $a\in A$ . Empty members and empty index types are included; an empty index type gives an open cover only when $X$ is empty, and the empty space satisfies this property.

`QAlgorithms.Papers.Independent.Intakethird100.P32.allCompactSubsets`

For a topological space $X$ with underlying type in universe $u$ , this defines a function whose inputs are subsets $K\subseteq X$ equipped with a proof that $K$ is compact, and whose output on such an input is the underlying subset $K$ itself. Thus it indexes the compact subsets of $X$ by those compact subsets together with their compactness proofs. The empty subset is included; there is no requirement that these compact subsets be nonempty or closed.

`QAlgorithms.Papers.Independent.Intakethird100.P32.pullbackProjection`

For types $X$ , $B$ , and $T$ in the same universe $u$ , and arbitrary functions $f:X\to B$ and $g:T\to B$ , this defines the function $\{(x,t)\in X\times T\mid f(x)=g(t)\}\to T$ that sends a pair $(x,t)$ , equipped with a proof of $f(x)=g(t)$ , to its second coordinate $t$ . No topologies, continuity assumptions, or nonemptiness assumptions are required; the domain may be empty.

`QAlgorithms.Papers.Independent.Intakethird100.P32.restrictedProjection`

For types $X$ and $B$ in the same universe $u$ , any function $f:X\to B$ , and any subset $V\subseteq B$ , this defines the function $f^{-1}(V)\to V$ that sends a point $x$ , equipped with the fact that $f(x)\in V$ , to $f(x)$ , equipped with that same membership fact. No topologies or continuity assumptions are required. If $V$ is empty, its domain is also empty and this is the function from the empty set to itself.

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