Lemma C.2

Proved

QAlgorithms.Papers.Independent.Intakethird100.P07.kOmega_iff_countableCompactHausdorffQuotient

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

prove2quantum

Let $X$ be a topological space. Say that $X$ is k-omega when a countable covering family of continuous maps from compact Hausdorff spaces determines its final topology, as in Definition C.1. Then

X\text{ is k-omega}\quad\Longleftrightarrow\quad\exists\text{ a countable family }(K_i)_{i\in I}\text{ of compact Hausdorff spaces and a quotient map }\coprod_{i\in I}K_i\twoheadrightarrow X.

The coproduct is a topological disjoint union, and quotient maps are surjective with the quotient topology. Finite and empty families are included; $X$ itself need not be Hausdorff.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P07

Formal statement

noncomputable section

universe u v

namespace QAlgorithms.Papers.Independent.Intakethird100.P07

open CategoryTheory Topology TopologicalSpace

/-- Lemma C.2, PDF p. 38: precisely the countable coproduct quotient
characterization, retaining compact Hausdorff source spaces. -/
theorem kOmega_iff_countableCompactHausdorffQuotient
    (X : Type u) [TopologicalSpace X] :
    IsKOmega X ↔
      ∃ (I : Type u) (_ : Countable I) (K : I → CompHaus.{u})
        (q : (Σ i, K i) → X), IsQuotientMap q := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P07

end

Source

Cohomology of Local Cochains, arXiv:1110.2661v2, PDF p. 38, Lemma C.2

Read-back

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

For every topological space $X$ whose underlying type lies in universe $u$ , the following are equivalent: there exist an at most countable index type $I$ in universe $u$ , compact Hausdorff spaces $K_i$ in universe $u$ , and continuous maps $f_i:K_i\to X$ whose images cover $X$ , such that a subset $A\subseteq X$ is open if and only if every $f_i^{-1}(A)$ is open; and there exist an at most countable index type $I$ in universe $u$ , compact Hausdorff spaces $K_i$ in universe $u$ , and a quotient map $q:\coprod_{i\in I}K_i\to X$ from their topological disjoint union. Here being a quotient map means that $q$ is surjective and that, for every $A\subseteq X$ , $A$ is open if and only if $q^{-1}(A)$ is open. The existentially chosen families on the two sides need not be the same. Finite and empty index types, and empty compact Hausdorff spaces, are allowed; an empty disjoint union can map surjectively to $X$ only when $X$ is 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