B.k-functor

Open

QAlgorithms.Papers.Independent.Intakethird100.P07.kification_functorial

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

prove2quantum

For continuous maps $f:X\to Y$ and $g:Y\to Z$ of arbitrary topological spaces, the same underlying function $k(f):kX\to kY$ is continuous. Moreover

k(f)(x)=f(x),\qquad k(\operatorname{id}_X)=\operatorname{id}_{kX},\qquad k(g\circ f)=k(g)\circ k(f).

Together with the final compact-Hausdorff-probe topology on objects, these maps define the specified functor $k:\mathrm{Top}\to\mathrm{kTop}$ . No separation condition 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

/-- The unnumbered k-functor assertion after B.4, PDF p. 36: continuity,
identity-on-points, and the identity and composition laws for the concrete lift. -/
theorem kification_functorial
    (X Y Z : Type u) [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z]
    (f : C(X, Y)) (g : C(Y, Z)) :
    Continuous (kMap f) ∧
    (∀ x : KSpace X, kMap f x = f x) ∧
    kMap (ContinuousMap.id X) = ContinuousMap.id (KSpace X) ∧
    kMap (g.comp f) = (kMap g).comp (kMap f) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P07

end

Source

Cohomology of Local Cochains, arXiv:1110.2661v2, PDF p. 36, B.k-functor

Read-back

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

For any topological spaces $X,Y,Z$ whose underlying types lie in universe $u$ , and any continuous maps $f:X\to Y$ and $g:Y\to Z$ , define $kT$ , for each such space $T$ , to have the same underlying set as $T$ , with $U\subseteq T$ open precisely when $p^{-1}(U)$ is open for every compact Hausdorff space $K$ in universe $u$ and every continuous map $p:K\to T$ for the original topology. For a continuous map $h:T\to S$ , let $h^k:kT\to kS$ be the same underlying function, regarded as a continuous map between these new topologies. Then $f^k$ is continuous, $f^k(x)=f(x)$ for every $x\in kX$ , $(\operatorname{id}_X)^k=\operatorname{id}_{kX}$ , and $(g\circ f)^k=g^k\circ f^k$ , with the last two equalities being equalities of continuous maps. No nonemptiness assumptions are imposed.

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