This entry is about a generalized notion of topology. For the notion of formal space in the sense of rational homotopy theory, see formal dg-algebra.
topology (point-set topology, point-free topology)
see also differential topology, algebraic topology, functional analysis and topological homotopy theory
Basic concepts
fiber space, space attachment
Extra stuff, structure, properties
Kolmogorov space, Hausdorff space, regular space, normal space
sequentially compact, countably compact, locally compact, sigma-compact, paracompact, countably paracompact, strongly compact
Examples
Basic statements
closed subspaces of compact Hausdorff spaces are equivalently compact subspaces
open subspaces of compact Hausdorff spaces are locally compact
compact spaces equivalently have converging subnet of every net
continuous metric space valued function on compact metric space is uniformly continuous
paracompact Hausdorff spaces equivalently admit subordinate partitions of unity
injective proper maps to locally compact spaces are equivalently the closed embeddings
locally compact and second-countable spaces are sigma-compact
Theorems
Analysis Theorems
Formal topology is a programme for doing topology in a finite, predicative, and constructive fashion.
It is a kind of pointless topology; in the context of classical mathematics, it reproduces the theory of locales rather than topological spaces (although of course one can recover topological spaces from locales).
The basic definitions can be motivated by an attempt to study locales entirely through the posites that generate them. However, in order to recover all basic topological notions (particularly those associated with closed rather than open features) predicatively, we need to add a ‘positivity’ relation to the ‘coverage’ relation of sites.
A formal topology or formal space is a set $S$ together with
such that
for all $a$, $b$, $U$, and $V$.
We interpret the elements of $S$ as basic opens in the formal space. We call $\top$ the entire space and $a \cap b$ the intersection of $a$ and $b$. We say that $a$ is covered by $U$ or that $U$ is a cover of $a$ if $a \lhd U$. We say that $a$ is positive or inhabited if $\Diamond a$. (For a topological space equipped with a strict topological base $S$, taking these intepretations literally does in fact define a formal space; see the Examples.)
Some immediate points to notice:
Let $X$ be a topological space, and let $S$ be the collection of open subsets of $X$. Let $\top$ be $X$ itself, and let $a \cap b$ be the literal intersection of $a$ and $b$ for $a, b \in S$. Let $a \lhd U$ if and only $U$ is literally an open cover of $a$, and let $\Diamond a$ if and only if $a$ is literally inhabited. Then $(S,\top,\cap,\lhd,\Diamond)$ is a formal topology.
The above example is impredicative (since the collection of open subsets is generally large), but now let $S$ be a base for the topology of $X$ which is strict in the sense that it is closed under finitary intersection. Let the other definitions be as before. Then $(S,\top,\cap,\lhd,\Diamond)$ is a formal topology.
More generally, let $B$ be a subbase for the topology of $X$, and let $S$ be the free monoid on $B$, that is the set of finite lists of elements of $B$ (so this example is not strictly finitist), modulo the equivalence relation by which two lists are identified if their intersections are equal. Let $\top$ be the empty list, let $a \cap b$ be the concatenation of $a$ and $b$, let $a \lhd U$ if the intersection of $a$ is contained in the union of the intersections of the elements of $U$, and let $\Diamond a$ if the intersection of $a$ is inhabited. Then $(S,\top,\cap,\lhd,\Diamond)$ is a formal topology.
Let $X$ be an accessible locale generated by a posite whose underlying poset $S$ is a (meet)-semilattice. Let $\top$ and $\cap$ be as in the semilattice structure on $S$, and let $a \lhd U$ if $U$ contains a basic cover (in the posite structure on $S$) of $a$. Then we get a formal topology, defining $\Diamond$ in the unique way.
The last example is not predicative, and this is in part why one studies formal topologies instead of sites, if one wishes to be strictly predicative. (It still needs to be motivated that we want $\Diamond$ at all.)
In dependent type theory, if one doesn’t have a type of all propositions, then one usually cannot define a relation between a type $S$ and the type of all subtypes of $S$, which is necessary for defining the coverage $\lhd$. Instead, one has to use a Tarski universe to define the type of all locally $U$-small subtypes of $S$, and use that to define a locally $U$-small formal topology on $S$.
Let $(U, T)$ be a Tarski universe, and let $\mathrm{Prop}_U$ be the type of all propositions in $U$
which comes with an embedding $\mathrm{asType}_U:\mathrm{Prop}_U \hookrightarrow U$. In addition, we define the relation $a \in_S^U A$ for $a:S$ and $A:S \to \mathrm{Prop}_U$ as
The singleton subtype function is a function $\{-\}:S \to (S \to \mathrm{Prop}_U)$, such that for all elements $a:S$, $p(a):a \in_S^U \{a\}$, and for all functions $R:S \to (S \to \mathrm{Prop}_U)$ such that for all elements $a:S$, $p_R(a):a \in_S^U R(a)$, the type of functions $(b \in_S^U \{a\}) \to (b \in_S^U R(a))$ is contractible for all $a:A$ and $b:A$.
Given a Tarski universe $(U, T)$, a locally $U$-small formal topology or locally $U$-small formal space is a type $S$ together with
such that
is an equivalence of types.
Mike Fourman and Grayson (1982); Formal Spaces. This is the original development, intended as an application of locale theory to logic.
Giovanni Sambin (1987); Intuitionistic formal spaces; pdf.
Giovanni Sambin (2001); Some points in formal topology; pdf. This has newer results, alternative formulations, etc.
Erik Palmgren, From Intuitionistic to Point-Free Topology: On the Foundation of Homotopy Theory, Logicism, Intuitionism, and Formalism Volume 341 of the series Synthese Library pp 237-253, 2005 (pdf)
Last revised on November 17, 2022 at 22:01:31. See the history of this page for a list of all contributions to it.