Lemma B.3

Proved

QAlgorithms.Papers.Independent.Intakethird100.P07.kification_identity_continuous

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

prove2quantum

Let $X$ be any topological space. Give its underlying set the final topology for all continuous maps from compact Hausdorff spaces, and denote the resulting space by $kX$ . Then

\operatorname{id}:kX\longrightarrow X\quad\text{is continuous}.

Thus the k-topology is finer than the given topology. No separation axiom on $X$ is imposed.

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 B.3, PDF p. 36: kX→X is the continuous set-theoretic identity. -/
theorem kification_identity_continuous (X : Type u) [TopologicalSpace X] :
    Continuous (fun x : KSpace X => (x : X)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P07

end

Source

Cohomology of Local Cochains, arXiv:1110.2661v2, PDF p. 36, Lemma B.3

Read-back

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

For every type $X$ in universe $u$ , equipped with any topology, the identity function on its underlying set is continuous from $kX$ to $X$ . Here $A\subseteq X$ is open in $kX$ precisely when $g^{-1}(A)$ is open for every compact Hausdorff space $S$ in universe $u$ and every continuous map $g:S\to X$ using the original topology of $X$ . No separation or nonemptiness assumption on $X$ is required.

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