Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Normal Spaces via Urysohn's Lemma as a Lifting Property

Robert Maxton

TL;DR

The paper addresses the problem of expressing Urysohn's lemma and hereditary normality in categorical lifting terms within $\mathbf{Top}$, correcting a previously erroneous translation. It introduces a modified interval $I_{0}^{1}$ with distinguished endpoints $0'$ and $1'$, and shows that a lifting square involving maps $\pi$, $\iota$, and $\chi$ yields a separating continuous map, thereby characterizing normal spaces via a lift. It also presents a simplified lifting formulation for hereditary normality by 'hoisting' the defining morphism to a new closed point, clarifying the relation between open subspaces and normality. The work provides a concise categorical account of standard separation axioms and includes a Lean/Mathlib formalization to support future formal verification.

Abstract

We present a translation of Urysohn's description of normal spaces (as those where disjoint closed subsets are separated by a continuous function) into the language of lifting properties in $\mathbf{Top}$, correcting a frequently-cited previous erroneous translation. We also present a translation of the definition of hereditarily normal spaces as those in which every open subspace is normal, by directly 'mapping' the translation of the usual description of normal spaces.

Normal Spaces via Urysohn's Lemma as a Lifting Property

TL;DR

The paper addresses the problem of expressing Urysohn's lemma and hereditary normality in categorical lifting terms within , correcting a previously erroneous translation. It introduces a modified interval with distinguished endpoints and , and shows that a lifting square involving maps , , and yields a separating continuous map, thereby characterizing normal spaces via a lift. It also presents a simplified lifting formulation for hereditary normality by 'hoisting' the defining morphism to a new closed point, clarifying the relation between open subspaces and normality. The work provides a concise categorical account of standard separation axioms and includes a Lean/Mathlib formalization to support future formal verification.

Abstract

We present a translation of Urysohn's description of normal spaces (as those where disjoint closed subsets are separated by a continuous function) into the language of lifting properties in , correcting a frequently-cited previous erroneous translation. We also present a translation of the definition of hereditarily normal spaces as those in which every open subspace is normal, by directly 'mapping' the translation of the usual description of normal spaces.
Paper Structure (4 sections, 4 equations)

This paper contains 4 sections, 4 equations.

Table of Contents

  1. Introduction
  2. A Modification
  3. A Simplification
  4. Conclusion

Theorems & Definitions (1)

  • proof