Lemma B.10

Open

QAlgorithms.Papers.Independent.Intakethird100.P07.kification_closedEmbedding

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

prove2quantum

Let $f:X\to Y$ be a closed embedding between arbitrary topological spaces. Give $kX$ and $kY$ the final topologies for their compact Hausdorff probes. Then

k(f):kX\longrightarrow kY,\qquad k(f)(x)=f(x),

is a closed embedding. This preserves the original underlying map and asserts the embedding property as well as closedness of its image.

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.10, PDF p. 37: k preserves closed embeddings, for the same
underlying map, with final probe topologies on its domain and codomain. -/
theorem kification_closedEmbedding
    (X Y : Type u) [TopologicalSpace X] [TopologicalSpace Y]
    (f : X → Y) (hf : IsClosedEmbedding f) :
    @IsClosedEmbedding (KSpace X) (KSpace Y) _ _ f := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P07

end

Source

Cohomology of Local Cochains, arXiv:1110.2661v2, PDF p. 37, Lemma B.10

Read-back

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

For any topological spaces $X,Y$ whose underlying types lie in universe $u$ , and any function $f:X\to Y$ that is a topological embedding with closed image, the same function is a topological embedding with closed image after replacing both topologies as follows: for $T=X$ or $T=Y$ , retain the underlying set of $T$ and declare $U\subseteq T$ open precisely when $p^{-1}(U)$ is open for every compact Hausdorff space $K$ in universe $u$ and every map $p:K\to T$ continuous for the original topology. Here a topological embedding means an injective function whose domain topology is the topology induced from its codomain. Empty spaces and an empty image are included.

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