Lemma B.12

Open

QAlgorithms.Papers.Independent.Intakethird100.P07.kification_openEmbedding

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

prove2quantum

Let $f:X\to Y$ be an open embedding between arbitrary topological spaces. Kification preserves this embedding:

k(f):kX\longrightarrow kY,\qquad k(f)(x)=f(x),\quad\text{is an open embedding}.

Here kification is the final compact-Hausdorff-probe topology. Neither source nor target is assumed 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 B.12, PDF p. 37: k preserves open embeddings, without a
separation hypothesis on either topological space. -/
theorem kification_openEmbedding
    (X Y : Type u) [TopologicalSpace X] [TopologicalSpace Y]
    (f : X → Y) (hf : IsOpenEmbedding f) :
    @IsOpenEmbedding (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.12

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 open image, the same function is a topological embedding with open 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